Merging with branch scratch and cleaning the code

diff --git a/src/1.log b/src/1.log
deleted file mode 100644 (file)
index 3b13110..0000000
--- a/src/1.log
+++ /dev/null
@@ -1,2018 +0,0 @@
-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

diff --git a/src/2.log b/src/2.log
deleted file mode 100644 (file)
index d57ea60..0000000
--- a/src/2.log
+++ /dev/null
@@ -1,2018 +0,0 @@
-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

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 8029049c5a165710238b2083d96b65dd7c699546..472fd279b255f5e84d003272c3314e0622188af7 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -114,7 +114,7 @@ void EncodingGraph::validate() {
 
 void EncodingGraph::encode() {
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
-       model_print("#SubGraph = %u", subgraphs.getSize());
+       DEBUG("#SubGraph = %u", subgraphs.getSize());
        while (itesg->hasNext()) {
                EncodingSubGraph *sg = itesg->next();
                sg->encode();
@@ -155,9 +155,6 @@ void EncodingGraph::encode() {
                                                ASSERT(encoding->isinUseElement(encodingIndex));
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
-                               } else{
-                                       model_print("DAMN in encode()\n");
-                                       e->print();
                                }
                        }
                        break;
@@ -333,15 +330,10 @@ void EncodingGraph::decideEdges() {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
-               //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
+               
                uint leftSize = 0, rightSize = 0, newSize = 0, max=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());
@@ -350,7 +342,6 @@ void EncodingGraph::decideEdges() {
                        newSize = (rightSize > newSize) ? rightSize : newSize;
                        totalCost = (newSize - leftSize) * left->elements.getSize() +
                                                                        (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        max = rightSize > leftSize? rightSize : leftSize;
                        if(newSize == max){
                                merge = true;
@@ -363,7 +354,6 @@ void EncodingGraph::decideEdges() {
                        newSize = (rightSize > newSize) ? rightSize : newSize;
                        totalCost = (newSize - leftSize) * leftGraph->numElements +
                                                                        (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        max = rightSize > leftSize? rightSize : leftSize;
                        if(newSize == max){
                                merge = true;
@@ -377,14 +367,10 @@ void EncodingGraph::decideEdges() {
                        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;
                        }
                }
-//             model_print("******************************\n");
                if (merge) {
                        //add the edge
                        mergeNodes(left, right);

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 6425c58b6ab7ee554dca680369e4fb2ac338c614..b35b45602efb98e76f2739e5a9cdbd934e6bc06e 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -575,9 +575,6 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 
 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);
 }
 
@@ -643,23 +640,17 @@ void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
        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);
        }
 }
 

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 4c49b16442950ea1aa7142afe87cd32b1a244cc0..659c0d980776e4689c4271873768580e1af4be48 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -37,13 +37,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        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;

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index f5aa44b955e0c67837f089d4d82d40d4b62a6445..7e33c1b26ca8fd307a4235c37891f3dd2fedde00 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -68,7 +68,7 @@ void naiveEncodingElement(Element *This) {
                if(This->type != ELEMCONST){
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
-               encoding->setElementEncodingType(UNARY);
+               encoding->setElementEncodingType(BINARYINDEX);
                encoding->encodingArrayInitialization();
        }
 

diff --git a/src/Makefile b/src/Makefile
index fcbf7103db3e33f64ae9b7b4c8b0f3f068d48513..838a47802ed595177b02e8eead9613f1cf3716c8 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -13,6 +13,7 @@ HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wi
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -O0 -g
+CXXFLAGS := -std=c++1y -pthread
 CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
 LDFLAGS := -ldl -lrt -rdynamic -g
 SHARED := -shared
@@ -58,7 +59,7 @@ ${OBJ_DIR}/$(LIB_SO): $(OBJECTS)
        $(CXX) -g $(SHARED) -o ${OBJ_DIR}/$(LIB_SO) $+ $(LDFLAGS)
 
 ${OBJ_DIR}/%.o: %.cc
-       $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable -std=c++1y -pthread
+       $(CXX) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable $(CXXFLAGS)
 
 ${OBJ_DIR}/%.o: %.c
        $(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable

diff --git a/src/csolver.cc b/src/csolver.cc
index 5cdca73eb0ce7c91ce3a3feb4ca405290d3fcfbd..b7c9aa4fcb9f9ac6d4bab090dc1b41b2a9e0c2bd 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -615,9 +615,9 @@ int CSolver::solve() {
        ElementOpt eop(this);
        eop.doTransform();
 
-       EncodingGraph eg(this);
-       eg.buildGraph();
-       eg.encode();
+//     EncodingGraph eg(this);
+//     eg.buildGraph();
+//     eg.encode();
 
        naiveEncodingDecision(this);
 //     eg.validate();