Adding sypet to repo
[Benchmarks_CSolver.git] / sypet / output / geometry / benchmark12.log
diff --git a/sypet/output/geometry/benchmark12.log b/sypet/output/geometry/benchmark12.log
new file mode 100644 (file)
index 0000000..f874804
--- /dev/null
@@ -0,0 +1,475 @@
+Buildfile: /scratch/satcheck/satproject/constraint_compiler/src/Benchmarks/sypet/build.xml
+
+sypet:
+     [java] ----------Options
+     [java] Verbose: false
+     [java] Timeout: 600000
+     [java] Round Robin: true
+     [java] Round Robin Iterations: 100
+     [java] Round Robin Range: 2
+     [java] Solver limit: 5
+     [java] ----------benchmarks/geometry/12/benchmark12.json
+     [java] Benchmark Id: 12
+     [java] Method name: rotateQuadrant
+     [java] Packages: [java.awt.geom]
+     [java] Libraries: [./lib/rt7.jar]
+     [java] Source type(s): [java.awt.geom.Rectangle2D, int]
+     [java] Target type: java.awt.geom.Rectangle2D
+     [java] --------------------------------------------------------
+     [java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Cipher is a phantom class!
+     [java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
+     [java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKey is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Mac is a phantom class!
+     [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+     [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+     [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+     [java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
+     [java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
+     [java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
+     [java] Warning: javax.crypto.CipherInputStream is a phantom class!
+     [java] Warning: javax.crypto.CipherOutputStream is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
+     [java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
+     [java] Warning: javax.crypto.KeyGenerator is a phantom class!
+     [java] #Classes: 50
+     [java] #Methods: 751
+     [java] Soot Time: 3604.704922
+     [java] PetriNet for path length: 1 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 2 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 3 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 4 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 5 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 17.784784
+     [java] Path Solving Time: 12.541405
+     [java] Path Solving Time: 6.796596
+     [java] PetriNet for path length: 6 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Path Solving Time: 13.029779
+     [java] Path Solving Time: 1.503346
+     [java] 1594753546350 Original Encoding Solving Time: 1.187447
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546350Satune Solving Time: 36.177726
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753546711 Original Encoding Solving Time: 0.144772
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546711Satune Solving Time: 0.102805
+     [java] 1594753546730 Original Encoding Solving Time: 0.049579
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753546730Satune Solving Time: 0.088184
+     [java] Path Solving Time: 6.011889
+     [java] Path Solving Time: 1.787563
+     [java] 1594753546760 Original Encoding Solving Time: 0.630248
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546760Satune Solving Time: 30.639639
+     [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] 1594753546811 Original Encoding Solving Time: 0.107157
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546811Satune Solving Time: 0.089311
+     [java] 1594753546827 Original Encoding Solving Time: 0.040033
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753546827Satune Solving Time: 0.096532
+     [java] Path Solving Time: 5.450963
+     [java] Path Solving Time: 1.48987
+     [java] 1594753546857 Original Encoding Solving Time: 1.127682
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546857Satune Solving Time: 38.221122
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Let's read clauses ...
+     [java] 1594753546912 Original Encoding Solving Time: 0.105755
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546912Satune Solving Time: 0.088591
+     [java] 1594753546927 Original Encoding Solving Time: 0.040152
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753546927Satune Solving Time: 0.085711
+     [java] Path Solving Time: 5.298263
+     [java] Path Solving Time: 1.417581
+     [java] 1594753546956 Original Encoding Solving Time: 0.476214
+     [java] Polarity time: 0.000031
+     [java] Preprocess time: 0.000020
+     [java] Decompose Order: 0.000016
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c9010....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c86c0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8d80....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8830....
+     [java] Encoding Graph Time: 0.000217
+     [java] Elapse Encode time: 0.000317
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.035796
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.036128
+     [java] Elapse Encode time: 0.000027
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000038
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000074
+     [java] Elapse Encode time: 0.000029
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 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:      UNSAT
+     [java] CSOLVER solve time: 0.000083
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000009
+     [java] Decompose Order: 0.000004
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4491670....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e44915f0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8d80....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4491570....
+     [java] Encoding Graph Time: 0.000151
+     [java] Elapse Encode time: 0.000184
+     [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.030437
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.030630
+     [java] Elapse Encode time: 0.000029
+     [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.000048
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000085
+     [java] Elapse Encode time: 0.000028
+     [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.000055
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000092
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49cb8a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49cb3d0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8d80....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49cb350....
+     [java] Encoding Graph Time: 0.000149
+     [java] Elapse Encode time: 0.000186
+     [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.038019
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.038212
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000047
+     [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 = 17      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000045
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000081
+     [java] Polarity time: 0.000009
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000002
+     [java] INFO: naive encoder is making the decision about element 0x7f35e44757a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49cbbe0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8d80....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4475720....
+     [java] Encoding Graph Time: 0.000111
+     [java] Elapse Encode time: 0.000140
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 15      #VarisSat= true ,SatuneSat= true
+     [java] 1594753546956Satune Solving Time: 23.617165
+     [java] 1594753546995 Original Encoding Solving Time: 0.109235
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753546995Satune Solving Time: 0.083878
+     [java] Done with finding holes : Flag = true
+     [java] assumption size = 0
+     [java] Conflict Array: 
+     [java] ***********************
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Done with finding holes : Flag = false
+     [java] 1594753547011 Original Encoding Solving Time: 0.043947
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753547011Satune Solving Time: 0.086604
+     [java] Path Solving Time: 8.135951
+     [java] Path Solving Time: 3.204981
+     [java] 1594753547044 Original Encoding Solving Time: 0.669012
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753547044Satune Solving Time: 23.472249
+     [java] 1594753547090 Original Encoding Solving Time: 0.057031
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753547090Satune Solving Time: 0.044673
+     [java] Path Solving Time: 10.770469
+     [java] Path Solving Time: 2.375485
+     [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] 1594753547125 Original Encoding Solving Time: 0.616755
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753547125Satune Solving Time: 33.112566
+     [java] 1594753547173 Original Encoding Solving Time: 0.033924
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753547173Satune Solving Time: 0.036949
+     [java] Path Solving Time: 11.669202
+     [java] Path Solving Time: 1.045718
+     [java] Path Solving Time: 1.079041
+     [java] Path Solving Time: 9.119515
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Path Solving Time: 38.321281
+     [java] 1594753547256 Original Encoding Solving Time: 0.445777
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753547256Satune Solving Time: 33.03691
+     [java] 1594753547302 Original Encoding Solving Time: 0.035158
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753547302Satune Solving Time: 0.034217
+     [java] Done with finding holes : Flag = false
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] Done with finding holes : Flag = false
+     [java] Path Solving Time: 17.369973
+     [java] Path Solving Time: 7.378186
+     [java] 1594753547348 Original Encoding Solving Time: 0.45559
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753547348Satune Solving Time: 21.303072
+     [java] 1594753547382 Original Encoding Solving Time: 0.030771
+     [java] isSat= false ,SatuneSat= false
+     [java] 1594753547382Satune Solving Time: 0.033429
+     [java] Path Solving Time: 23.593742
+     [java] PetriNet for path length: 7 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 4.251708
+     [java] Path Solving Time: 0.695916
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753548821 Original Encoding Solving Time: 0.491377
+     [java] s = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.023463
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.023609
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 16      #Vars = 10
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000042
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.000079
+     [java] Elapse Encode time: 0.000028
+     [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:      UNSAT
+     [java] CSOLVER solve time: 0.000082
+     [java] Polarity time: 0.000011
+     [java] Preprocess time: 0.000026
+     [java] Decompose Order: 0.000009
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47e3eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49c9e90....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4365010....
+     [java] Encoding Graph Time: 0.000187
+     [java] Elapse Encode time: 0.000255
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 9       #Vars = 6
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.023196
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.023461
+     [java] Elapse Encode time: 0.000028
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 10      #Vars = 6
+     [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.000016
+     [java] Preprocess time: 0.000019
+     [java] Decompose Order: 0.000009
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47e3eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4365010....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47c8ea0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4367400....
+     [java] Encoding Graph Time: 0.000171
+     [java] Elapse Encode time: 0.000232
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 9       #Vars = 6
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.032862
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.033102
+     [java] Elapse Encode time: 0.000023
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 10      #Vars = 6
+     [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.000007
+     [java] Preprocess time: 0.000010
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47e3eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47ca5e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4476280....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4365010....
+     [java] Encoding Graph Time: 0.000134
+     [java] Elapse Encode time: 0.000165
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 9       #Vars = 6
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.032859
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.033029
+     [java] Elapse Encode time: 0.000021
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 10      #Vars = 6
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000030
+     [java] Polarity time: 0.000006
+     [java] Preprocess time: 0.000013
+     [java] Decompose Order: 0.000003
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47e3eb0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4365010....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e47ca5e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4469330....
+     [java] Encoding Graph Time: 0.000065
+     [java] Elapse Encode time: 0.000093
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 9       #Vars = 6
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.021195
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.021293
+     [java] Elapse Encode time: 0.000021
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 10      #Vars = 6
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.000000
+     [java] Result Computed in SAT solver:      UNSAT
+     [java] CSOLVER solve time: 0.000030
+     [java] Polarity time: 0.000007
+     [java] Preprocess time: 0.000014
+     [java] Decompose Order: 0.000005
+     [java] INFO: naive encoder is making thisSat= true ,SatuneSat= true
+     [java] 1594753548821Satune Solving Time: 30.661371
+     [java] =========Statistics (time in milliseconds)=========
+     [java] Benchmark Id: 12
+     [java] Sketch Generation Time: 223.41230800000002
+     [java] Sketch Completion Time: 492.106273
+     [java] Compilation Time: 498.73862
+     [java] Running Test cases Time: 3.8008810000000004
+     [java] Synthesis Time: 719.319462
+     [java] Total Time: 1218.058082
+     [java] Number of components: 4
+     [java] Number of holes: 6
+     [java] Number of completed programs: 21
+     [java] Number of sketches: 9
+     [java] Solution:
+     [java]  java.awt.Shape sypet_var43 = sypet_arg0;
+     [java]  java.awt.geom.AffineTransform sypet_var44 = java.awt.geom.AffineTransform.getQuadrantRotateInstance(sypet_arg1);
+     [java]  java.awt.geom.Path2D.Double sypet_var45 = new java.awt.geom.Path2D.Double(sypet_var43,sypet_var44);
+     [java]  java.awt.geom.Rectangle2D sypet_var46 = sypet_var45.getBounds2D();
+     [java]  return sypet_var46;
+     [java]  
+     [java] ============================
+     [java] e decision about element 0x7f35e4469760....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e446b0e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e446b060....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e44696e0....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e49c9370....
+     [java] INFO: naive encoder is making the decision about element 0x7f35e4469330....
+     [java] Encoding Graph Time: 0.000192
+     [java] Elapse Encode time: 0.000238
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 13      #Vars = 8
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000000
+     [java] SAT Solving time: 0.030405
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.030653
+
+BUILD SUCCESSFUL
+Total time: 7 seconds