--- /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/7/benchmark7.json
+ [java] Benchmark Id: 7
+ [java] Method name: getOuterProduct
+ [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.DoubleMatrix1D, com.opengamma.analytics.math.matrix.DoubleMatrix1D]
+ [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: 4212.607594
+ [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] PetriNet for path length: 4 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 5 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 62.925452
+ [java] Path Solving Time: 76.723591
+ [java] PetriNet for path length: 6 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 40.094458
+ [java] Path Solving Time: 7.119048
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752885793 Original Encoding Solving Time: 0.73185
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752885793Satune Solving Time: 52.895759
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752886152 Original Encoding Solving Time: 0.106312
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886152Satune Solving Time: 0.097826
+ [java] 1594752886177 Original Encoding Solving Time: 0.038915
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752886177Satune Solving Time: 0.089365
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 31.791773
+ [java] Path Solving Time: 6.006309
+ [java] 1594752886271 Original Encoding Solving Time: 0.699148
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886271Satune Solving Time: 55.039883
+ [java] 1594752886349 Original Encoding Solving Time: 0.079279
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886349Satune Solving Time: 0.083359
+ [java] 1594752886369 Original Encoding Solving Time: 0.033602
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752886369Satune Solving Time: 0.076544
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 19.314255
+ [java] Path Solving Time: 6.965483
+ [java] 1594752886451 Original Encoding Solving Time: 1.209433
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886451Satune Solving Time: 64.062419
+ [java] 1594752886543 Original Encoding Solving Time: 0.091392
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886543Satune Solving Time: 0.077056
+ [java] 1594752886577 Original Encoding Solving Time: 0.055681
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752886577Satune Solving Time: 0.095298
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 20.674714
+ [java] Path Solving Time: 5.239086
+ [java] 1594752886656 Original Encoding Solving Time: 0.763724
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Polarity time: 0.000021
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000009
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1980....
+ [java] Encoding Graph Time: 0.000145
+ [java] Elapse Encode time: 0.000210
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.052645
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.052864
+ [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.000035
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000070
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000085
+ [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 0x7f7c483b1980....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] Encoding Graph Time: 0.000069
+ [java] Elapse Encode time: 0.000096
+ [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.054926
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055028
+ [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: SAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1980....
+ [java] Encoding Graph Time: 0.000104
+ [java] Elapse Encode time: 0.000142
+ [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.063907
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064054
+ [java] Elapse Encode time: 0.000026
+ [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: SAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000046
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000091
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1980....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] Encoding Graph Time: 0.000121
+ [java] Elapse Encode time: 0.000157
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 10
+ [java] DaisSat= true ,SatuneSat= true
+ [java] 1594752886656Satune Solving Time: 67.37937
+ [java] 1594752886744 Original Encoding Solving Time: 0.102481
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886744Satune Solving Time: 0.085724
+ [java] 1594752886762 Original Encoding Solving Time: 0.100013
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886762Satune Solving Time: 0.095723
+ [java] 1594752886779 Original Encoding Solving Time: 0.056697
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886779Satune Solving Time: 0.096124
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752886796 Original Encoding Solving Time: 0.074184
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752886796Satune Solving Time: 0.11139
+ [java] Path Solving Time: 15.97435
+ [java] Path Solving Time: 4.91531
+ [java] 1594752886869 Original Encoding Solving Time: 0.581801
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886869Satune Solving Time: 78.974638
+ [java] 1594752886967 Original Encoding Solving Time: 0.140336
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886967Satune Solving Time: 0.08869
+ [java] 1594752886983 Original Encoding Solving Time: 0.075931
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886983Satune Solving Time: 0.08704
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 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] 1594752886998 Original Encoding Solving Time: 0.046556
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752886998Satune Solving Time: 0.091025
+ [java] 1594752887014 Original Encoding Solving Time: 0.078054
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752887014Satune Solving Time: 0.112811
+ [java] Path Solving Time: 13.501185
+ [java] Path Solving Time: 4.590922
+ [java] 1594752887085 Original Encoding Solving Time: 0.682491
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887085Satune Solving Time: 68.389775
+ [java] 1594752887167 Original Encoding Solving Time: 0.076356
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887167Satune Solving Time: 0.082336
+ [java] 1594752887182 Original Encoding Solving Time: 0.109518
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887182Satune Solving Time: 0.087884
+ [java] 1594752887194 Original Encoding Solving Time: 0.071487
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887194Satune Solving Time: 0.094471
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 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] 1594752887211 Original Encoding Solving Time: 0.110727
+ [java] ta is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.067208
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.067371
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000052
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000091
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000051
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000092
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000066
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000107
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1980....
+ [java] Encoding Graph Time: 0.000136
+ [java] Elapse Encode time: 0.000179
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.078777
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.078964
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000046
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000083
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000045
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000087
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000067
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000108
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000008
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1980....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] Encoding Graph Time: 0.000130
+ [java] Elapse Encode time: 0.000173
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.068202
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.068382
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Elapse Encode time: 0.000036
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000045
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000089
+ [java] ElaisSat= false ,SatuneSat= false
+ [java] 1594752887211Satune Solving Time: 0.120034
+ [java] Path Solving Time: 36.752402
+ [java] Path Solving Time: 40.142274
+ [java] 1594752887340 Original Encoding Solving Time: 1.290856
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887340Satune Solving Time: 66.319064
+ [java] 1594752887673 Original Encoding Solving Time: 0.075125
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752887673Satune Solving Time: 0.076709
+ [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] 1594752887939 Original Encoding Solving Time: 0.032659
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752887939Satune Solving Time: 0.086819
+ [java] Path Solving Time: 47.785377
+ [java] Path Solving Time: 24.618583
+ [java] Path Solving Time: 10.591263
+ [java] 1594752888075 Original Encoding Solving Time: 0.984596
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888075Satune Solving Time: 54.200322
+ [java] 1594752888147 Original Encoding Solving Time: 0.062415
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888147Satune Solving Time: 0.081606
+ [java] 1594752888159 Original Encoding Solving Time: 0.062448
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888159Satune Solving Time: 0.082796
+ [java] 1594752888172 Original Encoding Solving Time: 0.040201
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888172Satune Solving Time: 0.08647
+ [java] 1594752888185 Original Encoding Solving Time: 0.055668
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752888185Satune Solving Time: 0.102655
+ [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: 22.369826
+ [java] Path Solving Time: 9.886783
+ [java] 1594752888268 Original Encoding Solving Time: 0.395319
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888268Satune Solving Time: 56.578781
+ [java] 1594752888338 Original Encoding Solving Time: 0.089862
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888338Satune Solving Time: 0.094588
+ [java] 1594752888353 Original Encoding Solving Time: 0.065181
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752888353Satune Solving Time: 0.092988
+ [java] Path Solving Time: 32.181648
+ [java] Path Solving Time: 3.980016
+ [java] Path Solving Time: 4.045647
+ [java] Path Solving Time: 191.325373
+ [java] Path Solving Time: 42.488832
+ [java] 1594752888680 Original Encoding Solving Time: 0.690009
+ [java] pse Encode time: 0.000043
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000057
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000115
+ [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 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] Encoding Graph Time: 0.000100
+ [java] Elapse Encode time: 0.000131
+ [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.066169
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066306
+ [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: SAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000082
+ [java] Polarity time: 0.000014
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] Encoding Graph Time: 0.000112
+ [java] Elapse Encode time: 0.000153
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054027
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054186
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000082
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000055
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000098
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] Encoding Graph Time: 0.000122
+ [java] Elapse Encode time: 0.000163
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 11 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.056397
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.056567
+ [java] Elapse Encode time: 0.000026
+ [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.000056
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000090
+ [java] Elapse Encode time: 0.000035
+ [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.000042
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000088
+ [java] Polarity time: 0.000010
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000002
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] INFO: naive encoder is making the decision aisSat= true ,SatuneSat= true
+ [java] 1594752888680Satune Solving Time: 55.183215
+ [java] 1594752888748 Original Encoding Solving Time: 0.058217
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752888748Satune Solving Time: 0.072958
+ [java] 1594752888759 Original Encoding Solving Time: 0.021021
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752888759Satune Solving Time: 0.076515
+ [java] Path Solving Time: 87.313045
+ [java] Path Solving Time: 398.904949
+ [java] Path Solving Time: 178.047625
+ [java] 1594752889474 Original Encoding Solving Time: 0.702548
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889474Satune Solving Time: 55.279379
+ [java] 1594752889541 Original Encoding Solving Time: 0.076531
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889541Satune Solving Time: 0.076009
+ [java] 1594752889554 Original Encoding Solving Time: 0.027859
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752889554Satune Solving Time: 0.095519
+ [java] Path Solving Time: 45.331783
+ [java] Path Solving Time: 10.780866
+ [java] 1594752889661 Original Encoding Solving Time: 0.405039
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889661Satune Solving Time: 56.657414
+ [java] 1594752889730 Original Encoding Solving Time: 0.080337
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889730Satune Solving Time: 0.118285
+ [java] 1594752889741 Original Encoding Solving Time: 0.022723
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752889741Satune Solving Time: 0.077946
+ [java] Path Solving Time: 126.312394
+ [java] Path Solving Time: 9.515021
+ [java] 1594752889927 Original Encoding Solving Time: 0.367543
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889927Satune Solving Time: 56.194001
+ [java] 1594752889998 Original Encoding Solving Time: 0.056101
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752889998Satune Solving Time: 0.088062
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752890014 Original Encoding Solving Time: 0.02533
+ [java] bout element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] Encoding Graph Time: 0.000095
+ [java] Elapse Encode time: 0.000134
+ [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.055031
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055172
+ [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.000034
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000069
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000072
+ [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 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] Encoding Graph Time: 0.000064
+ [java] Elapse Encode time: 0.000089
+ [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.055175
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055269
+ [java] Elapse Encode time: 0.000025
+ [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: SAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000090
+ [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 0x7f7c483b1810....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] Encoding Graph Time: 0.000084
+ [java] Elapse Encode time: 0.000114
+ [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.056523
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.056643
+ [java] Elapse Encode time: 0.000067
+ [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.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000114
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 12 #Vars = 7
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b16a0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1810....
+ [java] Encoding Graph Time: 0.000089
+ [java] Elapse Encode time: 0.000113
+ [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.056064
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.056182
+ [java] Elapse Encode time: 0.000031
+ [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: SAT
+ [java] CSOLVER solve time: 0.000083
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encodinisSat= false ,SatuneSat= false
+ [java] 1594752890014Satune Solving Time: 0.096618
+ [java] Path Solving Time: 341.776332
+ [java] PetriNet for path length: 7 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 46.286255
+ [java] Path Solving Time: 40.999162
+ [java] Path Solving Time: 3.773862
+ [java] 1594752901222 Original Encoding Solving Time: 0.403687
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901222Satune Solving Time: 66.128202
+ [java] 1594752901306 Original Encoding Solving Time: 0.079782
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901306Satune Solving Time: 0.109075
+ [java] 1594752901318 Original Encoding Solving Time: 0.049422
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752901318Satune Solving Time: 0.081471
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 18.866917
+ [java] Path Solving Time: 4.762803
+ [java] 1594752901402 Original Encoding Solving Time: 0.481479
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901402Satune Solving Time: 66.767416
+ [java] 1594752901482 Original Encoding Solving Time: 0.056774
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901482Satune Solving Time: 0.085274
+ [java] 1594752901498 Original Encoding Solving Time: 0.044823
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752901498Satune Solving Time: 0.121177
+ [java] Path Solving Time: 18.838684
+ [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: 4.688292
+ [java] 1594752901587 Original Encoding Solving Time: 0.535636
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901587Satune Solving Time: 67.786285
+ [java] 1594752901668 Original Encoding Solving Time: 0.090751
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901668Satune Solving Time: 0.081192
+ [java] 1594752901679 Original Encoding Solving Time: 0.029982
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752901679Satune Solving Time: 0.083778
+ [java] Path Solving Time: 17.947613
+ [java] Path Solving Time: 4.424042
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752901761 Original Encoding Solving Time: 0.809767
+ [java] g: 0
+ [java] #Clauses = 12 #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.000092
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000019
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000197
+ [java] Elapse Encode time: 0.000243
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065866
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066115
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000067
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000104
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000076
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000153
+ [java] Elapse Encode time: 0.000201
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.066550
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066759
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000080
+ [java] Elapse Encode time: 0.000039
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000064
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000116
+ [java] Polarity time: 0.000012
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000157
+ [java] Elapse Encode time: 0.000220
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.067548
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.067776
+ [java] Elapse Encode time: 0.000029
+ [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.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000076
+ [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.000079
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000007
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] INFO: naive encoisSat= true ,SatuneSat= true
+ [java] 1594752901761Satune Solving Time: 66.730498
+ [java] 1594752901841 Original Encoding Solving Time: 0.058704
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901841Satune Solving Time: 0.090909
+ [java] 1594752901851 Original Encoding Solving Time: 0.019222
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752901851Satune Solving Time: 0.075795
+ [java] Path Solving Time: 31.389235
+ [java] Path Solving Time: 4.398067
+ [java] 1594752901946 Original Encoding Solving Time: 0.406975
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752901946Satune Solving Time: 65.685109
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752902025 Original Encoding Solving Time: 0.059164
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902025Satune Solving Time: 0.092174
+ [java] 1594752902038 Original Encoding Solving Time: 0.022239
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902038Satune Solving Time: 0.118804
+ [java] Path Solving Time: 15.241878
+ [java] Path Solving Time: 4.092089
+ [java] 1594752902117 Original Encoding Solving Time: 0.316442
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902117Satune Solving Time: 64.765841
+ [java] 1594752902194 Original Encoding Solving Time: 0.044721
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902194Satune Solving Time: 0.100183
+ [java] 1594752902205 Original Encoding Solving Time: 0.026151
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902205Satune Solving Time: 0.110198
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 19.093611
+ [java] Path Solving Time: 4.273174
+ [java] 1594752902288 Original Encoding Solving Time: 0.375694
+ [java] der is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000102
+ [java] Elapse Encode time: 0.000144
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.066569
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066719
+ [java] Elapse Encode time: 0.000035
+ [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.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000086
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000036
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000131
+ [java] Elapse Encode time: 0.000172
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065494
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065674
+ [java] Elapse Encode time: 0.000036
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000087
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000074
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000114
+ [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 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000104
+ [java] Elapse Encode time: 0.000136
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064613
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064754
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000045
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000088
+ [java] Elapse Encode time: 0.000037
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000056
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000105
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000006
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] INFO: naive encoder is making the decision about eleisSat= true ,SatuneSat= true
+ [java] 1594752902288Satune Solving Time: 65.723259
+ [java] 1594752902365 Original Encoding Solving Time: 0.045855
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902365Satune Solving Time: 0.080007
+ [java] 1594752902374 Original Encoding Solving Time: 0.027237
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902374Satune Solving Time: 0.094631
+ [java] Path Solving Time: 16.221374
+ [java] Path Solving Time: 4.120641
+ [java] 1594752902454 Original Encoding Solving Time: 0.312932
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902454Satune Solving Time: 64.695259
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752902530 Original Encoding Solving Time: 0.044392
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902530Satune Solving Time: 0.081541
+ [java] 1594752902542 Original Encoding Solving Time: 0.02385
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902542Satune Solving Time: 0.085825
+ [java] Path Solving Time: 21.137701
+ [java] Path Solving Time: 6.186507
+ [java] 1594752902629 Original Encoding Solving Time: 0.459992
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902629Satune Solving Time: 65.408978
+ [java] 1594752902706 Original Encoding Solving Time: 0.043494
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902706Satune Solving Time: 0.07765
+ [java] 1594752902717 Original Encoding Solving Time: 0.02086
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902717Satune Solving Time: 0.07432
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 15.783842
+ [java] Path Solving Time: 4.123789
+ [java] 1594752902796 Original Encoding Solving Time: 0.28789
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902796Satune Solving Time: 65.750249
+ [java] 1594752902874 Original Encoding Solving Time: 0.045734
+ [java] ment 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000094
+ [java] Elapse Encode time: 0.000128
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065579
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065713
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000076
+ [java] Elapse Encode time: 0.000037
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [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.000089
+ [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 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000083
+ [java] Elapse Encode time: 0.000112
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064567
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064685
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000137
+ [java] Elapse Encode time: 0.000174
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065216
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065396
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000034
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000070
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000074
+ [java] Elapse Encode time: 0.000098
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065636
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065740
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encodisSat= true ,SatuneSat= true
+ [java] 1594752902874Satune Solving Time: 0.078899
+ [java] 1594752902888 Original Encoding Solving Time: 0.029566
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752902888Satune Solving Time: 0.105972
+ [java] Path Solving Time: 26.972895
+ [java] Path Solving Time: 4.543869
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752902980 Original Encoding Solving Time: 0.440532
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752902980Satune Solving Time: 68.081166
+ [java] 1594752903060 Original Encoding Solving Time: 0.049849
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903060Satune Solving Time: 0.081444
+ [java] 1594752903069 Original Encoding Solving Time: 0.020907
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752903069Satune Solving Time: 0.082343
+ [java] Path Solving Time: 17.996987
+ [java] Path Solving Time: 4.646806
+ [java] 1594752903152 Original Encoding Solving Time: 0.356309
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903152Satune Solving Time: 67.219221
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752903234 Original Encoding Solving Time: 0.055671
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903234Satune Solving Time: 0.133898
+ [java] 1594752903245 Original Encoding Solving Time: 0.027021
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752903245Satune Solving Time: 0.107726
+ [java] Path Solving Time: 31.461862
+ [java] Path Solving Time: 4.956482
+ [java] 1594752903342 Original Encoding Solving Time: 0.830373
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903342Satune Solving Time: 68.076655
+ [java] 1594752903421 Original Encoding Solving Time: 0.062334
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903421Satune Solving Time: 0.081229
+ [java] 1594752903431 Original Encoding Solving Time: 0.020992
+ [java] ing: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000034
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Elapse Encode time: 0.000038
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000100
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000099
+ [java] Elapse Encode time: 0.000128
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.067936
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.068069
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000097
+ [java] Elapse Encode time: 0.000135
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.067065
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.067206
+ [java] Elapse Encode time: 0.000040
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000074
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000126
+ [java] Elapse Encode time: 0.000039
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000050
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000103
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000135
+ [java] Elapse Encode time: 0.000182
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.067872
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.068063
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000035
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000076
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] ResisSat= false ,SatuneSat= false
+ [java] 1594752903431Satune Solving Time: 0.087634
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 15.199298
+ [java] Path Solving Time: 4.105921
+ [java] 1594752903509 Original Encoding Solving Time: 0.46923
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903509Satune Solving Time: 70.923244
+ [java] 1594752903591 Original Encoding Solving Time: 0.061133
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903591Satune Solving Time: 0.090926
+ [java] 1594752903603 Original Encoding Solving Time: 0.047032
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752903603Satune Solving Time: 0.098149
+ [java] Path Solving Time: 26.278183
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 4.312077
+ [java] 1594752903694 Original Encoding Solving Time: 0.972488
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752903694Satune Solving Time: 66.145145
+ [java] 1594752904008 Original Encoding Solving Time: 0.044948
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752904008Satune Solving Time: 0.088377
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752904254 Original Encoding Solving Time: 0.051521
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752904254Satune Solving Time: 0.087562
+ [java] 1594752904498 Original Encoding Solving Time: 0.032279
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752904498Satune Solving Time: 0.092307
+ [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] 1594752904743 Original Encoding Solving Time: 0.046333
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752904743Satune Solving Time: 0.102073
+ [java] Path Solving Time: 15.190386
+ [java] Path Solving Time: 4.145581
+ [java] 1594752904822 Original Encoding Solving Time: 0.682433
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752904822Satune Solving Time: 64.378352
+ [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] 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] 1594752905141 Original Encoding Solving Time: 0.04461
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752905141Satune Solving Time: 0.083801
+ [java] 1594752905392 Original Encoding Solving Time: 0.049739
+ [java] ult Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000160
+ [java] Elapse Encode time: 0.000192
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.070713
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.070911
+ [java] Elapse Encode time: 0.000036
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000086
+ [java] Elapse Encode time: 0.000038
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [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.000093
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000021
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd64a3d00....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a9321f0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a8c0100....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6b576c0....
+ [java] Encoding Graph Time: 0.000119
+ [java] Elapse Encode time: 0.000175
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065950
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066131
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Elapse Encode time: 0.000036
+ [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.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000083
+ [java] Elapse Encode time: 0.000037
+ [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.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000088
+ [java] Elapse Encode time: 0.000037
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000053
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000098
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6a66ec0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6a66f60....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6a67040....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4a3ad900....
+ [java] Encoding Graph Time: 0.000099
+ [java] Elapse Encode time: 0.000136
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064225
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064367
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT afteisSat= true ,SatuneSat= true
+ [java] 1594752905392Satune Solving Time: 0.088342
+ [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] 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] 1594752905647 Original Encoding Solving Time: 0.034934
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752905647Satune Solving Time: 0.089358
+ [java] 1594752905897 Original Encoding Solving Time: 0.039231
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752905897Satune Solving Time: 0.101636
+ [java] Path Solving Time: 16.007671
+ [java] Path Solving Time: 4.443486
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752905978 Original Encoding Solving Time: 0.345876
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752905978Satune Solving Time: 65.21418
+ [java] 1594752906055 Original Encoding Solving Time: 0.043087
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906055Satune Solving Time: 0.09403
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752906352 Original Encoding Solving Time: 0.047726
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906352Satune Solving Time: 0.084873
+ [java] 1594752906362 Original Encoding Solving Time: 0.029783
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906362Satune Solving Time: 0.086616
+ [java] 1594752906371 Original Encoding Solving Time: 0.036963
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752906371Satune Solving Time: 0.098464
+ [java] Path Solving Time: 13.825833
+ [java] Path Solving Time: 3.74696
+ [java] 1594752906447 Original Encoding Solving Time: 0.290461
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906447Satune Solving Time: 66.159821
+ [java] 1594752906525 Original Encoding Solving Time: 0.041704
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906525Satune Solving Time: 0.081829
+ [java] 1594752906535 Original Encoding Solving Time: 0.048463
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906535Satune Solving Time: 0.086533
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752906546 Original Encoding Solving Time: 0.030678
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906546Satune Solving Time: 0.090934
+ [java] 1594752906559 Original Encoding Solving Time: 0.046252
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752906559Satune Solving Time: 0.112716
+ [java] Path Solving Time: 16.288832
+ [java] Path Solving Time: 4.12665
+ [java] 1594752906641 Original Encoding Solving Time: 0.28806
+ [java] r encoding: 0
+ [java] #Clauses = 18 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Elapse Encode time: 0.000036
+ [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: SAT
+ [java] CSOLVER solve time: 0.000085
+ [java] Elapse Encode time: 0.000035
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000054
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000097
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000117
+ [java] Elapse Encode time: 0.000151
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065200
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000048
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000090
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Elapse Encode time: 0.000035
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000082
+ [java] Elapse Encode time: 0.000035
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 21 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000051
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000094
+ [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 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000085
+ [java] Elapse Encode time: 0.000113
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.066030
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066149
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000082
+ [java] Elapse Encode time: 0.000035
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000087
+ [java] Elapse Encode time: 0.000040
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 21 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000058
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000108
+ [java] Polarity time: 0.000005
+ [java] Preprocess tisSat= true ,SatuneSat= true
+ [java] 1594752906641Satune Solving Time: 64.234366
+ [java] 1594752906716 Original Encoding Solving Time: 0.043428
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906716Satune Solving Time: 0.088575
+ [java] 1594752906724 Original Encoding Solving Time: 0.049315
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906724Satune Solving Time: 0.091092
+ [java] 1594752906733 Original Encoding Solving Time: 0.031005
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906733Satune Solving Time: 0.090418
+ [java] 1594752906742 Original Encoding Solving Time: 0.038217
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752906742Satune Solving Time: 0.104424
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 26.714949
+ [java] Path Solving Time: 4.306001
+ [java] 1594752906832 Original Encoding Solving Time: 0.384648
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906832Satune Solving Time: 63.930453
+ [java] 1594752906913 Original Encoding Solving Time: 0.040127
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752906913Satune Solving Time: 0.071617
+ [java] 1594752906929 Original Encoding Solving Time: 0.019402
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752906929Satune Solving Time: 0.075416
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 191.22635
+ [java] Path Solving Time: 37.117313
+ [java] Path Solving Time: 17.717087
+ [java] Path Solving Time: 4.102305
+ [java] 1594752907238 Original Encoding Solving Time: 0.351281
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907238Satune Solving Time: 66.564926
+ [java] 1594752907317 Original Encoding Solving Time: 0.05086
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907317Satune Solving Time: 0.076066
+ [java] 1594752907328 Original Encoding Solving Time: 0.03774
+ [java] ime: 0.000008
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000077
+ [java] Elapse Encode time: 0.000106
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064108
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064222
+ [java] Elapse Encode time: 0.000033
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 19 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000086
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 20 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000086
+ [java] Elapse Encode time: 0.000035
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 21 #Vars = 12
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000056
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000100
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000126
+ [java] Elapse Encode time: 0.000167
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.063744
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.063917
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000033
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000068
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000035
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000071
+ [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 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000076
+ [java] Elapse Encode time: 0.000106
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.066443
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.066555
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000034
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000071
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving timisSat= false ,SatuneSat= false
+ [java] 1594752907328Satune Solving Time: 0.08297
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 30.615242
+ [java] Path Solving Time: 14.277833
+ [java] Path Solving Time: 4.058385
+ [java] 1594752907436 Original Encoding Solving Time: 0.291309
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907436Satune Solving Time: 64.911484
+ [java] 1594752907512 Original Encoding Solving Time: 0.040742
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907512Satune Solving Time: 0.077697
+ [java] 1594752907523 Original Encoding Solving Time: 0.025286
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752907523Satune Solving Time: 0.084125
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 24.012514
+ [java] Path Solving Time: 16.656172
+ [java] Path Solving Time: 5.007129
+ [java] 1594752907628 Original Encoding Solving Time: 0.374537
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907628Satune Solving Time: 64.073489
+ [java] 1594752907702 Original Encoding Solving Time: 0.039377
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907702Satune Solving Time: 0.072754
+ [java] 1594752907711 Original Encoding Solving Time: 0.021155
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752907711Satune Solving Time: 0.078034
+ [java] Path Solving Time: 20.636446
+ [java] Path Solving Time: 11.272496
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 4.171525
+ [java] 1594752907806 Original Encoding Solving Time: 0.782474
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907806Satune Solving Time: 63.986411
+ [java] 1594752907879 Original Encoding Solving Time: 0.038731
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752907879Satune Solving Time: 0.084125
+ [java] 1594752907888 Original Encoding Solving Time: 0.019438
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752907888Satune Solving Time: 0.085823
+ [java] Path Solving Time: 20.675309
+ [java] Path Solving Time: 11.79476
+ [java] Path Solving Time: 4.116652
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752907983 Original Encoding Solving Time: 0.258289
+ [java] e: 0.000039
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [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 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000084
+ [java] Elapse Encode time: 0.000115
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064780
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064901
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000080
+ [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 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000101
+ [java] Elapse Encode time: 0.000125
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.063930
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064061
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000033
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000068
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000075
+ [java] Elapse Encode time: 0.000102
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.063868
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.063976
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000080
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000045
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000082
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making theisSat= true ,SatuneSat= true
+ [java] 1594752907983Satune Solving Time: 65.44841
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752908060 Original Encoding Solving Time: 0.038187
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908060Satune Solving Time: 0.078213
+ [java] 1594752908070 Original Encoding Solving Time: 0.018714
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908070Satune Solving Time: 0.079896
+ [java] Path Solving Time: 19.792718
+ [java] Path Solving Time: 4.146071
+ [java] 1594752908153 Original Encoding Solving Time: 0.673861
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908153Satune Solving Time: 64.68448
+ [java] 1594752908229 Original Encoding Solving Time: 0.041052
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908229Satune Solving Time: 0.076345
+ [java] 1594752908240 Original Encoding Solving Time: 0.019737
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908240Satune Solving Time: 0.077074
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 20.434556
+ [java] Path Solving Time: 4.118545
+ [java] 1594752908322 Original Encoding Solving Time: 0.265084
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908322Satune Solving Time: 64.371403
+ [java] 1594752908398 Original Encoding Solving Time: 0.047447
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908398Satune Solving Time: 0.085066
+ [java] 1594752908408 Original Encoding Solving Time: 0.019622
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908408Satune Solving Time: 0.081785
+ [java] Path Solving Time: 17.503301
+ [java] Path Solving Time: 4.085275
+ [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] 1594752908488 Original Encoding Solving Time: 0.354999
+ [java] decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000065
+ [java] Elapse Encode time: 0.000093
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065335
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065436
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000075
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000007
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000087
+ [java] Elapse Encode time: 0.000115
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064553
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064673
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000036
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000036
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000073
+ [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 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000098
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064257
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064360
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000042
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000105
+ [java] Elapse Encode time: 0.000141
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Is problemisSat= true ,SatuneSat= true
+ [java] 1594752908488Satune Solving Time: 68.75567
+ [java] 1594752908569 Original Encoding Solving Time: 0.044689
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908569Satune Solving Time: 0.085031
+ [java] 1594752908580 Original Encoding Solving Time: 0.019823
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908580Satune Solving Time: 0.075927
+ [java] Path Solving Time: 17.704169
+ [java] Path Solving Time: 4.11147
+ [java] 1594752908660 Original Encoding Solving Time: 0.244409
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908660Satune Solving Time: 64.448114
+ [java] 1594752908735 Original Encoding Solving Time: 0.03903
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908735Satune Solving Time: 0.07516
+ [java] 1594752908745 Original Encoding Solving Time: 0.019784
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908745Satune Solving Time: 0.077885
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 17.578736
+ [java] Path Solving Time: 4.122182
+ [java] 1594752908826 Original Encoding Solving Time: 0.240503
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908826Satune Solving Time: 64.878148
+ [java] 1594752908902 Original Encoding Solving Time: 0.039623
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752908902Satune Solving Time: 0.078403
+ [java] 1594752908912 Original Encoding Solving Time: 0.019794
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752908912Satune Solving Time: 0.091766
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 80.953132
+ [java] Path Solving Time: 24.202762
+ [java] Path Solving Time: 20.340993
+ [java] Path Solving Time: 4.095882
+ [java] 1594752909101 Original Encoding Solving Time: 0.29705
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909101Satune Solving Time: 64.26245
+ [java] 1594752909185 Original Encoding Solving Time: 0.041783
+ [java] UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.068592
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.068743
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000080
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000035
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000071
+ [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 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000064
+ [java] Elapse Encode time: 0.000095
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064338
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064438
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000035
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000071
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000110
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064752
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064868
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Elapse Encode time: 0.000036
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000087
+ [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 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000075
+ [java] Elapse Encode time: 0.000106
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064140
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064252
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving isSat= true ,SatuneSat= true
+ [java] 1594752909185Satune Solving Time: 0.076297
+ [java] 1594752909202 Original Encoding Solving Time: 0.020877
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752909202Satune Solving Time: 0.080417
+ [java] Path Solving Time: 22.44596
+ [java] Path Solving Time: 4.46432
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752909292 Original Encoding Solving Time: 0.412465
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909292Satune Solving Time: 65.468328
+ [java] 1594752909377 Original Encoding Solving Time: 0.041583
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909377Satune Solving Time: 0.079834
+ [java] 1594752909395 Original Encoding Solving Time: 0.017826
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752909395Satune Solving Time: 0.085599
+ [java] Path Solving Time: 20.935055
+ [java] Path Solving Time: 4.398806
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752909482 Original Encoding Solving Time: 0.404985
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909482Satune Solving Time: 65.241588
+ [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] 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] 1594752909570 Original Encoding Solving Time: 0.060976
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909570Satune Solving Time: 0.158639
+ [java] 1594752909588 Original Encoding Solving Time: 0.019738
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752909588Satune Solving Time: 0.075456
+ [java] Path Solving Time: 18.013956
+ [java] Path Solving Time: 4.505059
+ [java] 1594752909670 Original Encoding Solving Time: 0.320172
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909670Satune Solving Time: 65.375002
+ [java] 1594752909756 Original Encoding Solving Time: 0.041599
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909756Satune Solving Time: 0.081595
+ [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] 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] 1594752909775 Original Encoding Solving Time: 0.017021
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752909775Satune Solving Time: 0.085541
+ [java] Path Solving Time: 20.728622
+ [java] Path Solving Time: 4.845309
+ [java] 1594752909860 Original Encoding Solving Time: 0.338495
+ [java] time: 0.000033
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000072
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000076
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000023
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000119
+ [java] Elapse Encode time: 0.000166
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065284
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065456
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000075
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000007
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46c70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46fd0....
+ [java] Encoding Graph Time: 0.000123
+ [java] Elapse Encode time: 0.000176
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065223
+ [java] Elapse Encode time: 0.000040
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000100
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000151
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000033
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000071
+ [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 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd45addb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6c244f0....
+ [java] Encoding Graph Time: 0.000100
+ [java] Elapse Encode time: 0.000139
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065217
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065362
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Polarity time: 0.000010
+ [java] PreprisSat= true ,SatuneSat= true
+ [java] 1594752909860Satune Solving Time: 65.19918
+ [java] 1594752909940 Original Encoding Solving Time: 0.042784
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752909940Satune Solving Time: 0.077639
+ [java] 1594752909953 Original Encoding Solving Time: 0.017161
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752909953Satune Solving Time: 0.080754
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 18.565659
+ [java] Path Solving Time: 4.159981
+ [java] 1594752910035 Original Encoding Solving Time: 0.253021
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910035Satune Solving Time: 65.089571
+ [java] 1594752910114 Original Encoding Solving Time: 0.038096
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910114Satune Solving Time: 0.10338
+ [java] 1594752910127 Original Encoding Solving Time: 0.0165
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752910127Satune Solving Time: 0.083066
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 71.603909
+ [java] Path Solving Time: 19.508667
+ [java] Path Solving Time: 4.048598
+ [java] 1594752910281 Original Encoding Solving Time: 0.302786
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910281Satune Solving Time: 64.46582
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752910364 Original Encoding Solving Time: 0.035779
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910364Satune Solving Time: 0.07327
+ [java] 1594752910380 Original Encoding Solving Time: 0.017363
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752910380Satune Solving Time: 0.078966
+ [java] Path Solving Time: 22.027314
+ [java] Path Solving Time: 4.076138
+ [java] 1594752910465 Original Encoding Solving Time: 0.271308
+ [java] ocess time: 0.000015
+ [java] Decompose Order: 0.000015
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46bf0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c4ab46b70....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6c5dbb0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6c65740....
+ [java] Encoding Graph Time: 0.000155
+ [java] Elapse Encode time: 0.000221
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064958
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065187
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000036
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000076
+ [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 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd659c6e0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd659c620....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd659c7c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd659cba0....
+ [java] Encoding Graph Time: 0.000088
+ [java] Elapse Encode time: 0.000116
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064958
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065079
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000060
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000099
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598b60....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598aa0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616950....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616d30....
+ [java] Encoding Graph Time: 0.000086
+ [java] Elapse Encode time: 0.000116
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.064334
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.064456
+ [java] Elapse Encode time: 0.000025
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000035
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000069
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000074
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616d30....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616950....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598aa0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598isSat= true ,SatuneSat= true
+ [java] 1594752910465Satune Solving Time: 65.788181
+ [java] 1594752910549 Original Encoding Solving Time: 0.06015
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910549Satune Solving Time: 0.138472
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752910570 Original Encoding Solving Time: 0.019303
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752910570Satune Solving Time: 0.09633
+ [java] Path Solving Time: 34.756504
+ [java] Path Solving Time: 4.090614
+ [java] 1594752910668 Original Encoding Solving Time: 0.375904
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752910668Satune Solving Time: 63.893515
+ [java] =========Statistics (time in milliseconds)=========
+ [java] Benchmark Id: 7
+ [java] Sketch Generation Time: 3550.527342000001
+ [java] Sketch Completion Time: 6686.460789999999
+ [java] Compilation Time: 1340.606511
+ [java] Running Test cases Time: 2915.7220029999985
+ [java] Synthesis Time: 13152.710135
+ [java] Total Time: 14493.316646
+ [java] Number of components: 4
+ [java] Number of holes: 6
+ [java] Number of completed programs: 172
+ [java] Number of sketches: 52
+ [java] Solution:
+ [java] double[] sypet_var296 = sypet_arg1.toArray();
+ [java] org.apache.commons.math.linear.RealVector sypet_var297 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.wrap(sypet_arg0);
+ [java] org.apache.commons.math.linear.RealMatrix sypet_var298 = sypet_var297.outerProduct(sypet_var296);
+ [java] com.opengamma.analytics.math.matrix.DoubleMatrix2D sypet_var299 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.unwrap(sypet_var298);
+ [java] return sypet_var299;
+ [java]
+ [java] ============================
+ [java] b60....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] Encoding Graph Time: 0.000108
+ [java] Elapse Encode time: 0.000142
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.065630
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.065778
+ [java] Elapse Encode time: 0.000039
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000076
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000132
+ [java] Elapse Encode time: 0.000031
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000090
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f7c483b1530....
+ [java] INFO: naive encoder is making the decision about element 0x7f7c482474c0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598b60....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6598aa0....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616950....
+ [java] INFO: naive encoder is making the decision about element 0x7f7bd6616d30....
+ [java] Encoding Graph Time: 0.000184
+ [java] Elapse Encode time: 0.000233
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.063641
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.063881
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+
+BUILD SUCCESSFUL
+Total time: 48 seconds
projects / Benchmarks_CSolver.git / blobdiff