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/submitted/manquinho/primes-dimacs-cnf/normalized-ii32d1.opb
MD5SUM	151e246868267296e134c3c76a3cb289
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	285
Optimality of the best value was proved	NO
Number of terms in the objective function	664
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	664
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	664
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02484
Number of variables	664
Total number of constraints	3035
Number of constraints which are clauses	3035
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 4706

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-13 20:04:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3539 boxname=wulflinc25 idbench=155 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc25/normalized-ii32d1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-ii32d1.opb /oldhome/oroussel/tmp/wulflinc25/normalized-ii32d1.opb
IDLAUNCH: 3539
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907052 kB
Buffers:         32404 kB
Cached:          60856 kB
SwapCached:         36 kB
Active:          43040 kB
Inactive:        53088 kB
HighTotal:      131008 kB
HighFree:        66528 kB
LowTotal:       903652 kB
LowFree:        840524 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            25948 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:24:40 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3539 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3035 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3035     9828 |    1011       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1320   maxlim: 345   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        22 |   12223    42626 |    4074      22      879    40.0 |  0.000 % |
c |       122 |   12223    42626 |    4481     122     4164    34.1 |  0.252 % |
c |       273 |   12223    42626 |    4929     273    12706    46.5 |  0.252 % |
c |       502 |   12223    42626 |    5422     502    24204    48.2 |  0.252 % |
c |       841 |   12223    42626 |    5964     841    36895    43.9 |  0.252 % |
c |      1350 |   12223    42626 |    6561    1350    57885    42.9 |  0.252 % |
c |      2111 |   12223    42626 |    7217    2111    85735    40.6 |  0.252 % |
c ==============================================================================
c [1mFound solution: 318[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 346   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2405 |   12228    42649 |    4076    2405   103796    43.2 |  0.252 % |
c |      2507 |   12228    42649 |    4483    2507   107104    42.7 |  0.302 % |
c ==============================================================================
c [1mFound solution: 316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 348   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2640 |   12232    42675 |    4077    2640   117521    44.5 |  0.302 % |
c |      2740 |   12232    42675 |    4484    2740   125925    46.0 |  0.402 % |
c |      2893 |   12232    42675 |    4933    2893   143569    49.6 |  0.402 % |
c |      3119 |   12232    42675 |    5426    3119   165398    53.0 |  0.402 % |
c |      3457 |   12232    42675 |    5969    3457   175597    50.8 |  0.402 % |
c ==============================================================================
c [1mFound solution: 311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 353   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3500 |   12236    42697 |    4078    3500   177420    50.7 |  0.402 % |
c |      3601 |   12236    42697 |    4485    3601   180146    50.0 |  0.502 % |
c |      3751 |   12236    42697 |    4934    3751   188281    50.2 |  0.502 % |
c |      3976 |   12236    42697 |    5427    3976   197751    49.7 |  0.502 % |
c ==============================================================================
c [1mFound solution: 299[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 365   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4059 |   12239    42724 |    4079    4059   201379    49.6 |  0.502 % |
c |      4159 |   12239    42724 |    4486    4159   207960    50.0 |  0.651 % |
c |      4310 |   12239    42724 |    4935    4310   211373    49.0 |  0.651 % |
c |      4536 |   12239    42724 |    5429    4536   224845    49.6 |  0.651 % |
c |      4874 |   12239    42724 |    5972    4874   242329    49.7 |  0.651 % |
c |      5381 |   12239    42724 |    6569    5381   278616    51.8 |  0.651 % |
c |      6140 |   12239    42724 |    7226    6140   329331    53.6 |  0.651 % |
c |      7281 |   12239    42724 |    7948    7281   363049    49.9 |  0.651 % |
c |      8990 |   12239    42724 |    8743    4949   222848    45.0 |  0.652 % |
c |     11553 |   12239    42724 |    9618    7512   361141    48.1 |  0.651 % |
c |     15398 |   12239    42724 |   10579    6396   272674    42.6 |  0.651 % |
c |     21165 |   12239    42724 |   11637   12163   749504    61.6 |  0.651 % |
c |     29815 |   12239    42724 |   12801    8188   848857   103.7 |  0.651 % |
c |     42789 |   12239    42724 |   14081    7443   753803   101.3 |  0.651 % |
c |     62253 |   12239    42724 |   15489   11358   896826    79.0 |  0.651 % |
c |     91445 |   12239    42724 |   17038    8744   658763    75.3 |  0.651 % |
c |    135234 |   12239    42724 |   18742   15557  1808674   116.3 |  0.651 % |
c |    200919 |   12239    42724 |   20617   12955  1460320   112.7 |  0.651 % |
c |    299448 |   12239    42724 |   22678   13041  1101745    84.5 |  0.651 % |
c |    447237 |   12239    42724 |   24946   17883  2377275   132.9 |  0.651 % |
c ==============================================================================
c [1mFound solution: 298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 366   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    638428 |   12240    42735 |    4080   15613  1727112   110.6 |  0.651 % |
c |    638529 |   12240    42735 |    4488    4005   231202    57.7 |  0.701 % |
c |    638680 |   12240    42735 |    4936    4156   243012    58.5 |  0.701 % |
c |    638905 |   12240    42735 |    5430    4381   259304    59.2 |  0.701 % |
c |    639242 |   12240    42735 |    5973    4718   290347    61.5 |  0.701 % |
c |    639748 |   12240    42735 |    6570    5224   325584    62.3 |  0.701 % |
c |    640508 |   12240    42735 |    7227    5984   372396    62.2 |  0.701 % |
c |    641650 |   12240    42735 |    7950    7126   448298    62.9 |  0.701 % |
c |    643361 |   12240    42735 |    8745    8837   543334    61.5 |  0.701 % |
c |    645923 |   12240    42735 |    9620    6981   407359    58.4 |  0.701 % |
c |    649768 |   12240    42735 |   10582   10826   801353    74.0 |  0.701 % |
c |    655535 |   12240    42735 |   11640   11180   771475    69.0 |  0.701 % |
c |    664184 |   12240    42735 |   12804    7114   947447   133.2 |  0.701 % |
c |    677158 |   12240    42735 |   14085   12946   893921    69.0 |  0.701 % |
c |    696619 |   12240    42735 |   15493    9734   714373    73.4 |  0.701 % |
c |    725811 |   12240    42735 |   17043   13588  1671154   123.0 |  0.701 % |
c |    769603 |   12240    42735 |   18747   10982  1512924   137.8 |  0.701 % |
c |    835289 |   12240    42735 |   20622   16009  1930474   120.6 |  0.701 % |
#### 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.97 0.88 2/54 29628
Raw data (stat): 29628 (runsolver) R 29627 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478698867 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.93 0.97 0.88 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 1138 0 0 0 994 3 0 0 25 0 1 0 478698867 6119424 1116 4294967295 134512640 134672761 3221224576 3221223680 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1494 1117 603 41 0 1453 0
vsize: 5976
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.97 0.88 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 1883 0 0 0 1991 6 0 0 25 0 1 0 478698867 9216000 1861 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2250 1861 603 41 0 2209 0
vsize: 9000
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2082 0 0 0 2990 7 0 0 25 0 1 0 478698867 10027008 2060 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2448 2060 603 41 0 2407 0
vsize: 9792
[startup+40.0008 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2301 0 0 0 3989 8 0 0 25 0 1 0 478698867 10969088 2279 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2279 603 41 0 2637 0
vsize: 10712
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2301 0 0 0 4989 8 0 0 25 0 1 0 478698867 10969088 2279 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2279 603 41 0 2637 0
vsize: 10712
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2301 0 0 0 5988 9 0 0 25 0 1 0 478698867 10969088 2279 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2279 603 41 0 2637 0
vsize: 10712
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 29628
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2301 0 0 0 6988 9 0 0 25 0 1 0 478698867 10969088 2279 4294967295 134512640 134672761 3221224576 3221223680 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2678 2279 603 41 0 2637 0
vsize: 10712
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2385 0 0 0 7987 10 0 0 25 0 1 0 478698867 11235328 2363 4294967295 134512640 134672761 3221224576 3221223592 1075353074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2743 2363 603 41 0 2702 0
vsize: 10972
[startup+90.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2616 0 0 0 8987 10 0 0 25 0 1 0 478698867 12234752 2594 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2594 603 41 0 2946 0
vsize: 11948
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 2817 0 0 0 9986 11 0 0 25 0 1 0 478698867 13045760 2795 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3185 2795 603 41 0 3144 0
vsize: 12740
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3008 0 0 0 10986 12 0 0 25 0 1 0 478698867 13852672 2986 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3382 2986 603 41 0 3341 0
vsize: 13528
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3309 0 0 0 11985 12 0 0 25 0 1 0 478698867 15077376 3287 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3287 603 41 0 3640 0
vsize: 14724
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3406 0 0 0 12985 13 0 0 25 0 1 0 478698867 15478784 3384 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3384 603 41 0 3738 0
vsize: 15116
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3406 0 0 0 13985 13 0 0 25 0 1 0 478698867 15478784 3384 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3384 603 41 0 3738 0
vsize: 15116
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3407 0 0 0 14986 13 0 0 25 0 1 0 478698867 15478784 3385 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3385 603 41 0 3738 0
vsize: 15116
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3407 0 0 0 15986 13 0 0 25 0 1 0 478698867 15478784 3385 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3385 603 41 0 3738 0
vsize: 15116
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3407 0 0 0 16986 13 0 0 25 0 1 0 478698867 15478784 3385 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3385 603 41 0 3738 0
vsize: 15116
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3407 0 0 0 17986 13 0 0 25 0 1 0 478698867 15478784 3385 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3385 603 41 0 3738 0
vsize: 15116
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3408 0 0 0 18986 13 0 0 25 0 1 0 478698867 15478784 3386 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3386 603 41 0 3738 0
vsize: 15116
[startup+199.999 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3408 0 0 0 19986 13 0 0 25 0 1 0 478698867 15478784 3386 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3386 603 41 0 3738 0
vsize: 15116
[startup+209.999 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3477 0 0 0 20987 13 0 0 25 0 1 0 478698867 15749120 3455 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3845 3455 603 41 0 3804 0
vsize: 15380
[startup+219.999 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3759 0 0 0 21985 14 0 0 25 0 1 0 478698867 16969728 3737 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4143 3737 603 41 0 4102 0
vsize: 16572
[startup+229.999 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3800 0 0 0 22985 15 0 0 25 0 1 0 478698867 17104896 3778 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3778 603 41 0 4135 0
vsize: 16704
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3800 0 0 0 23985 15 0 0 25 0 1 0 478698867 17104896 3778 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3778 603 41 0 4135 0
vsize: 16704
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3802 0 0 0 24986 15 0 0 25 0 1 0 478698867 17104896 3780 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3780 603 41 0 4135 0
vsize: 16704
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3802 0 0 0 25986 15 0 0 25 0 1 0 478698867 17104896 3780 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3780 603 41 0 4135 0
vsize: 16704
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3802 0 0 0 26986 15 0 0 25 0 1 0 478698867 17104896 3780 4294967295 134512640 134672761 3221224576 3221223152 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3780 603 41 0 4135 0
vsize: 16704
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3802 0 0 0 27986 15 0 0 25 0 1 0 478698867 17104896 3780 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3780 603 41 0 4135 0
vsize: 16704
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3802 0 0 0 28986 15 0 0 25 0 1 0 478698867 17104896 3780 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4176 3780 603 41 0 4135 0
vsize: 16704
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3888 0 0 0 29986 15 0 0 25 0 1 0 478698867 17506304 3866 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4274 3866 603 41 0 4233 0
vsize: 17096
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 3919 0 0 0 30986 15 0 0 25 0 1 0 478698867 17641472 3897 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4307 3897 603 41 0 4266 0
vsize: 17228
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4174 0 0 0 31986 16 0 0 25 0 1 0 478698867 18714624 4152 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4152 603 41 0 4528 0
vsize: 18276
[startup+329.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4174 0 0 0 32986 16 0 0 25 0 1 0 478698867 18714624 4152 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4152 603 41 0 4528 0
vsize: 18276
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4174 0 0 0 33986 16 0 0 25 0 1 0 478698867 18714624 4152 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4152 603 41 0 4528 0
vsize: 18276
[startup+349.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4174 0 0 0 34985 16 0 0 25 0 1 0 478698867 18714624 4152 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4152 603 41 0 4528 0
vsize: 18276
[startup+359.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4176 0 0 0 35986 16 0 0 25 0 1 0 478698867 18714624 4154 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4154 603 41 0 4528 0
vsize: 18276
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4177 0 0 0 36986 16 0 0 25 0 1 0 478698867 18714624 4155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4155 603 41 0 4528 0
vsize: 18276
[startup+379.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4177 0 0 0 37986 16 0 0 25 0 1 0 478698867 18714624 4155 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4155 603 41 0 4528 0
vsize: 18276
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4177 0 0 0 38986 16 0 0 25 0 1 0 478698867 18714624 4155 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4569 4155 603 41 0 4528 0
vsize: 18276
[startup+399.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4224 0 0 0 39986 16 0 0 25 0 1 0 478698867 18849792 4202 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4602 4202 603 41 0 4561 0
vsize: 18408
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4474 0 0 0 40986 17 0 0 25 0 1 0 478698867 19910656 4452 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4861 4452 603 41 0 4820 0
vsize: 19444
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4478 0 0 0 41986 17 0 0 25 0 1 0 478698867 19910656 4456 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4861 4456 603 41 0 4820 0
vsize: 19444
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4478 0 0 0 42986 17 0 0 25 0 1 0 478698867 19910656 4456 4294967295 134512640 134672761 3221224576 3221223712 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4861 4456 603 41 0 4820 0
vsize: 19444
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4502 0 0 0 43986 17 0 0 25 0 1 0 478698867 20045824 4480 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4894 4480 603 41 0 4853 0
vsize: 19576
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4502 0 0 0 44986 17 0 0 25 0 1 0 478698867 20045824 4480 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4894 4480 603 41 0 4853 0
vsize: 19576
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4502 0 0 0 45987 17 0 0 25 0 1 0 478698867 20045824 4480 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4894 4480 603 41 0 4853 0
vsize: 19576
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4502 0 0 0 46987 17 0 0 25 0 1 0 478698867 20045824 4480 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4894 4480 603 41 0 4853 0
vsize: 19576
[startup+479.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4903 0 0 0 47985 18 0 0 25 0 1 0 478698867 21663744 4881 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5289 4881 603 41 0 5248 0
vsize: 21156
[startup+489.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 4903 0 0 0 48986 18 0 0 25 0 1 0 478698867 21663744 4881 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5289 4881 603 41 0 5248 0
vsize: 21156
[startup+499.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5331 0 0 0 49985 19 0 0 25 0 1 0 478698867 23392256 5309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5711 5309 603 41 0 5670 0
vsize: 22844
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5331 0 0 0 50985 19 0 0 25 0 1 0 478698867 23392256 5309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5711 5309 603 41 0 5670 0
vsize: 22844
[startup+519.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5331 0 0 0 51985 19 0 0 25 0 1 0 478698867 23392256 5309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5711 5309 603 41 0 5670 0
vsize: 22844
[startup+529.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 52985 19 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 53985 19 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 54986 19 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 55986 19 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+569.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 56986 19 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5398 0 0 0 57986 20 0 0 25 0 1 0 478698867 23658496 5376 4294967295 134512640 134672761 3221224576 3221223744 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5376 603 41 0 5735 0
vsize: 23104
[startup+589.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 58986 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223680 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+599.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 59986 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+609.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 60986 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+619.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 61986 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+629.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 62986 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+639.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 63987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+649.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 64987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+659.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 65987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+669.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 66987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+679.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 67987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+689.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 68987 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223648 134553532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+699.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 69988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223680 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+709.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 70988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+719.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 71988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+729.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 72988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+739.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 73988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+749.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 74988 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+759.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 75989 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+769.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 76989 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+779.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 77989 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+789.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 78989 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+799.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 79989 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+809.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 80990 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+819.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5400 0 0 0 81990 20 0 0 25 0 1 0 478698867 23658496 5378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 5378 603 41 0 5735 0
vsize: 23104
[startup+829.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5488 0 0 0 82990 20 0 0 25 0 1 0 478698867 24059904 5466 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5466 603 41 0 5833 0
vsize: 23496
[startup+839.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5495 0 0 0 83990 20 0 0 25 0 1 0 478698867 24059904 5473 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5473 603 41 0 5833 0
vsize: 23496
[startup+849.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5495 0 0 0 84990 20 0 0 25 0 1 0 478698867 24059904 5473 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5473 603 41 0 5833 0
vsize: 23496
[startup+859.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 85990 20 0 0 25 0 1 0 478698867 24326144 5537 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5939 5537 603 41 0 5898 0
vsize: 23756
[startup+869.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 86990 20 0 0 25 0 1 0 478698867 24326144 5537 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5939 5537 603 41 0 5898 0
vsize: 23756
[startup+879.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 87990 20 0 0 25 0 1 0 478698867 24326144 5537 4294967295 134512640 134672761 3221224576 3221223680 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5939 5537 603 41 0 5898 0
vsize: 23756
[startup+889.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 88990 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+899.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 89990 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223680 134559910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+909.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 90991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+919.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 91991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+929.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 92991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+939.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 93991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+949.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 94991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+959.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 95991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+969.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 96991 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+979.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 97992 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+989.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 98992 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223680 134555114 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+999.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 99992 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 100992 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 101992 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 102993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 103993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 104993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 105993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 106993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 107993 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 108994 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 109994 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 110994 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 111994 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 112994 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 113995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 114995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 115995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 116995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 117995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 5559 0 0 0 118995 20 0 0 25 0 1 0 478698867 24182784 5513 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5513 603 41 0 5863 0
vsize: 23616
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29630
Raw data (stat): 29628 (minisat+) R 29627 28099 28098 0 -1 0 6028 0 0 0 119994 22 0 0 25 0 1 0 478698867 26202112 5982 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6397 5982 603 41 0 6356 0
vsize: 25588
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29630
Raw data (stat): 29628 (minisat+) Z 29627 28099 28098 0 -1 12 6031 0 0 0 119994 23 0 0 25 0 1 0 478698867 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.01
CPU time (s): 1200.18
CPU user time (s): 1199.94
CPU system time (s): 0.238963
CPU usage (%): 100.015
Max. virtual memory (Kb): 25588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####