Adding sypet to repo
[Benchmarks_CSolver.git] / sypet / output / xml / benchmark29.log
diff --git a/sypet/output/xml/benchmark29.log b/sypet/output/xml/benchmark29.log
new file mode 100644 (file)
index 0000000..a44500e
--- /dev/null
@@ -0,0 +1,1581 @@
+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/29/benchmark29.json
+     [java] Benchmark Id: 29
+     [java] Method name: evaluateByXpath
+     [java] Packages: [org.w3c.dom, javax.xml, org.xml.sax]
+     [java] Libraries: [./lib/rt7.jar]
+     [java] Source type(s): [java.io.File, java.lang.String, javax.xml.namespace.QName]
+     [java] Target type: java.lang.Object
+     [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: 599
+     [java] #Methods: 4130
+     [java] Soot Time: 3595.014864
+     [java] PetriNet for path length: 1 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] PetriNet for path length: 2 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] PetriNet for path length: 3 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] PetriNet for path length: 4 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] PetriNet for path length: 5 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] Path Solving Time: 46.668735
+     [java] Path Solving Time: 70.174674
+     [java] PetriNet for path length: 6 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] Path Solving Time: 74.558169
+     [java] Path Solving Time: 699.405512
+     [java] Path Solving Time: 237.67149
+     [java] PetriNet for path length: 7 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] Path Solving Time: 223.496827
+     [java] Path Solving Time: 8126.39586
+     [java] Path Solving Time: 1513.483461
+     [java] PetriNet for path length: 8 [places: 623 ; transitions: 4240 ; edges: 10563]
+     [java] Path Solving Time: 101.732096
+     [java] Path Solving Time: 211.995397
+     [java] Path Solving Time: 603.084261
+     [java] Path Solving Time: 5.103872
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594756825950 Original Encoding Solving Time: 0.648801
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756825950Satune Solving Time: 61.190066
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594756826295 Original Encoding Solving Time: 0.074078
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756826295Satune Solving Time: 0.104101
+     [java] 1594756826318 Original Encoding Solving Time: 0.041835
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756826318Satune Solving Time: 0.089843
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 110.338582
+     [java] Path Solving Time: 411.10498
+     [java] Path Solving Time: 55.237342
+     [java] Path Solving Time: 5.140556
+     [java] 1594756826964 Original Encoding Solving Time: 0.46173
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756826964Satune Solving Time: 63.94564
+     [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] 1594756827051 Original Encoding Solving Time: 0.074527
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756827051Satune Solving Time: 0.037409
+     [java] Path Solving Time: 348.382605
+     [java] Path Solving Time: 86.352365
+     [java] Path Solving Time: 355.702741
+     [java] Path Solving Time: 5.135981
+     [java] 1594756827908 Original Encoding Solving Time: 0.330235
+     [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] 1594756827908Satune Solving Time: 64.140124
+     [java] 1594756827991 Original Encoding Solving Time: 0.031356
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756827991Satune Solving Time: 0.038781
+     [java] Path Solving Time: 64.446842
+     [java] Path Solving Time: 49.379596
+     [java] Path Solving Time: 61.703186
+     [java] Path Solving Time: 5.411141
+     [java] 1594756828232 Original Encoding Solving Time: 0.354579
+     [java] Polarity time: 0.000054
+     [java] Preprocess time: 0.000015
+     [java] Decompose Order: 0.000009
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408d40....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4409190....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408bd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4409020....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4409300....
+     [java] Encoding Graph Time: 0.000121
+     [java] Elapse Encode time: 0.000217
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.060931
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.061160
+     [java] Elapse Encode time: 0.000028
+     [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.000039
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000077
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 20      #Vars = 11
+     [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.000085
+     [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 0x7f53a48da050....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48da0d0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48d9f50....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48d9fd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48d9c70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a444cf20....
+     [java] Encoding Graph Time: 0.000100
+     [java] Elapse Encode time: 0.000128
+     [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.063798
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063932
+     [java] Elapse Encode time: 0.000024
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000033
+     [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 0x7f53a4447330....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44472b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4447230....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44471b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f0920....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f1160....
+     [java] Encoding Graph Time: 0.000070
+     [java] Elapse Encode time: 0.000095
+     [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.064031
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064132
+     [java] Elapse Encode time: 0.000025
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000034
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4449ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4449a30....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [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: naisSat= true ,SatuneSat= true
+     [java] 1594756828232Satune Solving Time: 64.185038
+     [java] 1594756828315 Original Encoding Solving Time: 0.04049
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756828315Satune Solving Time: 0.036327
+     [java] Path Solving Time: 221.0008
+     [java] Path Solving Time: 114.729612
+     [java] Path Solving Time: 207.159657
+     [java] Path Solving Time: 5.139293
+     [java] 1594756828922 Original Encoding Solving Time: 0.30759
+     [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] 1594756828922Satune Solving Time: 66.657858
+     [java] 1594756829007 Original Encoding Solving Time: 0.022759
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756829007Satune Solving Time: 0.038327
+     [java] Path Solving Time: 172.353402
+     [java] Path Solving Time: 150.120682
+     [java] Path Solving Time: 5.125141
+     [java] 1594756829394 Original Encoding Solving Time: 0.458944
+     [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] 1594756829394Satune Solving Time: 63.423761
+     [java] 1594756829481 Original Encoding Solving Time: 0.057707
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756829481Satune Solving Time: 0.099322
+     [java] 1594756829503 Original Encoding Solving Time: 0.031489
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756829503Satune Solving Time: 0.098531
+     [java] Path Solving Time: 181.463522
+     [java] Path Solving Time: 58.89815
+     [java] Path Solving Time: 428.704959
+     [java] 1594756830230 Original Encoding Solving Time: 0.438894
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var52 = new javax.xml.transform.stream.StreamResult(sypet_arg1);java.lang.String sypet_var53 = sypet_arg2.getPrefix();sypet_var52.setSystemId(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var55 = new javax.xml.bind.GetPropertyAction(sypet_var53);java.lang.Object sypet_var56 = sypet_var55.run();return sypet_var56;}
+     [java]                                                                                                                                                                                                                       ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var52 = new javax.xml.transform.stream.StreamResult(sypet_arg1);java.lang.String sypet_var53 = sypet_arg2.getPrefix();sypet_var52.setSystemId(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var55 = new javax.xml.bind.GetPropertyAction(sypet_var53);java.lang.Object sypet_var56 = sypet_var55.run();return sypet_var56;}
+     [java]                                                                                                                                                                                                                                                                          ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] ive encoder is making the decision about element 0x7f53a4448610....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44499b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4448590....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f1160....
+     [java] Encoding Graph Time: 0.000070
+     [java] Elapse Encode time: 0.000097
+     [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.064074
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064177
+     [java] Elapse Encode time: 0.000023
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000033
+     [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 0x7f53a48fb4a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb520....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb3a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb420....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb0c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f1160....
+     [java] Encoding Graph Time: 0.000109
+     [java] Elapse Encode time: 0.000137
+     [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.066507
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.066650
+     [java] Elapse Encode time: 0.000024
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000034
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fa410....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fa310....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fa490....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fa390....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f9ff0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a444ac30....
+     [java] Encoding Graph Time: 0.000145
+     [java] Elapse Encode time: 0.000187
+     [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.063220
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063414
+     [java] Elapse Encode time: 0.000035
+     [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.000046
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000094
+     [java] Elapse Encode time: 0.000038
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 20      #Vars = 11
+     [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.000094
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000015
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4405dd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4406cd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4405d50....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4401030....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4401350....
+     [java] Encoding Graph Time: 0.000119
+     [java] Elapse Encode time: 0.000157
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SisSat= true ,SatuneSat= true
+     [java] 1594756830230Satune Solving Time: 64.058141
+     [java] 1594756830319 Original Encoding Solving Time: 0.028098
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756830319Satune Solving Time: 0.04608
+     [java] Path Solving Time: 105.317008
+     [java] Path Solving Time: 217.804243
+     [java] Path Solving Time: 31.000803
+     [java] 1594756830732 Original Encoding Solving Time: 0.374556
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var60 = new javax.xml.transform.stream.StreamResult(sypet_arg1);java.lang.String sypet_var61 = sypet_arg2.getNamespaceURI();sypet_var60.setSystemId(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var63 = new javax.xml.bind.GetPropertyAction(sypet_var61);java.lang.Object sypet_var64 = sypet_var63.run();return sypet_var64;}
+     [java]                                                                                                                                                                                                                             ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var60 = new javax.xml.transform.stream.StreamResult(sypet_arg1);java.lang.String sypet_var61 = sypet_arg2.getNamespaceURI();sypet_var60.setSystemId(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var63 = new javax.xml.bind.GetPropertyAction(sypet_var61);java.lang.Object sypet_var64 = sypet_var63.run();return sypet_var64;}
+     [java]                                                                                                                                                                                                                                                                                ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756830732Satune Solving Time: 63.520471
+     [java] 1594756830808 Original Encoding Solving Time: 0.020942
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756830808Satune Solving Time: 0.037014
+     [java] Path Solving Time: 37.493219
+     [java] Path Solving Time: 57.668833
+     [java] Path Solving Time: 11.729576
+     [java] 1594756830975 Original Encoding Solving Time: 0.260892
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756830975Satune Solving Time: 63.653826
+     [java] 1594756831051 Original Encoding Solving Time: 0.049918
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756831051Satune Solving Time: 0.079501
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var68 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var69 = sypet_arg2.getPrefix();javax.xml.bind.GetPropertyAction sypet_var70 = new javax.xml.bind.GetPropertyAction(sypet_var69);sypet_var68.setSystemId(sypet_arg1);java.lang.Object sypet_var72 = sypet_var70.run();return sypet_var72;}
+     [java]                                                                                                                                                                                   ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var68 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var69 = sypet_arg2.getPrefix();javax.xml.bind.GetPropertyAction sypet_var70 = new javax.xml.bind.GetPropertyAction(sypet_var69);sypet_var68.setSystemId(sypet_arg1);java.lang.Object sypet_var72 = sypet_var70.run();return sypet_var72;}
+     [java]                                                                                                                                                                                                                                      ^
+     [java] 2 errors
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var68 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var69 = sypet_arg2.getPrefix();javax.xml.bind.GetPropertyAction sypet_var70 = new javax.xml.bind.GetPropertyAction(sypet_arg1);sypet_var68.setSystemId(sypet_var69);java.lang.Object sypet_var72 = sypet_var70.run();return sypet_var72;}
+     [java]                                                                                                                                                                                   ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var68 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var69 = sypet_arg2.getPrefix();javax.xml.bind.GetPropertyAction sypet_var70 = new javax.xml.bind.GetPropertyAction(sypet_arg1);sypet_var68.setSystemId(sypet_var69);java.lang.Object sypet_var72 = sypet_var70.run();return sypet_var72;}
+     [java]                                                                                                                                                                                                                                      ^
+     [java] 2 errors
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594756831061 Original Encoding Solving Time: 0.022534
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756831061Satune Solving Time: 0.081542
+     [java] Path Solving Time: 99.062858
+     [java] Path Solving Time: 199.242645
+     [java] Path Solving Time: 12.625275
+     [java] 1594756831432 Original Encoding Solving Time: 0.332952
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var76 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var77 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamResult sypet_var78 = new javax.xml.transform.stream.StreamResult(sypet_arg0);sypet_var78.setSystemId(sypet_var77);java.lang.Object sypet_var80 = sypet_var76.run();return sypet_var80;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var76 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var77 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamResult sypet_var78 = new javax.xml.transform.stream.StreamResult(sypet_arg0);sypet_var78.setSystemId(sypet_var77);java.lang.Object sypet_var80 = sypet_var76.run();return sypet_var80;}
+     [java]                                                                  ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756831432Satune Solving Time: 63.648659
+     [java] 1594756831507 Original Encoding Solving Time: 0.020393
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756831507Satune Solving Time: 0.035465
+     [java] Path Solving Time: 220.725269
+     [java] Path Solving Time: 299.741658
+     [java] Path Solving Time: 12.462602
+     [java] 1594756832100 Original Encoding Solving Time: 0.365394
+     [java] AT Solving time: 0.063881
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064050
+     [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.000041
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4405dd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4401350....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4401030....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4405d50....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4406cd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408ab0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4408990....
+     [java] Encoding Graph Time: 0.000100
+     [java] Elapse Encode time: 0.000127
+     [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.063377
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063511
+     [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.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000033
+     [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 0x7f53a4901680....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901580....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901040....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901600....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901500....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901160....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4901480....
+     [java] Encoding Graph Time: 0.000067
+     [java] Elapse Encode time: 0.000091
+     [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.063549
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063646
+     [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.000036
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000075
+     [java] Elapse Encode time: 0.000029
+     [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.000039
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000077
+     [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 0x7f53a470e030....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470e8b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470e0b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470dc10....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470daf0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470dfb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470df30....
+     [java] Encoding Graph Time: 0.000064
+     [java] Elapse Encode time: 0.000088
+     [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.063546
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063640
+     [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.000005
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4710210....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4710310....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4710290....
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var84 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var85 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var86 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.Object sypet_var87 = sypet_var84.run();sypet_var86.setPublicId(sypet_var85);return sypet_var87;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var84 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var85 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var86 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.Object sypet_var87 = sypet_var84.run();sypet_var86.setPublicId(sypet_var85);return sypet_var87;}
+     [java]                                                                  ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] INFO: naive encodeisSat= true ,SatuneSat= true
+     [java] 1594756832100Satune Solving Time: 64.691303
+     [java] 1594756832176 Original Encoding Solving Time: 0.021325
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756832176Satune Solving Time: 0.035079
+     [java] Path Solving Time: 88.561255
+     [java] Path Solving Time: 142.987411
+     [java] Path Solving Time: 12.322439
+     [java] 1594756832478 Original Encoding Solving Time: 0.275738
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756832478Satune Solving Time: 64.247723
+     [java] 1594756832555 Original Encoding Solving Time: 0.021475
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756832555Satune Solving Time: 0.04006
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var92 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var93 = sypet_arg2.getNamespaceURI();javax.xml.transform.stream.StreamSource sypet_var94 = new javax.xml.transform.stream.StreamSource(sypet_arg0);sypet_var94.setSystemId(sypet_var93);java.lang.Object sypet_var96 = sypet_var92.run();return sypet_var96;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var92 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var93 = sypet_arg2.getNamespaceURI();javax.xml.transform.stream.StreamSource sypet_var94 = new javax.xml.transform.stream.StreamSource(sypet_arg0);sypet_var94.setSystemId(sypet_var93);java.lang.Object sypet_var96 = sypet_var92.run();return sypet_var96;}
+     [java]                                                                  ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 128.425107
+     [java] Path Solving Time: 88.595859
+     [java] Path Solving Time: 12.507131
+     [java] 1594756832842 Original Encoding Solving Time: 0.416175
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var100 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var101 = sypet_arg2.getLocalPart();javax.xml.transform.stream.StreamSource sypet_var102 = new javax.xml.transform.stream.StreamSource(sypet_arg0);sypet_var102.setSystemId(sypet_var101);java.lang.Object sypet_var104 = sypet_var100.run();return sypet_var104;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var100 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var101 = sypet_arg2.getLocalPart();javax.xml.transform.stream.StreamSource sypet_var102 = new javax.xml.transform.stream.StreamSource(sypet_arg0);sypet_var102.setSystemId(sypet_var101);java.lang.Object sypet_var104 = sypet_var100.run();return sypet_var104;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756832842Satune Solving Time: 63.639945
+     [java] 1594756832919 Original Encoding Solving Time: 0.020684
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756832919Satune Solving Time: 0.035863
+     [java] Path Solving Time: 151.999481
+     [java] Path Solving Time: 117.523031
+     [java] Path Solving Time: 11.933232
+     [java] 1594756833258 Original Encoding Solving Time: 0.356191
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756833258Satune Solving Time: 64.936155
+     [java] 1594756833334 Original Encoding Solving Time: 0.044406
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756833334Satune Solving Time: 0.084234
+     [java] 1594756833344 Original Encoding Solving Time: 0.021448
+     [java] r is making the decision about element 0x7f53a4710190....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470fe40....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a470fd70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4710110....
+     [java] Encoding Graph Time: 0.000097
+     [java] Elapse Encode time: 0.000126
+     [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.064550
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064682
+     [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 0x7f53a4712340....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4712440....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a47123c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4711f20....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4711e00....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a47122c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4712240....
+     [java] Encoding Graph Time: 0.000065
+     [java] Elapse Encode time: 0.000088
+     [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.064146
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064240
+     [java] Elapse Encode time: 0.000025
+     [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.000036
+     [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 0x7f53a4909dd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4909ed0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4909e50....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49099b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4909890....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4909d50....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4909cd0....
+     [java] Encoding Graph Time: 0.000100
+     [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.063493
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063631
+     [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.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000032
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e010....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e7b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e730....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e830....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e6b0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e130....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490e630....
+     [java] Encoding Graph Time: 0.000112
+     [java] Elapse Encode time: 0.000144
+     [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.064778
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064929
+     [java] Elapse Encode time: 0.000027
+     [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.000080
+     [java] Elapse Encode time: 0.000027
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 18      #Vars = 10
+     [java] Data is avaisSat= false ,SatuneSat= false
+     [java] 1594756833344Satune Solving Time: 0.085507
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] java.lang.String sypet_var108 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var109 = new javax.xml.transform.stream.StreamSource(sypet_var108);javax.xml.bind.GetPropertyAction sypet_var110 = new javax.xml.bind.GetPropertyAction(sypet_arg1);sypet_var109.setSystemId(sypet_arg0);java.lang.Object sypet_var112 = sypet_var110.run();return sypet_var112;}
+     [java]                                                                                                                                                                                       ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] java.lang.String sypet_var108 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var109 = new javax.xml.transform.stream.StreamSource(sypet_var108);javax.xml.bind.GetPropertyAction sypet_var110 = new javax.xml.bind.GetPropertyAction(sypet_arg1);sypet_var109.setSystemId(sypet_arg0);java.lang.Object sypet_var112 = sypet_var110.run();return sypet_var112;}
+     [java]                                                                                                                                                                                                                                           ^
+     [java] 2 errors
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] java.lang.String sypet_var108 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var109 = new javax.xml.transform.stream.StreamSource(sypet_arg1);javax.xml.bind.GetPropertyAction sypet_var110 = new javax.xml.bind.GetPropertyAction(sypet_var108);sypet_var109.setSystemId(sypet_arg0);java.lang.Object sypet_var112 = sypet_var110.run();return sypet_var112;}
+     [java]                                                                                                                                                                                     ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] java.lang.String sypet_var108 = sypet_arg2.getPrefix();javax.xml.transform.stream.StreamSource sypet_var109 = new javax.xml.transform.stream.StreamSource(sypet_arg1);javax.xml.bind.GetPropertyAction sypet_var110 = new javax.xml.bind.GetPropertyAction(sypet_var108);sypet_var109.setSystemId(sypet_arg0);java.lang.Object sypet_var112 = sypet_var110.run();return sypet_var112;}
+     [java]                                                                                                                                                                                                                                         ^
+     [java] 2 errors
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 192.049818
+     [java] Path Solving Time: 105.299804
+     [java] Path Solving Time: 11.880593
+     [java] 1594756833711 Original Encoding Solving Time: 0.315028
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var116 = new javax.xml.transform.stream.StreamResult(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var117 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var118 = sypet_arg2.getLocalPart();java.lang.Object sypet_var119 = sypet_var117.run();sypet_var116.setSystemId(sypet_var118);return sypet_var119;}
+     [java]                                                                                                                              ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamResult sypet_var116 = new javax.xml.transform.stream.StreamResult(sypet_arg0);javax.xml.bind.GetPropertyAction sypet_var117 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var118 = sypet_arg2.getLocalPart();java.lang.Object sypet_var119 = sypet_var117.run();sypet_var116.setSystemId(sypet_var118);return sypet_var119;}
+     [java]                                                                                                                                                                                  ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756833711Satune Solving Time: 63.733822
+     [java] 1594756833786 Original Encoding Solving Time: 0.0196
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756833786Satune Solving Time: 0.035978
+     [java] Path Solving Time: 76.12718
+     [java] Path Solving Time: 11.894948
+     [java] 1594756833932 Original Encoding Solving Time: 0.612299
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var124 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamSource sypet_var125 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var126 = sypet_arg2.getNamespaceURI();java.lang.Object sypet_var127 = sypet_var124.run();sypet_var125.setPublicId(sypet_var126);return sypet_var127;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var124 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamSource sypet_var125 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var126 = sypet_arg2.getNamespaceURI();java.lang.Object sypet_var127 = sypet_var124.run();sypet_var125.setPublicId(sypet_var126);return sypet_var127;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756833932Satune Solving Time: 63.321635
+     [java] 1594756834006 Original Encoding Solving Time: 0.019914
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756834006Satune Solving Time: 0.034899
+     [java] Path Solving Time: 143.664552
+     [java] Path Solving Time: 11.985822
+     [java] 1594756834221 Original Encoding Solving Time: 0.2754
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var132 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamSource sypet_var133 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.Object sypet_var134 = sypet_var132.run();java.lang.String sypet_var135 = sypet_arg2.getLocalPart();sypet_var133.setPublicId(sypet_var135);return sypet_var134;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var132 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamSource sypet_var133 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.Object sypet_var134 = sypet_var132.run();java.lang.String sypet_var135 = sypet_arg2.getLocalPart();sypet_var133.setPublicId(sypet_var135);return sypet_var134;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756834221Satune Solving Time: 64.085226
+     [java] 1594756834296 Original Encoding Solving Time: 0.026757
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756834296Satune Solving Time: 0.044176
+     [java] Path Solving Time: 138.906385
+     [java] Path Solving Time: 267.380655
+     [java] Path Solving Time: 11.877926
+     [java] 1594756834774 Original Encoding Solving Time: 0.316423
+     [java] ilable 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.000081
+     [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 0x7f53a4911310....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49109c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4910940....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4910400....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49108c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4910520....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4910840....
+     [java] Encoding Graph Time: 0.000068
+     [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.063628
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063727
+     [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.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 0x7f53a4912af0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912b70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912a70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49129f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912530....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912650....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912970....
+     [java] Encoding Graph Time: 0.000086
+     [java] Elapse Encode time: 0.000112
+     [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.063194
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063313
+     [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.000001
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000031
+     [java] Polarity time: 0.000004
+     [java] Preprocess time: 0.000007
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4914e80....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4914f00....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4914d80....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4914e00....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49148c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4914d00....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a49149e0....
+     [java] Encoding Graph Time: 0.000073
+     [java] Elapse Encode time: 0.000095
+     [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.063977
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064077
+     [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.000039
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000008
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4916ee0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4917040....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912530....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4916aa0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4916e60....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a490b270....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4912650....
+     [java] Encoding Graph Time: 0.000073
+     [java] Elapse Encode time: 0.000098
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 9
+     [java] Data is availablisSat= true ,SatuneSat= true
+     [java] 1594756834774Satune Solving Time: 63.648116
+     [java] 1594756834851 Original Encoding Solving Time: 0.030615
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756834851Satune Solving Time: 0.04467
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var140 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamResult sypet_var141 = new javax.xml.transform.stream.StreamResult(sypet_arg0);java.lang.Object sypet_var142 = sypet_var140.run();java.lang.String sypet_var143 = sypet_arg2.getNamespaceURI();sypet_var141.setSystemId(sypet_var143);return sypet_var142;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var140 = new javax.xml.bind.GetPropertyAction(sypet_arg1);javax.xml.transform.stream.StreamResult sypet_var141 = new javax.xml.transform.stream.StreamResult(sypet_arg0);java.lang.Object sypet_var142 = sypet_var140.run();java.lang.String sypet_var143 = sypet_arg2.getNamespaceURI();sypet_var141.setSystemId(sypet_var143);return sypet_var142;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 269.566996
+     [java] Path Solving Time: 259.727786
+     [java] Path Solving Time: 12.666906
+     [java] 1594756835452 Original Encoding Solving Time: 0.269747
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var148 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.Object sypet_var149 = sypet_var148.run();java.lang.String sypet_var150 = sypet_arg2.getLocalPart();javax.xml.transform.stream.StreamResult sypet_var151 = new javax.xml.transform.stream.StreamResult(sypet_var150);sypet_var151.setSystemId(sypet_arg0);return sypet_var149;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var148 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.Object sypet_var149 = sypet_var148.run();java.lang.String sypet_var150 = sypet_arg2.getLocalPart();javax.xml.transform.stream.StreamResult sypet_var151 = new javax.xml.transform.stream.StreamResult(sypet_var150);sypet_var151.setSystemId(sypet_arg0);return sypet_var149;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756835452Satune Solving Time: 63.817698
+     [java] 1594756835527 Original Encoding Solving Time: 0.026452
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756835527Satune Solving Time: 0.042252
+     [java] Path Solving Time: 204.419522
+     [java] Path Solving Time: 192.120683
+     [java] Path Solving Time: 12.667161
+     [java] 1594756835996 Original Encoding Solving Time: 0.381569
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756835996Satune Solving Time: 66.546968
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var156 = new javax.xml.transform.stream.StreamSource(sypet_arg1);sypet_var156.setSystemId(sypet_arg0);java.lang.String sypet_var158 = sypet_arg2.getLocalPart();javax.xml.bind.GetPropertyAction sypet_var159 = new javax.xml.bind.GetPropertyAction(sypet_var158);java.lang.Object sypet_var160 = sypet_var159.run();return sypet_var160;}
+     [java]                                                                                                                                                                                                                             ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.transform.stream.StreamSource sypet_var156 = new javax.xml.transform.stream.StreamSource(sypet_arg1);sypet_var156.setSystemId(sypet_arg0);java.lang.String sypet_var158 = sypet_arg2.getLocalPart();javax.xml.bind.GetPropertyAction sypet_var159 = new javax.xml.bind.GetPropertyAction(sypet_var158);java.lang.Object sypet_var160 = sypet_var159.run();return sypet_var160;}
+     [java]                                                                                                                                                                                                                                                                                 ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] 1594756836073 Original Encoding Solving Time: 0.020451
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756836073Satune Solving Time: 0.03522
+     [java] Path Solving Time: 56.364999
+     [java] Path Solving Time: 95.737595
+     [java] Path Solving Time: 13.151406
+     [java] 1594756836298 Original Encoding Solving Time: 0.261643
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756836298Satune Solving Time: 64.15639
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var164 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var165 = sypet_arg2.getNamespaceURI();javax.xml.transform.stream.StreamSource sypet_var166 = new javax.xml.transform.stream.StreamSource(sypet_var165);java.lang.Object sypet_var167 = sypet_var164.run();sypet_var166.setSystemId(sypet_arg0);return sypet_var167;}
+     [java]               ^
+     [java] /Source.java:3: error: GetPropertyAction is not public in javax.xml.bind; cannot be accessed from outside package
+     [java] javax.xml.bind.GetPropertyAction sypet_var164 = new javax.xml.bind.GetPropertyAction(sypet_arg1);java.lang.String sypet_var165 = sypet_arg2.getNamespaceURI();javax.xml.transform.stream.StreamSource sypet_var166 = new javax.xml.transform.stream.StreamSource(sypet_var165);java.lang.Object sypet_var167 = sypet_var164.run();sypet_var166.setSystemId(sypet_arg0);return sypet_var167;}
+     [java]                                                                   ^
+     [java] 2 errors
+     [java] Done with finding holes : Flag = false
+     [java] 1594756836373 Original Encoding Solving Time: 0.020495
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756836373Satune Solving Time: 0.036345
+     [java] Path Solving Time: 486.66585
+     [java] Path Solving Time: 3740.791519
+     [java] Path Solving Time: 6.677119
+     [java] Path Solving Time: 5.954279
+     [java] Path Solving Time: 79106.166162
+     [java] 1594756919782 Original Encoding Solving Time: 0.387032
+     [java] e now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.063535
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063640
+     [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.000040
+     [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 0x7f53a4918a80....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918fa0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918f20....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918da0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918e20....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4918960....
+     [java] Encoding Graph Time: 0.000076
+     [java] Elapse Encode time: 0.000099
+     [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.063704
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.063810
+     [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.000007
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491afe0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491b0e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491af60....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491b060....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491aaa0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491abc0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491aee0....
+     [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.066398
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.066538
+     [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.000004
+     [java] Preprocess time: 0.000008
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820950....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820e70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820df0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cf0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820d70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820830....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820c70....
+     [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.064050
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.064148
+     [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.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000032
+     [java] Polarity time: 0.000008
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822ad0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822f70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822e70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822ff0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822ef0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48229b0....
+     [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] INFO: naivisSat= true ,SatuneSat= true
+     [java] 1594756919782Satune Solving Time: 66.787677
+     [java] 1594756919867 Original Encoding Solving Time: 0.048333
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756919867Satune Solving Time: 0.085403
+     [java] 1594756919880 Original Encoding Solving Time: 0.043625
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756919880Satune Solving Time: 0.087225
+     [java] Path Solving Time: 1344.767347
+     [java] Path Solving Time: 210.591892
+     [java] Path Solving Time: 64442.530832
+     [java] 1594756985935 Original Encoding Solving Time: 0.768862
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756985935Satune Solving Time: 61.02844
+     [java] 1594756986016 Original Encoding Solving Time: 0.053188
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594756986016Satune Solving Time: 0.090407
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: AbstractUnmarshallerImpl is abstract; cannot be instantiated
+     [java] java.lang.String sypet_var179 = sypet_arg2.getLocalPart();org.xml.sax.InputSource sypet_var180 = new org.xml.sax.InputSource(sypet_var179);sypet_var180.setEncoding(sypet_arg1);javax.xml.bind.helpers.AbstractUnmarshallerImpl sypet_var182 = new javax.xml.bind.helpers.AbstractUnmarshallerImpl();java.lang.Object sypet_var183 = sypet_var182.unmarshal(sypet_arg0);return sypet_var183;}
+     [java]                                                                                                                                                                                                                                                ^
+     [java] 1 error
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: AbstractUnmarshallerImpl is abstract; cannot be instantiated
+     [java] java.lang.String sypet_var179 = sypet_arg2.getLocalPart();org.xml.sax.InputSource sypet_var180 = new org.xml.sax.InputSource(sypet_arg1);sypet_var180.setEncoding(sypet_var179);javax.xml.bind.helpers.AbstractUnmarshallerImpl sypet_var182 = new javax.xml.bind.helpers.AbstractUnmarshallerImpl();java.lang.Object sypet_var183 = sypet_var182.unmarshal(sypet_arg0);return sypet_var183;}
+     [java]                                                                                                                                                                                                                                                ^
+     [java] 1 error
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] 1594756986028 Original Encoding Solving Time: 0.031883
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594756986028Satune Solving Time: 0.129795
+     [java] Path Solving Time: 2859.281912
+     [java] Path Solving Time: 351.347076
+     [java] Path Solving Time: 64242.345885
+     [java] 1594757053533 Original Encoding Solving Time: 0.36426
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: HttpExchange is abstract; cannot be instantiated
+     [java] javax.xml.ws.spi.http.HttpExchange sypet_var187 = new javax.xml.ws.spi.http.HttpExchange();java.lang.Object sypet_var188 = sypet_var187.getAttribute(sypet_arg1);javax.xml.transform.stream.StreamSource sypet_var189 = new javax.xml.transform.stream.StreamSource(sypet_arg0);java.lang.String sypet_var190 = sypet_arg2.getPrefix();sypet_var189.setPublicId(sypet_var190);return sypet_var188;}
+     [java]                                                   ^
+     [java] 1 error
+     [java] Done with finding holes : Flag = false
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757053533Satune Solving Time: 67.355631
+     [java] 1594757053614 Original Encoding Solving Time: 0.025532
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594757053614Satune Solving Time: 0.048995
+     [java] Path Solving Time: 663.776102
+     [java] Path Solving Time: 136.060394
+     [java] Path Solving Time: 54611.705069
+     [java] 1594757109077 Original Encoding Solving Time: 0.314458
+     [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] 1594757109077Satune Solving Time: 55.67732
+     [java] 1594757109145 Original Encoding Solving Time: 0.021134
+     [java] e encoder is making the decision about element 0x7f53a4822df0....
+     [java] Encoding Graph Time: 0.000126
+     [java] Elapse Encode time: 0.000162
+     [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.066610
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.066778
+     [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.000040
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000081
+     [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.000040
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Polarity time: 0.000014
+     [java] Preprocess time: 0.000012
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4401720....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822ff0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48efaa0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4822f70....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4827fb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f09a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb9d0....
+     [java] Encoding Graph Time: 0.000100
+     [java] Elapse Encode time: 0.000139
+     [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.060873
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.061020
+     [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.000044
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000085
+     [java] Elapse Encode time: 0.000041
+     [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.000124
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494d010....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494d090....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494cf90....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494d110....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494cf10....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494cb80....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a494cc50....
+     [java] Encoding Graph Time: 0.000077
+     [java] Elapse Encode time: 0.000108
+     [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.067232
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.067347
+     [java] Elapse Encode time: 0.000030
+     [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.000044
+     [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 0x7f53a4401720....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44043a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4404750....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4404470....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48f09a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a48fb9d0....
+     [java] Encoding Graph Time: 0.000069
+     [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.055569
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.055669
+     [java] Elapse Encode time: 0.000024
+     [java] Is problem UNisSat= false ,SatuneSat= false
+     [java] 1594757109145Satune Solving Time: 0.041262
+     [java] Path Solving Time: 224.702472
+     [java] Path Solving Time: 570.289148
+     [java] Path Solving Time: 49174.018869
+     [java] 1594757159165 Original Encoding Solving Time: 0.37404
+     [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] 1594757159165Satune Solving Time: 54.077463
+     [java] 1594757159250 Original Encoding Solving Time: 0.051118
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757159250Satune Solving Time: 0.086479
+     [java] 1594757159263 Original Encoding Solving Time: 0.024923
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594757159263Satune Solving Time: 0.090102
+     [java] Path Solving Time: 441.154925
+     [java] Path Solving Time: 832.198216
+     [java] Path Solving Time: 81086.130939
+     [java] 1594757241673 Original Encoding Solving Time: 0.296149
+     [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] 1594757241673Satune Solving Time: 54.41352
+     [java] 1594757241746 Original Encoding Solving Time: 0.107637
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757241746Satune Solving Time: 0.10489
+     [java] 1594757241762 Original Encoding Solving Time: 0.029345
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594757241762Satune Solving Time: 0.12462
+     [java] Path Solving Time: 1455.959607
+     [java] Path Solving Time: 1151.931022
+     [java] Path Solving Time: 57040.447166
+     [java] 1594757301461 Original Encoding Solving Time: 0.377353
+     [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] 1594757301461Satune Solving Time: 53.082307
+     [java] 1594757301534 Original Encoding Solving Time: 0.021248
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594757301534Satune Solving Time: 0.036353
+     [java] Path Solving Time: 1234.89833
+     [java] Path Solving Time: 499.23076
+     [java] Path Solving Time: 26497.812329
+     [java] 1594757329816 Original Encoding Solving Time: 0.32489
+     [java] SAT 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.000037
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44043a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4919ff0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4404060....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491a070....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4403f40....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4919f70....
+     [java] Encoding Graph Time: 0.000096
+     [java] Elapse Encode time: 0.000128
+     [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.053934
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.054069
+     [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.000040
+     [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 = 18      #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:      UNSAT
+     [java] CSOLVER solve time: 0.000085
+     [java] Polarity time: 0.000005
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44043a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492c6c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493cca0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493cd20....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492c740....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492c640....
+     [java] Encoding Graph Time: 0.000069
+     [java] Elapse Encode time: 0.000100
+     [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.054298
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.054405
+     [java] Elapse Encode time: 0.000037
+     [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.000099
+     [java] Elapse Encode time: 0.000040
+     [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.000061
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000119
+     [java] Polarity time: 0.000009
+     [java] Preprocess time: 0.000011
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493c460....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492cdd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a44043a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493c7e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491a550....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492d170....
+     [java] Encoding Graph Time: 0.000110
+     [java] Elapse Encode time: 0.000150
+     [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.052917
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.053074
+     [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.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 0x7f53a44043a0....
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] /Source.java:3: error: AbstractUnmarshallerImpl is abstract; cannot be instantiated
+     [java] javax.xml.soap.SOAPFactory sypet_var227 = javax.xml.soap.SOAPFactory.newInstance(sypet_arg1);javax.xml.soap.SOAPElement sypet_var228 = sypet_var227.createElement(sypet_arg2);sypet_var228.removeContents();javax.xml.bind.helpers.AbstractUnmarshallerImpl sypet_var230 = new javax.xml.bind.helpers.AbstractUnmarshallerImpl();java.lang.Object sypet_var231 = sypet_var230.unmarshal(sypet_arg0);return sypet_var231;}
+     [java]                                                                                                                                                                                                                                                                            ^
+     [java] 1 error
+     [java] INFO: naive encoder is making the decision aboutisSat= true ,SatuneSat= true
+     [java] 1594757329816Satune Solving Time: 54.507625
+     [java] Path Solving Time: 267.080183
+     [java] Path Solving Time: 1777.427102
+     [java] Path Solving Time: 51323.946122
+     [java] 1594757383305 Original Encoding Solving Time: 0.302038
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757383305Satune Solving Time: 53.117016
+     [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] 1594757383370 Original Encoding Solving Time: 0.048431
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757383370Satune Solving Time: 0.088274
+     [java] 1594757383380 Original Encoding Solving Time: 0.023616
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594757383380Satune Solving Time: 0.085858
+     [java] Path Solving Time: 1663.43742
+     [java] Path Solving Time: 3634.499606
+     [java] Path Solving Time: 45693.790105
+     [java] 1594757434420 Original Encoding Solving Time: 0.393917
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594757434420Satune Solving Time: 54.092872
+     [java] =========Statistics=========
+     [java] Benchmark Id: 29
+     [java] Sketch Generation Time: 616000.2652870001
+     [java] Sketch Completion Time: 3690.3233769999997
+     [java] Compilation Time: 814.2386469999998
+     [java] Running Test cases Time: 27.050174000000002
+     [java] Number of completed programs: 70
+     [java] Number of sketches: 31
+     [java] TIMEOUT after 600000 ms
+     [java] ============================
+     [java]  element 0x7f53a492d170....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493c7e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a491a550....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a492cdd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a493c460....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4820cb0....
+     [java] Encoding Graph Time: 0.000107
+     [java] Elapse Encode time: 0.000138
+     [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.054350
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.054494
+     [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 0x7f53a4943480....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943500....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943380....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943600....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943580....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943300....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943400....
+     [java] Encoding Graph Time: 0.000070
+     [java] Elapse Encode time: 0.000097
+     [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.053006
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.053108
+     [java] Elapse Encode time: 0.000027
+     [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:     SAT
+     [java] CSOLVER solve time: 0.000084
+     [java] Elapse Encode time: 0.000028
+     [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.000044
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000016
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f53a495ff00....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943580....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4943600....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a495fa40....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a4970ad0....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a495fb60....
+     [java] INFO: naive encoder is making the decision about element 0x7f53a495fe80....
+     [java] Encoding Graph Time: 0.000122
+     [java] Elapse Encode time: 0.000165
+     [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.053906
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.054083
+
+BUILD SUCCESSFUL
+Total time: 10 minutes 40 seconds