--- /dev/null
+Buildfile: /scratch/satcheck/satproject/constraint_compiler/src/Benchmarks/sypet/build.xml
+
+sypet:
+ [java] ----------Options
+ [java] Verbose: false
+ [java] Timeout: 600000
+ [java] Round Robin: true
+ [java] Round Robin Iterations: 100
+ [java] Round Robin Range: 2
+ [java] Solver limit: 5
+ [java] ----------benchmarks/xml/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