--- /dev/null
+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/xml/27/benchmark27.json
+ [java] Benchmark Id: 27
+ [java] Method name: stringToElement
+ [java] Packages: [org.w3c.dom, javax.xml.parsers, org.xml.sax]
+ [java] Libraries: [./lib/rt7.jar]
+ [java] Source type(s): [java.lang.String]
+ [java] Target type: org.w3c.dom.Element
+ [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: 210
+ [java] #Methods: 1784
+ [java] Soot Time: 3475.631064
+ [java] PetriNet for path length: 1 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] PetriNet for path length: 2 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] PetriNet for path length: 3 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] PetriNet for path length: 4 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] PetriNet for path length: 5 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] Path Solving Time: 12.812716
+ [java] PetriNet for path length: 6 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] Path Solving Time: 8.137037
+ [java] PetriNet for path length: 7 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] Path Solving Time: 10.22481
+ [java] Path Solving Time: 36.062633
+ [java] Path Solving Time: 7.222453
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756775214 Original Encoding Solving Time: 0.581715
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756775214Satune Solving Time: 35.631842
+ [java] Renaming procedure ...
+ [java] Path Solving Time: 27.28137
+ [java] Path Solving Time: 12.178446
+ [java] 1594756775650 Original Encoding Solving Time: 3.53373
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756775650Satune Solving Time: 35.117953
+ [java] Path Solving Time: 14.515293
+ [java] Path Solving Time: 4.619761
+ [java] 1594756775780 Original Encoding Solving Time: 1.221913
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756775780Satune Solving Time: 43.38255
+ [java] Path Solving Time: 14.249988
+ [java] Path Solving Time: 3.137989
+ [java] Path Solving Time: 4.876158
+ [java] PetriNet for path length: 8 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] Path Solving Time: 5.40847
+ [java] Path Solving Time: 17.563701
+ [java] Path Solving Time: 4.340796
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756777517 Original Encoding Solving Time: 0.737776
+ [java] Polarity time: 0.000023
+ [java] Preprocess time: 0.000017
+ [java] Decompose Order: 0.000010
+ [java] INFO: naive encoder is making the decision about element 0x7f019c23f410....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4a7b30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c23f130....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c23f2a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c23f580....
+ [java] Encoding Graph Time: 0.000201
+ [java] Elapse Encode time: 0.000271
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.035315
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.035599
+ [java] Setting UNSAT %%%
+ [java] serializing ...
+ [java] {BooleanPredicate<0x7f019c969730>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f019c4deda0>:{Set(1)<0x7f019c4ded40>:Members: 6, } 0x7f019c4deda0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f019c21f750>: 6}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f019c21fa80>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f019c3dabc0>:{Set(1)<0x7f019c3dab80>:Members: 7, } 0x7f019c3dabc0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f019c21f980>: 7}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f019c21fd20>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f019c4deb60>:{Set(1)<0x7f019c3dac90>:Members: 8, } 0x7f019c4deb60 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f019c21fc20>: 8}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f019c2200e0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f019c4dec70>:{Set(1)<0x7f019c4dec30>:Members: 9, } 0x7f019c4dec70 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f019c21fec0>: 9}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f019c2202e0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f019c21f640>:{Set(1)<0x7f019c3dacd0>:Members: 10, } 0x7f019c21f640 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f019c220230>: 10}
+ [java] }
+ [java]
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4deda0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3dabc0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4deb60....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4dec70....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c21f640....
+ [java] Encoding Graph Time: 0.000077
+ [java] Elapse Encode time: 0.000097
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.035006
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.035109
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019c283510....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c2832d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c2833e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c283680....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4a46f0....
+ [java] Encoding Graph Time: 0.000171
+ [java] Elapse Encode time: 0.000219
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.043146
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.043374
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019c281c60....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4f2c20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c281d70....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4f2ab0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4f2d90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4f2f00....
+ [java] Encoding Graph Time: 0.000119
+ [java] Elapse Encode time: 0.000158
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047851
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVEisSat= true ,SatuneSat= true
+ [java] 1594756777517Satune Solving Time: 48.034275
+ [java] Path Solving Time: 15.765263
+ [java] Path Solving Time: 6.618356
+ [java] 1594756777651 Original Encoding Solving Time: 1.059896
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756777651Satune Solving Time: 38.618234
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 78.811459
+ [java] Path Solving Time: 7.532769
+ [java] Path Solving Time: 8.849584
+ [java] Path Solving Time: 3.312762
+ [java] Path Solving Time: 6.557359
+ [java] 1594756777855 Original Encoding Solving Time: 0.662194
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756777855Satune Solving Time: 40.426902
+ [java] Path Solving Time: 20.705594
+ [java] Path Solving Time: 6.499267
+ [java] Path Solving Time: 7.75868
+ [java] 1594756777984 Original Encoding Solving Time: 1.979584
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756777984Satune Solving Time: 37.637741
+ [java] Path Solving Time: 8.782096
+ [java] Path Solving Time: 3.838777
+ [java] 1594756778084 Original Encoding Solving Time: 0.318391
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756778084Satune Solving Time: 39.180063
+ [java] Path Solving Time: 24.339277
+ [java] Path Solving Time: 9.423614
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756778207 Original Encoding Solving Time: 0.446143
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756778207Satune Solving Time: 39.752091
+ [java] Path Solving Time: 11.423496
+ [java] Path Solving Time: 5.046331
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756778313 Original Encoding Solving Time: 0.487506
+ [java] R solve time: 0.048016
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000008
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d2f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d33f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d3370....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d32f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d3270....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c4d5910....
+ [java] Encoding Graph Time: 0.000136
+ [java] Elapse Encode time: 0.000177
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.038425
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.038609
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000011
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9969b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c996930....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c996ab0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c996a30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c996630....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c997850....
+ [java] Encoding Graph Time: 0.000114
+ [java] Elapse Encode time: 0.000158
+ [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.040253
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.040419
+ [java] Polarity time: 0.000011
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9b02e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9b0260....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9b03e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9b0360....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9affa0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c998390....
+ [java] Encoding Graph Time: 0.000144
+ [java] Elapse Encode time: 0.000194
+ [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.037426
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.037628
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9cb850....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9cbb30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9cbcb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9cbc30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9cbbb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9e1f20....
+ [java] Encoding Graph Time: 0.000067
+ [java] Elapse Encode time: 0.000089
+ [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.039078
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039172
+ [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 0x7f019c9e5480....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9e5580....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9e5500....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9e5160....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9fbcd0....
+ [java] Encoding Graph Time: 0.000087
+ [java] Elapse Encode time: 0.000109
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.039630
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039745
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9feaisSat= true ,SatuneSat= true
+ [java] 1594756778313Satune Solving Time: 54.381506
+ [java] Path Solving Time: 11.699805
+ [java] Path Solving Time: 3.99598
+ [java] 1594756778434 Original Encoding Solving Time: 0.975483
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756778434Satune Solving Time: 46.484288
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 10.032602
+ [java] PetriNet for path length: 9 [places: 236 ; transitions: 1917 ; edges: 4767]
+ [java] Path Solving Time: 5.976608
+ [java] Path Solving Time: 12.112774
+ [java] Path Solving Time: 5.451257
+ [java] 1594756780154 Original Encoding Solving Time: 0.505035
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756780154Satune Solving Time: 47.069064
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] 1594756780215 Original Encoding Solving Time: 0.050446
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756780215Satune Solving Time: 0.058744
+ [java] Path Solving Time: 12.974009
+ [java] Path Solving Time: 3.407783
+ [java] 1594756780272 Original Encoding Solving Time: 0.404384
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756780272Satune Solving Time: 44.772133
+ [java] 1594756780330 Original Encoding Solving Time: 0.04924
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756780330Satune Solving Time: 0.033713
+ [java] Path Solving Time: 14.468919
+ [java] Path Solving Time: 3.671973
+ [java] 1594756780389 Original Encoding Solving Time: 0.436295
+ [java] f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9feeb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9fee30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9fea20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c9fedb0....
+ [java] Encoding Graph Time: 0.000103
+ [java] Elapse Encode time: 0.000129
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054239
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054375
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca17ee0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca183b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca18330....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca17fb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca182b0....
+ [java] Encoding Graph Time: 0.000095
+ [java] Elapse Encode time: 0.000121
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046349
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046476
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31af0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31db0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca33b00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca192d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca19440....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca33990....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca33c70....
+ [java] Encoding Graph Time: 0.000127
+ [java] Elapse Encode time: 0.000159
+ [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.046895
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047060
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca192d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31db0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31eb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31af0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4d9b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4dad0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4ddf0....
+ [java] Encoding Graph Time: 0.000110
+ [java] Elapse Encode time: 0.000145
+ [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.044614
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044764
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4fea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31eb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31af0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31db0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca192d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4ffc0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca502e0....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] Encoding Graph Time: isSat= true ,SatuneSat= true
+ [java] 1594756780389Satune Solving Time: 46.097
+ [java] 1594756780447 Original Encoding Solving Time: 0.04748
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756780447Satune Solving Time: 0.032042
+ [java] Path Solving Time: 8.736581
+ [java] Path Solving Time: 3.492957
+ [java] 1594756780501 Original Encoding Solving Time: 0.376604
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756780501Satune Solving Time: 45.368597
+ [java] 1594756780562 Original Encoding Solving Time: 0.071706
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756780562Satune Solving Time: 0.040879
+ [java] Path Solving Time: 17.54933
+ [java] Path Solving Time: 3.688666
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756780624 Original Encoding Solving Time: 0.427481
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756780624Satune Solving Time: 45.967163
+ [java] 1594756780691 Original Encoding Solving Time: 0.037533
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756780691Satune Solving Time: 0.04276
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 26.467319
+ [java] Path Solving Time: 19.750955
+ [java] Path Solving Time: 40.046605
+ [java] Path Solving Time: 3.973765
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756780824 Original Encoding Solving Time: 1.360956
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756780824Satune Solving Time: 45.87867
+ [java] Path Solving Time: 10.722981
+ [java] Path Solving Time: 3.6614
+ [java] 1594756780941 Original Encoding Solving Time: 0.313018
+ [java] 0.000115
+ [java] Elapse Encode time: 0.000152
+ [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.045929
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046089
+ [java] Elapse Encode time: 0.000020
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [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 0x7f019ca31af0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca50360....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca31eb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4f550....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4f090....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4f1b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca4f4d0....
+ [java] Encoding Graph Time: 0.000075
+ [java] Elapse Encode time: 0.000100
+ [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.045239
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045349
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000037
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca503e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca52660....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca51a30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca519b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca514f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca51610....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca51930....
+ [java] Encoding Graph Time: 0.000137
+ [java] Elapse Encode time: 0.000183
+ [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.045769
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045959
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000038
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca514f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca519b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca503e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca51a30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca52660....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c29ba50....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c29b4b0....
+ [java] Encoding Graph Time: 0.000145
+ [java] Elapse Encode time: 0.000190
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045673
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045869
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ff670....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffa40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ff740....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c2bb8d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c2bba40....
+ [java] Encoding GrisSat= true ,SatuneSat= true
+ [java] 1594756780941Satune Solving Time: 48.311989
+ [java] 1594756781004 Original Encoding Solving Time: 0.04465
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781004Satune Solving Time: 0.038894
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 9.997251
+ [java] Path Solving Time: 3.544121
+ [java] 1594756781058 Original Encoding Solving Time: 0.391432
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781058Satune Solving Time: 45.298024
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] 1594756781120 Original Encoding Solving Time: 0.02496
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781120Satune Solving Time: 0.045885
+ [java] Path Solving Time: 13.073076
+ [java] Path Solving Time: 5.795885
+ [java] 1594756781181 Original Encoding Solving Time: 0.504688
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781181Satune Solving Time: 44.136482
+ [java] 1594756781237 Original Encoding Solving Time: 0.019479
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781237Satune Solving Time: 0.033092
+ [java] Path Solving Time: 9.407774
+ [java] Path Solving Time: 3.477368
+ [java] 1594756781291 Original Encoding Solving Time: 0.422186
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781291Satune Solving Time: 45.021072
+ [java] 1594756781348 Original Encoding Solving Time: 0.019752
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781348Satune Solving Time: 0.033602
+ [java] Path Solving Time: 8.458258
+ [java] Path Solving Time: 3.415011
+ [java] 1594756781401 Original Encoding Solving Time: 0.405554
+ [java] aph Time: 0.000096
+ [java] Elapse Encode time: 0.000134
+ [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.048164
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.048305
+ [java] Elapse Encode time: 0.000024
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000035
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca562d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca55d90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca56250....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca55eb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca561d0....
+ [java] Encoding Graph Time: 0.000104
+ [java] Elapse Encode time: 0.000133
+ [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.045151
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045290
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000041
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000008
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca586f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca581b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca58670....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca582d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca585f0....
+ [java] Encoding Graph Time: 0.000120
+ [java] Elapse Encode time: 0.000162
+ [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.043958
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044127
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000030
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5aeb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5aa90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5ae30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5a970....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5adb0....
+ [java] Encoding Graph Time: 0.000098
+ [java] Elapse Encode time: 0.000131
+ [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.044877
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045013
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000030
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000020
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5d430....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5d010....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] INFO: naive encoder is making the decisisSat= true ,SatuneSat= true
+ [java] 1594756781401Satune Solving Time: 46.434965
+ [java] 1594756781459 Original Encoding Solving Time: 0.019444
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781459Satune Solving Time: 0.035147
+ [java] Path Solving Time: 8.465681
+ [java] Path Solving Time: 3.789317
+ [java] 1594756781513 Original Encoding Solving Time: 0.390996
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781513Satune Solving Time: 48.439768
+ [java] 1594756781575 Original Encoding Solving Time: 0.020002
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781575Satune Solving Time: 0.03466
+ [java] Path Solving Time: 8.718171
+ [java] Path Solving Time: 3.337328
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756781627 Original Encoding Solving Time: 0.290487
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781627Satune Solving Time: 45.388976
+ [java] 1594756781683 Original Encoding Solving Time: 0.020256
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781683Satune Solving Time: 0.033873
+ [java] Path Solving Time: 7.552248
+ [java] Path Solving Time: 3.109826
+ [java] Done with finding holes : Flag = false
+ [java] 1594756781735 Original Encoding Solving Time: 0.409938
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781735Satune Solving Time: 45.090398
+ [java] 1594756781792 Original Encoding Solving Time: 0.025054
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781792Satune Solving Time: 0.042902
+ [java] Path Solving Time: 13.474867
+ [java] Path Solving Time: 5.52908
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] 1594756781855 Original Encoding Solving Time: 1.136251
+ [java] ion about element 0x7f019ca5d3b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5cef0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5d330....
+ [java] Encoding Graph Time: 0.000125
+ [java] Elapse Encode time: 0.000177
+ [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.046241
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046427
+ [java] Elapse Encode time: 0.000023
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000031
+ [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 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5fc00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5eb10....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5fb80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5eeb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5ee30....
+ [java] Encoding Graph Time: 0.000102
+ [java] Elapse Encode time: 0.000134
+ [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.048289
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.048431
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000031
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca620a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5d4b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca62020....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca61be0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca61fa0....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000093
+ [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.045283
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045381
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000030
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca47340....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca46e80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca472c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca47240....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca471c0....
+ [java] Encoding Graph Time: 0.000106
+ [java] Elapse Encode time: 0.000137
+ [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.044939
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045083
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000038
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca47340....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3fisSat= true ,SatuneSat= true
+ [java] 1594756781855Satune Solving Time: 45.462533
+ [java] 1594756781912 Original Encoding Solving Time: 0.043405
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756781912Satune Solving Time: 0.034672
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 21.458523
+ [java] Path Solving Time: 3.651856
+ [java] 1594756781980 Original Encoding Solving Time: 0.301204
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756781980Satune Solving Time: 44.631462
+ [java] 1594756782039 Original Encoding Solving Time: 0.024616
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756782039Satune Solving Time: 0.043938
+ [java] Path Solving Time: 49.834842
+ [java] Path Solving Time: 3.398289
+ [java] 1594756782135 Original Encoding Solving Time: 0.292735
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756782135Satune Solving Time: 44.769283
+ [java] 1594756782191 Original Encoding Solving Time: 0.019019
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756782191Satune Solving Time: 0.035463
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 68.828146
+ [java] Path Solving Time: 27.642174
+ [java] Path Solving Time: 3.370242
+ [java] Path Solving Time: 74.377006
+ [java] 1594756782408 Original Encoding Solving Time: 0.32779
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756782408Satune Solving Time: 45.2837
+ [java] Path Solving Time: 66.53604
+ [java] Path Solving Time: 30.315597
+ [java] Path Solving Time: 27.831768
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756782633 Original Encoding Solving Time: 0.280243
+ [java] fac0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca66bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca67010....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca66f90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca66f10....
+ [java] Encoding Graph Time: 0.000086
+ [java] Elapse Encode time: 0.000113
+ [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.045336
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045454
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000031
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca67090....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca47340....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca6e890....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca6ec30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca6e770....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca6ebb0....
+ [java] Encoding Graph Time: 0.000068
+ [java] Elapse Encode time: 0.000091
+ [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.044527
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044624
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000039
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca66750....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca71460....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca6ecb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca71040....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca713e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca70f20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca71360....
+ [java] Encoding Graph Time: 0.000069
+ [java] Elapse Encode time: 0.000091
+ [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.044664
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044762
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000032
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca66750....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c3ffb40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca79ca0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca79c20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca79760....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca79880....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000095
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045174
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045275
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000003
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca642c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca64340....
+ [java] INFO: naive encoder is making the decision about element isSat= true ,SatuneSat= true
+ [java] 1594756782633Satune Solving Time: 44.664992
+ [java] Path Solving Time: 11.704041
+ [java] Path Solving Time: 15.473554
+ [java] 1594756782760 Original Encoding Solving Time: 0.291016
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756782760Satune Solving Time: 45.450888
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 44.372348
+ [java] Path Solving Time: 13.713508
+ [java] Path Solving Time: 17.268247
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756782931 Original Encoding Solving Time: 0.300717
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756782931Satune Solving Time: 45.961489
+ [java] Path Solving Time: 18.056074
+ [java] Path Solving Time: 31.792547
+ [java] Path Solving Time: 15.515078
+ [java] 1594756783096 Original Encoding Solving Time: 0.341626
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756783096Satune Solving Time: 45.542814
+ [java] Path Solving Time: 21.102428
+ [java] Path Solving Time: 46.532929
+ [java] Path Solving Time: 14.68388
+ [java] 1594756783280 Original Encoding Solving Time: 0.32844
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756783280Satune Solving Time: 45.717306
+ [java] Path Solving Time: 23.050544
+ [java] Path Solving Time: 32.396991
+ [java] Path Solving Time: 10.088155
+ [java] 1594756783443 Original Encoding Solving Time: 0.355833
+ [java] 0x7f019ca64090....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca64160....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca64240....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca46230....
+ [java] Encoding Graph Time: 0.000067
+ [java] Elapse Encode time: 0.000087
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044566
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044658
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000003
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca8f600....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca8f580....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca8f130....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca8f200....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca8f500....
+ [java] INFO: naive encoder is making the decision about element 0x7f019caa5af0....
+ [java] Encoding Graph Time: 0.000059
+ [java] Elapse Encode time: 0.000079
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045360
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045444
+ [java] Setting UNSAT %%%
+ [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 0x7f019ca60050....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca60370....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca60470....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca603f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ca5ff80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cabf420....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cabf590....
+ [java] Encoding Graph Time: 0.000066
+ [java] Elapse Encode time: 0.000090
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045858
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045953
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f019cac2db0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cac2a90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019caa9c40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019caa9d90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cad9450....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cad95c0....
+ [java] Encoding Graph Time: 0.000087
+ [java] Elapse Encode time: 0.000120
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045405
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045534
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb007a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb00ed0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb00bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb00910....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb00a80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb00d60....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb01040....
+ [java] Encoding Graph Time: 0.000061
+ [java] Elapse Encode time: 0.000084
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045621
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045710
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb049a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1b040..isSat= true ,SatuneSat= true
+ [java] 1594756783443Satune Solving Time: 47.92289
+ [java] Path Solving Time: 18.048334
+ [java] Path Solving Time: 5.289417
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756783570 Original Encoding Solving Time: 0.383896
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756783570Satune Solving Time: 46.067473
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] Path Solving Time: 14.184622
+ [java] Path Solving Time: 20.177372
+ [java] Path Solving Time: 5.389542
+ [java] 1594756783708 Original Encoding Solving Time: 1.012123
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756783708Satune Solving Time: 44.300129
+ [java] Path Solving Time: 47.383806
+ [java] Path Solving Time: 7.565759
+ [java] Path Solving Time: 5.193889
+ [java] 1594756783864 Original Encoding Solving Time: 0.358453
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756783864Satune Solving Time: 46.177407
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 36.506167
+ [java] Path Solving Time: 7.898947
+ [java] 1594756784010 Original Encoding Solving Time: 0.340437
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784010Satune Solving Time: 47.947655
+ [java] Path Solving Time: 30.815354
+ [java] Path Solving Time: 6.04632
+ [java] 1594756784148 Original Encoding Solving Time: 0.385334
+ [java] ..
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb04a20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb044e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb04600....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb04920....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1b1b0....
+ [java] Encoding Graph Time: 0.000100
+ [java] Elapse Encode time: 0.000133
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047775
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047914
+ [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 0x7f019cb1ea50....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1ead0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1e590....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1e6b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb1e9d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb35060....
+ [java] Encoding Graph Time: 0.000059
+ [java] Elapse Encode time: 0.000095
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045958
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046059
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb4e5f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb4e8d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb4ea40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb38260....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb38560....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb4e760....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb4ebb0....
+ [java] Encoding Graph Time: 0.000049
+ [java] Elapse Encode time: 0.000081
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044205
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044292
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb52230....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb522b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb51d70....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb51e90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb521b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb68750....
+ [java] Encoding Graph Time: 0.000046
+ [java] Elapse Encode time: 0.000071
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046092
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046170
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb84650....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cac42f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb847a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb84910....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb84a80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb84bf0....
+ [java] Encoding Graph Time: 0.000051
+ [java] Elapse Encode time: 0.000078
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047856
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047940
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000014
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb88230....
+ [java] INFO: naive eisSat= true ,SatuneSat= true
+ [java] 1594756784148Satune Solving Time: 46.444035
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 29.760085
+ [java] Path Solving Time: 71.647451
+ [java] Path Solving Time: 5.497978
+ [java] 1594756784354 Original Encoding Solving Time: 0.343012
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784354Satune Solving Time: 45.034375
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 32.239125
+ [java] Path Solving Time: 5.602824
+ [java] 1594756784489 Original Encoding Solving Time: 0.327301
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784489Satune Solving Time: 45.023743
+ [java] Path Solving Time: 24.575936
+ [java] Path Solving Time: 6.211055
+ [java] 1594756784617 Original Encoding Solving Time: 0.321166
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784617Satune Solving Time: 45.126851
+ [java] Path Solving Time: 10.327747
+ [java] Path Solving Time: 6.409508
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756784732 Original Encoding Solving Time: 0.388389
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784732Satune Solving Time: 46.671014
+ [java] Path Solving Time: 10.592223
+ [java] Path Solving Time: 5.759113
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] 1594756784848 Original Encoding Solving Time: 0.371243
+ [java] ncoder is making the decision about element 0x7f019cb87f30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb9e5d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb9e740....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb9e8b0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb9ea20....
+ [java] Encoding Graph Time: 0.000135
+ [java] Elapse Encode time: 0.000195
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046232
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046434
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019cba1be0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cba2030....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cba1cb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cba1fb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbb84e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbb8650....
+ [java] Encoding Graph Time: 0.000043
+ [java] Elapse Encode time: 0.000066
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044954
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045026
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbbbc30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbbbd30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbbbcb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbbb860....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbbb930....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbd2160....
+ [java] Encoding Graph Time: 0.000056
+ [java] Elapse Encode time: 0.000085
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044924
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045016
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbd5820....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbd58a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbd54a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbd57a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbebcf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbebe60....
+ [java] Encoding Graph Time: 0.000044
+ [java] Elapse Encode time: 0.000069
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045044
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045119
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbef4a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbef520....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbef0d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cbef1a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc05cb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc05e20....
+ [java] Encoding Graph Time: 0.000071
+ [java] Elapse Encode time: 0.000100
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046556
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046663
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc09160....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc095isSat= true ,SatuneSat= true
+ [java] 1594756784848Satune Solving Time: 45.155009
+ [java] Path Solving Time: 13.627885
+ [java] Path Solving Time: 5.545971
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] 1594756784963 Original Encoding Solving Time: 0.289489
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756784963Satune Solving Time: 45.266501
+ [java] Path Solving Time: 9.616843
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] Path Solving Time: 5.224212
+ [java] 1594756785074 Original Encoding Solving Time: 0.41206
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756785074Satune Solving Time: 45.762195
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] Path Solving Time: 11.862676
+ [java] Path Solving Time: 5.447691
+ [java] 1594756785188 Original Encoding Solving Time: 0.261416
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756785188Satune Solving Time: 46.621069
+ [java] Path Solving Time: 9.281443
+ [java] Path Solving Time: 5.25642
+ [java] 1594756785299 Original Encoding Solving Time: 0.257245
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756785299Satune Solving Time: 46.422046
+ [java] Path Solving Time: 12.955715
+ [java] Path Solving Time: 5.752116
+ [java] 1594756785414 Original Encoding Solving Time: 0.384739
+ [java] 60....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc094e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc09090....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc09460....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc1f9c0....
+ [java] Encoding Graph Time: 0.000051
+ [java] Elapse Encode time: 0.000076
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045066
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045147
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc23000....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc23100....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc23080....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc22c30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc22d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc3d560....
+ [java] Encoding Graph Time: 0.000038
+ [java] Elapse Encode time: 0.000065
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045188
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045259
+ [java] Setting UNSAT %%%
+ [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 0x7f019cc40ba0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc40ca0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc40c20....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc407d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc408a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc56f60....
+ [java] Encoding Graph Time: 0.000040
+ [java] Elapse Encode time: 0.000061
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.045686
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045754
+ [java] Setting UNSAT %%%
+ [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 0x7f019cc66720....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc66820....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc667a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc66350....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc66420....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc6ab80....
+ [java] Encoding Graph Time: 0.000042
+ [java] Elapse Encode time: 0.000065
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046539
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046611
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc74180....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc74280....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc74200....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc73e40....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc73f10....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc8a640....
+ [java] Encoding Graph Time: 0.000038
+ [java] Elapse Encode time: 0.000064
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046344
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046414
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc8d890....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc8dc90....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] INFO: naive encoder is making the decision about isSat= true ,SatuneSat= true
+ [java] 1594756785414Satune Solving Time: 47.618411
+ [java] Path Solving Time: 11.306116
+ [java] Path Solving Time: 5.884826
+ [java] 1594756785532 Original Encoding Solving Time: 0.33129
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756785532Satune Solving Time: 54.856126
+ [java] Path Solving Time: 8.071562
+ [java] Path Solving Time: 14.010419
+ [java] Path Solving Time: 3.899165
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756785663 Original Encoding Solving Time: 0.401228
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756785663Satune Solving Time: 44.805695
+ [java] =========Statistics (time in milliseconds)=========
+ [java] Benchmark Id: 27
+ [java] Sketch Generation Time: 2033.9514380000005
+ [java] Sketch Completion Time: 4520.023097000001
+ [java] Compilation Time: 874.9431
+ [java] Running Test cases Time: 70.841163
+ [java] Synthesis Time: 6624.815698000001
+ [java] Total Time: 7499.758798000001
+ [java] Number of components: 7
+ [java] Number of holes: 8
+ [java] Number of completed programs: 103
+ [java] Number of sketches: 52
+ [java] Solution:
+ [java] java.io.StringReader sypet_var334 = new java.io.StringReader(sypet_arg0);
+ [java] java.io.Reader sypet_var335 = sypet_var334;
+ [java] org.xml.sax.InputSource sypet_var336 = new org.xml.sax.InputSource(sypet_var335);
+ [java] javax.xml.parsers.DocumentBuilderFactory sypet_var337 = javax.xml.parsers.DocumentBuilderFactory.newInstance();
+ [java] javax.xml.parsers.DocumentBuilder sypet_var338 = sypet_var337.newDocumentBuilder();
+ [java] org.w3c.dom.Document sypet_var339 = sypet_var338.parse(sypet_var336);
+ [java] org.w3c.dom.Element sypet_var340 = sypet_var339.getDocumentElement();
+ [java] return sypet_var340;
+ [java]
+ [java] ============================
+ [java] element 0x7f019cc8dc10....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc8d7c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cc8db90....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cca41a0....
+ [java] Encoding Graph Time: 0.000093
+ [java] Elapse Encode time: 0.000127
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047475
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047609
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb3a80....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb3b00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb3630....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb3700....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb3a00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019cb6cd40....
+ [java] Encoding Graph Time: 0.000063
+ [java] Elapse Encode time: 0.000092
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054749
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054848
+ [java] Setting UNSAT %%%
+ [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 0x7f019c422a30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019c422b00....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccb9660....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccd1210....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccd0f30....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccd10a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccd1380....
+ [java] INFO: naive encoder is making the decision about element 0x7f019ccd14f0....
+ [java] Encoding Graph Time: 0.000039
+ [java] Elapse Encode time: 0.000065
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044728
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044798
+ [java] Setting UNSAT %%%
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+
+BUILD SUCCESSFUL
+Total time: 20 seconds
projects / Benchmarks_CSolver.git / blobdiff