--- /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/math/5/benchmark5.json
+ [java] Benchmark Id: 5
+ [java] Method name: invert
+ [java] Packages: [com.opengamma.analytics.math, org.apache.commons.math.linear]
+ [java] Libraries: [./lib/commons-math-2.2.jar, ./lib/og-analytics-2.17.0.jar, ./lib/commons-lang-2.6.jar]
+ [java] Source type(s): [com.opengamma.analytics.math.matrix.DoubleMatrix2D]
+ [java] Target type: com.opengamma.analytics.math.matrix.DoubleMatrix2D
+ [java] --------------------------------------------------------
+ [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+ [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+ [java] Warning: javax.crypto.Cipher is a phantom class!
+ [java] Warning: javax.crypto.SealedObject is a phantom class!
+ [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+ [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+ [java] Warning: javax.crypto.spec.DHParameterSpec 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.SecretKey is a phantom class!
+ [java] Warning: com.opengamma.util.ArgumentChecker is a phantom class!
+ [java] Warning: com.opengamma.util.money.Currency is a phantom class!
+ [java] Warning: com.opengamma.util.money.CurrencyAmount is a phantom class!
+ [java] Warning: com.opengamma.util.money.MultipleCurrencyAmount is a phantom class!
+ [java] Warning: it.unimi.dsi.fastutil.doubles.DoubleArrayList is a phantom class!
+ [java] Warning: org.threeten.bp.Period is a phantom class!
+ [java] Warning: org.threeten.bp.ZonedDateTime is a phantom class!
+ [java] Warning: com.opengamma.id.ExternalId is a phantom class!
+ [java] Warning: com.opengamma.OpenGammaRuntimeException is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Pair is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Pairs is a phantom class!
+ [java] Warning: org.joda.convert.ToString is a phantom class!
+ [java] Warning: org.joda.convert.FromStringFactory is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAdjuster is a phantom class!
+ [java] Warning: org.threeten.bp.LocalDate is a phantom class!
+ [java] Warning: com.opengamma.util.time.Expiry is a phantom class!
+ [java] Warning: org.joda.beans.Bean is a phantom class!
+ [java] Warning: org.joda.beans.Property is a phantom class!
+ [java] Warning: org.joda.beans.MetaProperty is a phantom class!
+ [java] Warning: org.joda.beans.MetaBean is a phantom class!
+ [java] Warning: org.joda.beans.PropertyDefinition is a phantom class!
+ [java] Warning: org.joda.beans.JodaBeanUtils is a phantom class!
+ [java] Warning: org.joda.beans.BeanDefinition is a phantom class!
+ [java] Warning: org.joda.beans.ImmutableBean is a phantom class!
+ [java] Warning: com.opengamma.util.i18n.Country is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableSet is a phantom class!
+ [java] Warning: org.joda.beans.impl.flexi.FlexiBean is a phantom class!
+ [java] Warning: org.joda.convert.FromString is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableMap is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableMap$Builder is a phantom class!
+ [java] Warning: com.opengamma.util.CompareUtils is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.ObjectsPair is a phantom class!
+ [java] Warning: org.slf4j.Logger is a phantom class!
+ [java] Warning: org.slf4j.LoggerFactory is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.DoublesPair is a phantom class!
+ [java] Warning: org.threeten.bp.chrono.ChronoZonedDateTime is a phantom class!
+ [java] Warning: com.opengamma.util.time.DateUtils is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaBean is a phantom class!
+ [java] Warning: org.joda.beans.BeanBuilder is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaProperty is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaPropertyMap is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectBeanBuilder is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectFieldsBeanBuilder is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.Temporal is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAmount is a phantom class!
+ [java] Warning: com.opengamma.util.time.Tenor is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAdjusters is a phantom class!
+ [java] Warning: org.threeten.bp.Month is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.zdt.ZonedDateTimeDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.DoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Triple is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableList is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.FirstThenSecondDoublesPairComparator is a phantom class!
+ [java] Warning: com.opengamma.util.time.Tenor$BusinessDayTenor is a phantom class!
+ [java] Warning: org.threeten.bp.LocalDateTime is a phantom class!
+ [java] Warning: com.opengamma.util.ParallelArrayBinarySort is a phantom class!
+ [java] Warning: org.threeten.bp.LocalTime is a phantom class!
+ [java] Warning: org.threeten.bp.ZoneId is a phantom class!
+ [java] Warning: org.threeten.bp.chrono.ChronoLocalDate is a phantom class!
+ [java] Warning: org.threeten.bp.ZoneOffset is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.ImmutableLocalDateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.zdt.ImmutableZonedDateTimeDoubleTimeSeries is a phantom class!
+ [java] Warning: org.threeten.bp.format.DateTimeFormatter is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalField is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.JulianFields is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAccessor is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.FirstThenSecondPairComparator is a phantom class!
+ [java] Warning: com.google.common.collect.Maps is a phantom class!
+ [java] Warning: com.opengamma.util.ClassUtils is a phantom class!
+ [java] Warning: com.opengamma.util.money.MultipleCurrencyAmountPricer is a phantom class!
+ [java] Warning: cern.jet.random.Normal is a phantom class!
+ [java] Warning: cern.jet.stat.Probability is a phantom class!
+ [java] Warning: cern.jet.random.engine.RandomEngine is a phantom class!
+ [java] Warning: cern.jet.random.engine.MersenneTwister64 is a phantom class!
+ [java] Warning: com.opengamma.lang.annotation.ExternalFunction is a phantom class!
+ [java] Warning: com.google.common.primitives.Doubles is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleMatrix1D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleFactory2D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleFactory1D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleMatrix2D is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.Algebra is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.SingularValueDecomposition is a phantom class!
+ [java] Warning: com.google.common.collect.ArrayListMultimap is a phantom class!
+ [java] Warning: com.google.common.collect.ListMultimap is a phantom class!
+ [java] Warning: it.unimi.dsi.fastutil.ints.IntArrayList is a phantom class!
+ [java] Warning: com.google.common.collect.LinkedListMultimap is a phantom class!
+ [java] Warning: com.google.common.collect.Multimap is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectBean is a phantom class!
+ [java] Warning: com.google.common.collect.Iterators is a phantom class!
+ [java] Warning: cern.jet.random.engine.MersenneTwister is a phantom class!
+ [java] Warning: com.google.common.collect.Iterables is a phantom class!
+ [java] Warning: com.google.common.collect.Sets$SetView is a phantom class!
+ [java] Warning: com.google.common.collect.Sets is a phantom class!
+ [java] Warning: org.threeten.bp.DayOfWeek is a phantom class!
+ [java] Warning: org.threeten.bp.MonthDay is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.DateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.google.common.collect.Lists is a phantom class!
+ [java] Warning: org.joda.beans.PropertyStyle is a phantom class!
+ [java] Warning: cern.jet.math.Bessel is a phantom class!
+ [java] Warning: com.opengamma.util.types.ParameterizedTypeImpl is a phantom class!
+ [java] Warning: com.opengamma.util.types.VariantType is a phantom class!
+ [java] Warning: org.apache.log4j.Logger is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateToIntConverter is a phantom class!
+ [java] Warning: cern.jet.random.StudentT is a phantom class!
+ [java] Warning: com.opengamma.util.CalculationMode is a phantom class!
+ [java] Warning: com.opengamma.timeseries.TimeSeriesException is a phantom class!
+ [java] Warning: cern.colt.Arrays is a phantom class!
+ [java] Warning: cern.jet.random.ChiSquare is a phantom class!
+ [java] Warning: cern.colt.list.IntArrayList is a phantom class!
+ [java] Warning: org.testng.AssertJUnit is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.ChronoField is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalUnit is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.ChronoUnit is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleEntryIterator is a phantom class!
+ [java] Warning: edu.emory.mathcs.jtransforms.fft.DoubleFFT_1D is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.PreciseDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleTimeSeriesBuilder is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Quadruple is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.EigenvalueDecomposition is a phantom class!
+ [java] Warning: cern.jet.random.Gamma is a phantom class!
+ [java] Warning: org.threeten.bp.Year is a phantom class!
+ [java] #Classes: 615
+ [java] #Methods: 5526
+ [java] Soot Time: 4129.092714
+ [java] PetriNet for path length: 1 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 2 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 3 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 10.493035
+ [java] PetriNet for path length: 4 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 23.943298
+ [java] Path Solving Time: 11.10301
+ [java] 1594752238958 Original Encoding Solving Time: 0.519886
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752238958Satune Solving Time: 28.285096
+ [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] 1594752239247 Original Encoding Solving Time: 0.063793
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752239247Satune Solving Time: 0.052212
+ [java] Path Solving Time: 8.446629
+ [java] PetriNet for path length: 5 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 29.726572
+ [java] Path Solving Time: 7.470102
+ [java] Renaming procedure ...
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752245634 Original Encoding Solving Time: 2.78391
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752245634Satune Solving Time: 36.820504
+ [java] 1594752245698 Original Encoding Solving Time: 0.061788
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752245698Satune Solving Time: 0.032151
+ [java] /Source.java:3: error: package cern.colt.matrix does not exist
+ [java] cern.colt.matrix.DoubleMatrix2D sypet_var4 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_arg0);com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var5 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var4);return sypet_var5;}
+ [java] ^
+ [java] /Source.java:3: error: cannot access DoubleMatrix2D
+ [java] cern.colt.matrix.DoubleMatrix2D sypet_var4 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_arg0);com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var5 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var4);return sypet_var5;}
+ [java] ^
+ [java] class file for cern.colt.matrix.DoubleMatrix2D not found
+ [java] 2 errors
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 39.349635
+ [java] Path Solving Time: 15.011332
+ [java] 1594752245794 Original Encoding Solving Time: 0.644641
+ [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] 1594752245794Satune Solving Time: 41.782223
+ [java] 1594752245861 Original Encoding Solving Time: 0.032518
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752245861Satune Solving Time: 0.031219
+ [java] Path Solving Time: 18.556444
+ [java] Path Solving Time: 8.772175
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752245932 Original Encoding Solving Time: 1.055707
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752245932Satune Solving Time: 43.16681
+ [java] 1594752245995 Original Encoding Solving Time: 0.08369
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752245995Satune Solving Time: 0.078943
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 32.284637
+ [java] Path Solving Time: 6.558363
+ [java] 1594752246076 Original Encoding Solving Time: 0.860963
+ [java] Polarity time: 0.000021
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000009
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca642c220....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca642c340....
+ [java] Encoding Graph Time: 0.000192
+ [java] Elapse Encode time: 0.000257
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 5 #Vars = 4
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.027986
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.028255
+ [java] Elapse Encode time: 0.000019
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 6 #Vars = 4
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000027
+ [java] serializing ...
+ [java] !{BooleanLogic<0x7f4d12476e50>: AND
+ [java] !{BooleanPredicate<0x7f4ca642cc70>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f4ca642cce0>:{Set(1)<0x7f4d10408160>:Members: 3, } 0x7f4ca642cce0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f4ca6426940>: 3}
+ [java] }
+ [java] !{BooleanPredicate<0x7f4ca642c9c0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f4ca7665ce0>:{Set(1)<0x7f4d10276f70>:Members: 3, 5, } 0x7f4ca7665ce0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f4ca6426940>: 3}
+ [java] }
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f4ca642cb90>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f4ca6bafa30>:{Set(1)<0x7f4d10276e10>:Members: 4, } 0x7f4ca6bafa30 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f4d103c38b0>: 4}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7f4d10403960>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7f4ca7665ce0>:{Set(1)<0x7f4d10276f70>:Members: 3, 5, } 0x7f4ca7665ce0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7f4ca5dd9c30>: 5}
+ [java] }
+ [java]
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca642cce0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6bafa30....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7665ce0....
+ [java] Encoding Graph Time: 0.000080
+ [java] Elapse Encode time: 0.000107
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.036699
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.036812
+ [java] Elapse Encode time: 0.000020
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000028
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000010
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca642cce0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5d76ad0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5646470....
+ [java] Encoding Graph Time: 0.000106
+ [java] Elapse Encode time: 0.000144
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041625
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041774
+ [java] Elapse Encode time: 0.000020
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000027
+ [java] Polarity time: 0.000011
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000009
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5646470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5d76ad0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca642cce0....
+ [java] Encoding Graph Time: 0.000158
+ [java] Elapse Encode time: 0.000211
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.042939
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.043158
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000075
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision aboisSat= true ,SatuneSat= true
+ [java] 1594752246076Satune Solving Time: 40.529948
+ [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] 1594752246146 Original Encoding Solving Time: 0.023036
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246146Satune Solving Time: 0.032507
+ [java] Path Solving Time: 12.947364
+ [java] Path Solving Time: 6.380534
+ [java] 1594752246206 Original Encoding Solving Time: 1.024407
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752246206Satune Solving Time: 40.608819
+ [java] 1594752246269 Original Encoding Solving Time: 0.044262
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246269Satune Solving Time: 0.040889
+ [java] Path Solving Time: 11.157457
+ [java] Path Solving Time: 3.660764
+ [java] 1594752246320 Original Encoding Solving Time: 0.289832
+ [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] 1594752246320Satune Solving Time: 40.121377
+ [java] 1594752246380 Original Encoding Solving Time: 0.021378
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246380Satune Solving Time: 0.03288
+ [java] Path Solving Time: 10.659221
+ [java] Path Solving Time: 3.749586
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] 1594752246432 Original Encoding Solving Time: 0.394471
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752246432Satune Solving Time: 39.659635
+ [java] 1594752246490 Original Encoding Solving Time: 0.021401
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246490Satune Solving Time: 0.035008
+ [java] Path Solving Time: 11.489207
+ [java] Path Solving Time: 4.709628
+ [java] Done with finding holes : Flag = false
+ [java] 1594752246543 Original Encoding Solving Time: 0.346168
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752246543Satune Solving Time: 45.019756
+ [java] 1594752246608 Original Encoding Solving Time: 0.027524
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246608Satune Solving Time: 0.039599
+ [java] Path Solving Time: 11.722477
+ [java] Path Solving Time: 4.692032
+ [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] 1594752246661 Original Encoding Solving Time: 0.328067
+ [java] ut element 0x7f4ca5d76ad0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5646470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d10405f20....
+ [java] Encoding Graph Time: 0.000101
+ [java] Elapse Encode time: 0.000129
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.040387
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.040522
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] Encoding Graph Time: 0.000209
+ [java] Elapse Encode time: 0.000243
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.040349
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.040599
+ [java] Elapse Encode time: 0.000025
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000036
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] Encoding Graph Time: 0.000077
+ [java] Elapse Encode time: 0.000098
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.040010
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.040113
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] Encoding Graph Time: 0.000117
+ [java] Elapse Encode time: 0.000146
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.039497
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039651
+ [java] Elapse Encode time: 0.000023
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [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.000019
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] Encoding Graph Time: 0.000080
+ [java] Elapse Encode time: 0.000117
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044890
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.045012
+ [java] Elapse Encode time: 0.000024
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000035
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000043
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] Encoding Graph Time: 0.000088
+ [java] Elapse Encode time: 0.000152
+ [java] Is problem UNSAisSat= true ,SatuneSat= true
+ [java] 1594752246661Satune Solving Time: 49.261318
+ [java] 1594752246725 Original Encoding Solving Time: 0.021058
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246725Satune Solving Time: 0.031905
+ [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: 11.754401
+ [java] Path Solving Time: 3.534075
+ [java] 1594752246777 Original Encoding Solving Time: 0.260901
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752246777Satune Solving Time: 40.214321
+ [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] 1594752246831 Original Encoding Solving Time: 0.023028
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246831Satune Solving Time: 0.032336
+ [java] Path Solving Time: 8.955297
+ [java] Path Solving Time: 3.48866
+ [java] 1594752246881 Original Encoding Solving Time: 0.454094
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752246881Satune Solving Time: 39.862118
+ [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] 1594752246935 Original Encoding Solving Time: 0.020962
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752246935Satune Solving Time: 0.03298
+ [java] Path Solving Time: 17.655486
+ [java] Path Solving Time: 13.833651
+ [java] Path Solving Time: 4.256933
+ [java] Path Solving Time: 4.357243
+ [java] Path Solving Time: 47.787513
+ [java] 1594752247062 Original Encoding Solving Time: 0.39979
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752247062Satune Solving Time: 39.930108
+ [java] 1594752247111 Original Encoding Solving Time: 0.023835
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752247111Satune Solving Time: 0.032238
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: MatrixAlgebra is abstract; cannot be instantiated
+ [java] com.opengamma.analytics.math.matrix.MatrixAlgebra sypet_var37 = new com.opengamma.analytics.math.matrix.MatrixAlgebra();com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var38 = sypet_var37.matrixTransposeMultiplyMatrix(sypet_arg0);return sypet_var38;}
+ [java] ^
+ [java] 1 error
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 59.264603
+ [java] Path Solving Time: 27.488844
+ [java] Path Solving Time: 8.61831
+ [java] 1594752247245 Original Encoding Solving Time: 0.508613
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752247245Satune Solving Time: 52.053534
+ [java] Path Solving Time: 11.457923
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Path Solving Time: 10.335648
+ [java] 1594752247369 Original Encoding Solving Time: 0.359783
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752247369Satune Solving Time: 39.874221
+ [java] 1594752247425 Original Encoding Solving Time: 0.025565
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752247425Satune Solving Time: 0.037967
+ [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: 13.660748
+ [java] PetriNet for path length: 6 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 16.148805
+ [java] Path Solving Time: 3.799454
+ [java] 1594752253033 Original Encoding Solving Time: 0.331455
+ [java] T after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.049087
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.049253
+ [java] Elapse Encode time: 0.000020
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000028
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] Encoding Graph Time: 0.000073
+ [java] Elapse Encode time: 0.000103
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.040098
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.040206
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] Encoding Graph Time: 0.000093
+ [java] Elapse Encode time: 0.000117
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.039730
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039853
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000029
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000037
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca5149f70....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514a070....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca514c360....
+ [java] Encoding Graph Time: 0.000076
+ [java] Elapse Encode time: 0.000126
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 7 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.039789
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039921
+ [java] Elapse Encode time: 0.000020
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000028
+ [java] Polarity time: 0.000011
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4d12425260....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6794fa0....
+ [java] Encoding Graph Time: 0.000180
+ [java] Elapse Encode time: 0.000223
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 3 #Vars = 3
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.051814
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.052045
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4d124294c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d12427b40....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000101
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 5 #Vars = 4
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.039760
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.039866
+ [java] Elapse Encode time: 0.000023
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 6 #Vars = 4
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000001
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000033
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000005
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4d12428b10....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] INFO: naive encoder is making the decision about element 0x7f4d103c1530..isSat= true ,SatuneSat= true
+ [java] 1594752253033Satune Solving Time: 54.476701
+ [java] 1594752253100 Original Encoding Solving Time: 0.02408
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253100Satune Solving Time: 0.079187
+ [java] Path Solving Time: 12.568414
+ [java] Path Solving Time: 4.244955
+ [java] /Source.java:3: error: package cern.colt.matrix does not exist
+ [java] com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var44 = com.opengamma.analytics.math.matrix.DoubleMatrixUtils.getTranspose(sypet_arg0);cern.colt.matrix.DoubleMatrix2D sypet_var45 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var44);com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var46 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var45);return sypet_var46;}
+ [java] ^
+ [java] /Source.java:3: error: cannot access DoubleMatrix2D
+ [java] com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var44 = com.opengamma.analytics.math.matrix.DoubleMatrixUtils.getTranspose(sypet_arg0);cern.colt.matrix.DoubleMatrix2D sypet_var45 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var44);com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var46 = com.opengamma.analytics.math.util.wrapper.ColtMathWrapper.wrap(sypet_var45);return sypet_var46;}
+ [java] ^
+ [java] class file for cern.colt.matrix.DoubleMatrix2D not found
+ [java] 2 errors
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752253167 Original Encoding Solving Time: 0.996268
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752253167Satune Solving Time: 56.291672
+ [java] 1594752253237 Original Encoding Solving Time: 0.027039
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253237Satune Solving Time: 0.083219
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 15.234587
+ [java] Path Solving Time: 4.151965
+ [java] 1594752253306 Original Encoding Solving Time: 0.359268
+ [java] Let's read clauses ...
+ [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] 1594752253306Satune Solving Time: 54.43339
+ [java] 1594752253374 Original Encoding Solving Time: 0.024733
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253374Satune Solving Time: 0.082964
+ [java] Path Solving Time: 14.935459
+ [java] Path Solving Time: 4.017342
+ [java] 1594752253443 Original Encoding Solving Time: 0.355331
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752253443Satune Solving Time: 54.721151
+ [java] 1594752253513 Original Encoding Solving Time: 0.020447
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253513Satune Solving Time: 0.033172
+ [java] Path Solving Time: 12.632811
+ [java] Path Solving Time: 4.352209
+ [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] 1594752253585 Original Encoding Solving Time: 1.1345
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752253585Satune Solving Time: 53.640607
+ [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] 1594752253658 Original Encoding Solving Time: 0.028265
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253658Satune Solving Time: 0.041888
+ [java] Path Solving Time: 14.39997
+ [java] Path Solving Time: 4.46839
+ [java] 1594752253726 Original Encoding Solving Time: 0.491613
+ [java] ..
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca67810e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d10402f70....
+ [java] Encoding Graph Time: 0.000176
+ [java] Elapse Encode time: 0.000202
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054260
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054468
+ [java] Elapse Encode time: 0.000028
+ [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.000039
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000075
+ [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 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000151
+ [java] Elapse Encode time: 0.000185
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.056092
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.056284
+ [java] Elapse Encode time: 0.000027
+ [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.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [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 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000120
+ [java] Elapse Encode time: 0.000156
+ [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.054261
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054424
+ [java] Elapse Encode time: 0.000030
+ [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.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000132
+ [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.054542
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054713
+ [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.000029
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000095
+ [java] Elapse Encode time: 0.000127
+ [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.053499
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.053632
+ [java] Elapse Encode time: 0.000025
+ [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.000037
+ [java] Let's read clauses ...
+ [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] Polarity time: 0.00000isSat= true ,SatuneSat= true
+ [java] 1594752253726Satune Solving Time: 54.005649
+ [java] 1594752253795 Original Encoding Solving Time: 0.031912
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253795Satune Solving Time: 0.094354
+ [java] Path Solving Time: 15.201078
+ [java] Path Solving Time: 4.456475
+ [java] 1594752253865 Original Encoding Solving Time: 0.492526
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752253865Satune Solving Time: 54.526491
+ [java] 1594752253939 Original Encoding Solving Time: 0.020333
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752253939Satune Solving Time: 0.033425
+ [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: 14.128925
+ [java] Path Solving Time: 4.610924
+ [java] 1594752254008 Original Encoding Solving Time: 0.421783
+ [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] 1594752254008Satune Solving Time: 65.291021
+ [java] 1594752254089 Original Encoding Solving Time: 0.020501
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752254089Satune Solving Time: 0.031317
+ [java] Path Solving Time: 13.748017
+ [java] Path Solving Time: 4.196168
+ [java] 1594752254157 Original Encoding Solving Time: 0.381599
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752254157Satune Solving Time: 53.917562
+ [java] 1594752254228 Original Encoding Solving Time: 0.026671
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752254228Satune Solving Time: 0.0391
+ [java] Path Solving Time: 13.284983
+ [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: 4.691501
+ [java] 1594752254296 Original Encoding Solving Time: 0.368835
+ [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] 1594752254296Satune Solving Time: 54.685081
+ [java] 1594752254369 Original Encoding Solving Time: 0.019053
+ [java] 5
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000075
+ [java] Elapse Encode time: 0.000100
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.053891
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.053997
+ [java] Elapse Encode time: 0.000032
+ [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.000047
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000089
+ [java] Polarity time: 0.000010
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000132
+ [java] Elapse Encode time: 0.000180
+ [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.054331
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054518
+ [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.000005
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000080
+ [java] Elapse Encode time: 0.000109
+ [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.065167
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065282
+ [java] Elapse Encode time: 0.000020
+ [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.000028
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000071
+ [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.053811
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.053910
+ [java] Elapse Encode time: 0.000026
+ [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.000034
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000113
+ [java] Elapse Encode time: 0.000151
+ [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.054519
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054676
+ [java] Elapse Encode time: 0.000022
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10isSat= false ,SatuneSat= false
+ [java] 1594752254369Satune Solving Time: 0.038148
+ [java] Path Solving Time: 13.41659
+ [java] Path Solving Time: 4.345844
+ [java] 1594752254436 Original Encoding Solving Time: 0.318956
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752254436Satune Solving Time: 55.147308
+ [java] 1594752254507 Original Encoding Solving Time: 0.030291
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752254507Satune Solving Time: 0.090519
+ [java] Path Solving Time: 13.641439
+ [java] Path Solving Time: 4.225612
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752254579 Original Encoding Solving Time: 0.569748
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752254579Satune Solving Time: 53.885266
+ [java] 1594752254648 Original Encoding Solving Time: 0.025223
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752254648Satune Solving Time: 0.087322
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 13.324048
+ [java] Path Solving Time: 4.150294
+ [java] 1594752254715 Original Encoding Solving Time: 0.374077
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] 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] 1594752254715Satune Solving Time: 54.783476
+ [java] 1594752254785 Original Encoding Solving Time: 0.024321
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752254785Satune Solving Time: 0.080387
+ [java] Path Solving Time: 14.88788
+ [java] Path Solving Time: 4.323388
+ [java] 1594752254854 Original Encoding Solving Time: 0.423782
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752254854Satune Solving Time: 54.550296
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752255164 Original Encoding Solving Time: 0.024733
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752255164Satune Solving Time: 0.07713
+ [java] Path Solving Time: 12.110388
+ [java] Path Solving Time: 3.973611
+ [java] 1594752255229 Original Encoding Solving Time: 0.300305
+ [java] #Vars = 6
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000004
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000034
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000019
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000072
+ [java] Elapse Encode time: 0.000106
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.055027
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055139
+ [java] Elapse Encode time: 0.000033
+ [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.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000085
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000122
+ [java] Elapse Encode time: 0.000159
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.053709
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.053877
+ [java] Elapse Encode time: 0.000027
+ [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.000048
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000083
+ [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 0x7f4ca7644dd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000123
+ [java] Elapse Encode time: 0.000171
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054597
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054775
+ [java] Elapse Encode time: 0.000027
+ [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.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000076
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000008
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645370....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7644dd0....
+ [java] Encoding Graph Time: 0.000098
+ [java] Elapse Encode time: 0.000161
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054376
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054542
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d1383e2c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d1383e3c0....
+ [java] Encoding Graph Time: 0.000080
+ [java] Elapse Encode time: 0.000104
+ [java] Is problem UNSAT after encoding: 0
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] #Clauses = 10 #isSat= true ,SatuneSat= true
+ [java] 1594752255229Satune Solving Time: 54.376433
+ [java] 1594752255535 Original Encoding Solving Time: 0.025404
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752255535Satune Solving Time: 0.082925
+ [java] Path Solving Time: 13.534475
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 5.923372
+ [java] 1594752255606 Original Encoding Solving Time: 0.405136
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752255606Satune Solving Time: 54.120557
+ [java] 1594752255907 Original Encoding Solving Time: 0.025122
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752255907Satune Solving Time: 0.077114
+ [java] Path Solving Time: 11.997534
+ [java] Path Solving Time: 3.981221
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752255972 Original Encoding Solving Time: 0.291929
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752255972Satune Solving Time: 54.507334
+ [java] Let's read clauses ...
+ [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] 1594752256274 Original Encoding Solving Time: 0.024671
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256274Satune Solving Time: 0.079341
+ [java] Path Solving Time: 13.868232
+ [java] Path Solving Time: 3.971955
+ [java] 1594752256341 Original Encoding Solving Time: 0.280833
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752256341Satune Solving Time: 55.530377
+ [java] 1594752256408 Original Encoding Solving Time: 0.01984
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256408Satune Solving Time: 0.032546
+ [java] Path Solving Time: 13.108035
+ [java] Path Solving Time: 3.946022
+ [java] Done with finding holes : Flag = false
+ [java] 1594752256474 Original Encoding Solving Time: 0.273681
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752256474Satune Solving Time: 55.829182
+ [java] 1594752256541 Original Encoding Solving Time: 0.026518
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256541Satune Solving Time: 0.082251
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 15.262983
+ [java] Path Solving Time: 4.849208
+ [java] 1594752256612 Original Encoding Solving Time: 0.315064
+ [java] Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054259
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054368
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Polarity time: 0.000018
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000007
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d13fc3130....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d13fc31f0....
+ [java] Encoding Graph Time: 0.000093
+ [java] Elapse Encode time: 0.000135
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.053971
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054112
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d13fb36f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d13fb9650....
+ [java] Encoding Graph Time: 0.000083
+ [java] Elapse Encode time: 0.000115
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054379
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054499
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000075
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] Encoding Graph Time: 0.000097
+ [java] Elapse Encode time: 0.000121
+ [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.055395
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055522
+ [java] Elapse Encode time: 0.000020
+ [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.000029
+ [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 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000083
+ [java] Elapse Encode time: 0.000108
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.055709
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055821
+ [java] Elapse Encode time: 0.000027
+ [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.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] INFO: naive encoder is making the deisSat= true ,SatuneSat= true
+ [java] 1594752256612Satune Solving Time: 54.455365
+ [java] 1594752256681 Original Encoding Solving Time: 0.021114
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256681Satune Solving Time: 0.033944
+ [java] Path Solving Time: 12.743804
+ [java] Path Solving Time: 4.376489
+ [java] 1594752256749 Original Encoding Solving Time: 0.356996
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752256749Satune Solving Time: 54.766775
+ [java] 1594752256817 Original Encoding Solving Time: 0.02085
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256817Satune Solving Time: 0.03418
+ [java] Path Solving Time: 15.19931
+ [java] Path Solving Time: 4.119709
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] 1594752256888 Original Encoding Solving Time: 0.873726
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752256888Satune Solving Time: 54.881277
+ [java] 1594752256956 Original Encoding Solving Time: 0.030944
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752256956Satune Solving Time: 0.099404
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 13.671678
+ [java] Path Solving Time: 4.362327
+ [java] 1594752257024 Original Encoding Solving Time: 0.244695
+ [java] Let's read clauses ...
+ [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] 1594752257024Satune Solving Time: 54.79406
+ [java] 1594752257091 Original Encoding Solving Time: 0.031547
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257091Satune Solving Time: 0.090695
+ [java] Path Solving Time: 16.627566
+ [java] Path Solving Time: 3.990906
+ [java] 1594752257162 Original Encoding Solving Time: 0.244219
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752257162Satune Solving Time: 55.477829
+ [java] 1594752257233 Original Encoding Solving Time: 0.024681
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257233Satune Solving Time: 0.042146
+ [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: 28.043219
+ [java] Path Solving Time: 4.588878
+ [java] 1594752257315 Original Encoding Solving Time: 0.296272
+ [java] cision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] Encoding Graph Time: 0.000104
+ [java] Elapse Encode time: 0.000129
+ [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.054312
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054447
+ [java] Elapse Encode time: 0.000022
+ [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.000008
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000110
+ [java] Elapse Encode time: 0.000158
+ [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.054592
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054757
+ [java] Elapse Encode time: 0.000022
+ [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.000005
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000107
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054761
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054873
+ [java] Elapse Encode time: 0.000034
+ [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.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000094
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000095
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054684
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054786
+ [java] Elapse Encode time: 0.000033
+ [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.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000085
+ [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 0x7f4ca7645470....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] Encoding Graph Time: 0.000067
+ [java] Elapse Encode time: 0.000089
+ [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.055375
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055469
+ [java] Elapse Encode time: 0.000026
+ [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.000037
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000002
+ [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: naiveisSat= true ,SatuneSat= true
+ [java] 1594752257315Satune Solving Time: 54.920295
+ [java] 1594752257386 Original Encoding Solving Time: 0.031941
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257386Satune Solving Time: 0.035396
+ [java] Path Solving Time: 13.744971
+ [java] Path Solving Time: 4.660378
+ [java] 1594752257455 Original Encoding Solving Time: 0.595562
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752257455Satune Solving Time: 54.953099
+ [java] 1594752257530 Original Encoding Solving Time: 0.034984
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257530Satune Solving Time: 0.084972
+ [java] Path Solving Time: 13.480786
+ [java] Path Solving Time: 5.593018
+ [java] Let's read clauses ...
+ [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] 1594752257601 Original Encoding Solving Time: 0.262863
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752257601Satune Solving Time: 54.99126
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] Done with finding holes : Flag = false
+ [java] 1594752257672 Original Encoding Solving Time: 0.020704
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257672Satune Solving Time: 0.033836
+ [java] Path Solving Time: 14.449488
+ [java] Path Solving Time: 3.988829
+ [java] 1594752257740 Original Encoding Solving Time: 0.238528
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752257740Satune Solving Time: 55.035913
+ [java] 1594752257815 Original Encoding Solving Time: 0.019969
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752257815Satune Solving Time: 0.03473
+ [java] Path Solving Time: 14.123817
+ [java] Path Solving Time: 4.009146
+ [java] Done with finding holes : Flag = false
+ [java] 1594752257883 Original Encoding Solving Time: 0.239119
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752257883Satune Solving Time: 55.3872
+ [java] 1594752257961 Original Encoding Solving Time: 0.01937
+ [java] encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88e20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76453f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca7645470....
+ [java] Encoding Graph Time: 0.000080
+ [java] Elapse Encode time: 0.000103
+ [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.054803
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054912
+ [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.000031
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d124ebea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d124ece40....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d124ebf40....
+ [java] Encoding Graph Time: 0.000127
+ [java] Elapse Encode time: 0.000157
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054780
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054944
+ [java] Elapse Encode time: 0.000027
+ [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.000044
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000080
+ [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 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b75440....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b754e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b73770....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000101
+ [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.054876
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054983
+ [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.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca4e88ea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b7c1c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b7c240....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b7fb90....
+ [java] Encoding Graph Time: 0.000078
+ [java] Elapse Encode time: 0.000104
+ [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.054916
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055028
+ [java] Elapse Encode time: 0.000022
+ [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.000031
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca684ed20....
+ [java] Encoding Graph Time: 0.000087
+ [java] Elapse Encode time: 0.000126
+ [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.055247
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055379
+ [java] Elapse Encode time: 0.000022
+ [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] RisSat= false ,SatuneSat= false
+ [java] 1594752257961Satune Solving Time: 0.038306
+ [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: 13.294056
+ [java] Path Solving Time: 3.972199
+ [java] 1594752258028 Original Encoding Solving Time: 0.217742
+ [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] 1594752258028Satune Solving Time: 55.369233
+ [java] 1594752258101 Original Encoding Solving Time: 0.01981
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752258101Satune Solving Time: 0.033911
+ [java] Path Solving Time: 13.538867
+ [java] Path Solving Time: 3.96576
+ [java] 1594752258168 Original Encoding Solving Time: 0.228997
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752258168Satune Solving Time: 55.450093
+ [java] 1594752258243 Original Encoding Solving Time: 0.018861
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752258243Satune Solving Time: 0.032873
+ [java] Path Solving Time: 12.841647
+ [java] Path Solving Time: 3.944541
+ [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] 1594752258309 Original Encoding Solving Time: 0.241836
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752258309Satune Solving Time: 55.688191
+ [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] 1594752258385 Original Encoding Solving Time: 0.020846
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752258385Satune Solving Time: 0.034712
+ [java] Path Solving Time: 13.757226
+ [java] Path Solving Time: 4.609982
+ [java] 1594752258453 Original Encoding Solving Time: 0.415783
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752258453Satune Solving Time: 57.068754
+ [java] 1594752258535 Original Encoding Solving Time: 0.025004
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752258535Satune Solving Time: 0.042653
+ [java] Path Solving Time: 25.985766
+ [java] Path Solving Time: 5.013404
+ [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] 1594752258618 Original Encoding Solving Time: 0.448152
+ [java] Let's read clauses ...
+ [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] 1594752258618Satune Solving Time: 57.159305
+ [java] 1594752258696 Original Encoding Solving Time: 0.027037
+ [java] esult Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000034
+ [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 0x7f4ca684ed20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] Encoding Graph Time: 0.000083
+ [java] Elapse Encode time: 0.000109
+ [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.055247
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055361
+ [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.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca684ed20....
+ [java] Encoding Graph Time: 0.000076
+ [java] Elapse Encode time: 0.000101
+ [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.055337
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055442
+ [java] Elapse Encode time: 0.000020
+ [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.000029
+ [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 0x7f4ca684ed20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000101
+ [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.055574
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055680
+ [java] Elapse Encode time: 0.000022
+ [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.000008
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000007
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca684ed20....
+ [java] Encoding Graph Time: 0.000135
+ [java] Elapse Encode time: 0.000190
+ [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.056863
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.057060
+ [java] Elapse Encode time: 0.000026
+ [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.000038
+ [java] Polarity time: 0.000010
+ [java] Preprocess time: 0.000017
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca684ed20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d106d1330....
+ [java] Encoding Graph Time: 0.000142
+ [java] Elapse Encode time: 0.000198
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.056944
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.057150
+ [java] Elapse EncodisSat= false ,SatuneSat= false
+ [java] 1594752258696Satune Solving Time: 0.09926
+ [java] Path Solving Time: 17.245054
+ [java] Path Solving Time: 4.863682
+ [java] 1594752258769 Original Encoding Solving Time: 0.415279
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752258769Satune Solving Time: 59.910598
+ [java] 1594752258850 Original Encoding Solving Time: 0.02493
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752258850Satune Solving Time: 0.084697
+ [java] Path Solving Time: 14.070603
+ [java] Path Solving Time: 4.958905
+ [java] Let's read clauses ...
+ [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] 1594752258919 Original Encoding Solving Time: 0.341069
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Note: /Source.java uses or overrides a deprecated API.
+ [java] Note: Recompile with -Xlint:deprecation for details.
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752258919Satune Solving Time: 56.825356
+ [java] =========Statistics (time in milliseconds)=========
+ [java] Benchmark Id: 5
+ [java] Sketch Generation Time: 1285.9613060000001
+ [java] Sketch Completion Time: 5004.355726000001
+ [java] Compilation Time: 838.639762
+ [java] Running Test cases Time: 1402.9785850000003
+ [java] Synthesis Time: 7693.295617000002
+ [java] Total Time: 8531.935379000002
+ [java] Number of components: 3
+ [java] Number of holes: 4
+ [java] Number of completed programs: 101
+ [java] Number of sketches: 51
+ [java] Solution:
+ [java] org.apache.commons.math.linear.RealMatrix sypet_var184 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.wrap(sypet_arg0);
+ [java] org.apache.commons.math.linear.RealMatrix sypet_var185 = sypet_var184.inverse();
+ [java] com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var186 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.unwrap(sypet_var185);
+ [java] return sypet_var186;
+ [java]
+ [java] ============================
+ [java] e time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000044
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000094
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000016
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b798d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca6b79990....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca684ed20....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca67df9a0....
+ [java] Encoding Graph Time: 0.000180
+ [java] Elapse Encode time: 0.000222
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.059667
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.059898
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Polarity time: 0.000017
+ [java] Preprocess time: 0.000016
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f4d12c0b390....
+ [java] INFO: naive encoder is making the decision about element 0x7f4d12c0a930....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca76de0f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f4ca773d820....
+ [java] Encoding Graph Time: 0.000168
+ [java] Elapse Encode time: 0.000234
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.056575
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.056816
+
+BUILD SUCCESSFUL
+Total time: 31 seconds
projects / Benchmarks_CSolver.git / blobdiff