set -e
BASE=../
-SERVERS="dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
+SERVERS="dc-5.calit2.uci.edu dc-7.calit2.uci.edu dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.calit2.uci.edu"
REMOTEDIR="/scratch/hamed/"
INFILE="constraint_compiler/"
SRC="constraint_compiler/src/"
--- /dev/null
+deserializing ...
+**********************
+Polarity time: 0.004035
+Preprocess time: 0.013218
+Decompose Order: 0.000012
+Encoding Graph Time: 0.041886
+Elapse Encode time: 1.090344
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000001
+SAT Solving time: 172.826413
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 173.916775
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003925
+Preprocess time: 0.012769
+Decompose Order: 0.000007
+Encoding Graph Time: 0.077234
+Elapse Encode time: 0.175357
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 173.880185
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 174.055553
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 174055552888.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003697
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.078022
+Elapse Encode time: 0.162977
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 169.950790
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 170.113780
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 170113779509.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003722
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004957
+Elapse Encode time: 3.665021
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 185.708077
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 189.373110
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 189373110441.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003696
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004988
+Elapse Encode time: 3.656909
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 223.981770
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 227.638691
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 227638691365.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003746
+Preprocess time: 0.012362
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005093
+Elapse Encode time: 3.673204
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 204.648955
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 208.322172
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 208322171971.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003783
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005070
+Elapse Encode time: 3.660124
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 168.955967
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 172.616103
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 172616103387.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003876
+Preprocess time: 0.000014
+Decompose Order: 0.000033
+Encoding Graph Time: 0.005254
+Elapse Encode time: 3.743260
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 204.470081
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 208.213356
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 208213356243.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004094
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.080160
+Elapse Encode time: 0.165375
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 160.109910
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 160.275297
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 160275296708.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004059
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.078355
+Elapse Encode time: 0.163761
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 156.193350
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 156.357122
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 156357122315.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004075
+Preprocess time: 0.000012
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005185
+Elapse Encode time: 3.663215
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 203.557549
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 207.220776
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 207220776365.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003905
+Preprocess time: 0.000010
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005012
+Elapse Encode time: 3.644834
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 212.951258
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 216.596105
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 216596104827.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003877
+Preprocess time: 0.012756
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005143
+Elapse Encode time: 3.682618
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 209.801021
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 213.483652
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 213483652346.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003956
+Preprocess time: 0.012794
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005206
+Elapse Encode time: 3.699788
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 212.723803
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 216.423604
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 216423604309.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003936
+Preprocess time: 0.012737
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005156
+Elapse Encode time: 3.788655
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 193.596544
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 197.385211
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 197385211257.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003742
+Preprocess time: 0.012359
+Decompose Order: 0.000007
+Encoding Graph Time: 0.076438
+Elapse Encode time: 0.173937
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 160.742431
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 160.916381
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 160916380571.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003737
+Preprocess time: 0.012349
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005086
+Elapse Encode time: 3.669822
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 188.818087
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 192.487921
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 192487920763.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003727
+Preprocess time: 0.012391
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005276
+Elapse Encode time: 3.682198
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 211.634056
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 215.316267
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 215316267144.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003778
+Preprocess time: 0.012453
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005142
+Elapse Encode time: 3.676799
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 198.427101
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 202.103912
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 202103912479.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003800
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005169
+Elapse Encode time: 3.694777
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 213.284328
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 216.979118
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 216979117988.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003946
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005132
+Elapse Encode time: 3.723860
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 175.762665
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 179.486539
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 179486538926.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003912
+Preprocess time: 0.012528
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005059
+Elapse Encode time: 3.674142
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 211.915724
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 215.589878
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 215589878125.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004946
+Preprocess time: 0.014076
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005094
+Elapse Encode time: 3.698828
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 211.473552
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 215.172394
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 215172393540.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004016
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005101
+Elapse Encode time: 3.708234
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 175.099455
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 178.807702
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 178807701670.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003954
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005191
+Elapse Encode time: 3.710612
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 189.884156
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 193.594781
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 193594780541.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003990
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.077490
+Elapse Encode time: 0.162925
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 161.874690
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 162.037625
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 162037625387.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004718
+Preprocess time: 0.000019
+Decompose Order: 0.000004
+Encoding Graph Time: 0.006761
+Elapse Encode time: 3.685110
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 196.936218
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 200.621340
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 200621339784.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004118
+Preprocess time: 0.013453
+Decompose Order: 0.000009
+Encoding Graph Time: 0.005998
+Elapse Encode time: 3.686376
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 194.281813
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 197.968202
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 197968202182.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003897
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005008
+Elapse Encode time: 3.673334
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 209.588656
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 213.262002
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 213262001799.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003856
+Preprocess time: 0.012520
+Decompose Order: 0.000008
+Encoding Graph Time: 0.077373
+Elapse Encode time: 0.175199
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 160.810740
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 160.985950
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 160985949607.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003781
+Preprocess time: 0.000015
+Decompose Order: 0.000005
+Encoding Graph Time: 0.077545
+Elapse Encode time: 0.162992
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 160.765425
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 160.928428
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 160928427691.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003909
+Preprocess time: 0.000016
+Decompose Order: 0.000004
+Encoding Graph Time: 0.078728
+Elapse Encode time: 0.164136
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 162.124576
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 162.288723
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 162288723346.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003781
+Preprocess time: 0.000012
+Decompose Order: 0.000005
+Encoding Graph Time: 0.004942
+Elapse Encode time: 3.680737
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 209.995768
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 213.676518
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 213676517632.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003945
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.078411
+Elapse Encode time: 0.163838
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 164.902978
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 165.066828
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 165066827531.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003898
+Preprocess time: 0.000011
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005102
+Elapse Encode time: 3.732650
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 174.291819
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 178.024506
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 178024506426.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003741
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005041
+Elapse Encode time: 3.693665
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 210.357435
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 214.051112
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 214051112258.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003847
+Preprocess time: 0.012496
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005112
+Elapse Encode time: 3.687460
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 213.431153
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 217.118625
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 217118624848.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003863
+Preprocess time: 0.012529
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005267
+Elapse Encode time: 3.728645
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 176.863374
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 180.592032
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 180592031883.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003859
+Preprocess time: 0.012417
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005122
+Elapse Encode time: 3.670089
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 192.040423
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 195.710525
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 195710524957.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003848
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005036
+Elapse Encode time: 3.685831
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 197.900643
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 201.586486
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 201586486320.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003800
+Preprocess time: 0.000011
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005104
+Elapse Encode time: 3.653650
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 191.699499
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 195.353162
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 195353162260.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003814
+Preprocess time: 0.000012
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005189
+Elapse Encode time: 3.650501
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 201.154915
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 204.805428
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 204805427968.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003763
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005082
+Elapse Encode time: 3.699244
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 200.259792
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 203.959052
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 203959052436.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004775
+Preprocess time: 0.000015
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005933
+Elapse Encode time: 3.663216
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 191.255302
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 194.918530
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 194918530006.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003849
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005054
+Elapse Encode time: 3.650705
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 194.531983
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 198.182701
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 198182700896.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003755
+Preprocess time: 0.000012
+Decompose Order: 0.000004
+Encoding Graph Time: 0.077098
+Elapse Encode time: 0.163305
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 163.264840
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 163.428155
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 163428155146.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003749
+Preprocess time: 0.012392
+Decompose Order: 0.000007
+Encoding Graph Time: 0.078428
+Elapse Encode time: 0.176425
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 165.949550
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 166.125986
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 166125986333.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003869
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.076888
+Elapse Encode time: 0.162166
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 170.109839
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 170.272016
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 170272015757.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004817
+Preprocess time: 0.000020
+Decompose Order: 0.000004
+Encoding Graph Time: 0.078371
+Elapse Encode time: 0.164605
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 168.438953
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 168.603570
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 168603569572.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003824
+Preprocess time: 0.012402
+Decompose Order: 0.000008
+Encoding Graph Time: 0.076665
+Elapse Encode time: 0.182050
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 172.658556
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 172.840620
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 172840619808.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003732
+Preprocess time: 0.012341
+Decompose Order: 0.000007
+Encoding Graph Time: 0.038782
+Elapse Encode time: 1.084408
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 196.086515
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 197.170934
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 197170934389.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003798
+Preprocess time: 0.012459
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005163
+Elapse Encode time: 3.646471
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 196.787236
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 200.433720
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 200433720214.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003800
+Preprocess time: 0.012387
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005125
+Elapse Encode time: 3.736603
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 199.242297
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 202.978913
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 202978913249.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003796
+Preprocess time: 0.012289
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005060
+Elapse Encode time: 3.702186
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 230.594846
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 234.297043
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 234297042838.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003742
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005005
+Elapse Encode time: 3.657660
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 213.216063
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 216.873736
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 216873735962.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003802
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005021
+Elapse Encode time: 3.666980
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 190.150496
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 193.817488
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 193817487748.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003708
+Preprocess time: 0.012303
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005073
+Elapse Encode time: 3.691539
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 190.448437
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 194.139991
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 194139990727.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003739
+Preprocess time: 0.012630
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005020
+Elapse Encode time: 3.672934
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 209.209322
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 212.882268
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 212882267611.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003949
+Preprocess time: 0.012802
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005295
+Elapse Encode time: 3.687023
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 213.265444
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 216.952480
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 216952479581.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003912
+Preprocess time: 0.012691
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005183
+Elapse Encode time: 3.664000
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 232.840413
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 236.504427
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 236504426550.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003916
+Preprocess time: 0.012733
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005209
+Elapse Encode time: 3.735942
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 197.100228
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 200.836183
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 200836183201.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003979
+Preprocess time: 0.012754
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005272
+Elapse Encode time: 3.688929
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 194.572067
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 198.261009
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 198261009074.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003906
+Preprocess time: 0.012603
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005185
+Elapse Encode time: 3.679947
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 195.583452
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 199.263412
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 199263412053.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003884
+Preprocess time: 0.012608
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005214
+Elapse Encode time: 3.673056
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 196.515939
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 200.189008
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 200189008299.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004310
+Preprocess time: 0.013806
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005863
+Elapse Encode time: 3.672479
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 218.462610
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 222.135100
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 222135099600.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003947
+Preprocess time: 0.012763
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005078
+Elapse Encode time: 3.672946
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 216.175640
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 219.848599
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 219848599063.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003876
+Preprocess time: 0.012703
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005016
+Elapse Encode time: 3.681634
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 189.323384
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 193.005032
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 193005031629.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003947
+Preprocess time: 0.012753
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005069
+Elapse Encode time: 3.690430
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 213.451942
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 217.142385
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 217142384630.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003889
+Preprocess time: 0.012737
+Decompose Order: 0.000006
+Encoding Graph Time: 0.077964
+Elapse Encode time: 0.175904
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 168.975013
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 169.150954
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 169150954004.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003954
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.078389
+Elapse Encode time: 0.163362
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 162.638351
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 162.801724
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 162801723981.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003933
+Preprocess time: 0.012814
+Decompose Order: 0.000007
+Encoding Graph Time: 0.077829
+Elapse Encode time: 0.175715
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 167.368509
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 167.544236
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 167544235684.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003915
+Preprocess time: 0.012472
+Decompose Order: 0.000008
+Encoding Graph Time: 0.038816
+Elapse Encode time: 1.084491
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 157.594607
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 158.679111
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 158679110536.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003909
+Preprocess time: 0.012711
+Decompose Order: 0.000007
+Encoding Graph Time: 0.039867
+Elapse Encode time: 1.087709
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 196.644086
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 197.731808
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 197731807552.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003935
+Preprocess time: 0.012286
+Decompose Order: 0.000008
+Encoding Graph Time: 0.005066
+Elapse Encode time: 3.692239
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 212.237224
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 215.929477
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 215929476801.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003914
+Preprocess time: 0.012774
+Decompose Order: 0.000007
+Encoding Graph Time: 0.077064
+Elapse Encode time: 0.175014
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 163.079861
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 163.254888
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 163254887957.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003723
+Preprocess time: 0.012345
+Decompose Order: 0.000007
+Encoding Graph Time: 0.038708
+Elapse Encode time: 1.086417
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 173.854583
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 174.941041
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 174941041047.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003894
+Preprocess time: 0.012772
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005053
+Elapse Encode time: 3.645309
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 193.549004
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 197.194326
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 197194326176.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003943
+Preprocess time: 0.012657
+Decompose Order: 0.000008
+Encoding Graph Time: 0.039015
+Elapse Encode time: 1.086697
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 170.687788
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 171.774497
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 171774497026.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003915
+Preprocess time: 0.012660
+Decompose Order: 0.000006
+Encoding Graph Time: 0.038827
+Elapse Encode time: 1.091702
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 211.483507
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 212.575221
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 212575220713.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003908
+Preprocess time: 0.000011
+Decompose Order: 0.000003
+Encoding Graph Time: 0.040577
+Elapse Encode time: 1.075268
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 175.800611
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 176.875891
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 176875890670.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003938
+Preprocess time: 0.012794
+Decompose Order: 0.000008
+Encoding Graph Time: 0.038757
+Elapse Encode time: 1.091536
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 186.924864
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 188.016412
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 188016412411.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003900
+Preprocess time: 0.012565
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005207
+Elapse Encode time: 3.682209
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 192.647723
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 196.329945
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 196329945231.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003941
+Preprocess time: 0.012756
+Decompose Order: 0.000037
+Encoding Graph Time: 0.038824
+Elapse Encode time: 1.083426
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 179.833990
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 180.917429
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 180917428919.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003811
+Preprocess time: 0.012519
+Decompose Order: 0.000007
+Encoding Graph Time: 0.079074
+Elapse Encode time: 0.176448
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 170.526937
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 170.703396
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 170703395848.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003958
+Preprocess time: 0.012776
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005126
+Elapse Encode time: 3.666501
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 199.348463
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 203.014978
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 203014977559.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003882
+Preprocess time: 0.000010
+Decompose Order: 0.000003
+Encoding Graph Time: 0.077627
+Elapse Encode time: 0.162374
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000001
+SAT Solving time: 167.578118
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 167.740504
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 167740503520.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003840
+Preprocess time: 0.000011
+Decompose Order: 0.000004
+Encoding Graph Time: 0.004883
+Elapse Encode time: 3.645558
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 202.727908
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 206.373478
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 206373478044.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003943
+Preprocess time: 0.012472
+Decompose Order: 0.000007
+Encoding Graph Time: 0.076030
+Elapse Encode time: 0.173739
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 164.271451
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 164.445200
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 164445200208.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003937
+Preprocess time: 0.012865
+Decompose Order: 0.000009
+Encoding Graph Time: 0.005197
+Elapse Encode time: 3.736503
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 194.532342
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 198.268858
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 198268858437.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003731
+Preprocess time: 0.012372
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005044
+Elapse Encode time: 3.673733
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 195.935119
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 199.608864
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 199608864374.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003797
+Preprocess time: 0.000014
+Decompose Order: 0.000005
+Encoding Graph Time: 0.005054
+Elapse Encode time: 3.657081
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 187.706833
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 191.363926
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 191363925511.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003741
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005019
+Elapse Encode time: 3.656541
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 188.132679
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 191.789232
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 191789231675.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003762
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005036
+Elapse Encode time: 3.622179
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 200.267486
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 203.889678
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 203889677771.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003778
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005054
+Elapse Encode time: 3.682708
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 176.876994
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 180.559715
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 180559715113.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003776
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.039241
+Elapse Encode time: 1.071814
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 179.120002
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 180.191829
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 180191828542.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003753
+Preprocess time: 0.000014
+Decompose Order: 0.000005
+Encoding Graph Time: 0.038972
+Elapse Encode time: 1.077591
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 173.747742
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 174.825345
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 174825345064.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003741
+Preprocess time: 0.012412
+Decompose Order: 0.000007
+Encoding Graph Time: 0.038641
+Elapse Encode time: 1.083641
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 197.424468
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 198.508122
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 198508121760.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003766
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.077172
+Elapse Encode time: 0.162511
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 165.982214
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 166.144737
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 166144736612.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003798
+Preprocess time: 0.000012
+Decompose Order: 0.000004
+Encoding Graph Time: 0.078314
+Elapse Encode time: 0.163238
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 167.105501
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 167.268750
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 167268749810.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003741
+Preprocess time: 0.012401
+Decompose Order: 0.000006
+Encoding Graph Time: 0.076291
+Elapse Encode time: 0.178145
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 168.574659
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 168.752816
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 168752815677.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003763
+Preprocess time: 0.000012
+Decompose Order: 0.000005
+Encoding Graph Time: 0.076082
+Elapse Encode time: 0.160938
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 165.394703
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 165.555651
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 165555651137.000000
+Best tuner:
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 156357122315.000000
--- /dev/null
+deserializing ...
+**********************
+Polarity time: 0.003698
+Preprocess time: 0.011524
+Decompose Order: 0.000017
+Encoding Graph Time: 0.037881
+Elapse Encode time: 0.997790
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000001
+SAT Solving time: 22.486690
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 23.484500
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004408
+Preprocess time: 0.015162
+Decompose Order: 0.000007
+Encoding Graph Time: 0.075089
+Elapse Encode time: 0.170877
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.681346
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.852230
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 83852230129.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004306
+Preprocess time: 0.000012
+Decompose Order: 0.000003
+Encoding Graph Time: 0.041191
+Elapse Encode time: 0.993668
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 87.561080
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 88.554759
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 88554759182.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004242
+Preprocess time: 0.014907
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005495
+Elapse Encode time: 3.395448
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 59.817873
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 63.213332
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 63213332241.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004321
+Preprocess time: 0.015034
+Decompose Order: 0.000006
+Encoding Graph Time: 0.041278
+Elapse Encode time: 1.011671
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 89.444982
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 90.456664
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 90456664442.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003616
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.036958
+Elapse Encode time: 0.991289
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.786825
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.778125
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 31778124877.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004231
+Preprocess time: 0.014832
+Decompose Order: 0.000007
+Encoding Graph Time: 0.039483
+Elapse Encode time: 1.005092
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 31.087874
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 32.092977
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 32092977155.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004257
+Preprocess time: 0.014958
+Decompose Order: 0.000007
+Encoding Graph Time: 0.041401
+Elapse Encode time: 1.008422
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.392583
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.401015
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 31401015378.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004297
+Preprocess time: 0.014887
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005476
+Elapse Encode time: 3.399174
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 105.910181
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 109.309367
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 109309366995.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004377
+Preprocess time: 0.015036
+Decompose Order: 0.000007
+Encoding Graph Time: 0.041241
+Elapse Encode time: 1.013063
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 40.816514
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 41.829587
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 41829587127.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004338
+Preprocess time: 0.015042
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005625
+Elapse Encode time: 3.407410
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.632609
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 87.040030
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 87040029909.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004251
+Preprocess time: 0.014971
+Decompose Order: 0.000007
+Encoding Graph Time: 0.074759
+Elapse Encode time: 0.169985
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.095377
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.265372
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 83265371895.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003756
+Preprocess time: 0.000011
+Decompose Order: 0.000004
+Encoding Graph Time: 0.038465
+Elapse Encode time: 0.991921
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 41.302063
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 42.293995
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 42293995203.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004323
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.074547
+Elapse Encode time: 0.157879
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 81.915438
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.073324
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 82073324225.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004248
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.041180
+Elapse Encode time: 0.995260
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 26.421098
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 27.416369
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 27416368661.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004342
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005481
+Elapse Encode time: 3.371583
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 85.153587
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 88.525182
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 88525181902.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004275
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005308
+Elapse Encode time: 3.380358
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 87.043549
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 90.423918
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 90423918219.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004281
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.041230
+Elapse Encode time: 0.991263
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 52.397527
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 53.388801
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 53388800680.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004273
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.074555
+Elapse Encode time: 0.154938
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.008266
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.163213
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 83163213105.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003818
+Preprocess time: 0.011169
+Decompose Order: 0.000006
+Encoding Graph Time: 0.070034
+Elapse Encode time: 0.159874
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.624972
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.784855
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 82784854843.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004343
+Preprocess time: 0.015029
+Decompose Order: 0.000007
+Encoding Graph Time: 0.041378
+Elapse Encode time: 1.007336
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 31.199024
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 32.206371
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 32206370553.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004382
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.041151
+Elapse Encode time: 0.993579
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 20.294117
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 21.287706
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 21287706291.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003636
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.070066
+Elapse Encode time: 0.148509
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.965949
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 84.114467
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 84114467261.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003609
+Preprocess time: 0.011215
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037147
+Elapse Encode time: 0.998892
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.748693
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.747596
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 31747596132.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004389
+Preprocess time: 0.015054
+Decompose Order: 0.000007
+Encoding Graph Time: 0.074696
+Elapse Encode time: 0.170195
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.414739
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.584943
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 82584943418.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004320
+Preprocess time: 0.014481
+Decompose Order: 0.000007
+Encoding Graph Time: 0.004594
+Elapse Encode time: 3.396318
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 85.187796
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 88.584126
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 88584125805.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004375
+Preprocess time: 0.015001
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005633
+Elapse Encode time: 3.389372
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 87.848146
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 91.237530
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 91237529526.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004391
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.037852
+Elapse Encode time: 0.992423
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 61.716614
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 62.709048
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 62709047878.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004286
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.043198
+Elapse Encode time: 0.995987
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 5.946959
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 6.942956
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 6942956251.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004261
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005362
+Elapse Encode time: 3.384706
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 112.144277
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 115.528994
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 115528994215.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004353
+Preprocess time: 0.015062
+Decompose Order: 0.000006
+Encoding Graph Time: 0.041410
+Elapse Encode time: 1.007912
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.765756
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.773680
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 31773679622.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004336
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.041225
+Elapse Encode time: 0.995415
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 8.564521
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 9.559946
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 9559946211.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004269
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005307
+Elapse Encode time: 3.382184
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 89.076015
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 92.458210
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 92458209983.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003616
+Preprocess time: 0.000015
+Decompose Order: 0.000004
+Encoding Graph Time: 0.037030
+Elapse Encode time: 0.988529
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.816409
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.804950
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 31804949698.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003637
+Preprocess time: 0.000016
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004500
+Elapse Encode time: 3.381605
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 105.624640
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 109.006257
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 109006257268.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003609
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.070066
+Elapse Encode time: 0.148246
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.017586
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.165841
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 83165841166.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003793
+Preprocess time: 0.011294
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037214
+Elapse Encode time: 1.004501
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 40.405115
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 41.409626
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 41409625928.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003628
+Preprocess time: 0.000016
+Decompose Order: 0.000004
+Encoding Graph Time: 0.070005
+Elapse Encode time: 0.148406
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.673455
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.821879
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 82821878812.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003589
+Preprocess time: 0.000015
+Decompose Order: 0.000004
+Encoding Graph Time: 0.069845
+Elapse Encode time: 0.148089
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.260363
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.408461
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 82408461414.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003662
+Preprocess time: 0.011214
+Decompose Order: 0.000008
+Encoding Graph Time: 0.037162
+Elapse Encode time: 1.000221
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 63.581372
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 64.581604
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 64581603603.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003630
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.072271
+Elapse Encode time: 0.150898
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.865470
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.016377
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 83016377277.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003621
+Preprocess time: 0.000015
+Decompose Order: 0.000004
+Encoding Graph Time: 0.069953
+Elapse Encode time: 0.148476
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 84.333331
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 84.481840
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 84481839508.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003643
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.036907
+Elapse Encode time: 0.985214
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 31.198388
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 32.183612
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 32183612381.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003617
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.037008
+Elapse Encode time: 0.990691
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 8.581465
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 9.572166
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 9572165776.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003619
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.069792
+Elapse Encode time: 0.148374
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.737560
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.885944
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 82885943714.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003604
+Preprocess time: 0.000013
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004465
+Elapse Encode time: 3.380603
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 87.755807
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 91.136419
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 91136419414.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003638
+Preprocess time: 0.011222
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037182
+Elapse Encode time: 1.000609
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 33.460618
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 34.461239
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 34461238672.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003627
+Preprocess time: 0.011277
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037141
+Elapse Encode time: 1.000240
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 62.286329
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 63.286580
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 63286579834.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003603
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.036952
+Elapse Encode time: 0.989766
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 41.587196
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 42.576994
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 42576994380.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003607
+Preprocess time: 0.011245
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037129
+Elapse Encode time: 0.999497
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 8.630406
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 9.629913
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 9629913404.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003554
+Preprocess time: 0.011257
+Decompose Order: 0.000006
+Encoding Graph Time: 0.070039
+Elapse Encode time: 0.159810
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.135095
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.294914
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 83294914257.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003584
+Preprocess time: 0.011227
+Decompose Order: 0.000007
+Encoding Graph Time: 0.004614
+Elapse Encode time: 3.385892
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 49.465540
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 52.851444
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 52851443742.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003613
+Preprocess time: 0.011217
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037257
+Elapse Encode time: 1.000259
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 30.583907
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 31.584177
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 31584177331.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003614
+Preprocess time: 0.011239
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037056
+Elapse Encode time: 0.997787
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 20.157703
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 21.155500
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 21155500433.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003621
+Preprocess time: 0.000013
+Decompose Order: 0.000004
+Encoding Graph Time: 0.036958
+Elapse Encode time: 0.988231
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 8.732493
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 9.720734
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 9720733973.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003620
+Preprocess time: 0.000015
+Decompose Order: 0.000029
+Encoding Graph Time: 0.069906
+Elapse Encode time: 0.148470
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.287290
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.435769
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 82435769331.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003585
+Preprocess time: 0.011204
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037049
+Elapse Encode time: 0.997449
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 33.548497
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 34.545956
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 34545955994.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003584
+Preprocess time: 0.011194
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037103
+Elapse Encode time: 0.996823
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 68.995219
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 69.992053
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 69992053363.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003595
+Preprocess time: 0.011199
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037157
+Elapse Encode time: 0.998137
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 41.424740
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 42.422888
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 42422888244.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 1 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004368
+Preprocess time: 0.015122
+Decompose Order: 0.000006
+Encoding Graph Time: 0.041379
+Elapse Encode time: 1.006678
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 33.812083
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 34.818771
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 34818770810.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003610
+Preprocess time: 0.011172
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037203
+Elapse Encode time: 0.997866
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 27.557825
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 28.555701
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 28555701251.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004360
+Preprocess time: 0.015019
+Decompose Order: 0.000006
+Encoding Graph Time: 0.038774
+Elapse Encode time: 1.004089
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 63.353451
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 64.357551
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 64357550500.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004250
+Preprocess time: 0.014777
+Decompose Order: 0.000006
+Encoding Graph Time: 0.074700
+Elapse Encode time: 0.169764
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 86.908366
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 87.078139
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 87078139342.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004352
+Preprocess time: 0.014943
+Decompose Order: 0.000006
+Encoding Graph Time: 0.074774
+Elapse Encode time: 0.169911
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 86.319313
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 86.489234
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 86489233627.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003597
+Preprocess time: 0.011123
+Decompose Order: 0.000007
+Encoding Graph Time: 0.070011
+Elapse Encode time: 0.159512
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.454700
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.614221
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 82614221500.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003651
+Preprocess time: 0.011092
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037092
+Elapse Encode time: 1.000286
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 71.853457
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 72.853754
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 72853753763.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003643
+Preprocess time: 0.011101
+Decompose Order: 0.000006
+Encoding Graph Time: 0.070230
+Elapse Encode time: 0.159777
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 84.719625
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 84.879412
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 84879411582.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003634
+Preprocess time: 0.011164
+Decompose Order: 0.000007
+Encoding Graph Time: 0.037201
+Elapse Encode time: 0.997829
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 51.114738
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 52.112578
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 52112578141.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003674
+Preprocess time: 0.011182
+Decompose Order: 0.000007
+Encoding Graph Time: 0.004689
+Elapse Encode time: 3.383206
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 114.611367
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 117.994583
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 117994582967.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003620
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.036837
+Elapse Encode time: 0.985972
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 46.478543
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 47.464525
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 47464524931.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003605
+Preprocess time: 0.000016
+Decompose Order: 0.000003
+Encoding Graph Time: 0.036873
+Elapse Encode time: 0.986315
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 40.200536
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 41.186862
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 41186862150.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003663
+Preprocess time: 0.011276
+Decompose Order: 0.000007
+Encoding Graph Time: 0.070148
+Elapse Encode time: 0.159843
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.375232
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.535086
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 82535085668.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 4 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003602
+Preprocess time: 0.011101
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037077
+Elapse Encode time: 0.999875
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 14.009753
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 15.009639
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 15009639361.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003622
+Preprocess time: 0.011201
+Decompose Order: 0.000006
+Encoding Graph Time: 0.004631
+Elapse Encode time: 3.384540
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 75.543617
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 78.928167
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 78928166995.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003579
+Preprocess time: 0.011312
+Decompose Order: 0.000008
+Encoding Graph Time: 0.070124
+Elapse Encode time: 0.159894
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.061831
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.221734
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82221734235.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003551
+Preprocess time: 0.011259
+Decompose Order: 0.000007
+Encoding Graph Time: 0.070051
+Elapse Encode time: 0.159558
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.256872
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.416439
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82416439048.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003593
+Preprocess time: 0.011235
+Decompose Order: 0.000007
+Encoding Graph Time: 0.004582
+Elapse Encode time: 3.389657
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.307972
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.697641
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19697640893.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003576
+Preprocess time: 0.011259
+Decompose Order: 0.000006
+Encoding Graph Time: 0.004639
+Elapse Encode time: 3.385306
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.035999
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.421316
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19421316493.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 5 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003565
+Preprocess time: 0.011196
+Decompose Order: 0.000007
+Encoding Graph Time: 0.004553
+Elapse Encode time: 3.386017
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 32.369498
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 35.755526
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 5 range=[1,5]
+Received score 35755525576.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003605
+Preprocess time: 0.000016
+Decompose Order: 0.000004
+Encoding Graph Time: 0.004501
+Elapse Encode time: 3.374840
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 108.432511
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 111.807363
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 111807362878.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003596
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004528
+Elapse Encode time: 3.372506
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 61.460759
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 64.833276
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 64833276115.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003583
+Preprocess time: 0.011129
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037114
+Elapse Encode time: 0.997624
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 26.648506
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 27.646141
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 27646140703.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003623
+Preprocess time: 0.011095
+Decompose Order: 0.000006
+Encoding Graph Time: 0.037181
+Elapse Encode time: 1.000318
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 71.175752
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 72.176080
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 72176079940.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003619
+Preprocess time: 0.011116
+Decompose Order: 0.000006
+Encoding Graph Time: 0.004639
+Elapse Encode time: 3.385965
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.013478
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.399454
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19399453559.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003562
+Preprocess time: 0.011236
+Decompose Order: 0.000006
+Encoding Graph Time: 0.070376
+Elapse Encode time: 0.160124
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 83.829085
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 83.989220
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 83989219554.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003630
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.004486
+Elapse Encode time: 3.382889
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 15.896570
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.279470
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19279470399.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003534
+Preprocess time: 0.000015
+Decompose Order: 0.000003
+Encoding Graph Time: 0.069747
+Elapse Encode time: 0.148181
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.512962
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.661153
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82661152628.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003597
+Preprocess time: 0.011241
+Decompose Order: 0.000006
+Encoding Graph Time: 0.004552
+Elapse Encode time: 3.390503
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.391724
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.782237
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19782237090.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003606
+Preprocess time: 0.011243
+Decompose Order: 0.000006
+Encoding Graph Time: 0.069991
+Elapse Encode time: 0.159843
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.459144
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.618996
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82618995928.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003619
+Preprocess time: 0.011217
+Decompose Order: 0.000007
+Encoding Graph Time: 0.069986
+Elapse Encode time: 0.159895
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.789035
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.948966
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82948965952.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003641
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.004493
+Elapse Encode time: 3.379458
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.152344
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.531813
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19531813164.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003615
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004428
+Elapse Encode time: 3.388834
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 94.074652
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 97.463497
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 97463497348.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003597
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.004440
+Elapse Encode time: 3.379140
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 71.074409
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 74.453559
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 74453559426.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004336
+Preprocess time: 0.000022
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005427
+Elapse Encode time: 3.380403
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 86.655901
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 90.036315
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 90036314667.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPT = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004355
+Preprocess time: 0.000016
+Decompose Order: 0.000003
+Encoding Graph Time: 0.074442
+Elapse Encode time: 0.154603
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 82.257309
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 82.411922
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 82411922080.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 2 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004289
+Preprocess time: 0.000014
+Decompose Order: 0.000003
+Encoding Graph Time: 0.005336
+Elapse Encode time: 3.391593
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 87.475675
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 90.867278
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 2 range=[1,5]
+Received score 90867278483.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.003639
+Preprocess time: 0.011204
+Decompose Order: 0.000006
+Encoding Graph Time: 0.004632
+Elapse Encode time: 3.383923
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 16.068230
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.452165
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19452165317.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param ELEMENTOPTSETS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004319
+Preprocess time: 0.014972
+Decompose Order: 0.000007
+Encoding Graph Time: 0.005565
+Elapse Encode time: 3.398950
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 59.972419
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 63.371381
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 63371380931.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PROXYVARIABLE = 3 range=[1,5]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004375
+Preprocess time: 0.015001
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005624
+Elapse Encode time: 3.401645
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 72.692053
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 76.093709
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 3 range=[1,5]
+Received score 76093708689.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 0 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004366
+Preprocess time: 0.000014
+Decompose Order: 0.000004
+Encoding Graph Time: 0.005468
+Elapse Encode time: 3.380701
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 15.878807
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 19.259520
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 19259520074.000000
+Mutating 1 settings
+&&&&&&&&Mutating&&&&&&&
+Param PREPROCESS = 1 range=[0,1]
+&&&&&&&&&&&&&&&&&&&&&&&
+**********************
+Polarity time: 0.004352
+Preprocess time: 0.015053
+Decompose Order: 0.000006
+Encoding Graph Time: 0.005608
+Elapse Encode time: 3.403785
+Is problem UNSAT after encoding: 0
+CNF Encode time: 0.000000
+SAT Solving time: 71.899633
+Result Computed in SAT solver: SAT
+CSOLVER solve time: 75.303430
+Param PREPROCESS = 1 range=[0,1]
+Param ELEMENTOPTSETS = 1 range=[0,1]
+Param ELEMENTOPT = 0 range=[0,1]
+Param PROXYVARIABLE = 4 range=[1,5]
+Received score 75303429567.000000
+Best tuner:
+Param PREPROCESS = 0 range=[0,1]
+Param ELEMENTOPTSETS = 0 range=[0,1]
+Param ELEMENTOPT = 1 range=[0,1]
+Param PROXYVARIABLE = 1 range=[1,5]
+Received score 6942956251.000000
void EncodingGraph::encode() {
SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+ model_print("#SubGraph = %u", subgraphs.getSize());
while (itesg->hasNext()) {
EncodingSubGraph *sg = itesg->next();
sg->encode();
uint leftSize = 0, rightSize = 0, newSize = 0;
uint64_t totalCost = 0;
+ bool merge = false;
+// model_print("**************decideEdge*************\n");
+// model_print("LeftNode Size = %u\n", left->getSize());
+// model_print("rightNode Size = %u\n", right->getSize());
+// model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
+
if (leftGraph == NULL && rightGraph == NULL) {
leftSize = convertSize(left->getSize());
rightSize = convertSize(right->getSize());
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * left->elements.getSize() +
(newSize - rightSize) * right->elements.getSize();
+ if(leftSize == newSize && rightSize == newSize){
+ merge = true;
+ }
} else if (leftGraph != NULL && rightGraph == NULL) {
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(right->getSize());
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
(newSize - rightSize) * right->elements.getSize();
+ if(leftSize == newSize && rightSize == newSize){
+ merge = true;
+ }
} else {
//Neither are null
-
//Are we already merged?
if (leftGraph == rightGraph)
continue;
-
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(rightGraph->encodingSize);
newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
(newSize - rightSize) * rightGraph->numElements;
+// model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
+// model_print("RightGraph size=%u\n", rightGraph->encodingSize);
+// model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
+ if(rightSize < 64 && leftSize < 64){
+ merge = true;
+ }
}
-
- if ((totalCost * CONVERSIONFACTOR) < eeValue) {
+// model_print("******************************\n");
+ if (merge) {
//add the edge
mergeNodes(left, right);
}
void addClause(CNF *cnf, uint numliterals, int *literals){
cnf->clausecount++;
+ for(uint i=0; i< numliterals; i++)
+ model_print("%d ", literals[i]);
+ model_print("\n");
addArrayClauseLiteral(cnf->solver, numliterals, literals);
}
if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
// proxy => expression
Edge cnfexpr = simplifyCNF(cnf, expression);
+ Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
if (p == P_TRUE)
freeEdgeRec(expression);
outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
+ outputCNFOR(cnf, cnfnegexpr, proxy);
freeEdgeCNF(cnfexpr);
+ freeEdgeCNF(cnfnegexpr);
}
if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
// expression => proxy
Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
+ Edge cnfexpr = simplifyCNF(cnf, expression);
freeEdgeRec(expression);
outputCNFOR(cnf, cnfnegexpr, proxy);
+ outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
freeEdgeCNF(cnfnegexpr);
+ freeEdgeCNF(cnfexpr);
}
}
#include <fcntl.h>
#include "common.h"
#include <string.h>
+#include <stdexcept>
IncrementalSolver *allocIncrementalSolver() {
IncrementalSolver *This = (IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
ssize_t n = read(This->from_solver_fd, &((char *)result)[bytesread], bytestoread);
if (n == -1) {
model_print("Read failure\n");
- exit(-1);
+ throw std::runtime_error("Read failure\n");
}
bytestoread -= n;
bytesread += n;
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
+ model_print("**********************************************************\n");
+ constraint.print();
+ model_print("\n");
Edge c = encodeConstraintSATEncoder(constraint);
+ model_print("&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n");
+ printCNF(c);
+ model_print("\n");
addConstraintCNF(cnf, c);
}
delete iterator;
if(This->type != ELEMCONST){
model_print("INFO: naive encoder is making the decision about element %p....\n", This);
}
- encoding->setElementEncodingType(BINARYINDEX);
+ encoding->setElementEncodingType(UNARY);
encoding->encodingArrayInitialization();
}
$(CXX) -g $(SHARED) -o ${OBJ_DIR}/$(LIB_SO) $+ $(LDFLAGS)
${OBJ_DIR}/%.o: %.cc
- $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable
+ $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable -std=c++1y -pthread
${OBJ_DIR}/%.o: %.c
$(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable
exit(-1);
}
CSolver *solvers[argc - 1];
- AutoTuner *autotuner = new AutoTuner(100);
+ AutoTuner *autotuner = new AutoTuner(300);
for (int i = 1; i < argc; i++) {
solvers[i - 1] = CSolver::deserialize(argv[i]);
autotuner->addProblem(solvers[i - 1]);
#include <math.h>
#include <stdlib.h>
#include <float.h>
+#include <iostream>
+#include <chrono>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+#define TIMEOUT 1000s
#define UNSETVALUE -1
+#define POSINFINITY 9999999999L
+
+using namespace std::chrono_literals;
+
+int solve(CSolver *solver)
+{
+ try{
+ return solver->solve();
+ }
+ catch(std::runtime_error& e) {
+ return UNSETVALUE;
+ }
+}
+
+int solveWrapper(CSolver *solver)
+{
+ std::mutex m;
+ std::condition_variable cv;
+ int retValue;
+
+ std::thread t([&cv, &retValue, solver]()
+ {
+ retValue = solve(solver);
+ cv.notify_one();
+ });
+
+ t.detach();
+
+ {
+ std::unique_lock<std::mutex> l(m);
+ if(cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
+ throw std::runtime_error("Timeout");
+ }
+
+ return retValue;
+}
+
AutoTuner::AutoTuner(uint _budget) :
budget(_budget), result(UNSETVALUE) {
CSolver *copy = problem->clone();
copy->setTuner(tuner);
model_print("**********************\n");
- int sat = copy->solve();
- if (result == UNSETVALUE)
- result = sat;
- else if (result != sat) {
- model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
- copy->printConstraints();
+ long long metric = 0L;
+ try {
+ int sat = solveWrapper(copy);
+ if (result == UNSETVALUE)
+ result = sat;
+ else if (result != sat) {
+ model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+ copy->printConstraints();
+ }
+ metric = copy->getElapsedTime();
+ }
+ catch(std::runtime_error& e) {
+ metric = POSINFINITY;
+ model_print("TimeOut has hit\n");
}
- //model_print("SAT %d\n", result);
- long long elapsedTime = copy->getElapsedTime();
-// long long encodeTime = copy->getEncodeTime();
-// long long solveTime = copy->getSolveTime();
- long long metric = elapsedTime;
-// model_print("Elapsed Time: %llu\n", elapsedTime);
-// model_print("Encode Time: %llu\n", encodeTime);
-// model_print("Solve Time: %llu\n", solveTime);
+
delete copy;
return metric;
}
# A few common Makefile items
CC := gcc
-CXX := g++
+CXX := g++-5
UNAME := $(shell uname)
ElementOpt eop(this);
eop.doTransform();
-// EncodingGraph eg(this);
-// eg.buildGraph();
-// eg.encode();
+ EncodingGraph eg(this);
+ eg.buildGraph();
+ eg.encode();
naiveEncodingDecision(this);
// eg.validate();
projects / satune.git / commitdiff