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 19448

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 19:03:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16614 boxname=wulflinc27 idbench=1278 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 16614
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        778124 kB
Buffers:         19212 kB
Cached:         214740 kB
SwapCached:        512 kB
Active:          33424 kB
Inactive:       202500 kB
HighTotal:      131008 kB
HighFree:         5544 kB
LowTotal:       903652 kB
LowFree:        772580 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            15092 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:23:33 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 16614 7 1200.28 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 |   36957   102667 |   12319       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 |        25 |   92284   300283 |   30761      25     1588    63.5 |  0.000 % |
c ==============================================================================
c [1mFound solution: 8045[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1184708   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        37 |   92299   300397 |   30766      37     1920    51.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 7602[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185151   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        39 |   92309   300440 |   30769      39     2038    52.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: 7071[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185682   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        40 |   92322   300533 |   30774      40     2041    51.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 6228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186525   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   92330   300634 |   30776      43     4471   104.0 |  0.000 % |
c |       146 |   92287   300487 |   33853     142    20060   141.3 |  0.419 % |
c ==============================================================================
c [1mFound solution: 6155[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186598   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       286 |   92298   300568 |   30766     282    54056   191.7 |  0.419 % |
c ==============================================================================
c [1mFound solution: 6118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186635   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       317 |   92301   300608 |   30767     313    55297   176.7 |  0.419 % |
c ==============================================================================
c [1mFound solution: 5874[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186879   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       363 |   92303   300626 |   30767     359    62358   173.7 |  0.419 % |
c |       463 |   92295   300596 |   33843     457    89183   195.1 |  0.483 % |
c |       613 |   92295   300596 |   37228     607    98303   161.9 |  0.483 % |
c |       839 |   92295   300596 |   40950     833   108131   129.8 |  0.483 % |
c ==============================================================================
c [1mFound solution: 5710[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1187043   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1085 |   92305   300655 |   30768    1079   180637   167.4 |  0.483 % |
c |      1185 |   92305   300655 |   33844    1179   205973   174.7 |  0.507 % |
c |      1340 |   92266   300527 |   37229    1328   232416   175.0 |  0.513 % |
c |      1565 |   92266   300527 |   40952    1553   287797   185.3 |  0.513 % |
c |      1906 |   92266   300527 |   45047    1894   423841   223.8 |  0.513 % |
c ==============================================================================
c [1mFound solution: 5686[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5680   maxlim: 1186452   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2181 |  131914   442145 |   43971    2169   515824   237.8 |  0.513 % |
c |      2281 |  131914   442145 |   48368    2269   552824   243.6 |  0.455 % |
c |      2431 |  131914   442145 |   53204    2419   564533   233.4 |  0.455 % |
c |      2657 |  131914   442145 |   58525    2645   713146   269.6 |  0.455 % |
c |      2994 |  131914   442145 |   64377    2982   808284   271.1 |  0.455 % |
c |      3500 |  131878   442021 |   70815    3484   997316   286.3 |  0.485 % |
c ==============================================================================
c [1mFound solution: 5200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186938   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3758 |  131885   442118 |   43961    3742  1120517   299.4 |  0.485 % |
c |      3858 |  131885   442118 |   48357    3842  1142582   297.4 |  0.516 % |
c |      4011 |  131885   442118 |   53192    3995  1207722   302.3 |  0.516 % |
c |      4238 |  131885   442118 |   58512    4222  1329460   314.9 |  0.516 % |
c |      4576 |  131885   442118 |   64363    4560  1553557   340.7 |  0.516 % |
c |      5082 |  131814   441867 |   70799    5038  1705011   338.4 |  0.569 % |
c ==============================================================================
c [1mFound solution: 5149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186989   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5140 |  131819   441939 |   43939    5096  1713826   336.3 |  0.569 % |
c |      5240 |  131819   441939 |   48332    5196  1759631   338.7 |  0.591 % |
c |      5395 |  131819   441939 |   53166    5351  1778936   332.4 |  0.591 % |
c |      5623 |  131819   441939 |   58482    5579  1981123   355.1 |  0.591 % |
c |      5960 |  131718   441584 |   64331    5911  2117862   358.3 |  0.604 % |
c |      6469 |  131699   441521 |   70764    6418  2510617   391.2 |  0.626 % |
c |      7229 |  131699   441521 |   77840    7178  2746938   382.7 |  0.626 % |
c ==============================================================================
c [1mFound solution: 5103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5842   maxlim: 1185756   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7991 |  172505   587332 |   57501    7940  3016324   379.9 |  0.626 % |
c |      8095 |  172497   587302 |   63251    8042  3026841   376.4 |  0.568 % |
c |      8246 |  172497   587302 |   69576    8193  3121673   381.0 |  0.568 % |
c |      8471 |  172497   587302 |   76533    8418  3179608   377.7 |  0.568 % |
c |      8808 |  172490   587279 |   84187    8754  3262628   372.7 |  0.571 % |
c |      9314 |  172490   587279 |   92605    9260  3525891   380.8 |  0.571 % |
c |     10075 |  172490   587279 |  101866   10021  3918602   391.0 |  0.571 % |
c |     11214 |  172490   587279 |  112053   11160  4528254   405.8 |  0.571 % |
c ==============================================================================
c [1mFound solution: 4762[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186097   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11570 |  172474   587265 |   57491   11514  4549068   395.1 |  0.571 % |
c |     11672 |  172474   587265 |   63240   11616  4622997   398.0 |  0.592 % |
c |     11823 |  172474   587265 |   69564   11767  4655865   395.7 |  0.592 % |
c |     12048 |  172474   587265 |   76520   11992  4771881   397.9 |  0.592 % |
c ==============================================================================
c [1mFound solution: 4493[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186366   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12202 |  172491   587387 |   57497   12146  4810251   396.0 |  0.592 % |
c |     12303 |  172491   587387 |   63246   12247  4814925   393.2 |  0.617 % |
c |     12453 |  172491   587387 |   69571   12397  4855380   391.7 |  0.617 % |
c |     12682 |  172491   587387 |   76528   12626  4872784   385.9 |  0.617 % |
c |     13020 |  172491   587387 |   84181   12964  4910096   378.7 |  0.617 % |
c |     13527 |  172491   587387 |   92599   13471  4973987   369.2 |  0.617 % |
c |     14287 |  172491   587387 |  101859   14231  5297532   372.3 |  0.617 % |
c |     15426 |  172425   587161 |  112045   15359  5586821   363.7 |  0.624 % |
c |     17134 |  172356   586916 |  123249   17060  6103697   357.8 |  0.631 % |
c |     19698 |  172305   586744 |  135574   19620  7151850   364.5 |  0.634 % |
c |     23542 |  172297   586714 |  149132   23463  8904453   379.5 |  0.638 % |
c |     29308 |  172289   586684 |  164045   29227 11246200   384.8 |  0.641 % |
c |     37959 |  172212   586419 |  180450   37869 14748953   389.5 |  0.690 % |
c |     50936 |  172207   586404 |  198495   50841 19984087   393.1 |  0.694 % |
c |     70397 |  172043   585843 |  218344   70221 27253124   388.1 |  0.767 % |
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_bi#### 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.91 2/54 23683
Raw data (stat): 23683 (runsolver) R 23682 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547448948 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99992 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 6750 0 0 0 980 18 0 0 25 0 1 0 547448948 25702400 4993 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6275 4993 603 41 0 6234 0
vsize: 25100
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 7860 0 0 0 1977 20 0 0 25 0 1 0 547448948 26357760 5140 4294967295 134512640 134672761 3221224544 3221221940 1075346926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6435 5140 603 41 0 6394 0
vsize: 25740
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 8100 0 0 0 2976 21 0 0 25 0 1 0 547448948 27283456 5380 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6661 5380 603 41 0 6620 0
vsize: 26644
[startup+40.0023 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 9267 0 0 0 3972 25 0 0 25 0 1 0 547448948 31219712 6285 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7622 6285 603 41 0 7581 0
vsize: 30488
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 9893 0 0 0 4971 27 0 0 25 0 1 0 547448948 32964608 6732 4294967295 134512640 134672761 3221224544 3221223844 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8048 6732 603 41 0 8007 0
vsize: 32192
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 10200 0 0 0 5970 28 0 0 25 0 1 0 547448948 34295808 7039 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8373 7039 603 41 0 8332 0
vsize: 33492
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 10700 0 0 0 6968 29 0 0 25 0 1 0 547448948 35467264 7334 4294967295 134512640 134672761 3221224544 3221222340 134544418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8659 7334 603 41 0 8618 0
vsize: 34636
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11040 0 0 0 7967 30 0 0 25 0 1 0 547448948 36765696 7669 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8976 7669 603 41 0 8935 0
vsize: 35904
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11518 0 0 0 8966 32 0 0 25 0 1 0 547448948 38789120 8147 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9470 8147 603 41 0 9429 0
vsize: 37880
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11807 0 0 0 9966 32 0 0 25 0 1 0 547448948 39989248 8436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9763 8436 603 41 0 9722 0
vsize: 39052
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 12899 0 0 0 10963 35 0 0 25 0 1 0 547448948 43143168 9317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10533 9317 603 41 0 10492 0
vsize: 42132
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13246 0 0 0 11962 36 0 0 25 0 1 0 547448948 44470272 9664 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10857 9664 603 41 0 10816 0
vsize: 43428
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23683
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13638 0 0 0 12961 37 0 0 25 0 1 0 547448948 46059520 10056 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11245 10056 603 41 0 11204 0
vsize: 44980
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13996 0 0 0 13960 38 0 0 25 0 1 0 547448948 47607808 10414 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11623 10414 603 41 0 11582 0
vsize: 46492
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 14333 0 0 0 14959 40 0 0 25 0 1 0 547448948 48914432 10751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11942 10751 603 41 0 11901 0
vsize: 47768
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 14816 0 0 0 15958 41 0 0 25 0 1 0 547448948 49979392 11013 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12202 11013 603 41 0 12161 0
vsize: 48808
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15203 0 0 0 16957 42 0 0 25 0 1 0 547448948 50581504 11162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12349 11162 603 41 0 12308 0
vsize: 49396
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15406 0 0 0 17957 42 0 0 25 0 1 0 547448948 51388416 11365 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12546 11365 603 41 0 12505 0
vsize: 50184
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15653 0 0 0 18956 43 0 0 25 0 1 0 547448948 52420608 11612 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12798 11612 603 41 0 12757 0
vsize: 51192
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15814 0 0 0 19956 43 0 0 25 0 1 0 547448948 53096448 11773 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12963 11773 603 41 0 12922 0
vsize: 51852
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16064 0 0 0 20956 44 0 0 25 0 1 0 547448948 54034432 12023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13192 12023 603 41 0 13151 0
vsize: 52768
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16341 0 0 0 21955 45 0 0 25 0 1 0 547448948 55279616 12300 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13496 12300 603 41 0 13455 0
vsize: 53984
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16646 0 0 0 22954 46 0 0 25 0 1 0 547448948 56487936 12605 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 12605 603 41 0 13750 0
vsize: 55164
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16910 0 0 0 23954 47 0 0 25 0 1 0 547448948 57536512 12869 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14047 12869 603 41 0 14006 0
vsize: 56188
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17001 0 0 0 24954 47 0 0 25 0 1 0 547448948 57942016 12960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14146 12960 603 41 0 14105 0
vsize: 56584
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17431 0 0 0 25953 48 0 0 25 0 1 0 547448948 59682816 13390 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14571 13390 603 41 0 14530 0
vsize: 58284
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17748 0 0 0 26952 49 0 0 25 0 1 0 547448948 61005824 13707 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14894 13707 603 41 0 14853 0
vsize: 59576
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18120 0 0 0 27952 49 0 0 25 0 1 0 547448948 62472192 14079 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15252 14079 603 41 0 15211 0
vsize: 61008
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18379 0 0 0 28951 50 0 0 25 0 1 0 547448948 63524864 14338 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15509 14338 603 41 0 15468 0
vsize: 62036
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18756 0 0 0 29951 51 0 0 25 0 1 0 547448948 65097728 14715 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14715 603 41 0 15852 0
vsize: 63572
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19134 0 0 0 30950 52 0 0 25 0 1 0 547448948 66703360 15093 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16285 15093 603 41 0 16244 0
vsize: 65140
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19479 0 0 0 31949 53 0 0 25 0 1 0 547448948 68116480 15438 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16630 15438 603 41 0 16589 0
vsize: 66520
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19844 0 0 0 32948 54 0 0 25 0 1 0 547448948 69550080 15803 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16980 15803 603 41 0 16939 0
vsize: 67920
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20167 0 0 0 33947 55 0 0 25 0 1 0 547448948 70836224 16126 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17294 16126 603 41 0 17253 0
vsize: 69176
[startup+350.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20554 0 0 0 34947 57 0 0 25 0 1 0 547448948 72458240 16513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17690 16513 603 41 0 17649 0
vsize: 70760
[startup+360.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20855 0 0 0 35948 57 0 0 25 0 1 0 547448948 73670656 16814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17986 16814 603 41 0 17945 0
vsize: 71944
[startup+370.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21108 0 0 0 36947 58 0 0 25 0 1 0 547448948 74731520 17067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18245 17067 603 41 0 18204 0
vsize: 72980
[startup+380.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21350 0 0 0 37947 58 0 0 25 0 1 0 547448948 75755520 17309 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18495 17309 603 41 0 18454 0
vsize: 73980
[startup+390.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21595 0 0 0 38946 59 0 0 25 0 1 0 547448948 76664832 17554 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18717 17554 603 41 0 18676 0
vsize: 74868
[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21876 0 0 0 39945 61 0 0 25 0 1 0 547448948 77864960 17835 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19010 17835 603 41 0 18969 0
vsize: 76040
[startup+410.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22146 0 0 0 40944 61 0 0 25 0 1 0 547448948 78934016 18105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19271 18105 603 41 0 19230 0
vsize: 77084
[startup+420.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22414 0 0 0 41943 62 0 0 25 0 1 0 547448948 80011264 18373 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19534 18373 603 41 0 19493 0
vsize: 78136
[startup+430.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22707 0 0 0 42943 63 0 0 25 0 1 0 547448948 81309696 18666 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19851 18666 603 41 0 19810 0
vsize: 79404
[startup+440.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23008 0 0 0 43942 64 0 0 25 0 1 0 547448948 82485248 18967 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20138 18967 603 41 0 20097 0
vsize: 80552
[startup+450.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23268 0 0 0 44942 65 0 0 25 0 1 0 547448948 83677184 19227 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20429 19227 603 41 0 20388 0
vsize: 81716
[startup+460.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23578 0 0 0 45941 66 0 0 25 0 1 0 547448948 84996096 19537 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20751 19537 603 41 0 20710 0
vsize: 83004
[startup+470.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23887 0 0 0 46940 67 0 0 25 0 1 0 547448948 86163456 19846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21036 19846 603 41 0 20995 0
vsize: 84144
[startup+480.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24206 0 0 0 47939 68 0 0 25 0 1 0 547448948 87498752 20165 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21362 20165 603 41 0 21321 0
vsize: 85448
[startup+490.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24490 0 0 0 48939 68 0 0 25 0 1 0 547448948 88678400 20449 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21650 20449 603 41 0 21609 0
vsize: 86600
[startup+500.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24698 0 0 0 49939 69 0 0 25 0 1 0 547448948 89473024 20657 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21844 20657 603 41 0 21803 0
vsize: 87376
[startup+510.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24976 0 0 0 50938 69 0 0 25 0 1 0 547448948 90660864 20935 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22134 20935 603 41 0 22093 0
vsize: 88536
[startup+520.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25230 0 0 0 51938 69 0 0 25 0 1 0 547448948 91725824 21189 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22394 21189 603 41 0 22353 0
vsize: 89576
[startup+530.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25454 0 0 0 52937 71 0 0 25 0 1 0 547448948 92655616 21413 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 21413 603 41 0 22580 0
vsize: 90484
[startup+540.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25850 0 0 0 53936 72 0 0 25 0 1 0 547448948 94265344 21809 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23014 21809 603 41 0 22973 0
vsize: 92056
[startup+550.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26135 0 0 0 54935 73 0 0 25 0 1 0 547448948 95440896 22094 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23301 22094 603 41 0 23260 0
vsize: 93204
[startup+560.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26457 0 0 0 55934 74 0 0 25 0 1 0 547448948 96747520 22416 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23620 22416 603 41 0 23579 0
vsize: 94480
[startup+570.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26688 0 0 0 56934 74 0 0 25 0 1 0 547448948 97685504 22647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23849 22647 603 41 0 23808 0
vsize: 95396
[startup+580.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26917 0 0 0 57934 75 0 0 25 0 1 0 547448948 98619392 22876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24077 22876 603 41 0 24036 0
vsize: 96308
[startup+590.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27139 0 0 0 58934 75 0 0 25 0 1 0 547448948 99561472 23098 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24307 23098 603 41 0 24266 0
vsize: 97228
[startup+600.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27360 0 0 0 59933 76 0 0 25 0 1 0 547448948 100352000 23319 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24500 23319 603 41 0 24459 0
vsize: 98000
[startup+610.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27581 0 0 0 60932 77 0 0 25 0 1 0 547448948 101285888 23540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24728 23540 603 41 0 24687 0
vsize: 98912
[startup+620.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27841 0 0 0 61932 77 0 0 25 0 1 0 547448948 102367232 23800 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24992 23800 603 41 0 24951 0
vsize: 99968
[startup+630.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28053 0 0 0 62931 78 0 0 25 0 1 0 547448948 103301120 24012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 24012 603 41 0 25179 0
vsize: 100880
[startup+640.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28352 0 0 0 63931 79 0 0 25 0 1 0 547448948 104497152 24311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25512 24311 603 41 0 25471 0
vsize: 102048
[startup+650.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28658 0 0 0 64930 80 0 0 25 0 1 0 547448948 105684992 24617 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25802 24617 603 41 0 25761 0
vsize: 103208
[startup+660.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28857 0 0 0 65930 80 0 0 25 0 1 0 547448948 106491904 24816 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25999 24816 603 41 0 25958 0
vsize: 103996
[startup+670.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29120 0 0 0 66929 81 0 0 25 0 1 0 547448948 107569152 25079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26262 25079 603 41 0 26221 0
vsize: 105048
[startup+680.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29376 0 0 0 67929 81 0 0 25 0 1 0 547448948 108650496 25335 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26526 25335 603 41 0 26485 0
vsize: 106104
[startup+690.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29685 0 0 0 68928 82 0 0 25 0 1 0 547448948 109862912 25644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26822 25644 603 41 0 26781 0
vsize: 107288
[startup+700.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30040 0 0 0 69927 83 0 0 25 0 1 0 547448948 111349760 25999 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27185 25999 603 41 0 27144 0
vsize: 108740
[startup+710.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30322 0 0 0 70926 84 0 0 25 0 1 0 547448948 112562176 26281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27481 26281 603 41 0 27440 0
vsize: 109924
[startup+720.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30578 0 0 0 71925 86 0 0 25 0 1 0 547448948 113635328 26537 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27743 26537 603 41 0 27702 0
vsize: 110972
[startup+730.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30792 0 0 0 72925 86 0 0 25 0 1 0 547448948 114462720 26751 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27945 26751 603 41 0 27904 0
vsize: 111780
[startup+740.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31015 0 0 0 73924 87 0 0 25 0 1 0 547448948 115392512 26974 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28172 26974 603 41 0 28131 0
vsize: 112688
[startup+750.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31220 0 0 0 74924 87 0 0 25 0 1 0 547448948 116195328 27179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28368 27179 603 41 0 28327 0
vsize: 113472
[startup+760.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31437 0 0 0 75923 88 0 0 25 0 1 0 547448948 117129216 27396 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28596 27396 603 41 0 28555 0
vsize: 114384
[startup+770.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31654 0 0 0 76923 89 0 0 25 0 1 0 547448948 117940224 27613 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28794 27613 603 41 0 28753 0
vsize: 115176
[startup+780.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31914 0 0 0 77923 89 0 0 25 0 1 0 547448948 118996992 27873 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29052 27873 603 41 0 29011 0
vsize: 116208
[startup+790.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32124 0 0 0 78922 90 0 0 25 0 1 0 547448948 119922688 28083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29278 28083 603 41 0 29237 0
vsize: 117112
[startup+800.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32336 0 0 0 79922 91 0 0 25 0 1 0 547448948 120721408 28295 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29473 28295 603 41 0 29432 0
vsize: 117892
[startup+810.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32554 0 0 0 80921 92 0 0 25 0 1 0 547448948 121659392 28513 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29702 28513 603 41 0 29661 0
vsize: 118808
[startup+820.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32781 0 0 0 81921 93 0 0 25 0 1 0 547448948 122601472 28740 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29932 28740 603 41 0 29891 0
vsize: 119728
[startup+830.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33057 0 0 0 82920 93 0 0 25 0 1 0 547448948 123654144 29016 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30189 29016 603 41 0 30148 0
vsize: 120756
[startup+840.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33266 0 0 0 83920 94 0 0 25 0 1 0 547448948 124575744 29225 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30414 29225 603 41 0 30373 0
vsize: 121656
[startup+850.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33509 0 0 0 84919 94 0 0 25 0 1 0 547448948 125616128 29468 4294967295 134512640 134672761 3221224544 3221223648 134560028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30668 29468 603 41 0 30627 0
vsize: 122672
[startup+860.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33753 0 0 0 85919 95 0 0 25 0 1 0 547448948 126533632 29712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30892 29712 603 41 0 30851 0
vsize: 123568
[startup+870.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33993 0 0 0 86919 95 0 0 25 0 1 0 547448948 127594496 29952 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31151 29952 603 41 0 31110 0
vsize: 124604
[startup+880.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34277 0 0 0 87918 96 0 0 25 0 1 0 547448948 128643072 30236 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31407 30236 603 41 0 31366 0
vsize: 125628
[startup+890.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34529 0 0 0 88918 97 0 0 25 0 1 0 547448948 129716224 30488 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31669 30488 603 41 0 31628 0
vsize: 126676
[startup+900.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34727 0 0 0 89917 97 0 0 25 0 1 0 547448948 130498560 30686 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31860 30686 603 41 0 31819 0
vsize: 127440
[startup+910.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34904 0 0 0 90917 98 0 0 25 0 1 0 547448948 131297280 30863 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32055 30863 603 41 0 32014 0
vsize: 128220
[startup+920.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35071 0 0 0 91916 99 0 0 25 0 1 0 547448948 131960832 31030 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32217 31030 603 41 0 32176 0
vsize: 128868
[startup+930.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35193 0 0 0 92916 99 0 0 25 0 1 0 547448948 132501504 31152 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32349 31152 603 41 0 32308 0
vsize: 129396
[startup+940.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35374 0 0 0 93916 100 0 0 25 0 1 0 547448948 133136384 31333 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32504 31333 603 41 0 32463 0
vsize: 130016
[startup+950.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35578 0 0 0 94915 100 0 0 25 0 1 0 547448948 134041600 31537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32725 31537 603 41 0 32684 0
vsize: 130900
[startup+960.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35762 0 0 0 95915 101 0 0 25 0 1 0 547448948 134819840 31721 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32915 31721 603 41 0 32874 0
vsize: 131660
[startup+970.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35890 0 0 0 96915 101 0 0 25 0 1 0 547448948 135344128 31849 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33043 31849 603 41 0 33002 0
vsize: 132172
[startup+980.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36060 0 0 0 97915 102 0 0 25 0 1 0 547448948 135979008 32019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33198 32019 603 41 0 33157 0
vsize: 132792
[startup+990.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36246 0 0 0 98914 102 0 0 25 0 1 0 547448948 136765440 32205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33390 32205 603 41 0 33349 0
vsize: 133560
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36397 0 0 0 99914 102 0 0 25 0 1 0 547448948 137306112 32356 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33522 32356 603 41 0 33481 0
vsize: 134088
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36540 0 0 0 100914 103 0 0 25 0 1 0 547448948 137916416 32499 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33671 32499 603 41 0 33630 0
vsize: 134684
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36638 0 0 0 101914 103 0 0 25 0 1 0 547448948 138661888 32597 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33853 32597 603 41 0 33812 0
vsize: 135412
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36796 0 0 0 102913 104 0 0 25 0 1 0 547448948 139292672 32755 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34007 32755 603 41 0 33966 0
vsize: 136028
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36983 0 0 0 103913 104 0 0 25 0 1 0 547448948 140087296 32942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34201 32942 603 41 0 34160 0
vsize: 136804
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37139 0 0 0 104913 105 0 0 25 0 1 0 547448948 140611584 33098 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34329 33098 603 41 0 34288 0
vsize: 137316
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37329 0 0 0 105913 105 0 0 25 0 1 0 547448948 141389824 33288 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34519 33288 603 41 0 34478 0
vsize: 138076
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37606 0 0 0 106913 105 0 0 25 0 1 0 547448948 142548992 33565 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34802 33565 603 41 0 34761 0
vsize: 139208
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37823 0 0 0 107912 106 0 0 25 0 1 0 547448948 143462400 33782 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35025 33782 603 41 0 34984 0
vsize: 140100
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38050 0 0 0 108912 107 0 0 25 0 1 0 547448948 144375808 34009 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35248 34009 603 41 0 35207 0
vsize: 140992
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38275 0 0 0 109911 107 0 0 25 0 1 0 547448948 145281024 34234 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35469 34234 603 41 0 35428 0
vsize: 141876
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38493 0 0 0 110910 108 0 0 25 0 1 0 547448948 146219008 34452 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35698 34452 603 41 0 35657 0
vsize: 142792
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38717 0 0 0 111909 109 0 0 25 0 1 0 547448948 147161088 34676 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35928 34676 603 41 0 35887 0
vsize: 143712
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38916 0 0 0 112909 109 0 0 25 0 1 0 547448948 147963904 34875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36124 34875 603 41 0 36083 0
vsize: 144496
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39154 0 0 0 113909 110 0 0 25 0 1 0 547448948 148897792 35113 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36352 35113 603 41 0 36311 0
vsize: 145408
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39282 0 0 0 114908 110 0 0 25 0 1 0 547448948 149438464 35241 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36484 35241 603 41 0 36443 0
vsize: 145936
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39588 0 0 0 115908 111 0 0 25 0 1 0 547448948 150642688 35547 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36778 35547 603 41 0 36737 0
vsize: 147112
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39889 0 0 0 116908 111 0 0 25 0 1 0 547448948 151842816 35848 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37071 35848 603 41 0 37030 0
vsize: 148284
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40223 0 0 0 117907 112 0 0 25 0 1 0 547448948 153313280 36182 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37430 36182 603 41 0 37389 0
vsize: 149720
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40534 0 0 0 118907 113 0 0 25 0 1 0 547448948 154488832 36493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37717 36493 603 41 0 37676 0
vsize: 150868
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23685
Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40791 0 0 0 119907 113 0 0 25 0 1 0 547448948 155537408 36750 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37973 36750 603 41 0 37932 0
vsize: 151892
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 23685
Raw data (stat): 23683 (minisat+) Z 23682 18865 18864 0 -1 12 40794 0 0 0 119907 120 0 0 25 0 1 0 547448948 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.28
CPU user time (s): 1199.07
CPU system time (s): 1.20782
CPU usage (%): 100.012
Max. virtual memory (Kb): 151892
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####