Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_50_pb.cnf.cr.opb |
MD5SUM | 2cb05b3a6451c60276a625949666f14e |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 51 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.12498 |
Number of variables | 4000 |
Total number of constraints | 180 |
Number of constraints which are clauses | 100 |
Number of constraints which are cardinality constraints (but not clauses) | 80 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 50 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc32 THE 2005-04-13 20:22:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=167 boxname=wulflinc32 idbench=19 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 2cb05b3a6451c60276a625949666f14e /oldhome/oroussel/tmp/wulflinc32/normalized-chnl40_50_pb.cnf.cr.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc32/normalized-chnl40_50_pb.cnf.cr.opb IDLAUNCH: 167 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034724 kB MemFree: 753508 kB Buffers: 33772 kB Cached: 135968 kB SwapCached: 1212 kB Active: 138688 kB Inactive: 111420 kB HighTotal: 131072 kB HighFree: 256 kB LowTotal: 903652 kB LowFree: 753252 kB SwapTotal: 2097892 kB SwapFree: 2096680 kB Dirty: 2244 kB Writeback: 0 kB Mapped: 81768 kB Slab: 25064 kB Committed_AS: 174000 kB PageTables: 432 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 20:37:09 (client local time) WITH STATUS 0 IN 906.996 SECONDS stats: 167 7 906.996 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 180 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................... c ---[ 79]---> BDD-cost: 97 c ---[ 78]---> BDD-cost: 97 c ---[ 77]---> BDD-cost: 97 c ---[ 76]---> BDD-cost: 97 c ---[ 75]---> BDD-cost: 97 c ---[ 74]---> BDD-cost: 97 c ---[ 73]---> BDD-cost: 97 c ---[ 72]---> BDD-cost: 97 c ---[ 71]---> BDD-cost: 97 c ---[ 70]---> BDD-cost: 97 c ---[ 69]---> BDD-cost: 97 c ---[ 68]---> BDD-cost: 97 c ---[ 67]---> BDD-cost: 97 c ---[ 66]---> BDD-cost: 97 c ---[ 65]---> BDD-cost: 97 c ---[ 64]---> BDD-cost: 97 c ---[ 63]---> BDD-cost: 97 c ---[ 62]---> BDD-cost: 97 c ---[ 61]---> BDD-cost: 97 c ---[ 60]---> BDD-cost: 97 c ---[ 59]---> BDD-cost: 97 c ---[ 58]---> BDD-cost: 97 c ---[ 57]---> BDD-cost: 97 c ---[ 56]---> BDD-cost: 97 c ---[ 55]---> BDD-cost: 97 c ---[ 54]---> BDD-cost: 97 c ---[ 53]---> BDD-cost: 97 c ---[ 52]---> BDD-cost: 97 c ---[ 51]---> BDD-cost: 97 c ---[ 50]---> BDD-cost: 97 c ---[ 49]---> BDD-cost: 97 c ---[ 48]---> BDD-cost: 97 c ---[ 47]---> BDD-cost: 97 c ---[ 46]---> BDD-cost: 97 c ---[ 45]---> BDD-cost: 97 c ---[ 44]---> BDD-cost: 97 c ---[ 43]---> BDD-cost: 97 c ---[ 42]---> BDD-cost: 97 c ---[ 41]---> BDD-cost: 97 c ---[ 40]---> BDD-cost: 97 c ---[ 39]---> BDD-cost: 97 c ---[ 38]---> BDD-cost: 97 c ---[ 37]---> BDD-cost: 97 c ---[ 36]---> BDD-cost: 97 c ---[ 35]---> BDD-cost: 97 c ---[ 34]---> BDD-cost: 97 c ---[ 33]---> BDD-cost: 97 c ---[ 32]---> BDD-cost: 97 c ---[ 31]---> BDD-cost: 97 c ---[ 30]---> BDD-cost: 97 c ---[ 29]---> BDD-cost: 97 c ---[ 28]---> BDD-cost: 97 c ---[ 27]---> BDD-cost: 97 c ---[ 26]---> BDD-cost: 97 c ---[ 25]---> BDD-cost: 97 c ---[ 24]---> BDD-cost: 97 c ---[ 23]---> BDD-cost: 97 c ---[ 22]---> BDD-cost: 97 c ---[ 21]---> BDD-cost: 97 c ---[ 20]---> BDD-cost: 97 c ---[ 19]---> BDD-cost: 97 c ---[ 18]---> BDD-cost: 97 c ---[ 17]---> BDD-cost: 97 c ---[ 16]---> BDD-cost: 97 c ---[ 15]---> BDD-cost: 97 c ---[ 14]---> BDD-cost: 97 c ---[ 13]---> BDD-cost: 97 c ---[ 12]---> BDD-cost: 97 c ---[ 11]---> BDD-cost: 97 c ---[ 10]---> BDD-cost: 97 c ---[ 9]---> BDD-cost: 97 c ---[ 8]---> BDD-cost: 97 c ---[ 7]---> BDD-cost: 97 c ---[ 6]---> BDD-cost: 97 c ---[ 5]---> BDD-cost: 97 c ---[ 4]---> BDD-cost: 97 c ---[ 3]---> BDD-cost: 97 c ---[ 2]---> BDD-cost: 97 c ---[ 1]---> BDD-cost: 97 c ---[ 0]---> BDD-cost: 97 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19380 54160 | 6460 0 0 nan | 0.000 % | c | 103 | 19380 54160 | 7106 103 15224 147.8 | 0.680 % | c | 264 | 19380 54160 | 7816 264 48573 184.0 | 0.680 % | c | 491 | 19380 54160 | 8598 491 85624 174.4 | 0.680 % | c | 828 | 19380 54160 | 9458 828 154823 187.0 | 0.680 % | c | 1334 | 19380 54160 | 10403 1334 306589 229.8 | 0.680 % | c | 2093 | 19380 54160 | 11444 2093 485053 231.8 | 0.680 % | c | 3234 | 19380 54160 | 12588 3234 825279 255.2 | 0.680 % | c | 4943 | 19380 54160 | 13847 4943 1417289 286.7 | 0.680 % | c | 7505 | 19380 54160 | 15232 7505 2438701 324.9 | 0.680 % | c | 11349 | 19380 54160 | 16755 11349 3669460 323.3 | 0.680 % | c | 17115 | 19380 54160 | 18431 17115 6183322 361.3 | 0.680 % | c | 25765 | 19380 54160 | 20274 14106 6524975 462.6 | 0.680 % | c | 38745 | 19380 54160 | 22301 13797 6591558 477.8 | 0.680 % | c | 58212 | 19380 54160 | 24531 17990 8193323 455.4 | 0.680 % | c | 87406 | 19380 54160 | 26985 14543 4843174 333.0 | 0.680 % | c | 131196 | 19380 54160 | 29683 19996 12157179 608.0 | 0.680 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.97 0.90 2/53 11032 Raw data (stat): 11032 (runsolver) R 11031 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478789046 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0017 s] Raw data (loadavg): 0.93 0.97 0.90 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 3202 0 0 0 992 6 0 0 25 0 1 0 478789046 14917632 3180 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3642 3181 603 41 0 3601 0 vsize: 14568 [startup+20.0027 s] Raw data (loadavg): 0.94 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 5015 0 0 0 1988 10 0 0 25 0 1 0 478789046 22351872 4993 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5457 4993 603 41 0 5416 0 vsize: 21828 [startup+30.0034 s] Raw data (loadavg): 0.95 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 6431 0 0 0 2985 13 0 0 25 0 1 0 478789046 28135424 6409 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6869 6409 603 41 0 6828 0 vsize: 27476 [startup+40.004 s] Raw data (loadavg): 0.95 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 7400 0 0 0 3982 16 0 0 25 0 1 0 478789046 32141312 7378 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7847 7378 603 41 0 7806 0 vsize: 31388 [startup+50.0049 s] Raw data (loadavg): 0.96 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 8981 0 0 0 4979 19 0 0 25 0 1 0 478789046 38612992 8959 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9427 8959 603 41 0 9386 0 vsize: 37708 [startup+60.0067 s] Raw data (loadavg): 0.97 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 10221 0 0 0 5976 22 0 0 25 0 1 0 478789046 43741184 10199 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10679 10199 603 41 0 10638 0 vsize: 42716 [startup+70.0072 s] Raw data (loadavg): 0.97 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 10689 0 0 0 6975 24 0 0 25 0 1 0 478789046 45629440 10667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11140 10667 603 41 0 11099 0 vsize: 44560 [startup+80.0082 s] Raw data (loadavg): 0.98 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 10689 0 0 0 7975 24 0 0 25 0 1 0 478789046 45629440 10667 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11140 10667 603 41 0 11099 0 vsize: 44560 [startup+90.0088 s] Raw data (loadavg): 0.98 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 10689 0 0 0 8975 24 0 0 25 0 1 0 478789046 45629440 10667 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11140 10667 603 41 0 11099 0 vsize: 44560 [startup+100.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 11926 0 0 0 9972 27 0 0 25 0 1 0 478789046 50753536 11904 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12391 11904 603 41 0 12350 0 vsize: 49564 [startup+110.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 12977 0 0 0 10970 30 0 0 25 0 1 0 478789046 55074816 12955 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13446 12955 603 41 0 13405 0 vsize: 53784 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 12977 0 0 0 11970 30 0 0 25 0 1 0 478789046 55074816 12955 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13446 12955 603 41 0 13405 0 vsize: 53784 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 12977 0 0 0 12970 30 0 0 25 0 1 0 478789046 55074816 12955 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13446 12955 603 41 0 13405 0 vsize: 53784 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 12977 0 0 0 13970 30 0 0 25 0 1 0 478789046 55074816 12955 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13446 12955 603 41 0 13405 0 vsize: 53784 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 12977 0 0 0 14971 30 0 0 25 0 1 0 478789046 55074816 12955 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13446 12955 603 41 0 13405 0 vsize: 53784 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 13187 0 0 0 15970 30 0 0 25 0 1 0 478789046 55885824 13165 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13644 13165 603 41 0 13603 0 vsize: 54576 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 13912 0 0 0 16969 32 0 0 25 0 1 0 478789046 58863616 13890 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14371 13890 603 41 0 14330 0 vsize: 57484 [startup+180.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14769 0 0 0 17966 35 0 0 25 0 1 0 478789046 62373888 14747 4294967295 134512640 134672761 3221224624 3221222048 134565762 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14747 603 41 0 15187 0 vsize: 60912 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14771 0 0 0 18966 35 0 0 25 0 1 0 478789046 62373888 14749 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14749 603 41 0 15187 0 vsize: 60912 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14771 0 0 0 19966 35 0 0 25 0 1 0 478789046 62373888 14749 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14749 603 41 0 15187 0 vsize: 60912 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14771 0 0 0 20966 35 0 0 25 0 1 0 478789046 62373888 14749 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14749 603 41 0 15187 0 vsize: 60912 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14771 0 0 0 21966 35 0 0 25 0 1 0 478789046 62373888 14749 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14749 603 41 0 15187 0 vsize: 60912 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14771 0 0 0 22966 35 0 0 25 0 1 0 478789046 62373888 14749 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14749 603 41 0 15187 0 vsize: 60912 [startup+240.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14772 0 0 0 23967 35 0 0 25 0 1 0 478789046 62373888 14750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15228 14750 603 41 0 15187 0 vsize: 60912 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 24967 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 25967 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+270.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 26967 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 27968 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 28968 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 29968 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+310.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 30968 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 31969 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 32969 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+340.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 33969 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+350.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 34969 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 35969 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+370.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 36970 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+380.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 37970 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223760 134560622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+390.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 38970 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 39970 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 40971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 41971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 42971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223808 134559583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+440.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 43971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+450.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 44971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+460.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 45971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223728 134559974 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14773 0 0 0 46971 35 0 0 25 0 1 0 478789046 62369792 14751 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15227 14751 603 41 0 15186 0 vsize: 60908 [startup+480.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 14877 0 0 0 47971 36 0 0 25 0 1 0 478789046 62775296 14855 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15326 14855 603 41 0 15285 0 vsize: 61304 [startup+490.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 48970 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+500.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 49970 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+510.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 50970 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+520.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 51970 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+530.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 52971 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+540.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 53971 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+550.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 54971 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+560.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 55971 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+570.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15601 0 0 0 56972 38 0 0 25 0 1 0 478789046 65777664 15579 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15579 603 41 0 16018 0 vsize: 64236 [startup+580.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 15609 0 0 0 57972 38 0 0 25 0 1 0 478789046 65777664 15587 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16059 15587 603 41 0 16018 0 vsize: 64236 [startup+590.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 16340 0 0 0 58970 40 0 0 25 0 1 0 478789046 68816896 16318 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16801 16318 603 41 0 16760 0 vsize: 67204 [startup+600.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 16979 0 0 0 59969 41 0 0 25 0 1 0 478789046 71507968 16957 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17458 16957 603 41 0 17417 0 vsize: 69832 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 17627 0 0 0 60968 43 0 0 25 0 1 0 478789046 74207232 17605 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18117 17605 603 41 0 18076 0 vsize: 72468 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 18497 0 0 0 61967 44 0 0 25 0 1 0 478789046 77721600 18475 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18975 18475 603 41 0 18934 0 vsize: 75900 [startup+630.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 19319 0 0 0 62965 46 0 0 25 0 1 0 478789046 81104896 19297 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19801 19297 603 41 0 19760 0 vsize: 79204 [startup+640.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 19685 0 0 0 63964 47 0 0 25 0 1 0 478789046 82620416 19663 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20171 19663 603 41 0 20130 0 vsize: 80684 [startup+650.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 20154 0 0 0 64963 48 0 0 25 0 1 0 478789046 84643840 20132 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20665 20132 603 41 0 20624 0 vsize: 82660 [startup+660.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 20652 0 0 0 65962 49 0 0 25 0 1 0 478789046 86622208 20630 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21148 20630 603 41 0 21107 0 vsize: 84592 [startup+670.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21241 0 0 0 66961 51 0 0 25 0 1 0 478789046 89071616 21219 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21746 21219 603 41 0 21705 0 vsize: 86984 [startup+680.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 67961 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223808 134558890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+690.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 68961 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+700.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 69962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 70962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 71962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+730.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 72962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+740.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 73962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+750.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 74962 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21256 0 0 0 75961 51 0 0 25 0 1 0 478789046 89206784 21234 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21779 21234 603 41 0 21738 0 vsize: 87116 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21289 0 0 0 76961 51 0 0 25 0 1 0 478789046 89468928 21267 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21843 21267 603 41 0 21802 0 vsize: 87372 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21291 0 0 0 77962 51 0 0 25 0 1 0 478789046 89468928 21269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21843 21269 603 41 0 21802 0 vsize: 87372 [startup+790.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 78961 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223808 134558497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 79962 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+810.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 80962 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+820.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 81962 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 82962 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 83963 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+850.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 84963 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+860.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 85963 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 86963 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+880.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 87964 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+890.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 88964 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 89964 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 88428 [startup+906.901 s] Raw data (loadavg): 0.99 0.97 0.91 1/52 11032 Raw data (stat): 11032 (minisat+) R 11031 7987 7986 0 -1 0 21573 0 0 0 89964 52 0 0 25 0 1 0 478789046 90550272 21551 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22107 21551 603 41 0 22066 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 906.9 CPU time (s): 906.996 CPU user time (s): 906.432 CPU system time (s): 0.563914 CPU usage (%): 100.011 Max. virtual memory (Kb): 88428 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####