PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air01.opb
MD5SUM	90db1995bd949fc5ac74143a523f3bcf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3398
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	3698
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	1192753
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3698
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	1192753
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03384
Number of variables	771
Total number of constraints	794
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	438
Trace number 22539

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-22 03:19:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11614 boxname=wulflinc1 idbench=894 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-air01.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-air01.opb
IDLAUNCH: 11614
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:      1034660 kB
MemFree:        503800 kB
Buffers:          5752 kB
Cached:         500304 kB
SwapCached:          0 kB
Active:          90676 kB
Inactive:       418584 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        503548 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            15740 kB
Committed_AS:    92816 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:39:17 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 11614 7 1200.35 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> BDD-cost:   49
c ---[  42]---> BDD-cost:   39
c ---[  40]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   61
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  139
c ---[  26]---> BDD-cost:  197
c ---[  24]---> BDD-cost:  233
c ---[  22]---> BDD-cost:  273
c ---[  20]---> BDD-cost:  353
c ---[  18]---> BDD-cost:  331
c ---[  16]---> BDD-cost:  527
c ---[  14]---> BDD-cost:  589
c ---[  12]---> BDD-cost:  607
c ---[  10]---> BDD-cost:  559
c ---[   8]---> BDD-cost:  755
c ---[   6]---> BDD-cost:  769
c ---[   4]---> BDD-cost:  741
c ---[   2]---> BDD-cost:  781
c ---[   0]---> BDD-cost:  873
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20564    53488 |    6854       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 9600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7920   maxlim: 1183153   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        26 |   75865   251014 |   25288      26     1591    61.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 8437[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1184316   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75889   251167 |   25296      43     2039    47.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 8097[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1184656   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75893   251220 |   25297      43     2039    47.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 7212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185541   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   75898   251280 |   25299      43     2039    47.4 |  0.000 % |
c |       144 |   75898   251280 |   27828     144    12635    87.7 |  0.325 % |
c |       299 |   75898   251280 |   30611     299    56525   189.0 |  0.325 % |
c ==============================================================================
c [1mFound solution: 7192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185561   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       380 |   75902   251328 |   25300     380    64997   171.0 |  0.325 % |
c |       482 |   75902   251328 |   27830     482    73689   152.9 |  0.342 % |
c ==============================================================================
c [1mFound solution: 6795[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185958   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       500 |   75913   251422 |   25304     500    75462   150.9 |  0.342 % |
c |       602 |   75911   251416 |   27834     589   101508   172.3 |  0.383 % |
c ==============================================================================
c [1mFound solution: 6136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186617   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       627 |   75922   251503 |   25307     614   102021   166.2 |  0.383 % |
c ==============================================================================
c [1mFound solution: 5674[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1187079   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       636 |   75926   251538 |   25308     623   104929   168.4 |  0.383 % |
c ==============================================================================
c [1mFound solution: 5268[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1187485   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       707 |   75935   251625 |   25311     694   148809   214.4 |  0.383 % |
c |       807 |   75935   251625 |   27842     794   164116   206.7 |  0.471 % |
c |       959 |   75935   251625 |   30626     946   216548   228.9 |  0.471 % |
c ==============================================================================
c [1mFound solution: 4967[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1187786   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1024 |   75947   251722 |   25315    1011   227278   224.8 |  0.471 % |
c |      1126 |   75849   251378 |   27846    1082   230798   213.3 |  0.618 % |
c |      1276 |   75849   251378 |   30631    1232   255783   207.6 |  0.618 % |
c |      1503 |   75849   251378 |   33694    1459   341321   233.9 |  0.618 % |
c |      1843 |   75849   251378 |   37063    1799   484561   269.4 |  0.618 % |
c |      2351 |   75849   251378 |   40770    2307   614206   266.2 |  0.618 % |
c ==============================================================================
c [1mFound solution: 4424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1188329   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2373 |   75863   251475 |   25287    2329   622610   267.3 |  0.618 % |
c |      2473 |   75863   251475 |   27815    2429   647783   266.7 |  0.659 % |
c ==============================================================================
c [1mFound solution: 4031[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1188722   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2502 |   75874   251568 |   25291    2458   651822   265.2 |  0.659 % |
c |      2604 |   75874   251568 |   27820    2560   693972   271.1 |  0.700 % |
c |      2758 |   75874   251568 |   30602    2714   760000   280.0 |  0.700 % |
c |      2983 |   75858   251516 |   33662    2937   780081   265.6 |  0.717 % |
c |      3320 |   75778   251253 |   37028    3270   839332   256.7 |  0.747 % |
c |      3828 |   75778   251253 |   40731    3778   917899   243.0 |  0.747 % |
c |      4588 |   75778   251253 |   44804    4538  1017540   224.2 |  0.747 % |
c |      5740 |   75778   251253 |   49285    5690  1245667   218.9 |  0.747 % |
c |      7450 |   75740   251123 |   54213    7391  1736031   234.9 |  0.752 % |
c |     10012 |   75732   251093 |   59634    9950  2505022   251.8 |  0.788 % |
c |     13858 |   75641   250272 |   65598   13790  3638851   263.9 |  0.805 % |
c |     19627 |   75497   249754 |   72158   19517  5744723   294.3 |  0.946 % |
c |     28277 |   75249   248858 |   79373   28087  8142276   289.9 |  1.193 % |
c |     41260 |   74584   246540 |   87311   40517 12845986   317.1 |  1.834 % |
c ==============================================================================
c [1mFound solution: 4028[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5870   maxlim: 1181265   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41313 |  115415   392358 |   38471   40551 12854302   317.0 |  1.834 % |
c |     41413 |  115315   392026 |   42318   14973  4495990   300.3 |  1.573 % |
c |     41564 |  115315   392026 |   46549   15124  4551965   301.0 |  1.573 % |
c |     41792 |  115228   391725 |   51204   15339  4602004   300.0 |  1.643 % |
c |     42129 |  115159   391482 |   56325   15665  4654142   297.1 |  1.695 % |
c |     42635 |  115159   391482 |   61957   16171  4847597   299.8 |  1.695 % |
c |     43394 |  115110   391319 |   68153   16923  5099834   301.4 |  1.735 % |
c |     44533 |  115110   391319 |   74969   18062  5440269   301.2 |  1.735 % |
c |     46242 |  114998   390919 |   82466   19703  5960565   302.5 |  1.813 % |
c |     48809 |  114805   390274 |   90712   22236  6719946   302.2 |  1.962 % |
c ==============================================================================
c [1mFound solution: 3964[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1181329   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49554 |  114811   390324 |   38270   22981  6981447   303.8 |  1.962 % |
c |     49654 |  114811   390324 |   42097   23081  6996626   303.1 |  1.975 % |
c |     49807 |  114811   390324 |   46306   23234  7021554   302.2 |  1.975 % |
c |     50034 |  114811   390324 |   50937   23461  7067586   301.2 |  1.975 % |
c |     50371 |  114804   390301 |   56031   23796  7121915   299.3 |  1.979 % |
c |     50881 |  114804   390301 |   61634   24306  7286853   299.8 |  1.979 % |
c |     51640 |  114804   390301 |   67797   25065  7605785   303.4 |  1.979 % |
c |     52779 |  114804   390301 |   74577   26204  7898848   301.4 |  1.979 % |
c ==============================================================================
c [1mFound solution: 3513[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4434   maxlim: 1178082   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52959 |  145575   500184 |   48525   26382  7970230   302.1 |  1.979 % |
c |     53059 |  145575   500184 |   53377   26482  8010334   302.5 |  1.745 % |
c |     53213 |  145575   500184 |   58715   26636  8062283   302.7 |  1.745 % |
c |     53438 |  145575   500184 |   64586   26861  8163983   303.9 |  1.745 % |
c |     53776 |  145575   500184 |   71045   27199  8322697   306.0 |  1.745 % |
c |     54284 |  145575   500184 |   78149   27707  8492379   306.5 |  1.745 % |
c |     55043 |  145575   500184 |   85964   28466  8839787   310.5 |  1.745 % |
c |     56182 |  145559   500132 |   94561   29603  9240486   312.1 |  1.756 % |
c |     57890 |  145559   500132 |  104017   31311  9754725   311.5 |  1.756 % |
c |     60453 |  145559   500132 |  114419   33874 10762969   317.7 |  1.756 % |
c |     64297 |  145444   499735 |  125861   37706 12206060   323.7 |  1.807 % |
c |     70063 |  145444   499735 |  138447   43472 14511566   333.8 |  1.807 % |
c |     78713 |  145428   499683 |  152292   52119 17507350   335.9 |  1.818 % |
c |     91688 |  145301   499260 |  167521   65067 21564811   331.4 |  1.866 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bit#### 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.84 0.94 0.90 2/56 8999
Raw data (stat): 8999 (runsolver) R 8998 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 435350199 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 8999
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 6402 0 0 0 984 14 0 0 25 0 1 0 435350199 25440256 4918 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6211 4918 603 41 0 6170 0
vsize: 24844
[startup+20.001 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 8999
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 7532 0 0 0 1981 17 0 0 25 0 1 0 435350199 26218496 5079 4294967295 134512640 134672761 3221224624 3221223168 134597493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6401 5079 603 41 0 6360 0
vsize: 25604
[startup+30.0078 s]
Raw data (loadavg): 0.90 0.94 0.90 2/56 8999
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 7874 0 0 0 2980 18 0 0 25 0 1 0 435350199 27680768 5421 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6758 5421 603 41 0 6717 0
vsize: 27032
[startup+40.0077 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 8588 0 0 0 3978 20 0 0 25 0 1 0 435350199 28807168 5700 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7033 5700 603 41 0 6992 0
vsize: 28132
[startup+50.0094 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 8868 0 0 0 4977 21 0 0 25 0 1 0 435350199 30011392 5980 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7327 5980 603 41 0 7286 0
vsize: 29308
[startup+60.0188 s]
Raw data (loadavg): 0.94 0.95 0.90 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 9140 0 0 0 5976 22 0 0 25 0 1 0 435350199 31092736 6252 4294967295 134512640 134672761 3221224624 3221223624 1075349680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7591 6252 603 41 0 7550 0
vsize: 30364
[startup+70.024 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 9547 0 0 0 6975 23 0 0 25 0 1 0 435350199 32698368 6659 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7983 6659 603 41 0 7942 0
vsize: 31932
[startup+80.0388 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 9874 0 0 0 7975 24 0 0 25 0 1 0 435350199 34050048 6986 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8313 6986 603 41 0 8272 0
vsize: 33252
[startup+90.0386 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 10246 0 0 0 8975 25 0 0 25 0 1 0 435350199 35655680 7358 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8705 7358 603 41 0 8664 0
vsize: 34820
[startup+100.038 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 10587 0 0 0 9974 25 0 0 25 0 1 0 435350199 36978688 7699 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9028 7699 603 41 0 8987 0
vsize: 36112
[startup+110.054 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 10985 0 0 0 10975 27 0 0 25 0 1 0 435350199 38584320 8097 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9420 8097 603 41 0 9379 0
vsize: 37680
[startup+120.082 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 11317 0 0 0 11977 28 0 0 25 0 1 0 435350199 40054784 8429 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9779 8429 603 41 0 9738 0
vsize: 39116
[startup+130.082 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 11679 0 0 0 12975 29 0 0 25 0 1 0 435350199 41533440 8791 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10140 8791 603 41 0 10099 0
vsize: 40560
[startup+140.081 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 11994 0 0 0 13973 30 0 0 25 0 1 0 435350199 42721280 9106 4294967295 134512640 134672761 3221224624 3221223728 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10430 9106 603 41 0 10389 0
vsize: 41720
[startup+150.104 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 12332 0 0 0 14974 32 0 0 25 0 1 0 435350199 44179456 9444 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10786 9444 603 41 0 10745 0
vsize: 43144
[startup+160.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 12704 0 0 0 15974 32 0 0 25 0 1 0 435350199 45752320 9816 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11170 9816 603 41 0 11129 0
vsize: 44680
[startup+170.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 13145 0 0 0 16973 33 0 0 25 0 1 0 435350199 47472640 10257 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11590 10257 603 41 0 11549 0
vsize: 46360
[startup+180.108 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 13544 0 0 0 17972 35 0 0 25 0 1 0 435350199 49217536 10656 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12016 10656 603 41 0 11975 0
vsize: 48064
[startup+190.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 14031 0 0 0 18972 36 0 0 25 0 1 0 435350199 51195904 11143 4294967295 134512640 134672761 3221224624 3221223760 134565048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12499 11143 603 41 0 12458 0
vsize: 49996
[startup+200.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 14432 0 0 0 19971 37 0 0 25 0 1 0 435350199 52789248 11544 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12888 11544 603 41 0 12847 0
vsize: 51552
[startup+210.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 14725 0 0 0 20970 38 0 0 25 0 1 0 435350199 53968896 11837 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13176 11837 603 41 0 13135 0
vsize: 52704
[startup+220.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 14909 0 0 0 21970 38 0 0 25 0 1 0 435350199 54767616 12021 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13371 12021 603 41 0 13330 0
vsize: 53484
[startup+230.114 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 15302 0 0 0 22969 40 0 0 25 0 1 0 435350199 56385536 12414 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13766 12414 603 41 0 13725 0
vsize: 55064
[startup+240.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 15621 0 0 0 23967 41 0 0 25 0 1 0 435350199 57585664 12733 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14059 12733 603 41 0 14018 0
vsize: 56236
[startup+250.115 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 15902 0 0 0 24966 42 0 0 25 0 1 0 435350199 58789888 13014 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14353 13014 603 41 0 14312 0
vsize: 57412
[startup+260.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 16188 0 0 0 25965 44 0 0 25 0 1 0 435350199 59998208 13300 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14648 13300 603 41 0 14607 0
vsize: 58592
[startup+270.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 16481 0 0 0 26964 45 0 0 25 0 1 0 435350199 61198336 13593 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13593 603 41 0 14900 0
vsize: 59764
[startup+280.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 16773 0 0 0 27963 46 0 0 25 0 1 0 435350199 62398464 13885 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15234 13885 603 41 0 15193 0
vsize: 60936
[startup+290.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 17271 0 0 0 28961 48 0 0 25 0 1 0 435350199 64397312 14383 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15722 14383 603 41 0 15681 0
vsize: 62888
[startup+300.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 17436 0 0 0 29962 48 0 0 25 0 1 0 435350199 65073152 14548 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 14548 603 41 0 15846 0
vsize: 63548
[startup+310.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 17686 0 0 0 30962 49 0 0 25 0 1 0 435350199 66150400 14798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16150 14798 603 41 0 16109 0
vsize: 64600
[startup+320.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 17831 0 0 0 31962 49 0 0 25 0 1 0 435350199 66686976 14943 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16281 14943 603 41 0 16240 0
vsize: 65124
[startup+330.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9001
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 18146 0 0 0 32962 49 0 0 25 0 1 0 435350199 68157440 15258 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16640 15258 603 41 0 16599 0
vsize: 66560
[startup+340.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 18492 0 0 0 33961 50 0 0 25 0 1 0 435350199 69500928 15604 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16968 15604 603 41 0 16927 0
vsize: 67872
[startup+350.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 18846 0 0 0 34960 51 0 0 25 0 1 0 435350199 70963200 15958 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17325 15958 603 41 0 17284 0
vsize: 69300
[startup+360.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 19184 0 0 0 35959 52 0 0 25 0 1 0 435350199 72298496 16296 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17651 16296 603 41 0 17610 0
vsize: 70604
[startup+370.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 19520 0 0 0 36959 53 0 0 25 0 1 0 435350199 73760768 16632 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18008 16632 603 41 0 17967 0
vsize: 72032
[startup+380.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 19867 0 0 0 37958 54 0 0 25 0 1 0 435350199 75194368 16979 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18358 16979 603 41 0 18317 0
vsize: 73432
[startup+390.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 20213 0 0 0 38957 55 0 0 25 0 1 0 435350199 76513280 17325 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18680 17325 603 41 0 18639 0
vsize: 74720
[startup+400.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 20573 0 0 0 39956 56 0 0 25 0 1 0 435350199 77987840 17685 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19040 17685 603 41 0 18999 0
vsize: 76160
[startup+410.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 20974 0 0 0 40955 57 0 0 25 0 1 0 435350199 79712256 18086 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19461 18086 603 41 0 19420 0
vsize: 77844
[startup+420.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21828 0 0 0 41954 59 0 0 25 0 1 0 435350199 81707008 18696 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18696 603 41 0 19907 0
vsize: 79792
[startup+430.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21830 0 0 0 42953 59 0 0 25 0 1 0 435350199 81707008 18698 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18698 603 41 0 19907 0
vsize: 79792
[startup+440.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21830 0 0 0 43954 59 0 0 25 0 1 0 435350199 81707008 18698 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18698 603 41 0 19907 0
vsize: 79792
[startup+450.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21830 0 0 0 44954 59 0 0 25 0 1 0 435350199 81707008 18698 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18698 603 41 0 19907 0
vsize: 79792
[startup+460.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21830 0 0 0 45954 59 0 0 25 0 1 0 435350199 81707008 18698 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18698 603 41 0 19907 0
vsize: 79792
[startup+470.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21831 0 0 0 46954 59 0 0 25 0 1 0 435350199 81707008 18699 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18699 603 41 0 19907 0
vsize: 79792
[startup+480.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21831 0 0 0 47955 59 0 0 25 0 1 0 435350199 81707008 18699 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18699 603 41 0 19907 0
vsize: 79792
[startup+490.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21831 0 0 0 48955 59 0 0 25 0 1 0 435350199 81707008 18699 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18699 603 41 0 19907 0
vsize: 79792
[startup+500.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21831 0 0 0 49955 60 0 0 25 0 1 0 435350199 81707008 18699 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18699 603 41 0 19907 0
vsize: 79792
[startup+510.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21979 0 0 0 50954 60 0 0 25 0 1 0 435350199 81854464 18722 4294967295 134512640 134672761 3221224624 3221222896 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19984 18722 603 41 0 19943 0
vsize: 79936
[startup+520.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21991 0 0 0 51955 60 0 0 25 0 1 0 435350199 81854464 18734 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19984 18734 603 41 0 19943 0
vsize: 79936
[startup+530.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21991 0 0 0 52955 60 0 0 25 0 1 0 435350199 81854464 18734 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19984 18734 603 41 0 19943 0
vsize: 79936
[startup+540.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 21991 0 0 0 53955 61 0 0 25 0 1 0 435350199 81854464 18734 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19984 18734 603 41 0 19943 0
vsize: 79936
[startup+550.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22213 0 0 0 54954 61 0 0 25 0 1 0 435350199 82378752 18831 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18831 603 41 0 20071 0
vsize: 80448
[startup+560.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 55954 61 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+570.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 56955 61 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+580.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 57955 61 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+590.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 58955 61 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+600.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 59956 61 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+610.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 60956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+620.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 61956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+630.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9003
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 62956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+640.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 63956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+650.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 64956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+660.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 65956 62 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+670.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 66956 63 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+680.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22215 0 0 0 67956 63 0 0 25 0 1 0 435350199 82378752 18833 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18833 603 41 0 20071 0
vsize: 80448
[startup+690.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22415 0 0 0 68956 63 0 0 25 0 1 0 435350199 83181568 19033 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20308 19033 603 41 0 20267 0
vsize: 81232
[startup+700.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 22699 0 0 0 69955 64 0 0 25 0 1 0 435350199 84258816 19317 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20571 19317 603 41 0 20530 0
vsize: 82284
[startup+710.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 23034 0 0 0 70955 65 0 0 25 0 1 0 435350199 85725184 19652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20929 19652 603 41 0 20888 0
vsize: 83716
[startup+720.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 23424 0 0 0 71954 66 0 0 25 0 1 0 435350199 87318528 20042 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21318 20042 603 41 0 21277 0
vsize: 85272
[startup+730.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 23774 0 0 0 72953 67 0 0 25 0 1 0 435350199 88649728 20392 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21643 20392 603 41 0 21602 0
vsize: 86572
[startup+740.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 24129 0 0 0 73952 68 0 0 25 0 1 0 435350199 90107904 20747 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21999 20747 603 41 0 21958 0
vsize: 87996
[startup+750.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 24476 0 0 0 74952 69 0 0 25 0 1 0 435350199 91566080 21094 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22355 21094 603 41 0 22314 0
vsize: 89420
[startup+760.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 24770 0 0 0 75951 69 0 0 25 0 1 0 435350199 92770304 21388 4294967295 134512640 134672761 3221224624 3221223728 134559787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22649 21388 603 41 0 22608 0
vsize: 90596
[startup+770.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 25150 0 0 0 76951 70 0 0 25 0 1 0 435350199 94367744 21768 4294967295 134512640 134672761 3221224624 3221223808 134558938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23039 21768 603 41 0 22998 0
vsize: 92156
[startup+780.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 25398 0 0 0 77951 70 0 0 25 0 1 0 435350199 95305728 22016 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23268 22016 603 41 0 23227 0
vsize: 93072
[startup+790.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 25694 0 0 0 78950 71 0 0 25 0 1 0 435350199 96497664 22312 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23559 22312 603 41 0 23518 0
vsize: 94236
[startup+800.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 25994 0 0 0 79949 72 0 0 25 0 1 0 435350199 97841152 22612 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23887 22612 603 41 0 23846 0
vsize: 95548
[startup+810.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 26308 0 0 0 80949 73 0 0 25 0 1 0 435350199 99037184 22926 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24179 22926 603 41 0 24138 0
vsize: 96716
[startup+820.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 26628 0 0 0 81948 74 0 0 25 0 1 0 435350199 100364288 23246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24503 23246 603 41 0 24462 0
vsize: 98012
[startup+830.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 26927 0 0 0 82948 74 0 0 25 0 1 0 435350199 101560320 23545 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24795 23545 603 41 0 24754 0
vsize: 99180
[startup+840.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 27132 0 0 0 83948 75 0 0 25 0 1 0 435350199 102494208 23750 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25023 23750 603 41 0 24982 0
vsize: 100092
[startup+850.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 27335 0 0 0 84947 75 0 0 25 0 1 0 435350199 103280640 23953 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25215 23953 603 41 0 25174 0
vsize: 100860
[startup+860.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 27542 0 0 0 85947 76 0 0 25 0 1 0 435350199 104075264 24160 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25409 24160 603 41 0 25368 0
vsize: 101636
[startup+870.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 27703 0 0 0 86947 76 0 0 25 0 1 0 435350199 104726528 24321 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 24321 603 41 0 25527 0
vsize: 102272
[startup+880.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 27799 0 0 0 87947 76 0 0 25 0 1 0 435350199 105123840 24417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25665 24417 603 41 0 25624 0
vsize: 102660
[startup+890.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 28026 0 0 0 88947 77 0 0 25 0 1 0 435350199 106057728 24644 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25893 24644 603 41 0 25852 0
vsize: 103572
[startup+900.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 28219 0 0 0 89947 77 0 0 25 0 1 0 435350199 106860544 24837 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26089 24837 603 41 0 26048 0
vsize: 104356
[startup+910.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 28465 0 0 0 90946 78 0 0 25 0 1 0 435350199 107941888 25083 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26353 25083 603 41 0 26312 0
vsize: 105412
[startup+920.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 28678 0 0 0 91945 78 0 0 25 0 1 0 435350199 108752896 25296 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26551 25296 603 41 0 26510 0
vsize: 106204
[startup+930.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9005
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 28913 0 0 0 92945 79 0 0 25 0 1 0 435350199 109686784 25531 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26779 25531 603 41 0 26738 0
vsize: 107116
[startup+940.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 29101 0 0 0 93944 80 0 0 25 0 1 0 435350199 110489600 25719 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26975 25719 603 41 0 26934 0
vsize: 107900
[startup+950.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 29311 0 0 0 94944 80 0 0 25 0 1 0 435350199 111419392 25929 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27202 25929 603 41 0 27161 0
vsize: 108808
[startup+960.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 29490 0 0 0 95944 80 0 0 25 0 1 0 435350199 112087040 26108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27365 26108 603 41 0 27324 0
vsize: 109460
[startup+970.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 29712 0 0 0 96943 81 0 0 25 0 1 0 435350199 113020928 26330 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27593 26331 603 41 0 27552 0
vsize: 110372
[startup+980.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 29966 0 0 0 97943 82 0 0 25 0 1 0 435350199 114085888 26584 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27853 26584 603 41 0 27812 0
vsize: 111412
[startup+990.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 30141 0 0 0 98942 83 0 0 25 0 1 0 435350199 114753536 26759 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28016 26759 603 41 0 27975 0
vsize: 112064
[startup+1000.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 30351 0 0 0 99941 84 0 0 25 0 1 0 435350199 115552256 26969 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28211 26969 603 41 0 28170 0
vsize: 112844
[startup+1010.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 30591 0 0 0 100941 85 0 0 25 0 1 0 435350199 116621312 27209 4294967295 134512640 134672761 3221224624 3221223728 134559946 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28472 27209 603 41 0 28431 0
vsize: 113888
[startup+1020.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 30831 0 0 0 101940 85 0 0 25 0 1 0 435350199 117559296 27449 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28701 27449 603 41 0 28660 0
vsize: 114804
[startup+1030.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31035 0 0 0 102940 86 0 0 25 0 1 0 435350199 118353920 27653 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28895 27653 603 41 0 28854 0
vsize: 115580
[startup+1040.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31245 0 0 0 103940 86 0 0 25 0 1 0 435350199 119283712 27863 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29122 27863 603 41 0 29081 0
vsize: 116488
[startup+1050.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31496 0 0 0 104939 87 0 0 25 0 1 0 435350199 120344576 28114 4294967295 134512640 134672761 3221224624 3221223728 134560322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29381 28114 603 41 0 29340 0
vsize: 117524
[startup+1060.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31682 0 0 0 105939 88 0 0 25 0 1 0 435350199 121008128 28300 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29543 28300 603 41 0 29502 0
vsize: 118172
[startup+1070.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31786 0 0 0 106938 88 0 0 25 0 1 0 435350199 121708544 28404 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29714 28404 603 41 0 29673 0
vsize: 118856
[startup+1080.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 31964 0 0 0 107938 88 0 0 25 0 1 0 435350199 122503168 28582 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29908 28582 603 41 0 29867 0
vsize: 119632
[startup+1090.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 32179 0 0 0 108937 90 0 0 25 0 1 0 435350199 123437056 28797 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30136 28797 603 41 0 30095 0
vsize: 120544
[startup+1100.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 32494 0 0 0 109935 91 0 0 25 0 1 0 435350199 124653568 29112 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30433 29112 603 41 0 30392 0
vsize: 121732
[startup+1110.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 32835 0 0 0 110935 92 0 0 25 0 1 0 435350199 126115840 29453 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30790 29453 603 41 0 30749 0
vsize: 123160
[startup+1120.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 33136 0 0 0 111934 92 0 0 25 0 1 0 435350199 127315968 29754 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31083 29754 603 41 0 31042 0
vsize: 124332
[startup+1130.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 33476 0 0 0 112934 93 0 0 25 0 1 0 435350199 128655360 30094 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31410 30094 603 41 0 31369 0
vsize: 125640
[startup+1140.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 33825 0 0 0 113932 95 0 0 25 0 1 0 435350199 130109440 30443 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 30443 603 41 0 31724 0
vsize: 127060
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 34201 0 0 0 114932 95 0 0 25 0 1 0 435350199 131698688 30819 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32153 30819 603 41 0 32112 0
vsize: 128612
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 34542 0 0 0 115931 96 0 0 25 0 1 0 435350199 133021696 31160 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32476 31160 603 41 0 32435 0
vsize: 129904
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 34942 0 0 0 116931 97 0 0 25 0 1 0 435350199 134635520 31560 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32870 31560 603 41 0 32829 0
vsize: 131480
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 35317 0 0 0 117929 99 0 0 25 0 1 0 435350199 136216576 31935 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33256 31935 603 41 0 33215 0
vsize: 133024
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 35696 0 0 0 118929 99 0 0 25 0 1 0 435350199 137822208 32314 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33648 32314 603 41 0 33607 0
vsize: 134592
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 9007
Raw data (stat): 8999 (minisat+) R 8998 12452 12451 0 -1 0 36058 0 0 0 119928 100 0 0 25 0 1 0 435350199 139280384 32676 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34004 32676 603 41 0 33963 0
vsize: 136016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 9007
Raw data (stat): 8999 (minisat+) Z 8998 12452 12451 0 -1 12 36061 0 0 0 119928 106 0 0 25 0 1 0 435350199 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.24
CPU time (s): 1200.35
CPU user time (s): 1199.29
CPU system time (s): 1.06684
CPU usage (%): 100.009
Max. virtual memory (Kb): 136016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####