Adding sypet to repo

[Benchmarks_CSolver.git] / sypet / output / geometry / benchmark11.log

diff --git a/sypet/output/geometry/benchmark11.log b/sypet/output/geometry/benchmark11.log
new file mode 100644 (file)
index 0000000..ba0a771
--- /dev/null
+++ b/sypet/output/geometry/benchmark11.log
@@ -0,0 +1,2811 @@
+Buildfile: /scratch/satcheck/satproject/constraint_compiler/src/Benchmarks/sypet/build.xml
+
+sypet:
+     [java] ----------Options
+     [java] Verbose: false
+     [java] Timeout: 600000
+     [java] Round Robin: true
+     [java] Round Robin Iterations: 100
+     [java] Round Robin Range: 2
+     [java] Solver limit: 5
+     [java] ----------benchmarks/geometry/11/benchmark11.json
+     [java] Benchmark Id: 11
+     [java] Method name: shear
+     [java] Packages: [java.awt.geom]
+     [java] Libraries: [./lib/rt7.jar]
+     [java] Source type(s): [java.awt.geom.Rectangle2D, double, double]
+     [java] Target type: java.awt.geom.Rectangle2D
+     [java] --------------------------------------------------------
+     [java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Cipher is a phantom class!
+     [java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
+     [java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKey is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Mac is a phantom class!
+     [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+     [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+     [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+     [java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
+     [java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
+     [java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
+     [java] Warning: javax.crypto.CipherInputStream is a phantom class!
+     [java] Warning: javax.crypto.CipherOutputStream is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
+     [java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
+     [java] Warning: javax.crypto.KeyGenerator is a phantom class!
+     [java] #Classes: 50
+     [java] #Methods: 751
+     [java] Soot Time: 3516.935495
+     [java] PetriNet for path length: 1 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 2 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 3 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 4 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 5 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Path Solving Time: 20.496211
+     [java] Path Solving Time: 6.547989
+     [java] Path Solving Time: 21.837127
+     [java] Path Solving Time: 1.223573
+     [java] 1594753536598 Original Encoding Solving Time: 0.793343
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753536598Satune Solving Time: 19.552031
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753536906 Original Encoding Solving Time: 0.25415
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753536906Satune Solving Time: 0.134409
+     [java] 1594753536923 Original Encoding Solving Time: 0.074535
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753536923Satune Solving Time: 0.130466
+     [java] Path Solving Time: 5.546149
+     [java] PetriNet for path length: 6 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 8.934483
+     [java] Path Solving Time: 1.40564
+     [java] 1594753537219 Original Encoding Solving Time: 1.007007
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537219Satune Solving Time: 36.273401
+     [java] 1594753537286 Original Encoding Solving Time: 0.187502
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537286Satune Solving Time: 0.087109
+     [java] 1594753537303 Original Encoding Solving Time: 0.040397
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537303Satune Solving Time: 0.089122
+     [java] Path Solving Time: 4.928626
+     [java] Path Solving Time: 1.392366
+     [java] 1594753537330 Original Encoding Solving Time: 0.531998
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537330Satune Solving Time: 22.494396
+     [java] 1594753537370 Original Encoding Solving Time: 0.09594
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537370Satune Solving Time: 0.07906
+     [java] 1594753537386 Original Encoding Solving Time: 0.039238
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537386Satune Solving Time: 0.091827
+     [java] Path Solving Time: 13.155355
+     [java] Path Solving Time: 2.255871
+     [java] 1594753537422 Original Encoding Solving Time: 0.437478
+     [java] Polarity time: 0.000036
+     [java] Preprocess time: 0.000025
+     [java] Decompose Order: 0.000018
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d5fd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d6450....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d60f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d6260....
+     [java] Encoding Graph Time: 0.000190
+     [java] Elapse Encode time: 0.000303
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 9       #Vars = 7
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.019178
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.019499
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 10      #Vars = 7
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000057
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000102
+     [java] Elapse Encode time: 0.000041
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 11      #Vars = 7
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000070
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000124
+     [java] Polarity time: 0.000010
+     [java] Preprocess time: 0.000019
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c26a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2340....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2620....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d6350....
+     [java] Encoding Graph Time: 0.000228
+     [java] Elapse Encode time: 0.000284
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.035968
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.036264
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000082
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000046
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d0cd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d05f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c524e50....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c5261e0....
+     [java] Encoding Graph Time: 0.000139
+     [java] Elapse Encode time: 0.000176
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.022302
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.022485
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000074
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000048
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d27f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c383b30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d2770....
+     [java] Encoding Graph Time: 0.000126
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Elapse EncisSat= true ,SatuneSat= true
+     [java] 1594753537422Satune Solving Time: 24.636659
+     [java] 1594753537466 Original Encoding Solving Time: 0.093379
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537466Satune Solving Time: 0.091248
+     [java] 1594753537482 Original Encoding Solving Time: 0.040015
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537482Satune Solving Time: 0.099001
+     [java] Path Solving Time: 11.594211
+     [java] Path Solving Time: 2.326656
+     [java] 1594753537519 Original Encoding Solving Time: 1.049029
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537519Satune Solving Time: 25.740847
+     [java] 1594753537565 Original Encoding Solving Time: 0.116079
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537565Satune Solving Time: 0.117048
+     [java] 1594753537580 Original Encoding Solving Time: 0.036895
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537580Satune Solving Time: 0.09423
+     [java] Path Solving Time: 5.198225
+     [java] Path Solving Time: 1.994934
+     [java] 1594753537610 Original Encoding Solving Time: 0.624838
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537610Satune Solving Time: 38.05581
+     [java] 1594753537663 Original Encoding Solving Time: 0.083421
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537663Satune Solving Time: 0.090412
+     [java] 1594753537676 Original Encoding Solving Time: 0.034606
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537676Satune Solving Time: 0.094111
+     [java] Path Solving Time: 4.546573
+     [java] Path Solving Time: 1.775078
+     [java] 1594753537704 Original Encoding Solving Time: 0.492658
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537704Satune Solving Time: 32.549661
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753537751 Original Encoding Solving Time: 0.080465
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537751Satune Solving Time: 0.08753
+     [java] 1594753537762 Original Encoding Solving Time: 0.036124
+     [java] ode time: 0.000155
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.024463
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.024627
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000046
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000086
+     [java] Elapse Encode time: 0.000038
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000094
+     [java] Polarity time: 0.000009
+     [java] Preprocess time: 0.000007
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c394440....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d1df0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d1d70....
+     [java] Encoding Graph Time: 0.000192
+     [java] Elapse Encode time: 0.000246
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.025478
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.025732
+     [java] Elapse Encode time: 0.000039
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000060
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000112
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000052
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7d0df0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3ae450....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3ae910....
+     [java] Encoding Graph Time: 0.000150
+     [java] Elapse Encode time: 0.000183
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.037857
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.038047
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000048
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000086
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Polarity time: 0.000012
+     [java] Preprocess time: 0.000015
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c392380....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c392dd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c391cd0....
+     [java] Encoding Graph Time: 0.000153
+     [java] Elapse Encode time: 0.000197
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.032336
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.032539
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.0isSat= false ,SatuneSat= false
+     [java] 1594753537762Satune Solving Time: 0.090983
+     [java] Path Solving Time: 4.633443
+     [java] Path Solving Time: 1.742567
+     [java] 1594753537790 Original Encoding Solving Time: 0.563694
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537790Satune Solving Time: 25.566788
+     [java] 1594753537830 Original Encoding Solving Time: 0.080678
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537830Satune Solving Time: 0.081397
+     [java] 1594753537843 Original Encoding Solving Time: 0.03448
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537843Satune Solving Time: 0.085283
+     [java] Path Solving Time: 5.401003
+     [java] Path Solving Time: 2.733667
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753537874 Original Encoding Solving Time: 0.532168
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537874Satune Solving Time: 24.692087
+     [java] 1594753537914 Original Encoding Solving Time: 0.077663
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537914Satune Solving Time: 0.119464
+     [java] 1594753537927 Original Encoding Solving Time: 0.033801
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753537927Satune Solving Time: 0.084038
+     [java] Path Solving Time: 5.209322
+     [java] Path Solving Time: 1.986211
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753537956 Original Encoding Solving Time: 0.463157
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537956Satune Solving Time: 21.29612
+     [java] 1594753537989 Original Encoding Solving Time: 0.076957
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753537989Satune Solving Time: 0.078456
+     [java] 1594753538000 Original Encoding Solving Time: 0.033426
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538000Satune Solving Time: 0.079679
+     [java] Path Solving Time: 3.944564
+     [java] Path Solving Time: 1.252615
+     [java] 1594753538026 Original Encoding Solving Time: 0.388596
+     [java] 00000
+     [java] SAT Solving time: 0.000047
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Polarity time: 0.000010
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000010
+     [java] INFO: naive encoder is making the decision about element 0x7f866c22a200....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c2720....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c229a50....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c2299d0....
+     [java] Encoding Graph Time: 0.000173
+     [java] Elapse Encode time: 0.000221
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.025330
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.025558
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000077
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c22c710....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230c70....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c22c290....
+     [java] Encoding Graph Time: 0.000172
+     [java] Elapse Encode time: 0.000211
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.024467
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.024683
+     [java] Elapse Encode time: 0.000065
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000039
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000115
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000080
+     [java] Polarity time: 0.000009
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c390010....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3aebe0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3af250....
+     [java] Encoding Graph Time: 0.000142
+     [java] Elapse Encode time: 0.000176
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.021105
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.021286
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000074
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000039
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000075
+     [java] Polarity time: 0.000004
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c498470....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4991a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c390bc0....
+     [java] Encoding Graph Time: isSat= true ,SatuneSat= true
+     [java] 1594753538026Satune Solving Time: 22.366739
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753538061 Original Encoding Solving Time: 0.101946
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538061Satune Solving Time: 0.091485
+     [java] 1594753538071 Original Encoding Solving Time: 0.031689
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538071Satune Solving Time: 0.092934
+     [java] Path Solving Time: 3.709853
+     [java] Path Solving Time: 1.205977
+     [java] 1594753538098 Original Encoding Solving Time: 0.402623
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538098Satune Solving Time: 20.692082
+     [java] 1594753538130 Original Encoding Solving Time: 0.080233
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538130Satune Solving Time: 0.074738
+     [java] 1594753538140 Original Encoding Solving Time: 0.032951
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538140Satune Solving Time: 0.084381
+     [java] Path Solving Time: 3.850173
+     [java] Path Solving Time: 0.944987
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753538166 Original Encoding Solving Time: 0.819199
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538166Satune Solving Time: 20.844106
+     [java] 1594753538198 Original Encoding Solving Time: 0.096301
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538198Satune Solving Time: 0.113695
+     [java] 1594753538207 Original Encoding Solving Time: 0.048603
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538207Satune Solving Time: 0.094628
+     [java] Path Solving Time: 11.934116
+     [java] Path Solving Time: 8.275923
+     [java] Path Solving Time: 0.640327
+     [java] Path Solving Time: 0.420748
+     [java] Path Solving Time: 62.530447
+     [java] 1594753538314 Original Encoding Solving Time: 1.045818
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538314Satune Solving Time: 23.249015
+     [java] 1594753538346 Original Encoding Solving Time: 0.079521
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538346Satune Solving Time: 0.082272
+     [java] 1594753538355 Original Encoding Solving Time: 0.029698
+     [java] 0.000120
+     [java] Elapse Encode time: 0.000145
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.022207
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.022359
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000050
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000089
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4984f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c498e70....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c22d2a0....
+     [java] Encoding Graph Time: 0.000123
+     [java] Elapse Encode time: 0.000150
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.020528
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.020684
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000032
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000071
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000080
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e73a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230c30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3af250....
+     [java] Encoding Graph Time: 0.000105
+     [java] Elapse Encode time: 0.000131
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.020699
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.020836
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000072
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000109
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000052
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e90f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e9b20....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e9070....
+     [java] Encoding Graph Time: 0.000188
+     [java] Elapse Encode time: 0.000223
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 12      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.023010
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.023240
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000077
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CisSat= false ,SatuneSat= false
+     [java] 1594753538355Satune Solving Time: 0.087384
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 37.359371
+     [java] Path Solving Time: 28.936168
+     [java] Path Solving Time: 35.914616
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753538478 Original Encoding Solving Time: 0.314847
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538478Satune Solving Time: 21.462787
+     [java] 1594753538510 Original Encoding Solving Time: 0.118406
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538510Satune Solving Time: 0.076676
+     [java] 1594753538519 Original Encoding Solving Time: 0.027106
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538519Satune Solving Time: 0.087781
+     [java] Path Solving Time: 7.817032
+     [java] Path Solving Time: 4.152737
+     [java] 1594753538557 Original Encoding Solving Time: 0.602547
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538557Satune Solving Time: 33.714978
+     [java] 1594753538602 Original Encoding Solving Time: 0.076387
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538602Satune Solving Time: 0.083275
+     [java] 1594753538611 Original Encoding Solving Time: 0.030046
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538611Satune Solving Time: 0.095879
+     [java] Path Solving Time: 7.515698
+     [java] Path Solving Time: 4.016533
+     [java] 1594753538650 Original Encoding Solving Time: 1.270839
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538650Satune Solving Time: 25.673951
+     [java] 1594753538687 Original Encoding Solving Time: 0.104678
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538687Satune Solving Time: 0.074889
+     [java] 1594753538697 Original Encoding Solving Time: 0.031918
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538697Satune Solving Time: 0.08212
+     [java] Path Solving Time: 21.6664
+     [java] Path Solving Time: 34.490525
+     [java] Path Solving Time: 2.080395
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753538779 Original Encoding Solving Time: 1.174527
+     [java] NF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Polarity time: 0.000004
+     [java] Preprocess time: 0.000005
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3a75e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c38e500....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c38e360....
+     [java] Encoding Graph Time: 0.000078
+     [java] Elapse Encode time: 0.000097
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.021353
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.021455
+     [java] Elapse Encode time: 0.000027
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000072
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Polarity time: 0.000015
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7c48b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c3aa5d0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7c4830....
+     [java] Encoding Graph Time: 0.000210
+     [java] Elapse Encode time: 0.000263
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.033434
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.033704
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000079
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000053
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000092
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c36ce80....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c38f080....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000121
+     [java] Elapse Encode time: 0.000162
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.025497
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.025664
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000034
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000071
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000078
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c46fee0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c36e200....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c36e180....
+     [java] EnisSat= true ,SatuneSat= true
+     [java] 1594753538779Satune Solving Time: 21.215359
+     [java] 1594753538810 Original Encoding Solving Time: 0.065596
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538810Satune Solving Time: 0.078712
+     [java] 1594753538819 Original Encoding Solving Time: 0.023641
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538819Satune Solving Time: 0.08154
+     [java] Path Solving Time: 14.385788
+     [java] Path Solving Time: 2.078416
+     [java] 1594753538857 Original Encoding Solving Time: 0.369611
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538857Satune Solving Time: 23.599122
+     [java] 1594753538892 Original Encoding Solving Time: 0.066717
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538892Satune Solving Time: 0.088385
+     [java] 1594753538902 Original Encoding Solving Time: 0.024307
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538902Satune Solving Time: 0.1439
+     [java] Path Solving Time: 4.033772
+     [java] Path Solving Time: 2.204307
+     [java] 1594753538931 Original Encoding Solving Time: 1.236204
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538931Satune Solving Time: 26.166145
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753538969 Original Encoding Solving Time: 0.114397
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753538969Satune Solving Time: 0.078152
+     [java] 1594753538979 Original Encoding Solving Time: 0.036636
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753538979Satune Solving Time: 0.089608
+     [java] Path Solving Time: 3.906345
+     [java] Path Solving Time: 2.166896
+     [java] 1594753539007 Original Encoding Solving Time: 0.381786
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539007Satune Solving Time: 22.220066
+     [java] 1594753539041 Original Encoding Solving Time: 0.060668
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539041Satune Solving Time: 0.078862
+     [java] 1594753539051 Original Encoding Solving Time: 0.026049
+     [java] coding Graph Time: 0.000138
+     [java] Elapse Encode time: 0.000178
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.021019
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.021205
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000074
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000038
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000077
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000006
+     [java] Decompose Order: 0.000006
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c243910....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c248710....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c243890....
+     [java] Encoding Graph Time: 0.000101
+     [java] Elapse Encode time: 0.000129
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.023458
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.023592
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000055
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000139
+     [java] Polarity time: 0.000012
+     [java] Preprocess time: 0.000014
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c471500....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c248eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c249370....
+     [java] Encoding Graph Time: 0.000147
+     [java] Elapse Encode time: 0.000196
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.025954
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026158
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000035
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000073
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000085
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000008
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4bdc60....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c2438c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c248bf0....
+     [java] Encoding Graph Time: 0.000076
+     [java] Elapse Encode time: 0.000100
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.022106
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.022212
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000075
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data isSat= false ,SatuneSat= false
+     [java] 1594753539051Satune Solving Time: 0.098772
+     [java] Path Solving Time: 4.001084
+     [java] Path Solving Time: 2.567813
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753539081 Original Encoding Solving Time: 0.596276
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539081Satune Solving Time: 28.920318
+     [java] 1594753539121 Original Encoding Solving Time: 0.061211
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539121Satune Solving Time: 0.074631
+     [java] 1594753539131 Original Encoding Solving Time: 0.024408
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539131Satune Solving Time: 0.088871
+     [java] Path Solving Time: 4.037605
+     [java] Path Solving Time: 2.116417
+     [java] 1594753539159 Original Encoding Solving Time: 0.276034
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539159Satune Solving Time: 22.695784
+     [java] 1594753539193 Original Encoding Solving Time: 0.076583
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539193Satune Solving Time: 0.09983
+     [java] 1594753539204 Original Encoding Solving Time: 0.022219
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539204Satune Solving Time: 0.092199
+     [java] Path Solving Time: 4.618295
+     [java] Path Solving Time: 2.570469
+     [java] 1594753539235 Original Encoding Solving Time: 0.988136
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539235Satune Solving Time: 26.998161
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753539273 Original Encoding Solving Time: 0.107581
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539273Satune Solving Time: 0.082477
+     [java] 1594753539284 Original Encoding Solving Time: 0.04665
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539284Satune Solving Time: 0.096445
+     [java] Path Solving Time: 4.857101
+     [java] Path Solving Time: 2.589762
+     [java] 1594753539314 Original Encoding Solving Time: 0.367068
+     [java] is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000052
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000094
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000017
+     [java] Decompose Order: 0.000014
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c0750....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4bfce0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c27a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4bf670....
+     [java] Encoding Graph Time: 0.000194
+     [java] Elapse Encode time: 0.000248
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.028658
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.028912
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000033
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000070
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000005
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c2f40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c2360....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c1cf0....
+     [java] Encoding Graph Time: 0.000078
+     [java] Elapse Encode time: 0.000102
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.022582
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.022688
+     [java] Elapse Encode time: 0.000035
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000095
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c57b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c4cc0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4c4730....
+     [java] Encoding Graph Time: 0.000117
+     [java] Elapse Encode time: 0.000152
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026829
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026988
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000039
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000077
+     [java] Elapse Encode time: 0.000036
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000092
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4a8420....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4a7910....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0xisSat= true ,SatuneSat= true
+     [java] 1594753539314Satune Solving Time: 22.972745
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] 1594753539465 Original Encoding Solving Time: 0.071826
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539465Satune Solving Time: 0.076647
+     [java] 1594753539473 Original Encoding Solving Time: 0.020058
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539473Satune Solving Time: 0.090146
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 11.516469
+     [java] Path Solving Time: 1.22399
+     [java] 1594753539511 Original Encoding Solving Time: 0.323578
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539511Satune Solving Time: 27.610311
+     [java] 1594753539547 Original Encoding Solving Time: 0.112166
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539547Satune Solving Time: 0.178933
+     [java] 1594753539557 Original Encoding Solving Time: 0.020625
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539557Satune Solving Time: 0.09445
+     [java] Path Solving Time: 4.439856
+     [java] Path Solving Time: 1.455052
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753539590 Original Encoding Solving Time: 0.442158
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539590Satune Solving Time: 26.307002
+     [java] 1594753539625 Original Encoding Solving Time: 0.053863
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539625Satune Solving Time: 0.084802
+     [java] 1594753539633 Original Encoding Solving Time: 0.023575
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539633Satune Solving Time: 0.085374
+     [java] Path Solving Time: 3.01339
+     [java] Path Solving Time: 1.533864
+     [java] 1594753539664 Original Encoding Solving Time: 0.382624
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539664Satune Solving Time: 26.940213
+     [java] 1594753539700 Original Encoding Solving Time: 0.050798
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539700Satune Solving Time: 0.087742
+     [java] 1594753539708 Original Encoding Solving Time: 0.021636
+     [java] 7f866c4a7450....
+     [java] Encoding Graph Time: 0.000119
+     [java] Elapse Encode time: 0.000153
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.022804
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.022963
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000035
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000072
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000046
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000086
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c8a1ac0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4aa290....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4a9c30....
+     [java] Encoding Graph Time: 0.000103
+     [java] Elapse Encode time: 0.000127
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027470
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027603
+     [java] Elapse Encode time: 0.000063
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000093
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000170
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4ac970....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4ac8f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4ac4f0....
+     [java] Encoding Graph Time: 0.000120
+     [java] Elapse Encode time: 0.000156
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026133
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026297
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000044
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4a8710....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4ad910....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c382d20....
+     [java] Encoding Graph Time: 0.000110
+     [java] Elapse Encode time: 0.000140
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026785
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026932
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000044
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses =isSat= false ,SatuneSat= false
+     [java] 1594753539708Satune Solving Time: 0.098276
+     [java] Path Solving Time: 3.166588
+     [java] Path Solving Time: 1.992974
+     [java] 1594753539740 Original Encoding Solving Time: 0.431955
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539740Satune Solving Time: 27.614138
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753539779 Original Encoding Solving Time: 0.06135
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539779Satune Solving Time: 0.094961
+     [java] 1594753539788 Original Encoding Solving Time: 0.023833
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539788Satune Solving Time: 0.088378
+     [java] Path Solving Time: 3.053176
+     [java] Path Solving Time: 1.817193
+     [java] 1594753539819 Original Encoding Solving Time: 0.496121
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539819Satune Solving Time: 28.051279
+     [java] 1594753539857 Original Encoding Solving Time: 0.081092
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539857Satune Solving Time: 0.086724
+     [java] 1594753539864 Original Encoding Solving Time: 0.026475
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753539864Satune Solving Time: 0.085288
+     [java] Path Solving Time: 4.716569
+     [java] Path Solving Time: 1.541065
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753539897 Original Encoding Solving Time: 0.417364
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539897Satune Solving Time: 26.066298
+     [java] 1594753539932 Original Encoding Solving Time: 0.051651
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539932Satune Solving Time: 0.098142
+     [java] 1594753539940 Original Encoding Solving Time: 0.057118
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539940Satune Solving Time: 0.128836
+     [java] 1594753539948 Original Encoding Solving Time: 0.03402
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539948Satune Solving Time: 0.10008
+     [java] 1594753539956 Original Encoding Solving Time: 0.07043
+     [java]  15        #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000054
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000093
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000006
+     [java] Decompose Order: 0.000006
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79bae0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79b200....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79b180....
+     [java] Encoding Graph Time: 0.000114
+     [java] Elapse Encode time: 0.000143
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027456
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027604
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000048
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000044
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000009
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79e240....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79d8c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79d280....
+     [java] Encoding Graph Time: 0.000131
+     [java] Elapse Encode time: 0.000169
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027869
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.028044
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000082
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79fc20....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7a09c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79fdc0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000076
+     [java] Elapse Encode time: 0.000111
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.025941
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026058
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000052
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000093
+     [java] Elapse Encode time: 0.000048
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000061
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000122
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000053
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000096
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000071
+     [java] Result Computed in SAT solisSat= false ,SatuneSat= false
+     [java] 1594753539956Satune Solving Time: 0.119816
+     [java] Path Solving Time: 2.927437
+     [java] Path Solving Time: 1.45325
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753539988 Original Encoding Solving Time: 0.527756
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753539988Satune Solving Time: 27.666359
+     [java] 1594753540026 Original Encoding Solving Time: 0.054149
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540026Satune Solving Time: 0.095136
+     [java] 1594753540034 Original Encoding Solving Time: 0.051121
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540034Satune Solving Time: 0.087578
+     [java] 1594753540042 Original Encoding Solving Time: 0.047175
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540042Satune Solving Time: 0.098469
+     [java] 1594753540050 Original Encoding Solving Time: 0.07759
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540050Satune Solving Time: 0.100217
+     [java] Path Solving Time: 2.680703
+     [java] Path Solving Time: 1.874004
+     [java] 1594753540081 Original Encoding Solving Time: 0.360549
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540081Satune Solving Time: 26.191268
+     [java] 1594753540116 Original Encoding Solving Time: 0.053107
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540116Satune Solving Time: 0.084432
+     [java] 1594753540123 Original Encoding Solving Time: 0.055775
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540123Satune Solving Time: 0.09654
+     [java] 1594753540131 Original Encoding Solving Time: 0.033622
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540131Satune Solving Time: 0.088783
+     [java] 1594753540138 Original Encoding Solving Time: 0.072154
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540138Satune Solving Time: 0.113619
+     [java] Path Solving Time: 2.484715
+     [java] Path Solving Time: 1.765103
+     [java] 1594753540169 Original Encoding Solving Time: 0.413057
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540169Satune Solving Time: 28.921811
+     [java] 1594753540207 Original Encoding Solving Time: 0.058813
+     [java] ver:        UNSAT
+     [java] CSOLVER solve time: 0.000115
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000007
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7a2350....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7a4bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7a2920....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] Encoding Graph Time: 0.000118
+     [java] Elapse Encode time: 0.000151
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027501
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027658
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Elapse Encode time: 0.000036
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000094
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000053
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000096
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c8960....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c9cb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c7a50e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000103
+     [java] Elapse Encode time: 0.000140
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026184
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000080
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000091
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000035
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000063
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000108
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9cbfe0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9cd360....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79db20....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] Encoding Graph Time: 0.000124
+     [java] Elapse Encode time: 0.000158
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.028749
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.028913
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #ClausesisSat= true ,SatuneSat= true
+     [java] 1594753540207Satune Solving Time: 0.09405
+     [java] 1594753540215 Original Encoding Solving Time: 0.056087
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540215Satune Solving Time: 0.092146
+     [java] 1594753540222 Original Encoding Solving Time: 0.031809
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540222Satune Solving Time: 0.086646
+     [java] 1594753540229 Original Encoding Solving Time: 0.069558
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540229Satune Solving Time: 0.094841
+     [java] Path Solving Time: 2.573453
+     [java] Path Solving Time: 1.493095
+     [java] 1594753540259 Original Encoding Solving Time: 0.401908
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540259Satune Solving Time: 26.717125
+     [java] 1594753540295 Original Encoding Solving Time: 0.052711
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540295Satune Solving Time: 0.094495
+     [java] 1594753540303 Original Encoding Solving Time: 0.060866
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540303Satune Solving Time: 0.098158
+     [java] 1594753540311 Original Encoding Solving Time: 0.032898
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540311Satune Solving Time: 0.092562
+     [java] 1594753540318 Original Encoding Solving Time: 0.059895
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540318Satune Solving Time: 0.113261
+     [java] Path Solving Time: 2.951489
+     [java] Path Solving Time: 1.787072
+     [java] 1594753540349 Original Encoding Solving Time: 0.404199
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540349Satune Solving Time: 28.332174
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753540388 Original Encoding Solving Time: 0.054173
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540388Satune Solving Time: 0.099125
+     [java] 1594753540395 Original Encoding Solving Time: 0.057829
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540395Satune Solving Time: 0.089151
+     [java] 1594753540402 Original Encoding Solving Time: 0.032566
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540402Satune Solving Time: 0.094923
+     [java] 1594753540409 Original Encoding Solving Time: 0.043784
+     [java]  = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000047
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000089
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000047
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000082
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000091
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000014
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9cd7b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c4948f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9c9c60....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000107
+     [java] Elapse Encode time: 0.000147
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026552
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026706
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000050
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000094
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000044
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000088
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000067
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000108
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c79db20....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9da300....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c496e20....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] Encoding Graph Time: 0.000125
+     [java] Elapse Encode time: 0.000162
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.028155
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.028324
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000052
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000095
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000049
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000090
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000053
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER soisSat= false ,SatuneSat= false
+     [java] 1594753540409Satune Solving Time: 0.101673
+     [java] Path Solving Time: 2.618934
+     [java] Path Solving Time: 1.315453
+     [java] 1594753540440 Original Encoding Solving Time: 0.374697
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540440Satune Solving Time: 26.780173
+     [java] 1594753540476 Original Encoding Solving Time: 0.060744
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540476Satune Solving Time: 0.084686
+     [java] 1594753540483 Original Encoding Solving Time: 0.073283
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540483Satune Solving Time: 0.092093
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753540492 Original Encoding Solving Time: 0.033662
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540492Satune Solving Time: 0.088887
+     [java] 1594753540499 Original Encoding Solving Time: 0.040764
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540499Satune Solving Time: 0.091326
+     [java] Path Solving Time: 3.343973
+     [java] Path Solving Time: 1.474879
+     [java] 1594753540530 Original Encoding Solving Time: 1.019531
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540530Satune Solving Time: 29.45437
+     [java] 1594753540568 Original Encoding Solving Time: 0.059202
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540568Satune Solving Time: 0.096503
+     [java] 1594753540576 Original Encoding Solving Time: 0.050479
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540576Satune Solving Time: 0.088005
+     [java] 1594753540583 Original Encoding Solving Time: 0.031165
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540583Satune Solving Time: 0.091155
+     [java] 1594753540590 Original Encoding Solving Time: 0.056199
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540590Satune Solving Time: 0.119896
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 3.664797
+     [java] Path Solving Time: 1.482122
+     [java] 1594753540622 Original Encoding Solving Time: 0.496663
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540622Satune Solving Time: 27.269123
+     [java] 1594753540658 Original Encoding Solving Time: 0.055626
+     [java] lve time: 0.000095
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000006
+     [java] Decompose Order: 0.000006
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9dc860....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9dde90....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9db5d0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000138
+     [java] Elapse Encode time: 0.000168
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.026597
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.026771
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000080
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000047
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000087
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9df150....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e19c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e0360....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] Encoding Graph Time: 0.000074
+     [java] Elapse Encode time: 0.000104
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.029331
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.029442
+     [java] Elapse Encode time: 0.000036
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000091
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000036
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000086
+     [java] Elapse Encode time: 0.000042
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000058
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000114
+     [java] Polarity time: 0.000009
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9dde40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9d1320....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9db580....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000121
+     [java] Elapse Encode time: 0.000164
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027090
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027261
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data isSat= true ,SatuneSat= true
+     [java] 1594753540658Satune Solving Time: 0.087724
+     [java] 1594753540666 Original Encoding Solving Time: 0.069271
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540666Satune Solving Time: 0.224137
+     [java] 1594753540674 Original Encoding Solving Time: 0.04519
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540674Satune Solving Time: 0.104197
+     [java] 1594753540682 Original Encoding Solving Time: 0.044689
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540682Satune Solving Time: 0.116538
+     [java] Path Solving Time: 2.701315
+     [java] Path Solving Time: 1.891933
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753540714 Original Encoding Solving Time: 0.441976
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540714Satune Solving Time: 28.623822
+     [java] 1594753540752 Original Encoding Solving Time: 0.054497
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540752Satune Solving Time: 0.095972
+     [java] 1594753540759 Original Encoding Solving Time: 0.056917
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540759Satune Solving Time: 0.09812
+     [java] 1594753540767 Original Encoding Solving Time: 0.031965
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540767Satune Solving Time: 0.087131
+     [java] 1594753540774 Original Encoding Solving Time: 0.053012
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540774Satune Solving Time: 0.116863
+     [java] Path Solving Time: 5.17697
+     [java] Path Solving Time: 1.367628
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753540808 Original Encoding Solving Time: 0.409835
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540808Satune Solving Time: 27.762653
+     [java] 1594753540844 Original Encoding Solving Time: 0.048601
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540844Satune Solving Time: 0.084896
+     [java] 1594753540850 Original Encoding Solving Time: 0.046566
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540850Satune Solving Time: 0.073551
+     [java] 1594753540858 Original Encoding Solving Time: 0.03328
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540858Satune Solving Time: 0.102437
+     [java] 1594753540865 Original Encoding Solving Time: 0.042564
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540865Satune Solving Time: 0.10543
+     [java] Path Solving Time: 4.284723
+     [java] Path Solving Time: 0.471361
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Renaming procedure ...
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753540898 Original Encoding Solving Time: 2.174767
+     [java] is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Elapse Encode time: 0.000036
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000174
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000219
+     [java] Elapse Encode time: 0.000035
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000054
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000099
+     [java] Elapse Encode time: 0.000035
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000068
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000112
+     [java] Polarity time: 0.000017
+     [java] Preprocess time: 0.000018
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c492a40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9eedc0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c244bd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] Encoding Graph Time: 0.000142
+     [java] Elapse Encode time: 0.000205
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.028396
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.028610
+     [java] Elapse Encode time: 0.000032
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000091
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000051
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000093
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000041
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Elapse Encode time: 0.000035
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000067
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000112
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c1e6e30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9eff40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f2630....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f0f60....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c230bb0....
+     [java] Encoding Graph Time: 0.000128
+     [java] Elapse Encode time: 0.000173
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 14      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027574
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027754
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000039
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000080
+     [java] Elapse Encode time: 0.000027
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000035
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000069
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000054
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000097
+     [java] Elapse Encode time: 0.000034
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000057
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000101
+     [java] serisSat= true ,SatuneSat= true
+     [java] 1594753540898Satune Solving Time: 23.493544
+     [java] 1594753540933 Original Encoding Solving Time: 0.0469
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753540933Satune Solving Time: 0.07982
+     [java] 1594753540941 Original Encoding Solving Time: 0.029651
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753540941Satune Solving Time: 0.10269
+     [java] Path Solving Time: 3.463077
+     [java] Path Solving Time: 0.384285
+     [java] 1594753540971 Original Encoding Solving Time: 0.381274
+     [java] ializing ...
+     [java] !{BooleanLogic<0x7f866c4a7520>: AND
+     [java] !{BooleanPredicate<0x7f866c79b810>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f6230>:{Set(1)<0x7f866c9f3eb0>:Members: 244, } 0x7f866c9f6230 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c7a7500>: 244}
+     [java] }
+     [java] !{BooleanPredicate<0x7f866c9f2000>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f0f60>:{Set(1)<0x7f866c9f29c0>:Members: 244, 250, } 0x7f866c9f0f60 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c7a7500>: 244}
+     [java] }
+     [java] }
+     [java] 
+     [java] !{BooleanLogic<0x7f866c9eeb30>: AND
+     [java] !{BooleanPredicate<0x7f866c9f13b0>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f3c30>:{Set(1)<0x7f866c9dd860>:Members: 245, 246, } 0x7f866c9f3c30 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c391d50>: 245}
+     [java] }
+     [java] !{BooleanPredicate<0x7f866c494230>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f38f0>:{Set(1)<0x7f866c9e0360>:Members: 245, 246, } 0x7f866c9f38f0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c391d50>: 245}
+     [java] }
+     [java] }
+     [java] 
+     [java] !{BooleanLogic<0x7f866c9d0fe0>: AND
+     [java] !{BooleanPredicate<0x7f866c4c4640>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f3c30>:{Set(1)<0x7f866c9dd860>:Members: 245, 246, } 0x7f866c9f3c30 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c9cacc0>: 246}
+     [java] }
+     [java] !{BooleanPredicate<0x7f866c9e08b0>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f38f0>:{Set(1)<0x7f866c9e0360>:Members: 245, 246, } 0x7f866c9f38f0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c9cacc0>: 246}
+     [java] }
+     [java] }
+     [java] 
+     [java] {BooleanPredicate<0x7f866c79bd90>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9e16c0>:{Set(1)<0x7f866c494cd0>:Members: 247, } 0x7f866c9e16c0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c495090>: 247}
+     [java] }
+     [java] 
+     [java] {BooleanPredicate<0x7f866c9cc3c0>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f3bb0>:{Set(1)<0x7f866c244c50>:Members: 248, } 0x7f866c9f3bb0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c79de60>: 248}
+     [java] }
+     [java] 
+     [java] {BooleanPredicate<0x7f866c9f5c00>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c492a40>:{Set(1)<0x7f866c9f2090>:Members: 249, } 0x7f866c492a40 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c38e820>: 249}
+     [java] }
+     [java] 
+     [java] {BooleanPredicate<0x7f866c9f4f70>:
+     [java] PredicateOperator: ==
+     [java] elements:
+     [java] {ElementSet<0x7f866c9f0f60>:{Set(1)<0x7f866c9f29c0>:Members: 244, 250, } 0x7f866c9f0f60 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f866c4c3190>: 250}
+     [java] }
+     [java] 
+     [java] Polarity time: 0.000014
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f6230....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f3c30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f38f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e16c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f3bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c492a40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f0f60....
+     [java] Encoding Graph Time: 0.000104
+     [java] Elapse Encode time: 0.000147
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.023331
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.023484
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000037
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000076
+     [java] Elapse Encode time: 0.000033
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 19      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000055
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000097
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000015
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f3c30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f6230....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e5de0....
+     [java] INFO: naive encoder is making the isSat= true ,SatuneSat= true
+     [java] 1594753540971Satune Solving Time: 27.151788
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594753541007 Original Encoding Solving Time: 0.047513
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753541007Satune Solving Time: 0.084413
+     [java] 1594753541015 Original Encoding Solving Time: 0.01914
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753541015Satune Solving Time: 0.088109
+     [java] Path Solving Time: 1.828193
+     [java] Path Solving Time: 0.330935
+     [java] 1594753541043 Original Encoding Solving Time: 0.466639
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753541043Satune Solving Time: 27.589975
+     [java] 1594753541079 Original Encoding Solving Time: 0.046838
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753541079Satune Solving Time: 0.082641
+     [java] =========Statistics (time in milliseconds)=========
+     [java] Benchmark Id: 11
+     [java] Sketch Generation Time: 608.1687719999999
+     [java] Sketch Completion Time: 2418.8304510000007
+     [java] Compilation Time: 1268.0002710000003
+     [java] Running Test cases Time: 19.67078899999999
+     [java] Synthesis Time: 3046.6700120000005
+     [java] Total Time: 4314.670283000001
+     [java] Number of components: 4
+     [java] Number of holes: 7
+     [java] Number of completed programs: 153
+     [java] Number of sketches: 44
+     [java] Solution:
+     [java]  java.awt.Shape sypet_var261 = sypet_arg0;
+     [java]  java.awt.geom.AffineTransform sypet_var262 = java.awt.geom.AffineTransform.getShearInstance(sypet_arg1,sypet_arg2);
+     [java]  java.awt.geom.Path2D.Double sypet_var263 = new java.awt.geom.Path2D.Double(sypet_var261,sypet_var262);
+     [java]  java.awt.geom.Rectangle2D sypet_var264 = sypet_var263.getBounds2D();
+     [java]  return sypet_var264;
+     [java]  
+     [java] ============================
+     [java] decision about element 0x7f866c9ce540....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e5d00....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9ce660....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9e4ff0....
+     [java] Encoding Graph Time: 0.000123
+     [java] Elapse Encode time: 0.000171
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.026964
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027143
+     [java] Elapse Encode time: 0.000030
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000079
+     [java] Elapse Encode time: 0.000031
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 19      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000043
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000016
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f6230....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f3c30....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9d1f40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9fc920....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f3bb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c492a40....
+     [java] INFO: naive encoder is making the decision about element 0x7f866c9f0f60....
+     [java] Encoding Graph Time: 0.000151
+     [java] Elapse Encode time: 0.000196
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.027376
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.027582
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000039
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000078
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+
+BUILD SUCCESSFUL
+Total time: 9 seconds