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-par32-3.opb
MD5SUM	3d08363a486acbc90a149ca8c58297b8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13473
Number of constraints which are clauses	13473
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	1
Maximum length of a constraint	3
Trace number 4962

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881396 kB
Buffers:         33392 kB
Cached:          82992 kB
SwapCached:       3160 kB
Active:          48328 kB
Inactive:        74072 kB
HighTotal:      131008 kB
HighFree:        44576 kB
LowTotal:       903652 kB
LowFree:        836820 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25408 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:19:34 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 1868 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13063 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9829    24580 |    3276       0        0     nan |  0.000 % |
c |       101 |    9829    24580 |    3603     101     1984    19.6 | 24.591 % |
c |       251 |    9829    24580 |    3963     251     3855    15.4 | 24.591 % |
c |       477 |    9829    24580 |    4360     477    11273    23.6 | 24.591 % |
c |       814 |    9829    24580 |    4796     814    15937    19.6 | 24.591 % |
c |      1321 |    9829    24580 |    5276    1321    31940    24.2 | 24.591 % |
c |      2081 |    9819    24558 |    5803    2080    47902    23.0 | 24.654 % |
c |      3220 |    9819    24558 |    6383    3219    76879    23.9 | 24.654 % |
c |      4930 |    9819    24558 |    7022    4929   124463    25.3 | 24.654 % |
c |      7492 |    9819    24558 |    7724    7491   193897    25.9 | 24.654 % |
c |     11336 |    9819    24558 |    8497    6666   165567    24.8 | 24.654 % |
c |     17102 |    9819    24558 |    9346    7321   192064    26.2 | 24.654 % |
c |     25751 |    9819    24558 |   10281   10435   254160    24.4 | 24.654 % |
c |     38726 |    9819    24558 |   11309   11433   268668    23.5 | 24.654 % |
c |     58187 |    9819    24558 |   12440   11477   264672    23.1 | 24.654 % |
c |     87379 |    9819    24558 |   13684   12371   274649    22.2 | 24.654 % |
c |    131169 |    9819    24558 |   15053   10129   219378    21.7 | 24.654 % |
c |    196853 |    9819    24558 |   16558    8870   182958    20.6 | 24.654 % |
c |    295381 |    9819    24558 |   18214   16209   376666    23.2 | 24.654 % |
c |    443170 |    9819    24558 |   20035   14819   321798    21.7 | 24.654 % |
#### 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.99 0.96 0.91 2/54 21318
Raw data (stat): 21318 (runsolver) R 21317 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479016300 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21318
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1253 0 0 0 994 4 0 0 25 0 1 0 479016300 6541312 1192 4294967295 134512640 134672761 3221224640 3221223792 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+20.0009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21318
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1253 0 0 0 1993 4 0 0 25 0 1 0 479016300 6541312 1192 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+30.0601 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21318
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1254 0 0 0 2998 5 0 0 25 0 1 0 479016300 6545408 1193 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.06 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1278 0 0 0 3993 9 0 0 25 0 1 0 479016300 6680576 1217 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1631 1217 603 41 0 1590 0
vsize: 6524
[startup+50.0608 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1299 0 0 0 4993 9 0 0 25 0 1 0 479016300 6815744 1238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1238 603 41 0 1623 0
vsize: 6656
[startup+60.0606 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1304 0 0 0 5993 9 0 0 25 0 1 0 479016300 6815744 1243 4294967295 134512640 134672761 3221224640 3221223764 134566136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1243 603 41 0 1623 0
vsize: 6656
[startup+70.0604 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1324 0 0 0 6993 9 0 0 25 0 1 0 479016300 6950912 1263 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1263 603 41 0 1656 0
vsize: 6788
[startup+80.0615 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1334 0 0 0 7993 9 0 0 25 0 1 0 479016300 6950912 1273 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1273 603 41 0 1656 0
vsize: 6788
[startup+90.0611 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1342 0 0 0 8993 9 0 0 25 0 1 0 479016300 6950912 1281 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1281 603 41 0 1656 0
vsize: 6788
[startup+100.062 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 21371
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1348 0 0 0 9994 9 0 0 25 0 1 0 479016300 7090176 1287 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1287 603 41 0 1690 0
vsize: 6924
[startup+110.063 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1391 0 0 0 10993 10 0 0 25 0 1 0 479016300 7225344 1330 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1330 603 41 0 1723 0
vsize: 7056
[startup+120.063 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1399 0 0 0 11993 10 0 0 25 0 1 0 479016300 7225344 1338 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1338 603 41 0 1723 0
vsize: 7056
[startup+130.063 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1414 0 0 0 12993 10 0 0 25 0 1 0 479016300 7368704 1353 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1353 603 41 0 1758 0
vsize: 7196
[startup+140.063 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1414 0 0 0 13993 10 0 0 25 0 1 0 479016300 7368704 1353 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1353 603 41 0 1758 0
vsize: 7196
[startup+150.064 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1425 0 0 0 14993 10 0 0 25 0 1 0 479016300 7368704 1364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+160.064 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1425 0 0 0 15993 10 0 0 25 0 1 0 479016300 7368704 1364 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+170.063 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1446 0 0 0 16993 10 0 0 25 0 1 0 479016300 7499776 1385 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1385 603 41 0 1790 0
vsize: 7324
[startup+180.063 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1448 0 0 0 17993 10 0 0 25 0 1 0 479016300 7499776 1387 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1387 603 41 0 1790 0
vsize: 7324
[startup+190.064 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1456 0 0 0 18994 10 0 0 25 0 1 0 479016300 7499776 1395 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1395 603 41 0 1790 0
vsize: 7324
[startup+200.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1461 0 0 0 19994 10 0 0 25 0 1 0 479016300 7499776 1400 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1400 603 41 0 1790 0
vsize: 7324
[startup+210.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1470 0 0 0 20994 10 0 0 25 0 1 0 479016300 7634944 1409 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+220.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1470 0 0 0 21994 10 0 0 25 0 1 0 479016300 7634944 1409 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+230.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1473 0 0 0 22994 10 0 0 25 0 1 0 479016300 7634944 1412 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+240.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1473 0 0 0 23994 10 0 0 25 0 1 0 479016300 7634944 1412 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+250.066 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1474 0 0 0 24995 10 0 0 25 0 1 0 479016300 7634944 1413 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1413 603 41 0 1823 0
vsize: 7456
[startup+260.067 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1480 0 0 0 25995 10 0 0 25 0 1 0 479016300 7634944 1419 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1419 603 41 0 1823 0
vsize: 7456
[startup+270.067 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1529 0 0 0 26995 11 0 0 25 0 1 0 479016300 7942144 1468 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1468 603 41 0 1898 0
vsize: 7756
[startup+280.068 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1542 0 0 0 27995 11 0 0 25 0 1 0 479016300 7942144 1481 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+290.067 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1542 0 0 0 28995 11 0 0 25 0 1 0 479016300 7942144 1481 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+300.068 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1542 0 0 0 29995 11 0 0 25 0 1 0 479016300 7942144 1481 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+310.068 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1542 0 0 0 30995 11 0 0 25 0 1 0 479016300 7942144 1481 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+320.068 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1548 0 0 0 31995 11 0 0 25 0 1 0 479016300 7942144 1487 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+330.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1548 0 0 0 32996 11 0 0 25 0 1 0 479016300 7942144 1487 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+340.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1551 0 0 0 33996 11 0 0 25 0 1 0 479016300 8089600 1490 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+350.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1551 0 0 0 34996 11 0 0 25 0 1 0 479016300 8089600 1490 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+360.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1551 0 0 0 35996 11 0 0 25 0 1 0 479016300 8089600 1490 4294967295 134512640 134672761 3221224640 3221223824 134558378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+370.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21373
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1552 0 0 0 36996 11 0 0 25 0 1 0 479016300 8089600 1491 4294967295 134512640 134672761 3221224640 3221223808 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+380.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1552 0 0 0 37996 11 0 0 25 0 1 0 479016300 8089600 1491 4294967295 134512640 134672761 3221224640 3221223824 134559569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+390.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1554 0 0 0 38996 11 0 0 25 0 1 0 479016300 8089600 1493 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+400.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1554 0 0 0 39996 11 0 0 25 0 1 0 479016300 8089600 1493 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+410.071 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1588 0 0 0 40996 12 0 0 25 0 1 0 479016300 8224768 1527 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1527 603 41 0 1967 0
vsize: 8032
[startup+420.071 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1596 0 0 0 41996 12 0 0 25 0 1 0 479016300 8224768 1535 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1535 603 41 0 1967 0
vsize: 8032
[startup+430.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1603 0 0 0 42996 12 0 0 25 0 1 0 479016300 8224768 1542 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1542 603 41 0 1967 0
vsize: 8032
[startup+440.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1605 0 0 0 43997 12 0 0 25 0 1 0 479016300 8224768 1544 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+450.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1605 0 0 0 44997 12 0 0 25 0 1 0 479016300 8224768 1544 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+460.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1606 0 0 0 45997 12 0 0 25 0 1 0 479016300 8224768 1545 4294967295 134512640 134672761 3221224640 3221223824 134558694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1545 603 41 0 1967 0
vsize: 8032
[startup+470.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1607 0 0 0 46997 12 0 0 25 0 1 0 479016300 8224768 1546 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+480.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1610 0 0 0 47997 12 0 0 25 0 1 0 479016300 8224768 1549 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1549 603 41 0 1967 0
vsize: 8032
[startup+490.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1611 0 0 0 48997 12 0 0 25 0 1 0 479016300 8224768 1550 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+500.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1611 0 0 0 49997 12 0 0 25 0 1 0 479016300 8224768 1550 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+510.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1611 0 0 0 50998 12 0 0 25 0 1 0 479016300 8224768 1550 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+520.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1612 0 0 0 51998 12 0 0 25 0 1 0 479016300 8224768 1551 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+530.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1612 0 0 0 52998 12 0 0 25 0 1 0 479016300 8224768 1551 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+540.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1612 0 0 0 53998 12 0 0 25 0 1 0 479016300 8224768 1551 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+550.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1613 0 0 0 54998 12 0 0 25 0 1 0 479016300 8224768 1552 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1552 603 41 0 1967 0
vsize: 8032
[startup+560.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1614 0 0 0 55998 12 0 0 25 0 1 0 479016300 8224768 1553 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+570.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1614 0 0 0 56998 12 0 0 25 0 1 0 479016300 8224768 1553 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+580.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1614 0 0 0 57999 12 0 0 25 0 1 0 479016300 8224768 1553 4294967295 134512640 134672761 3221224640 3221223744 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+590.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1614 0 0 0 58999 12 0 0 25 0 1 0 479016300 8224768 1553 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+600.075 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1664 0 0 0 59998 13 0 0 25 0 1 0 479016300 8491008 1603 4294967295 134512640 134672761 3221224640 3221223808 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1603 603 41 0 2032 0
vsize: 8292
[startup+610.076 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1694 0 0 0 60998 13 0 0 25 0 1 0 479016300 8491008 1633 4294967295 134512640 134672761 3221224640 3221223808 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1633 603 41 0 2032 0
vsize: 8292
[startup+620.076 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1694 0 0 0 61998 13 0 0 25 0 1 0 479016300 8491008 1633 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1633 603 41 0 2032 0
vsize: 8292
[startup+630.077 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1699 0 0 0 62999 13 0 0 25 0 1 0 479016300 8638464 1638 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1638 603 41 0 2068 0
vsize: 8436
[startup+640.077 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1701 0 0 0 63999 13 0 0 25 0 1 0 479016300 8638464 1640 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+650.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1701 0 0 0 64999 13 0 0 25 0 1 0 479016300 8638464 1640 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+660.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1715 0 0 0 65999 13 0 0 25 0 1 0 479016300 8638464 1654 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1654 603 41 0 2068 0
vsize: 8436
[startup+670.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1719 0 0 0 66999 13 0 0 25 0 1 0 479016300 8638464 1658 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1658 603 41 0 2068 0
vsize: 8436
[startup+680.079 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1719 0 0 0 67999 13 0 0 25 0 1 0 479016300 8638464 1658 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1658 603 41 0 2068 0
vsize: 8436
[startup+690.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1721 0 0 0 69000 13 0 0 25 0 1 0 479016300 8638464 1660 4294967295 134512640 134672761 3221224640 3221223640 1075350251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1660 603 41 0 2068 0
vsize: 8436
[startup+700.079 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1721 0 0 0 70000 13 0 0 25 0 1 0 479016300 8638464 1660 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1660 603 41 0 2068 0
vsize: 8436
[startup+710.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1732 0 0 0 71000 13 0 0 25 0 1 0 479016300 8818688 1671 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+720.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1732 0 0 0 72000 13 0 0 25 0 1 0 479016300 8818688 1671 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+730.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1733 0 0 0 73000 13 0 0 25 0 1 0 479016300 8818688 1672 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+740.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1733 0 0 0 74000 14 0 0 25 0 1 0 479016300 8818688 1672 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+750.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1733 0 0 0 75000 14 0 0 25 0 1 0 479016300 8818688 1672 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+760.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1742 0 0 0 76001 14 0 0 25 0 1 0 479016300 8818688 1681 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1681 603 41 0 2112 0
vsize: 8612
[startup+770.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1751 0 0 0 77000 14 0 0 25 0 1 0 479016300 8818688 1690 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+780.083 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1751 0 0 0 78001 14 0 0 25 0 1 0 479016300 8818688 1690 4294967295 134512640 134672761 3221224640 3221223776 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+790.083 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1751 0 0 0 79001 14 0 0 25 0 1 0 479016300 8818688 1690 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+800.084 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1761 0 0 0 80001 14 0 0 25 0 1 0 479016300 9015296 1700 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+810.084 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1761 0 0 0 81001 14 0 0 25 0 1 0 479016300 9015296 1700 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+820.084 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1771 0 0 0 82001 14 0 0 25 0 1 0 479016300 9015296 1710 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+830.085 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1771 0 0 0 83001 14 0 0 25 0 1 0 479016300 9015296 1710 4294967295 134512640 134672761 3221224640 3221223808 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+840.085 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1771 0 0 0 84002 14 0 0 25 0 1 0 479016300 9015296 1710 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+850.086 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1771 0 0 0 85002 14 0 0 25 0 1 0 479016300 9015296 1710 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+860.087 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1771 0 0 0 86002 14 0 0 25 0 1 0 479016300 9015296 1710 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+870.086 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1780 0 0 0 87001 15 0 0 25 0 1 0 479016300 9015296 1719 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1719 603 41 0 2160 0
vsize: 8804
[startup+880.087 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1781 0 0 0 88001 15 0 0 25 0 1 0 479016300 9015296 1720 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+890.088 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1781 0 0 0 89002 15 0 0 25 0 1 0 479016300 9015296 1720 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+900.089 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1781 0 0 0 90002 15 0 0 25 0 1 0 479016300 9015296 1720 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+910.088 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1781 0 0 0 91002 15 0 0 25 0 1 0 479016300 9015296 1720 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+920.089 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1781 0 0 0 92002 15 0 0 25 0 1 0 479016300 9015296 1720 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+930.089 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1789 0 0 0 93002 15 0 0 25 0 1 0 479016300 9146368 1728 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1728 603 41 0 2192 0
vsize: 8932
[startup+940.089 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1796 0 0 0 94002 15 0 0 25 0 1 0 479016300 9146368 1735 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1735 603 41 0 2192 0
vsize: 8932
[startup+950.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1808 0 0 0 95002 15 0 0 25 0 1 0 479016300 9146368 1747 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1747 603 41 0 2192 0
vsize: 8932
[startup+960.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1808 0 0 0 96002 15 0 0 25 0 1 0 479016300 9146368 1747 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1747 603 41 0 2192 0
vsize: 8932
[startup+970.091 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1809 0 0 0 97002 15 0 0 25 0 1 0 479016300 9146368 1748 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+980.092 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1809 0 0 0 98002 15 0 0 25 0 1 0 479016300 9146368 1748 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+990.092 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1817 0 0 0 99003 15 0 0 25 0 1 0 479016300 9306112 1756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1756 603 41 0 2231 0
vsize: 9088
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1820 0 0 0 100003 15 0 0 25 0 1 0 479016300 9306112 1759 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1010.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1820 0 0 0 101003 15 0 0 25 0 1 0 479016300 9306112 1759 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1020.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1820 0 0 0 102003 15 0 0 25 0 1 0 479016300 9306112 1759 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1829 0 0 0 103003 16 0 0 25 0 1 0 479016300 9306112 1768 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1829 0 0 0 104003 16 0 0 25 0 1 0 479016300 9306112 1768 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1050.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1830 0 0 0 105004 16 0 0 25 0 1 0 479016300 9306112 1769 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1060.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1830 0 0 0 106004 16 0 0 25 0 1 0 479016300 9306112 1769 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1830 0 0 0 107004 16 0 0 25 0 1 0 479016300 9306112 1769 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1080.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1831 0 0 0 108004 16 0 0 25 0 1 0 479016300 9306112 1770 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1770 603 41 0 2231 0
vsize: 9088
[startup+1090.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 109004 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 110006 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 111006 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1120.11 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 112006 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1130.11 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 113007 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1140.11 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 114007 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223724 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1150.12 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 115007 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1160.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 116008 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1170.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 117008 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 118009 16 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 119009 17 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 21375
Raw data (stat): 21318 (minisat+) R 21317 18865 18864 0 -1 0 1842 0 0 0 120009 17 0 0 25 0 1 0 479016300 9469952 1781 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 21375
Raw data (stat): 21318 (minisat+) Z 21317 18865 18864 0 -1 12 1844 0 0 0 120009 17 0 0 25 0 1 0 479016300 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: 0
Real time (s): 1200.14
CPU time (s): 1200.27
CPU user time (s): 1200.1
CPU system time (s): 0.175973
CPU usage (%): 100.011
Max. virtual memory (Kb): 9248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####