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-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02884
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 19457

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 19:05:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16606 boxname=wulflinc22 idbench=1278 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 16606
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        340452 kB
Buffers:         31812 kB
Cached:         633820 kB
SwapCached:         20 kB
Active:         139540 kB
Inactive:       528756 kB
HighTotal:      131008 kB
HighFree:         1792 kB
LowTotal:       903652 kB
LowFree:        338660 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            20368 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:25:10 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 16606 7 1200.29 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.92 0.98 0.92 2/54 6464
Raw data (stat): 6464 (runsolver) R 6463 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547459941 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 6464
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 6402 0 0 0 982 17 0 0 25 0 1 0 547459941 25440256 4918 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6211 4918 603 41 0 6170 0
vsize: 24844
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 6464
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 7532 0 0 0 1978 21 0 0 25 0 1 0 547459941 26218496 5079 4294967295 134512640 134672761 3221224624 3221223184 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6401 5079 603 41 0 6360 0
vsize: 25604
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 6464
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 7852 0 0 0 2976 22 0 0 25 0 1 0 547459941 27545600 5399 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6725 5399 603 41 0 6684 0
vsize: 26900
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 6464
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 8579 0 0 0 3974 24 0 0 25 0 1 0 547459941 28807168 5691 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7033 5691 603 41 0 6992 0
vsize: 28132
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 6464
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 8852 0 0 0 4974 25 0 0 25 0 1 0 547459941 29876224 5964 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7294 5964 603 41 0 7253 0
vsize: 29176
[startup+60.003 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 9114 0 0 0 5973 26 0 0 25 0 1 0 547459941 30957568 6226 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7558 6226 603 41 0 7517 0
vsize: 30232
[startup+70.0062 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 9533 0 0 0 6972 28 0 0 25 0 1 0 547459941 32698368 6645 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7983 6645 603 41 0 7942 0
vsize: 31932
[startup+80.0074 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 9846 0 0 0 7970 29 0 0 25 0 1 0 547459941 34050048 6958 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 6958 603 41 0 8272 0
vsize: 33252
[startup+90.0075 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 10212 0 0 0 8969 31 0 0 25 0 1 0 547459941 35520512 7324 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8672 7324 603 41 0 8631 0
vsize: 34688
[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 10551 0 0 0 9968 32 0 0 25 0 1 0 547459941 36843520 7663 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8995 7663 603 41 0 8954 0
vsize: 35980
[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 10944 0 0 0 10967 33 0 0 25 0 1 0 547459941 38453248 8056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9388 8056 603 41 0 9347 0
vsize: 37552
[startup+120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 11284 0 0 0 11965 35 0 0 25 0 1 0 547459941 39919616 8396 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9746 8396 603 41 0 9705 0
vsize: 38984
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 11612 0 0 0 12964 36 0 0 25 0 1 0 547459941 41267200 8724 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10075 8724 603 41 0 10034 0
vsize: 40300
[startup+140.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 11946 0 0 0 13963 37 0 0 25 0 1 0 547459941 42586112 9058 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10397 9058 603 41 0 10356 0
vsize: 41588
[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 12281 0 0 0 14963 38 0 0 25 0 1 0 547459941 43917312 9393 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10722 9393 603 41 0 10681 0
vsize: 42888
[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 12630 0 0 0 15962 39 0 0 25 0 1 0 547459941 45481984 9742 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11104 9742 603 41 0 11063 0
vsize: 44416
[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 13072 0 0 0 16961 40 0 0 25 0 1 0 547459941 47218688 10184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11528 10184 603 41 0 11487 0
vsize: 46112
[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 13476 0 0 0 17960 41 0 0 25 0 1 0 547459941 48943104 10588 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11949 10588 603 41 0 11908 0
vsize: 47796
[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 13936 0 0 0 18959 43 0 0 25 0 1 0 547459941 50802688 11048 4294967295 134512640 134672761 3221224624 3221223728 134560039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12403 11048 603 41 0 12362 0
vsize: 49612
[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 14331 0 0 0 19958 44 0 0 25 0 1 0 547459941 52387840 11443 4294967295 134512640 134672761 3221224624 3221223728 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12790 11443 603 41 0 12749 0
vsize: 51160
[startup+210.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 14713 0 0 0 20957 45 0 0 25 0 1 0 547459941 53968896 11825 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13176 11825 603 41 0 13135 0
vsize: 52704
[startup+220.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 14843 0 0 0 21957 45 0 0 25 0 1 0 547459941 54497280 11955 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13305 11955 603 41 0 13264 0
vsize: 53220
[startup+230.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 15244 0 0 0 22955 47 0 0 25 0 1 0 547459941 56115200 12356 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13700 12356 603 41 0 13659 0
vsize: 54800
[startup+240.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 15571 0 0 0 23955 48 0 0 25 0 1 0 547459941 57454592 12683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14027 12683 603 41 0 13986 0
vsize: 56108
[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 15830 0 0 0 24954 49 0 0 25 0 1 0 547459941 58519552 12942 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14287 12942 603 41 0 14246 0
vsize: 57148
[startup+260.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 16133 0 0 0 25954 50 0 0 25 0 1 0 547459941 59731968 13245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14583 13245 603 41 0 14542 0
vsize: 58332
[startup+270.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 16416 0 0 0 26952 52 0 0 25 0 1 0 547459941 60923904 13528 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14874 13528 603 41 0 14833 0
vsize: 59496
[startup+280.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 16703 0 0 0 27951 53 0 0 25 0 1 0 547459941 62001152 13815 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15137 13815 603 41 0 15096 0
vsize: 60548
[startup+290.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 17117 0 0 0 28950 54 0 0 25 0 1 0 547459941 63725568 14229 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15558 14229 603 41 0 15517 0
vsize: 62232
[startup+300.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 17422 0 0 0 29949 55 0 0 25 0 1 0 547459941 64937984 14534 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15854 14534 603 41 0 15813 0
vsize: 63416
[startup+310.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 17607 0 0 0 30948 56 0 0 25 0 1 0 547459941 65736704 14719 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 14719 603 41 0 16008 0
vsize: 64196
[startup+320.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 17786 0 0 0 31948 57 0 0 25 0 1 0 547459941 66551808 14898 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16248 14898 603 41 0 16207 0
vsize: 64992
[startup+330.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 18053 0 0 0 32947 57 0 0 25 0 1 0 547459941 67760128 15165 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16543 15165 603 41 0 16502 0
vsize: 66172
[startup+340.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 18408 0 0 0 33946 58 0 0 25 0 1 0 547459941 69234688 15520 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16903 15520 603 41 0 16862 0
vsize: 67612
[startup+350.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 18742 0 0 0 34946 59 0 0 25 0 1 0 547459941 70557696 15854 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17226 15854 603 41 0 17185 0
vsize: 68904
[startup+360.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 19087 0 0 0 35944 61 0 0 25 0 1 0 547459941 71905280 16199 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17555 16199 603 41 0 17514 0
vsize: 70220
[startup+370.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 19429 0 0 0 36943 62 0 0 25 0 1 0 547459941 73359360 16541 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17910 16541 603 41 0 17869 0
vsize: 71640
[startup+380.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 19777 0 0 0 37943 63 0 0 25 0 1 0 547459941 74809344 16889 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18264 16889 603 41 0 18223 0
vsize: 73056
[startup+390.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 20116 0 0 0 38941 64 0 0 25 0 1 0 547459941 76107776 17228 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18581 17228 603 41 0 18540 0
vsize: 74324
[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 20468 0 0 0 39941 65 0 0 25 0 1 0 547459941 77582336 17580 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18941 17580 603 41 0 18900 0
vsize: 75764
[startup+410.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 20871 0 0 0 40939 67 0 0 25 0 1 0 547459941 79314944 17983 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19364 17983 603 41 0 19323 0
vsize: 77456
[startup+420.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21379 0 0 0 41938 68 0 0 25 0 1 0 547459941 80355328 18265 4294967295 134512640 134672761 3221224624 3221223040 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19618 18265 603 41 0 19577 0
vsize: 78472
[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21830 0 0 0 42937 69 0 0 25 0 1 0 547459941 81707008 18698 4294967295 134512640 134672761 3221224624 3221223796 134556639 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.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21830 0 0 0 43937 69 0 0 25 0 1 0 547459941 81707008 18698 4294967295 134512640 134672761 3221224624 3221223728 134559890 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.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21830 0 0 0 44937 69 0 0 25 0 1 0 547459941 81707008 18698 4294967295 134512640 134672761 3221224624 3221223792 134561201 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.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21830 0 0 0 45937 69 0 0 25 0 1 0 547459941 81707008 18698 4294967295 134512640 134672761 3221224624 3221223760 134560677 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21831 0 0 0 46937 69 0 0 25 0 1 0 547459941 81707008 18699 4294967295 134512640 134672761 3221224624 3221223728 134559847 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21831 0 0 0 47937 70 0 0 25 0 1 0 547459941 81707008 18699 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21831 0 0 0 48937 70 0 0 25 0 1 0 547459941 81707008 18699 4294967295 134512640 134672761 3221224624 3221223808 134559542 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21831 0 0 0 49937 70 0 0 25 0 1 0 547459941 81707008 18699 4294967295 134512640 134672761 3221224624 3221223728 134560410 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21831 0 0 0 50937 70 0 0 25 0 1 0 547459941 81707008 18699 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19948 18699 603 41 0 19907 0
vsize: 79792
[startup+520.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21991 0 0 0 51937 70 0 0 25 0 1 0 547459941 81854464 18734 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21991 0 0 0 52937 70 0 0 25 0 1 0 547459941 81854464 18734 4294967295 134512640 134672761 3221224624 3221223728 134560235 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.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 21991 0 0 0 53937 71 0 0 25 0 1 0 547459941 81854464 18734 4294967295 134512640 134672761 3221224624 3221223728 134560160 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.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22212 0 0 0 54937 71 0 0 25 0 1 0 547459941 82378752 18830 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 18830 603 41 0 20071 0
vsize: 80448
[startup+560.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 55937 71 0 0 25 0 1 0 547459941 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+570.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 56937 71 0 0 25 0 1 0 547459941 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+580.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 57937 71 0 0 25 0 1 0 547459941 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.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 58937 71 0 0 25 0 1 0 547459941 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+600.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 59937 71 0 0 25 0 1 0 547459941 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134561201 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.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 60938 71 0 0 25 0 1 0 547459941 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+620.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 61938 72 0 0 25 0 1 0 547459941 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.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 62938 72 0 0 25 0 1 0 547459941 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134561151 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.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 63938 72 0 0 25 0 1 0 547459941 82378752 18833 4294967295 134512640 134672761 3221224624 3221223728 134560212 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.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 64938 72 0 0 25 0 1 0 547459941 82378752 18833 4294967295 134512640 134672761 3221224624 3221223824 134557911 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.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 65938 72 0 0 25 0 1 0 547459941 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+670.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 66938 72 0 0 25 0 1 0 547459941 82378752 18833 4294967295 134512640 134672761 3221224624 3221223792 134561164 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.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22215 0 0 0 67938 72 0 0 25 0 1 0 547459941 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+690.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22337 0 0 0 68938 72 0 0 25 0 1 0 547459941 82776064 18955 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20209 18955 603 41 0 20168 0
vsize: 80836
[startup+700.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22610 0 0 0 69937 73 0 0 25 0 1 0 547459941 83992576 19228 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20506 19228 603 41 0 20465 0
vsize: 82024
[startup+710.045 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 22943 0 0 0 70936 74 0 0 25 0 1 0 547459941 85327872 19561 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20832 19561 603 41 0 20791 0
vsize: 83328
[startup+720.061 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 23308 0 0 0 71937 75 0 0 25 0 1 0 547459941 86794240 19926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21190 19926 603 41 0 21149 0
vsize: 84760
[startup+730.061 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 23662 0 0 0 72937 76 0 0 25 0 1 0 547459941 88240128 20280 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21543 20280 603 41 0 21502 0
vsize: 86172
[startup+740.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 24021 0 0 0 73936 77 0 0 25 0 1 0 547459941 89702400 20639 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21900 20639 603 41 0 21859 0
vsize: 87600
[startup+750.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 24366 0 0 0 74935 78 0 0 25 0 1 0 547459941 91164672 20984 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22257 20984 603 41 0 22216 0
vsize: 89028
[startup+760.061 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 24688 0 0 0 75934 79 0 0 25 0 1 0 547459941 92499968 21306 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22583 21306 603 41 0 22542 0
vsize: 90332
[startup+770.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 25042 0 0 0 76934 80 0 0 25 0 1 0 547459941 93835264 21660 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22909 21660 603 41 0 22868 0
vsize: 91636
[startup+780.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 25334 0 0 0 77933 81 0 0 25 0 1 0 547459941 95039488 21952 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23203 21952 603 41 0 23162 0
vsize: 92812
[startup+790.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 25598 0 0 0 78932 82 0 0 25 0 1 0 547459941 96235520 22216 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23495 22216 603 41 0 23454 0
vsize: 93980
[startup+800.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 25924 0 0 0 79931 83 0 0 25 0 1 0 547459941 97439744 22542 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23789 22542 603 41 0 23748 0
vsize: 95156
[startup+810.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 26229 0 0 0 80931 84 0 0 25 0 1 0 547459941 98775040 22847 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24115 22847 603 41 0 24074 0
vsize: 96460
[startup+820.064 s]
Raw data (loadavg): 0.99 0.98 0.92 3/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 26536 0 0 0 81930 85 0 0 25 0 1 0 547459941 99966976 23154 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24406 23154 603 41 0 24365 0
vsize: 97624
[startup+830.064 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 26868 0 0 0 82929 86 0 0 25 0 1 0 547459941 101306368 23486 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24733 23486 603 41 0 24692 0
vsize: 98932
[startup+840.064 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27094 0 0 0 83929 86 0 0 25 0 1 0 547459941 102232064 23712 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24959 23712 603 41 0 24918 0
vsize: 99836
[startup+850.065 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27292 0 0 0 84928 87 0 0 25 0 1 0 547459941 103149568 23910 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25183 23910 603 41 0 25142 0
vsize: 100732
[startup+860.065 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27509 0 0 0 85928 88 0 0 25 0 1 0 547459941 103940096 24127 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25376 24127 603 41 0 25335 0
vsize: 101504
[startup+870.067 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27703 0 0 0 86928 88 0 0 25 0 1 0 547459941 104726528 24321 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25568 24321 603 41 0 25527 0
vsize: 102272
[startup+880.066 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27749 0 0 0 87928 88 0 0 25 0 1 0 547459941 104996864 24367 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25634 24367 603 41 0 25593 0
vsize: 102536
[startup+890.066 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 27997 0 0 0 88927 89 0 0 25 0 1 0 547459941 105922560 24615 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25860 24615 603 41 0 25819 0
vsize: 103440
[startup+900.067 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 28193 0 0 0 89927 90 0 0 25 0 1 0 547459941 106725376 24811 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26056 24811 603 41 0 26015 0
vsize: 104224
[startup+910.067 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 28424 0 0 0 90927 90 0 0 25 0 1 0 547459941 107671552 25042 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26287 25042 603 41 0 26246 0
vsize: 105148
[startup+920.068 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 28654 0 0 0 91926 90 0 0 25 0 1 0 547459941 108617728 25272 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26518 25272 603 41 0 26477 0
vsize: 106072
[startup+930.069 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 28885 0 0 0 92926 91 0 0 25 0 1 0 547459941 109555712 25503 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26747 25503 603 41 0 26706 0
vsize: 106988
[startup+940.069 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 29091 0 0 0 93926 92 0 0 25 0 1 0 547459941 110489600 25709 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26975 25709 603 41 0 26934 0
vsize: 107900
[startup+950.069 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 29285 0 0 0 94925 93 0 0 25 0 1 0 547459941 111284224 25903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27169 25903 603 41 0 27128 0
vsize: 108676
[startup+960.069 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 29473 0 0 0 95924 93 0 0 25 0 1 0 547459941 111951872 26091 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27332 26091 603 41 0 27291 0
vsize: 109328
[startup+970.069 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 29688 0 0 0 96924 94 0 0 25 0 1 0 547459941 112885760 26306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27560 26306 603 41 0 27519 0
vsize: 110240
[startup+980.068 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 29947 0 0 0 97924 94 0 0 25 0 1 0 547459941 113950720 26565 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27820 26565 603 41 0 27779 0
vsize: 111280
[startup+990.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 30133 0 0 0 98923 95 0 0 25 0 1 0 547459941 114753536 26751 4294967295 134512640 134672761 3221224624 3221223728 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28016 26751 603 41 0 27975 0
vsize: 112064
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 30338 0 0 0 99923 95 0 0 25 0 1 0 547459941 115552256 26956 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28211 26956 603 41 0 28170 0
vsize: 112844
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 30580 0 0 0 100923 96 0 0 25 0 1 0 547459941 116486144 27198 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28439 27198 603 41 0 28398 0
vsize: 113756
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 30823 0 0 0 101922 97 0 0 25 0 1 0 547459941 117559296 27441 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28701 27441 603 41 0 28660 0
vsize: 114804
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31030 0 0 0 102922 97 0 0 25 0 1 0 547459941 118353920 27648 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28895 27648 603 41 0 28854 0
vsize: 115580
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31242 0 0 0 103922 98 0 0 25 0 1 0 547459941 119283712 27860 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29122 27860 603 41 0 29081 0
vsize: 116488
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31496 0 0 0 104921 98 0 0 25 0 1 0 547459941 120344576 28114 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29381 28114 603 41 0 29340 0
vsize: 117524
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31686 0 0 0 105920 99 0 0 25 0 1 0 547459941 121008128 28304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29543 28304 603 41 0 29502 0
vsize: 118172
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31789 0 0 0 106920 100 0 0 25 0 1 0 547459941 121708544 28407 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29714 28407 603 41 0 29673 0
vsize: 118856
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 31965 0 0 0 107919 100 0 0 25 0 1 0 547459941 122503168 28583 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29908 28583 603 41 0 29867 0
vsize: 119632
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 32180 0 0 0 108919 101 0 0 25 0 1 0 547459941 123437056 28798 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30136 28798 603 41 0 30095 0
vsize: 120544
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 32497 0 0 0 109918 101 0 0 25 0 1 0 547459941 124653568 29115 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30433 29115 603 41 0 30392 0
vsize: 121732
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 32835 0 0 0 110918 103 0 0 25 0 1 0 547459941 126115840 29453 4294967295 134512640 134672761 3221224624 3221223728 134560031 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.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 33138 0 0 0 111917 103 0 0 25 0 1 0 547459941 127315968 29756 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31083 29756 603 41 0 31042 0
vsize: 124332
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 33478 0 0 0 112916 105 0 0 25 0 1 0 547459941 128655360 30096 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31410 30096 603 41 0 31369 0
vsize: 125640
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 33828 0 0 0 113915 106 0 0 25 0 1 0 547459941 130109440 30446 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31765 30446 603 41 0 31724 0
vsize: 127060
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 34203 0 0 0 114914 107 0 0 25 0 1 0 547459941 131698688 30821 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32153 30821 603 41 0 32112 0
vsize: 128612
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 34546 0 0 0 115913 108 0 0 25 0 1 0 547459941 133021696 31164 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32476 31164 603 41 0 32435 0
vsize: 129904
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 34946 0 0 0 116913 109 0 0 25 0 1 0 547459941 134635520 31564 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32870 31564 603 41 0 32829 0
vsize: 131480
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 35320 0 0 0 117912 110 0 0 25 0 1 0 547459941 136216576 31938 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33256 31938 603 41 0 33215 0
vsize: 133024
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 35699 0 0 0 118911 111 0 0 25 0 1 0 547459941 137822208 32317 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33648 32317 603 41 0 33607 0
vsize: 134592
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 6466
Raw data (stat): 6464 (minisat+) R 6463 26298 26297 0 -1 0 36060 0 0 0 119910 112 0 0 25 0 1 0 547459941 139280384 32678 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34004 32678 603 41 0 33963 0
vsize: 136016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 6466
Raw data (stat): 6464 (minisat+) Z 6463 26298 26297 0 -1 12 36063 0 0 0 119910 118 0 0 25 0 1 0 547459941 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.14
CPU time (s): 1200.29
CPU user time (s): 1199.11
CPU system time (s): 1.18382
CPU usage (%): 100.013
Max. virtual memory (Kb): 136016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####