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-jnh217.opb
MD5SUM	c4040960fadc5a0c2fe39dd858a66385
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	89
Optimality of the best value was proved	NO
Number of terms in the objective function	200
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	200
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	200
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	200
Total number of constraints	900
Number of constraints which are clauses	900
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	11
Trace number 5142

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 22:13:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3572 boxname=wulflinc20 idbench=188 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c4040960fadc5a0c2fe39dd858a66385  /oldhome/oroussel/tmp/wulflinc20/normalized-jnh217.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-jnh217.opb /oldhome/oroussel/tmp/wulflinc20/normalized-jnh217.opb
IDLAUNCH: 3572
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        893888 kB
Buffers:         33720 kB
Cached:          71560 kB
SwapCached:       2636 kB
Active:          45824 kB
Inactive:        64992 kB
HighTotal:      131008 kB
HighFree:        55636 kB
LowTotal:       903652 kB
LowFree:        838252 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24340 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:33:09 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3572 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 900 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 |     900     4139 |     300       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 95[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 394   maxlim: 105   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        58 |    3614    13816 |    1204      58      697    12.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 94[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 106   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       148 |    3619    13837 |    1206     148     3026    20.4 |  0.000 % |
c |       249 |    3619    13837 |    1326     249     3963    15.9 |  0.835 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 107   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       252 |    3620    13844 |    1206     252     4006    15.9 |  0.835 % |
c ==============================================================================
c [1mFound solution: 92[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 108   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       259 |    3623    13859 |    1207     259     4097    15.8 |  0.835 % |
c |       359 |    3623    13859 |    1327     359     7053    19.6 |  1.165 % |
c |       510 |    3623    13859 |    1460     510     8507    16.7 |  1.165 % |
c |       736 |    3623    13859 |    1606     736    18034    24.5 |  1.165 % |
c |      1073 |    3623    13859 |    1767    1073    31109    29.0 |  1.165 % |
c |      1580 |    3623    13859 |    1943    1580    37169    23.5 |  1.165 % |
c |      2339 |    3623    13859 |    2138    2339    75523    32.3 |  1.165 % |
c |      3481 |    3623    13859 |    2352    1218    34319    28.2 |  1.165 % |
c |      5191 |    3623    13859 |    2587    1573    53572    34.1 |  1.165 % |
c |      7753 |    3623    13859 |    2846    2668   110699    41.5 |  1.165 % |
c |     11599 |    3623    13859 |    3130    2173    65262    30.0 |  1.165 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 109   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12818 |    3624    13867 |    1208    1787    32038    17.9 |  1.165 % |
c |     12918 |    3624    13867 |    1328     994     9952    10.0 |  1.329 % |
c |     13068 |    3624    13867 |    1461    1144    11802    10.3 |  1.329 % |
c |     13294 |    3624    13867 |    1607    1370    20558    15.0 |  1.329 % |
c |     13631 |    3624    13867 |    1768     866    13820    16.0 |  1.329 % |
c |     14139 |    3624    13867 |    1945    1374    29662    21.6 |  1.329 % |
c |     14900 |    3624    13867 |    2140    2135    53555    25.1 |  1.329 % |
c |     16039 |    3624    13867 |    2354    2186    79083    36.2 |  1.329 % |
c |     17747 |    3624    13867 |    2589    1339    24990    18.7 |  1.329 % |
c |     20309 |    3624    13867 |    2848    2522    91814    36.4 |  1.329 % |
c |     24153 |    3624    13867 |    3133    2006    60226    30.0 |  1.329 % |
c |     29921 |    3624    13867 |    3446    2672    99944    37.4 |  1.329 % |
c |     38571 |    3624    13867 |    3791    2394    69119    28.9 |  1.329 % |
c |     51545 |    3624    13867 |    4170    2972   133633    45.0 |  1.329 % |
c |     71007 |    3624    13867 |    4587    2559    89687    35.0 |  1.330 % |
c |    100200 |    3624    13867 |    5046    2743    65556    23.9 |  1.329 % |
c |    143990 |    3624    13867 |    5550    4838   169156    35.0 |  1.329 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 110   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180832 |    3625    13876 |    1208    3661   109859    30.0 |  1.329 % |
c |    180933 |    3625    13876 |    1328    1017    10182    10.0 |  1.493 % |
c |    181083 |    3625    13876 |    1461    1167    14532    12.5 |  1.493 % |
c |    181311 |    3625    13876 |    1607    1395    16800    12.0 |  1.493 % |
c |    181648 |    3625    13876 |    1768    1732    33146    19.1 |  1.498 % |
c |    182154 |    3625    13876 |    1945    1338    13657    10.2 |  1.493 % |
c |    182913 |    3625    13876 |    2140    1106     9993     9.0 |  1.493 % |
c |    184054 |    3625    13876 |    2354    2247    55698    24.8 |  1.493 % |
c |    185763 |    3625    13876 |    2589    1517    21739    14.3 |  1.493 % |
c |    188325 |    3625    13876 |    2848    2739   102298    37.3 |  1.493 % |
c |    192170 |    3625    13876 |    3133    1846    43049    23.3 |  1.493 % |
c |    197936 |    3625    13876 |    3446    2402    89505    37.3 |  1.493 % |
c |    206587 |    3625    13876 |    3791    1986    59349    29.9 |  1.493 % |
c |    219561 |    3625    13876 |    4170    2953    80896    27.4 |  1.493 % |
c |    239022 |    3625    13876 |    4587    2525    84751    33.6 |  1.493 % |
c |    268215 |    3625    13876 |    5046    4790   258066    53.9 |  1.493 % |
c |    312004 |    3625    13876 |    5550    3164   148730    47.0 |  1.493 % |
c |    377688 |    3589    13690 |    6105    3621   163908    45.3 |  1.824 % |
c |    476214 |    3589    13690 |    6716    4607   176231    38.3 |  1.824 % |
c |    624004 |    3589    13690 |    7388    5384   215092    40.0 |  1.825 % |
c ==============================================================================
c [1mFound solution: 89[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 208   maxlim: 110   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    806187 |    5016    18782 |    1672    4582   183995    40.2 |  1.825 % |
c |    806288 |    5016    18782 |    1839    1247    15885    12.7 |  2.081 % |
c |    806440 |    5016    18782 |    2023    1399    23563    16.8 |  2.081 % |
c |    806668 |    5016    18782 |    2225    1627    26206    16.1 |  2.081 % |
c |    807006 |    5016    18782 |    2447    1965    32470    16.5 |  2.081 % |
c |    807512 |    5016    18782 |    2692    2471    37304    15.1 |  2.081 % |
c |    808272 |    5016    18782 |    2962    1730    42230    24.4 |  2.081 % |
c |    809412 |    5016    18782 |    3258    2870    64035    22.3 |  2.081 % |
c |    811120 |    5016    18782 |    3584    2755    61608    22.4 |  2.081 % |
c |    813682 |    5016    18782 |    3942    3498   106754    30.5 |  2.081 % |
c |    817527 |    5016    18782 |    4336    3028   122452    40.4 |  2.081 % |
c |    823293 |    5016    18782 |    4770    4385   142286    32.4 |  2.081 % |
c |    831943 |    5016    18782 |    5247    3097   135945    43.9 |  2.081 % |
c |    844917 |    5016    18782 |    5772    4808   153957    32.0 |  2.081 % |
c |    864379 |    5016    18782 |    6349    3250    90859    28.0 |  2.081 % |
c |    893571 |    5016    18782 |    6984    6230   195092    31.3 |  2.081 % |
c |    937360 |    5016    18782 |    7682    6775   207829    30.7 |  2.081 % |
c |   1003044 |    5016    18782 |    8451    4591   150386    32.8 |  2.082 % |
c |   1101570 |    5016    18782 |    9296    6870   272138    39.6 |  2.081 % |
c |   1249359 |    5016    18782 |   10225    6376   263257    41.3 |  2.081 % |
c |   1471042 |    5007    18751 |   11248    4239   117255    27.7 |  2.204 % |
c |   1803567 |    4998    18720 |   12373    9419   258385    27.4 |  2.330 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 31295
Raw data (stat): 31295 (runsolver) R 31294 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479459457 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 569 0 0 0 997 1 0 0 25 0 1 0 479459457 3895296 547 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 951 547 603 41 0 910 0
vsize: 3804
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 676 0 0 0 1996 1 0 0 25 0 1 0 479459457 4296704 654 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1049 654 603 41 0 1008 0
vsize: 4196
[startup+30.0004 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 680 0 0 0 2997 1 0 0 25 0 1 0 479459457 4296704 658 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1049 658 603 41 0 1008 0
vsize: 4196
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 684 0 0 0 3996 1 0 0 25 0 1 0 479459457 4296704 662 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1049 662 603 41 0 1008 0
vsize: 4196
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 726 0 0 0 4996 2 0 0 25 0 1 0 479459457 4427776 704 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1081 704 603 41 0 1040 0
vsize: 4324
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 750 0 0 0 5996 2 0 0 25 0 1 0 479459457 4558848 728 4294967295 134512640 134672761 3221224576 3221223760 134559298 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1113 728 603 41 0 1072 0
vsize: 4452
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 806 0 0 0 6996 2 0 0 25 0 1 0 479459457 4825088 784 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1178 784 603 41 0 1137 0
vsize: 4712
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 817 0 0 0 7996 2 0 0 25 0 1 0 479459457 4825088 795 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1178 795 603 41 0 1137 0
vsize: 4712
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 817 0 0 0 8996 2 0 0 25 0 1 0 479459457 4825088 795 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1178 795 603 41 0 1137 0
vsize: 4712
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 817 0 0 0 9996 2 0 0 25 0 1 0 479459457 4825088 795 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1178 795 603 41 0 1137 0
vsize: 4712
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 850 0 0 0 10996 2 0 0 25 0 1 0 479459457 4960256 828 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1211 828 603 41 0 1170 0
vsize: 4844
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 900 0 0 0 11995 3 0 0 25 0 1 0 479459457 5226496 878 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1276 878 603 41 0 1235 0
vsize: 5104
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 900 0 0 0 12995 3 0 0 25 0 1 0 479459457 5226496 878 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1276 878 603 41 0 1235 0
vsize: 5104
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 900 0 0 0 13995 3 0 0 25 0 1 0 479459457 5226496 878 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1276 878 603 41 0 1235 0
vsize: 5104
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 927 0 0 0 14995 3 0 0 25 0 1 0 479459457 5361664 905 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1309 905 603 41 0 1268 0
vsize: 5236
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 927 0 0 0 15995 3 0 0 25 0 1 0 479459457 5361664 905 4294967295 134512640 134672761 3221224576 3221223680 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1309 905 603 41 0 1268 0
vsize: 5236
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 927 0 0 0 16996 3 0 0 25 0 1 0 479459457 5361664 905 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1309 905 603 41 0 1268 0
vsize: 5236
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 994 0 0 0 17995 3 0 0 25 0 1 0 479459457 5619712 972 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 972 603 41 0 1331 0
vsize: 5488
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 994 0 0 0 18996 4 0 0 25 0 1 0 479459457 5619712 972 4294967295 134512640 134672761 3221224576 3221223792 134558131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 972 603 41 0 1331 0
vsize: 5488
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 994 0 0 0 19996 4 0 0 25 0 1 0 479459457 5619712 972 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 972 603 41 0 1331 0
vsize: 5488
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 994 0 0 0 20996 4 0 0 25 0 1 0 479459457 5619712 972 4294967295 134512640 134672761 3221224576 3221223760 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 972 603 41 0 1331 0
vsize: 5488
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 995 0 0 0 21996 4 0 0 25 0 1 0 479459457 5619712 973 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 973 603 41 0 1331 0
vsize: 5488
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 997 0 0 0 22996 4 0 0 25 0 1 0 479459457 5619712 975 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1372 975 603 41 0 1331 0
vsize: 5488
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1029 0 0 0 23996 4 0 0 25 0 1 0 479459457 5750784 1007 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1404 1007 603 41 0 1363 0
vsize: 5616
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1038 0 0 0 24996 4 0 0 25 0 1 0 479459457 5750784 1016 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1404 1016 603 41 0 1363 0
vsize: 5616
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1050 0 0 0 25996 4 0 0 25 0 1 0 479459457 5750784 1028 4294967295 134512640 134672761 3221224576 3221223680 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1404 1028 603 41 0 1363 0
vsize: 5616
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1063 0 0 0 26996 5 0 0 25 0 1 0 479459457 5885952 1041 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1437 1041 603 41 0 1396 0
vsize: 5748
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1071 0 0 0 27996 5 0 0 25 0 1 0 479459457 5885952 1049 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1437 1049 603 41 0 1396 0
vsize: 5748
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1076 0 0 0 28996 5 0 0 25 0 1 0 479459457 5885952 1054 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1437 1054 603 41 0 1396 0
vsize: 5748
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 29996 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 30996 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223680 134554866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 31996 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 32996 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 33997 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223744 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1125 0 0 0 34997 5 0 0 25 0 1 0 479459457 6156288 1103 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1103 603 41 0 1462 0
vsize: 6012
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1167 0 0 0 35997 5 0 0 25 0 1 0 479459457 6291456 1145 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1145 603 41 0 1495 0
vsize: 6144
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1167 0 0 0 36997 5 0 0 25 0 1 0 479459457 6291456 1145 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1145 603 41 0 1495 0
vsize: 6144
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1176 0 0 0 37997 5 0 0 25 0 1 0 479459457 6291456 1154 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1154 603 41 0 1495 0
vsize: 6144
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1178 0 0 0 38997 5 0 0 25 0 1 0 479459457 6291456 1156 4294967295 134512640 134672761 3221224576 3221223760 134559310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1156 603 41 0 1495 0
vsize: 6144
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1181 0 0 0 39997 6 0 0 25 0 1 0 479459457 6291456 1159 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1159 603 41 0 1495 0
vsize: 6144
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 40997 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 41996 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223760 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 42996 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 43996 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 44996 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 45996 6 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1206 0 0 0 46996 7 0 0 25 0 1 0 479459457 6422528 1184 4294967295 134512640 134672761 3221224576 3221223728 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1568 1184 603 41 0 1527 0
vsize: 6272
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1245 0 0 0 47996 7 0 0 25 0 1 0 479459457 6553600 1223 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1600 1223 603 41 0 1559 0
vsize: 6400
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1280 0 0 0 48996 7 0 0 25 0 1 0 479459457 6815744 1258 4294967295 134512640 134672761 3221224576 3221223740 134559748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1258 603 41 0 1623 0
vsize: 6656
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1280 0 0 0 49996 7 0 0 25 0 1 0 479459457 6815744 1258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1258 603 41 0 1623 0
vsize: 6656
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1280 0 0 0 50996 7 0 0 25 0 1 0 479459457 6787072 1258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1657 1258 603 41 0 1616 0
vsize: 6628
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1281 0 0 0 51996 7 0 0 25 0 1 0 479459457 6782976 1259 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1656 1259 603 41 0 1615 0
vsize: 6624
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1281 0 0 0 52997 7 0 0 25 0 1 0 479459457 6782976 1259 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1656 1259 603 41 0 1615 0
vsize: 6624
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1335 0 0 0 53996 8 0 0 25 0 1 0 479459457 7049216 1313 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1721 1313 603 41 0 1680 0
vsize: 6884
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1408 0 0 0 54996 8 0 0 25 0 1 0 479459457 7315456 1386 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1786 1386 603 41 0 1745 0
vsize: 7144
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1408 0 0 0 55996 8 0 0 25 0 1 0 479459457 7315456 1386 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1786 1386 603 41 0 1745 0
vsize: 7144
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1411 0 0 0 56997 8 0 0 25 0 1 0 479459457 7315456 1389 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1786 1389 603 41 0 1745 0
vsize: 7144
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 57996 8 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134559670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 58996 8 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 59997 8 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 60997 8 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 61997 9 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 62997 9 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 63997 9 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223680 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 64997 9 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+660.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 65997 9 0 0 25 0 1 0 479459457 7446528 1419 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1419 603 41 0 1777 0
vsize: 7272
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 66997 9 0 0 25 0 1 0 479459457 7430144 1419 4294967295 134512640 134672761 3221224576 3221223232 134565743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1814 1419 603 41 0 1773 0
vsize: 7256
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 67997 9 0 0 25 0 1 0 479459457 7430144 1419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1814 1419 603 41 0 1773 0
vsize: 7256
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1441 0 0 0 68998 9 0 0 25 0 1 0 479459457 7430144 1419 4294967295 134512640 134672761 3221224576 3221223680 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1814 1419 603 41 0 1773 0
vsize: 7256
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1445 0 0 0 69998 9 0 0 25 0 1 0 479459457 7430144 1423 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1814 1423 603 41 0 1773 0
vsize: 7256
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1522 0 0 0 70998 9 0 0 25 0 1 0 479459457 7843840 1500 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1915 1500 603 41 0 1874 0
vsize: 7660
[startup+720.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1524 0 0 0 71998 9 0 0 25 0 1 0 479459457 7843840 1502 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1915 1502 603 41 0 1874 0
vsize: 7660
[startup+730.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1524 0 0 0 72998 9 0 0 25 0 1 0 479459457 7843840 1502 4294967295 134512640 134672761 3221224576 3221223744 134564698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1915 1502 603 41 0 1874 0
vsize: 7660
[startup+740.003 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1524 0 0 0 73998 9 0 0 25 0 1 0 479459457 7843840 1502 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1915 1502 603 41 0 1874 0
vsize: 7660
[startup+750.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1589 0 0 0 74998 10 0 0 25 0 1 0 479459457 8122368 1567 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1567 603 41 0 1942 0
vsize: 7932
[startup+760.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1599 0 0 0 75998 10 0 0 25 0 1 0 479459457 8122368 1577 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1577 603 41 0 1942 0
vsize: 7932
[startup+770.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 76998 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+780.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 77998 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+790.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 78999 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+800.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 79999 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223760 134559532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+810.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 80999 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+820.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1600 0 0 0 81999 10 0 0 25 0 1 0 479459457 8122368 1578 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1578 603 41 0 1942 0
vsize: 7932
[startup+830.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1601 0 0 0 82999 10 0 0 25 0 1 0 479459457 8122368 1579 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1579 603 41 0 1942 0
vsize: 7932
[startup+840.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1601 0 0 0 83999 10 0 0 25 0 1 0 479459457 8122368 1579 4294967295 134512640 134672761 3221224576 3221223760 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1579 603 41 0 1942 0
vsize: 7932
[startup+850.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1602 0 0 0 84999 10 0 0 25 0 1 0 479459457 8122368 1580 4294967295 134512640 134672761 3221224576 3221223760 134559079 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1580 603 41 0 1942 0
vsize: 7932
[startup+860.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 85999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+870.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 86999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+880.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 87999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+890.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 88999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+900.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 89999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+910.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 90999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+920.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 91999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+930.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 92999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+940.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 93999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+950.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1603 0 0 0 94999 11 0 0 25 0 1 0 479459457 8122368 1581 4294967295 134512640 134672761 3221224576 3221223760 134559188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1581 603 41 0 1942 0
vsize: 7932
[startup+960.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1606 0 0 0 96000 11 0 0 25 0 1 0 479459457 8122368 1584 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1584 603 41 0 1942 0
vsize: 7932
[startup+970.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1613 0 0 0 97000 11 0 0 25 0 1 0 479459457 8122368 1591 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1983 1591 603 41 0 1942 0
vsize: 7932
[startup+980.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1662 0 0 0 98000 12 0 0 25 0 1 0 479459457 8392704 1640 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1640 603 41 0 2008 0
vsize: 8196
[startup+990.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1662 0 0 0 99000 12 0 0 25 0 1 0 479459457 8392704 1640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1640 603 41 0 2008 0
vsize: 8196
[startup+1000 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1662 0 0 0 100000 12 0 0 25 0 1 0 479459457 8392704 1640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1640 603 41 0 2008 0
vsize: 8196
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1662 0 0 0 101000 12 0 0 25 0 1 0 479459457 8392704 1640 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1640 603 41 0 2008 0
vsize: 8196
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1665 0 0 0 102000 12 0 0 25 0 1 0 479459457 8392704 1643 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1643 603 41 0 2008 0
vsize: 8196
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1665 0 0 0 103000 12 0 0 25 0 1 0 479459457 8392704 1643 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1643 603 41 0 2008 0
vsize: 8196
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1665 0 0 0 104000 12 0 0 25 0 1 0 479459457 8392704 1643 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1643 603 41 0 2008 0
vsize: 8196
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1669 0 0 0 105000 12 0 0 25 0 1 0 479459457 8392704 1647 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1647 603 41 0 2008 0
vsize: 8196
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1669 0 0 0 106000 12 0 0 25 0 1 0 479459457 8392704 1647 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1647 603 41 0 2008 0
vsize: 8196
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1669 0 0 0 107000 13 0 0 25 0 1 0 479459457 8392704 1647 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1647 603 41 0 2008 0
vsize: 8196
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1669 0 0 0 108001 13 0 0 25 0 1 0 479459457 8392704 1647 4294967295 134512640 134672761 3221224576 3221223680 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1647 603 41 0 2008 0
vsize: 8196
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1673 0 0 0 109001 13 0 0 25 0 1 0 479459457 8392704 1651 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1651 603 41 0 2008 0
vsize: 8196
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1680 0 0 0 110001 13 0 0 25 0 1 0 479459457 8392704 1658 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1658 603 41 0 2008 0
vsize: 8196
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1687 0 0 0 111001 13 0 0 25 0 1 0 479459457 8540160 1665 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2085 1665 603 41 0 2044 0
vsize: 8340
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1702 0 0 0 112000 13 0 0 25 0 1 0 479459457 8540160 1680 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2085 1680 603 41 0 2044 0
vsize: 8340
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1766 0 0 0 113001 13 0 0 25 0 1 0 479459457 8806400 1744 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2150 1744 603 41 0 2109 0
vsize: 8600
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1769 0 0 0 114001 13 0 0 25 0 1 0 479459457 8806400 1747 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2150 1747 603 41 0 2109 0
vsize: 8600
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1792 0 0 0 115001 13 0 0 25 0 1 0 479459457 8937472 1770 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2182 1770 603 41 0 2141 0
vsize: 8728
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1980 0 0 0 115999 15 0 0 25 0 1 0 479459457 9740288 1958 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1958 603 41 0 2337 0
vsize: 9512
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1980 0 0 0 117000 15 0 0 25 0 1 0 479459457 9740288 1958 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1958 603 41 0 2337 0
vsize: 9512
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1980 0 0 0 118000 15 0 0 25 0 1 0 479459457 9740288 1958 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1958 603 41 0 2337 0
vsize: 9512
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1980 0 0 0 119000 15 0 0 25 0 1 0 479459457 9740288 1958 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1958 603 41 0 2337 0
vsize: 9512
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31295
Raw data (stat): 31295 (minisat+) R 31294 27565 27564 0 -1 0 1980 0 0 0 120000 15 0 0 25 0 1 0 479459457 9740288 1958 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1958 603 41 0 2337 0
vsize: 9512
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31295
Raw data (stat): 31295 (minisat+) Z 31294 27565 27564 0 -1 12 1983 0 0 0 120000 15 0 0 25 0 1 0 479459457 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.01
CPU time (s): 1200.16
CPU user time (s): 1200.01
CPU system time (s): 0.156976
CPU usage (%): 100.013
Max. virtual memory (Kb): 9512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####