PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-22 03:17:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11622 boxname=wulflinc23 idbench=894 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-air01.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-air01.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-air01.opb
IDLAUNCH: 11622
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        299032 kB
Buffers:         29272 kB
Cached:         682616 kB
SwapCached:        548 kB
Active:         128976 kB
Inactive:       584904 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        298780 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16208 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:37:37 (client local time) WITH STATUS 10 IN 1200.4 SECONDS
stats: 11622 7 1200.4 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.85 0.97 0.91 2/54 22293
Raw data (stat): 22293 (runsolver) R 22292 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550416135 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.9996 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 6750 0 0 0 982 17 0 0 25 0 1 0 550416135 25702400 4993 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6275 4993 603 41 0 6234 0
vsize: 25100
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 7848 0 0 0 1978 21 0 0 25 0 1 0 550416135 26243072 5128 4294967295 134512640 134672761 3221224544 3221221984 134523140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6407 5128 603 41 0 6366 0
vsize: 25628
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 8095 0 0 0 2977 22 0 0 25 0 1 0 550416135 27283456 5375 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6661 5375 603 41 0 6620 0
vsize: 26644
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 9250 0 0 0 3974 25 0 0 25 0 1 0 550416135 31084544 6268 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7589 6268 603 41 0 7548 0
vsize: 30356
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 9854 0 0 0 4972 27 0 0 25 0 1 0 550416135 32833536 6693 4294967295 134512640 134672761 3221224544 3221222800 134544702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8016 6693 603 41 0 7975 0
vsize: 32064
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 10177 0 0 0 5972 28 0 0 25 0 1 0 550416135 34160640 7016 4294967295 134512640 134672761 3221224544 3221223648 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8340 7016 603 41 0 8299 0
vsize: 33360
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 10688 0 0 0 6970 29 0 0 25 0 1 0 550416135 35352576 7322 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8631 7322 603 41 0 8590 0
vsize: 34524
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 11011 0 0 0 7969 30 0 0 25 0 1 0 550416135 36765696 7640 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8976 7640 603 41 0 8935 0
vsize: 35904
[startup+90.0036 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 11486 0 0 0 8968 32 0 0 25 0 1 0 550416135 38649856 8115 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9436 8115 603 41 0 9395 0
vsize: 37744
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 11759 0 0 0 9967 33 0 0 25 0 1 0 550416135 39854080 8388 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9730 8388 603 41 0 9689 0
vsize: 38920
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 12868 0 0 0 10964 36 0 0 25 0 1 0 550416135 42946560 9286 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10485 9286 603 41 0 10444 0
vsize: 41940
[startup+120.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 13179 0 0 0 11964 37 0 0 25 0 1 0 550416135 44208128 9597 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10793 9597 603 41 0 10752 0
vsize: 43172
[startup+130.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 13573 0 0 0 12963 38 0 0 25 0 1 0 550416135 45920256 9991 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11211 9991 603 41 0 11170 0
vsize: 44844
[startup+140.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 13910 0 0 0 13962 39 0 0 25 0 1 0 550416135 47202304 10328 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11524 10328 603 41 0 11483 0
vsize: 46096
[startup+150.013 s]
Raw data (loadavg): 0.98 0.97 0.91 3/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 14300 0 0 0 14960 41 0 0 25 0 1 0 550416135 48779264 10718 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11909 10718 603 41 0 11868 0
vsize: 47636
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 14752 0 0 0 15959 42 0 0 25 0 1 0 550416135 49741824 10949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12144 10949 603 41 0 12103 0
vsize: 48576
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 15179 0 0 0 16957 44 0 0 25 0 1 0 550416135 50446336 11138 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12316 11138 603 41 0 12275 0
vsize: 49264
[startup+180.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 15327 0 0 0 17957 45 0 0 25 0 1 0 550416135 50982912 11286 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12447 11286 603 41 0 12406 0
vsize: 49788
[startup+190.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 15605 0 0 0 18958 45 0 0 25 0 1 0 550416135 52162560 11564 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 11564 603 41 0 12694 0
vsize: 50940
[startup+200.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 15775 0 0 0 19959 46 0 0 25 0 1 0 550416135 52826112 11734 4294967295 134512640 134672761 3221224544 3221223712 134559131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12897 11734 603 41 0 12856 0
vsize: 51588
[startup+210.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 16007 0 0 0 20959 46 0 0 25 0 1 0 550416135 53764096 11966 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13126 11966 603 41 0 13085 0
vsize: 52504
[startup+220.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 16240 0 0 0 21958 47 0 0 25 0 1 0 550416135 54829056 12199 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13386 12199 603 41 0 13345 0
vsize: 53544
[startup+230.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 16537 0 0 0 22958 48 0 0 25 0 1 0 550416135 56086528 12496 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13693 12496 603 41 0 13652 0
vsize: 54772
[startup+240.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 16856 0 0 0 23958 49 0 0 25 0 1 0 550416135 57405440 12815 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14015 12815 603 41 0 13974 0
vsize: 56060
[startup+250.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 16976 0 0 0 24958 49 0 0 25 0 1 0 550416135 57806848 12935 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14113 12935 603 41 0 14072 0
vsize: 56452
[startup+260.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 17268 0 0 0 25957 51 0 0 25 0 1 0 550416135 59006976 13227 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13227 603 41 0 14365 0
vsize: 57624
[startup+270.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 17594 0 0 0 26960 52 0 0 25 0 1 0 550416135 60325888 13553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14728 13553 603 41 0 14687 0
vsize: 58912
[startup+280.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 17995 0 0 0 27959 52 0 0 25 0 1 0 550416135 61952000 13954 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15125 13954 603 41 0 15084 0
vsize: 60500
[startup+290.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 18302 0 0 0 28958 53 0 0 25 0 1 0 550416135 63254528 14261 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15443 14261 603 41 0 15402 0
vsize: 61772
[startup+300.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 18615 0 0 0 29958 54 0 0 25 0 1 0 550416135 64589824 14574 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15769 14574 603 41 0 15728 0
vsize: 63076
[startup+310.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 19011 0 0 0 30957 55 0 0 25 0 1 0 550416135 66179072 14970 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16157 14970 603 41 0 16116 0
vsize: 64628
[startup+320.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 19342 0 0 0 31956 56 0 0 25 0 1 0 550416135 67457024 15301 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16469 15301 603 41 0 16428 0
vsize: 65876
[startup+330.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 19748 0 0 0 32955 57 0 0 25 0 1 0 550416135 69181440 15707 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16890 15707 603 41 0 16849 0
vsize: 67560
[startup+340.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 20014 0 0 0 33955 58 0 0 25 0 1 0 550416135 70307840 15973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17165 15973 603 41 0 17124 0
vsize: 68660
[startup+350.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 20398 0 0 0 34954 59 0 0 25 0 1 0 550416135 71786496 16357 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17526 16357 603 41 0 17485 0
vsize: 70104
[startup+360.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 20758 0 0 0 35953 60 0 0 25 0 1 0 550416135 73269248 16717 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17888 16717 603 41 0 17847 0
vsize: 71552
[startup+370.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 21005 0 0 0 36954 60 0 0 25 0 1 0 550416135 74338304 16964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18149 16964 603 41 0 18108 0
vsize: 72596
[startup+380.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 21242 0 0 0 37954 61 0 0 25 0 1 0 550416135 75239424 17201 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18369 17201 603 41 0 18328 0
vsize: 73476
[startup+390.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 21481 0 0 0 38953 62 0 0 25 0 1 0 550416135 76271616 17440 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18621 17440 603 41 0 18580 0
vsize: 74484
[startup+400.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 21742 0 0 0 39953 63 0 0 25 0 1 0 550416135 77332480 17701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18880 17701 603 41 0 18839 0
vsize: 75520
[startup+410.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 22036 0 0 0 40952 63 0 0 25 0 1 0 550416135 78532608 17995 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19173 17995 603 41 0 19132 0
vsize: 76692
[startup+420.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 22276 0 0 0 41951 64 0 0 25 0 1 0 550416135 79466496 18235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19401 18235 603 41 0 19360 0
vsize: 77604
[startup+430.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 22564 0 0 0 42951 65 0 0 25 0 1 0 550416135 80678912 18523 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19697 18523 603 41 0 19656 0
vsize: 78788
[startup+440.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 22872 0 0 0 43950 66 0 0 25 0 1 0 550416135 81956864 18831 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20009 18831 603 41 0 19968 0
vsize: 80036
[startup+450.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 23155 0 0 0 44950 66 0 0 25 0 1 0 550416135 83148800 19114 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20300 19114 603 41 0 20259 0
vsize: 81200
[startup+460.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 23433 0 0 0 45950 67 0 0 25 0 1 0 550416135 84336640 19392 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20590 19392 603 41 0 20549 0
vsize: 82360
[startup+470.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 23747 0 0 0 46949 67 0 0 25 0 1 0 550416135 85651456 19706 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20911 19706 603 41 0 20870 0
vsize: 83644
[startup+480.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 24039 0 0 0 47949 68 0 0 25 0 1 0 550416135 86831104 19998 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21199 19998 603 41 0 21158 0
vsize: 84796
[startup+490.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 24349 0 0 0 48948 69 0 0 25 0 1 0 550416135 88145920 20308 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21520 20308 603 41 0 21479 0
vsize: 86080
[startup+500.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 24586 0 0 0 49948 69 0 0 25 0 1 0 550416135 89067520 20545 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21745 20545 603 41 0 21704 0
vsize: 86980
[startup+510.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 24812 0 0 0 50947 70 0 0 25 0 1 0 550416135 89993216 20771 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21971 20771 603 41 0 21930 0
vsize: 87884
[startup+520.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 25106 0 0 0 51946 71 0 0 25 0 1 0 550416135 91185152 21065 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22262 21065 603 41 0 22221 0
vsize: 89048
[startup+530.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 25338 0 0 0 52945 72 0 0 25 0 1 0 550416135 92123136 21297 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22491 21297 603 41 0 22450 0
vsize: 89964
[startup+540.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 25625 0 0 0 53944 73 0 0 25 0 1 0 550416135 93335552 21584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22787 21584 603 41 0 22746 0
vsize: 91148
[startup+550.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 25976 0 0 0 54944 74 0 0 25 0 1 0 550416135 94773248 21935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23138 21935 603 41 0 23097 0
vsize: 92552
[startup+560.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 26274 0 0 0 55944 74 0 0 25 0 1 0 550416135 95977472 22233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23432 22233 603 41 0 23391 0
vsize: 93728
[startup+570.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 26560 0 0 0 56943 75 0 0 25 0 1 0 550416135 97153024 22519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23719 22519 603 41 0 23678 0
vsize: 94876
[startup+580.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 26782 0 0 0 57943 75 0 0 25 0 1 0 550416135 98086912 22741 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23947 22741 603 41 0 23906 0
vsize: 95788
[startup+590.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 27011 0 0 0 58943 76 0 0 25 0 1 0 550416135 99024896 22970 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24176 22970 603 41 0 24135 0
vsize: 96704
[startup+600.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 27234 0 0 0 59942 77 0 0 25 0 1 0 550416135 99831808 23193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24373 23193 603 41 0 24332 0
vsize: 97492
[startup+610.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 27433 0 0 0 60941 78 0 0 25 0 1 0 550416135 100749312 23392 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24597 23392 603 41 0 24556 0
vsize: 98388
[startup+620.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 27677 0 0 0 61941 79 0 0 25 0 1 0 550416135 101691392 23636 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24827 23636 603 41 0 24786 0
vsize: 99308
[startup+630.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 27920 0 0 0 62941 79 0 0 25 0 1 0 550416135 102764544 23879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25089 23879 603 41 0 25048 0
vsize: 100356
[startup+640.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 28116 0 0 0 63941 80 0 0 25 0 1 0 550416135 103571456 24075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25286 24075 603 41 0 25245 0
vsize: 101144
[startup+650.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 28454 0 0 0 64940 80 0 0 25 0 1 0 550416135 104902656 24413 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25611 24413 603 41 0 25570 0
vsize: 102444
[startup+660.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 28730 0 0 0 65940 81 0 0 25 0 1 0 550416135 105959424 24689 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25869 24689 603 41 0 25828 0
vsize: 103476
[startup+670.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 28915 0 0 0 66940 81 0 0 25 0 1 0 550416135 106762240 24874 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26065 24874 603 41 0 26024 0
vsize: 104260
[startup+680.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 29207 0 0 0 67939 82 0 0 25 0 1 0 550416135 107974656 25166 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26361 25166 603 41 0 26320 0
vsize: 105444
[startup+690.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 29463 0 0 0 68939 83 0 0 25 0 1 0 550416135 109056000 25422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26625 25422 603 41 0 26584 0
vsize: 106500
[startup+700.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 29778 0 0 0 69938 84 0 0 25 0 1 0 550416135 110268416 25737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26921 25737 603 41 0 26880 0
vsize: 107684
[startup+710.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 30104 0 0 0 70938 84 0 0 25 0 1 0 550416135 111616000 26063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27250 26063 603 41 0 27209 0
vsize: 109000
[startup+720.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 30384 0 0 0 71937 85 0 0 25 0 1 0 550416135 112832512 26343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27547 26343 603 41 0 27506 0
vsize: 110188
[startup+730.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 30616 0 0 0 72937 86 0 0 25 0 1 0 550416135 113770496 26575 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27776 26575 603 41 0 27735 0
vsize: 111104
[startup+740.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 30843 0 0 0 73936 86 0 0 25 0 1 0 550416135 114593792 26802 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27977 26802 603 41 0 27936 0
vsize: 111908
[startup+750.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 31053 0 0 0 74936 87 0 0 25 0 1 0 550416135 115527680 27012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28205 27012 603 41 0 28164 0
vsize: 112820
[startup+760.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 31260 0 0 0 75935 88 0 0 25 0 1 0 550416135 116330496 27219 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28401 27219 603 41 0 28360 0
vsize: 113604
[startup+770.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 31474 0 0 0 76935 88 0 0 25 0 1 0 550416135 117264384 27433 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28629 27433 603 41 0 28588 0
vsize: 114516
[startup+780.157 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 31698 0 0 0 77934 89 0 0 25 0 1 0 550416135 118198272 27657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28857 27657 603 41 0 28816 0
vsize: 115428
[startup+790.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 31950 0 0 0 78934 89 0 0 25 0 1 0 550416135 119123968 27909 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29083 27909 603 41 0 29042 0
vsize: 116332
[startup+800.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 32154 0 0 0 79934 89 0 0 25 0 1 0 550416135 120049664 28113 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29309 28113 603 41 0 29268 0
vsize: 117236
[startup+810.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 32358 0 0 0 80934 89 0 0 25 0 1 0 550416135 120856576 28317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29506 28317 603 41 0 29465 0
vsize: 118024
[startup+820.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 32579 0 0 0 81934 90 0 0 25 0 1 0 550416135 121786368 28538 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29733 28538 603 41 0 29692 0
vsize: 118932
[startup+830.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 32805 0 0 0 82933 90 0 0 25 0 1 0 550416135 122736640 28764 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29965 28764 603 41 0 29924 0
vsize: 119860
[startup+840.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 33082 0 0 0 83933 91 0 0 25 0 1 0 550416135 123793408 29041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30223 29041 603 41 0 30182 0
vsize: 120892
[startup+850.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 33284 0 0 0 84932 92 0 0 25 0 1 0 550416135 124710912 29243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30447 29243 603 41 0 30406 0
vsize: 121788
[startup+860.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 33531 0 0 0 85932 93 0 0 25 0 1 0 550416135 125616128 29490 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30668 29490 603 41 0 30627 0
vsize: 122672
[startup+870.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 33776 0 0 0 86931 93 0 0 25 0 1 0 550416135 126660608 29735 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30923 29735 603 41 0 30882 0
vsize: 123692
[startup+880.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 34009 0 0 0 87931 94 0 0 25 0 1 0 550416135 127594496 29968 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31151 29968 603 41 0 31110 0
vsize: 124604
[startup+890.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 34299 0 0 0 88930 95 0 0 25 0 1 0 550416135 128782336 30258 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31441 30258 603 41 0 31400 0
vsize: 125764
[startup+900.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 34538 0 0 0 89930 95 0 0 25 0 1 0 550416135 129835008 30497 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31698 30497 603 41 0 31657 0
vsize: 126792
[startup+910.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 34736 0 0 0 90929 96 0 0 25 0 1 0 550416135 130629632 30695 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31892 30695 603 41 0 31851 0
vsize: 127568
[startup+920.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 34909 0 0 0 91929 97 0 0 25 0 1 0 550416135 131297280 30868 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32055 30868 603 41 0 32014 0
vsize: 128220
[startup+930.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35074 0 0 0 92929 97 0 0 25 0 1 0 550416135 131960832 31033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32217 31033 603 41 0 32176 0
vsize: 128868
[startup+940.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35193 0 0 0 93929 97 0 0 25 0 1 0 550416135 132501504 31152 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32349 31152 603 41 0 32308 0
vsize: 129396
[startup+950.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35374 0 0 0 94929 97 0 0 25 0 1 0 550416135 133136384 31333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32504 31333 603 41 0 32463 0
vsize: 130016
[startup+960.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35578 0 0 0 95928 98 0 0 25 0 1 0 550416135 134041600 31537 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32725 31537 603 41 0 32684 0
vsize: 130900
[startup+970.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35762 0 0 0 96928 99 0 0 25 0 1 0 550416135 134819840 31721 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32915 31721 603 41 0 32874 0
vsize: 131660
[startup+980.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 35885 0 0 0 97928 99 0 0 25 0 1 0 550416135 135208960 31844 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33010 31844 603 41 0 32969 0
vsize: 132040
[startup+990.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36056 0 0 0 98928 99 0 0 25 0 1 0 550416135 135979008 32015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33198 32015 603 41 0 33157 0
vsize: 132792
[startup+1000.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36239 0 0 0 99927 100 0 0 25 0 1 0 550416135 136765440 32198 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33390 32198 603 41 0 33349 0
vsize: 133560
[startup+1010.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36389 0 0 0 100927 100 0 0 25 0 1 0 550416135 137306112 32348 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33522 32348 603 41 0 33481 0
vsize: 134088
[startup+1020.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36537 0 0 0 101927 101 0 0 25 0 1 0 550416135 137916416 32496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33671 32496 603 41 0 33630 0
vsize: 134684
[startup+1030.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36625 0 0 0 102927 101 0 0 25 0 1 0 550416135 138543104 32584 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33824 32584 603 41 0 33783 0
vsize: 135296
[startup+1040.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36786 0 0 0 103927 102 0 0 25 0 1 0 550416135 139165696 32745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33976 32745 603 41 0 33935 0
vsize: 135904
[startup+1050.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 36960 0 0 0 104926 102 0 0 25 0 1 0 550416135 139952128 32919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34168 32919 603 41 0 34127 0
vsize: 136672
[startup+1060.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 37139 0 0 0 105926 102 0 0 25 0 1 0 550416135 140611584 33098 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34329 33098 603 41 0 34288 0
vsize: 137316
[startup+1070.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 37301 0 0 0 106926 103 0 0 25 0 1 0 550416135 141258752 33260 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34487 33260 603 41 0 34446 0
vsize: 137948
[startup+1080.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 37572 0 0 0 107925 104 0 0 25 0 1 0 550416135 142426112 33531 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34772 33531 603 41 0 34731 0
vsize: 139088
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 37800 0 0 0 108924 105 0 0 25 0 1 0 550416135 143343616 33759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34996 33759 603 41 0 34955 0
vsize: 139984
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 38025 0 0 0 109923 106 0 0 25 0 1 0 550416135 144257024 33984 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35219 33984 603 41 0 35178 0
vsize: 140876
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 38238 0 0 0 110923 106 0 0 25 0 1 0 550416135 145154048 34197 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35438 34197 603 41 0 35397 0
vsize: 141752
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 38455 0 0 0 111922 107 0 0 25 0 1 0 550416135 146083840 34414 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35665 34414 603 41 0 35624 0
vsize: 142660
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 38677 0 0 0 112922 108 0 0 25 0 1 0 550416135 146890752 34636 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35862 34636 603 41 0 35821 0
vsize: 143448
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 38886 0 0 0 113921 108 0 0 25 0 1 0 550416135 147828736 34845 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36091 34845 603 41 0 36050 0
vsize: 144364
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 39117 0 0 0 114922 109 0 0 25 0 1 0 550416135 148766720 35076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36320 35076 603 41 0 36279 0
vsize: 145280
[startup+1160.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 39260 0 0 0 115922 109 0 0 25 0 1 0 550416135 149303296 35219 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36451 35219 603 41 0 36410 0
vsize: 145804
[startup+1170.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 39520 0 0 0 116921 110 0 0 25 0 1 0 550416135 150376448 35479 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36713 35479 603 41 0 36672 0
vsize: 146852
[startup+1180.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 39827 0 0 0 117921 111 0 0 25 0 1 0 550416135 151576576 35786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37006 35786 603 41 0 36965 0
vsize: 148024
[startup+1190.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 40145 0 0 0 118920 111 0 0 25 0 1 0 550416135 152907776 36104 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37331 36104 603 41 0 37290 0
vsize: 149324
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22293
Raw data (stat): 22293 (minisat+) R 22292 3260 3259 0 -1 0 40454 0 0 0 119919 112 0 0 25 0 1 0 550416135 154230784 36413 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37654 36413 603 41 0 37613 0
vsize: 150616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22293
Raw data (stat): 22293 (minisat+) Z 22292 3260 3259 0 -1 12 40457 0 0 0 119920 119 0 0 25 0 1 0 550416135 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.25
CPU time (s): 1200.4
CPU user time (s): 1199.2
CPU system time (s): 1.19782
CPU usage (%): 100.013
Max. virtual memory (Kb): 150616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####