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-1.opb
MD5SUM	64e81a7b23abbb8a6da4e2377ea69dee
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	13453
Number of constraints which are clauses	13453
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 4941

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-13 20:57:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1832 boxname=wulflinc29 idbench=204 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  64e81a7b23abbb8a6da4e2377ea69dee  /oldhome/oroussel/tmp/wulflinc29/normalized-par32-1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-par32-1.opb
IDLAUNCH: 1832
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        857948 kB
Buffers:         35664 kB
Cached:         103452 kB
SwapCached:         12 kB
Active:          52516 kB
Inactive:        89476 kB
HighTotal:      131008 kB
HighFree:        24080 kB
LowTotal:       903652 kB
LowFree:        833868 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29228 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:17:45 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 1832 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13039 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9878    24638 |    3292       0        0     nan |  0.000 % |
c |       101 |    9878    24638 |    3621     101     1231    12.2 | 23.867 % |
c |       251 |    9878    24638 |    3983     251     5277    21.0 | 23.867 % |
c |       476 |    9878    24638 |    4381     476     8655    18.2 | 23.867 % |
c |       814 |    9878    24638 |    4819     814    19600    24.1 | 23.867 % |
c |      1320 |    9878    24638 |    5301    1320    27899    21.1 | 23.867 % |
c |      2082 |    9878    24638 |    5831    2082    57645    27.7 | 23.867 % |
c |      3221 |    9878    24638 |    6415    3221    93388    29.0 | 23.867 % |
c |      4931 |    9878    24638 |    7056    4931   143848    29.2 | 23.867 % |
c |      7493 |    9878    24638 |    7762    7493   210661    28.1 | 23.867 % |
c |     11338 |    9878    24638 |    8538    6644   169658    25.5 | 23.867 % |
c |     17105 |    9878    24638 |    9392    7285   177959    24.4 | 23.867 % |
c |     25754 |    9878    24638 |   10331   10409   254945    24.5 | 23.867 % |
c |     38729 |    9878    24638 |   11364   11455   286759    25.0 | 23.867 % |
c |     58191 |    9878    24638 |   12501   11386   282530    24.8 | 23.867 % |
c |     87384 |    9878    24638 |   13751   12309   296202    24.1 | 23.867 % |
c |    131173 |    9868    24616 |   15126   10027   237728    23.7 | 23.929 % |
c |    196858 |    9868    24616 |   16639    8659   223250    25.8 | 23.929 % |
c |    295384 |    9868    24616 |   18303   16056   367503    22.9 | 23.929 % |
c |    443174 |    9868    24616 |   20133   14387   321561    22.4 | 23.929 % |
#### 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.66 0.87 0.88 2/54 30189
Raw data (stat): 30189 (runsolver) R 30188 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479004982 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.71 0.87 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1255 0 0 0 994 4 0 0 25 0 1 0 479004982 6541312 1194 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+20.001 s]
Raw data (loadavg): 0.76 0.88 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1255 0 0 0 1994 4 0 0 25 0 1 0 479004982 6541312 1194 4294967295 134512640 134672761 3221224640 3221223840 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+30.0022 s]
Raw data (loadavg): 0.79 0.88 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1255 0 0 0 2994 5 0 0 25 0 1 0 479004982 6541312 1194 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+40.0026 s]
Raw data (loadavg): 0.82 0.89 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1259 0 0 0 3993 5 0 0 25 0 1 0 479004982 6680576 1198 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1631 1198 603 41 0 1590 0
vsize: 6524
[startup+50.0024 s]
Raw data (loadavg): 0.85 0.89 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1298 0 0 0 4993 6 0 0 25 0 1 0 479004982 6815744 1237 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1237 603 41 0 1623 0
vsize: 6656
[startup+60.0026 s]
Raw data (loadavg): 0.87 0.89 0.88 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1311 0 0 0 5992 6 0 0 25 0 1 0 479004982 6815744 1250 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1250 603 41 0 1623 0
vsize: 6656
[startup+70.0034 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1326 0 0 0 6991 7 0 0 25 0 1 0 479004982 6950912 1265 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1265 603 41 0 1656 0
vsize: 6788
[startup+80.0037 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1375 0 0 0 7991 7 0 0 25 0 1 0 479004982 7081984 1314 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1729 1314 603 41 0 1688 0
vsize: 6916
[startup+90.0039 s]
Raw data (loadavg): 0.92 0.90 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1389 0 0 0 8990 8 0 0 25 0 1 0 479004982 7221248 1328 4294967295 134512640 134672761 3221224640 3221223816 134559124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1328 603 41 0 1722 0
vsize: 7052
[startup+100.003 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1393 0 0 0 9990 8 0 0 25 0 1 0 479004982 7221248 1332 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1332 603 41 0 1722 0
vsize: 7052
[startup+110.004 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1397 0 0 0 10990 9 0 0 25 0 1 0 479004982 7221248 1336 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1336 603 41 0 1722 0
vsize: 7052
[startup+120.005 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1410 0 0 0 11990 9 0 0 25 0 1 0 479004982 7368704 1349 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1349 603 41 0 1758 0
vsize: 7196
[startup+130.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1441 0 0 0 12989 9 0 0 25 0 1 0 479004982 7368704 1380 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1380 603 41 0 1758 0
vsize: 7196
[startup+140.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 30189
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1448 0 0 0 13988 10 0 0 25 0 1 0 479004982 7516160 1387 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1387 603 41 0 1794 0
vsize: 7340
[startup+150.006 s]
Raw data (loadavg): 1.05 0.93 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1448 0 0 0 14985 14 0 0 25 0 1 0 479004982 7516160 1387 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1387 603 41 0 1794 0
vsize: 7340
[startup+160.007 s]
Raw data (loadavg): 1.04 0.93 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1457 0 0 0 15985 14 0 0 25 0 1 0 479004982 7516160 1396 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1396 603 41 0 1794 0
vsize: 7340
[startup+170.007 s]
Raw data (loadavg): 1.03 0.94 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1465 0 0 0 16985 14 0 0 25 0 1 0 479004982 7516160 1404 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1404 603 41 0 1794 0
vsize: 7340
[startup+180.007 s]
Raw data (loadavg): 1.03 0.94 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1467 0 0 0 17985 14 0 0 25 0 1 0 479004982 7516160 1406 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1406 603 41 0 1794 0
vsize: 7340
[startup+190.007 s]
Raw data (loadavg): 1.02 0.94 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1475 0 0 0 18985 14 0 0 25 0 1 0 479004982 7651328 1414 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1868 1414 603 41 0 1827 0
vsize: 7472
[startup+200.007 s]
Raw data (loadavg): 1.02 0.94 0.90 2/54 30242
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1507 0 0 0 19985 14 0 0 25 0 1 0 479004982 7798784 1446 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1446 603 41 0 1863 0
vsize: 7616
[startup+210.007 s]
Raw data (loadavg): 1.02 0.94 0.90 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1510 0 0 0 20985 14 0 0 25 0 1 0 479004982 7798784 1449 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1449 603 41 0 1863 0
vsize: 7616
[startup+220.006 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1516 0 0 0 21985 14 0 0 25 0 1 0 479004982 7798784 1455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1455 603 41 0 1863 0
vsize: 7616
[startup+230.006 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1521 0 0 0 22986 14 0 0 25 0 1 0 479004982 7798784 1460 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1460 603 41 0 1863 0
vsize: 7616
[startup+240.006 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1544 0 0 0 23985 14 0 0 25 0 1 0 479004982 7933952 1483 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1483 603 41 0 1896 0
vsize: 7748
[startup+250.006 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1549 0 0 0 24986 14 0 0 25 0 1 0 479004982 7933952 1488 4294967295 134512640 134672761 3221224640 3221223808 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1488 603 41 0 1896 0
vsize: 7748
[startup+260.007 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1554 0 0 0 25986 14 0 0 25 0 1 0 479004982 7933952 1493 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1493 603 41 0 1896 0
vsize: 7748
[startup+270.007 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1555 0 0 0 26986 14 0 0 25 0 1 0 479004982 7933952 1494 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1494 603 41 0 1896 0
vsize: 7748
[startup+280.007 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1562 0 0 0 27986 14 0 0 25 0 1 0 479004982 8073216 1501 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1971 1501 603 41 0 1930 0
vsize: 7884
[startup+290.007 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1634 0 0 0 28985 15 0 0 25 0 1 0 479004982 8429568 1573 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2058 1573 603 41 0 2017 0
vsize: 8232
[startup+300.007 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1643 0 0 0 29986 15 0 0 25 0 1 0 479004982 8429568 1582 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2058 1582 603 41 0 2017 0
vsize: 8232
[startup+310.008 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1678 0 0 0 30986 15 0 0 25 0 1 0 479004982 8564736 1617 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1617 603 41 0 2050 0
vsize: 8364
[startup+320.007 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1684 0 0 0 31986 15 0 0 25 0 1 0 479004982 8564736 1623 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1623 603 41 0 2050 0
vsize: 8364
[startup+330.008 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1692 0 0 0 32986 15 0 0 25 0 1 0 479004982 8564736 1631 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+340.008 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1692 0 0 0 33986 15 0 0 25 0 1 0 479004982 8564736 1631 4294967295 134512640 134672761 3221224640 3221223776 134565036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+350.008 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1692 0 0 0 34987 15 0 0 25 0 1 0 479004982 8564736 1631 4294967295 134512640 134672761 3221224640 3221223744 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+360.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1692 0 0 0 35987 15 0 0 25 0 1 0 479004982 8564736 1631 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+370.008 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1692 0 0 0 36987 15 0 0 25 0 1 0 479004982 8564736 1631 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+380.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1694 0 0 0 37987 15 0 0 25 0 1 0 479004982 8564736 1633 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1633 603 41 0 2050 0
vsize: 8364
[startup+390.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1694 0 0 0 38987 15 0 0 25 0 1 0 479004982 8564736 1633 4294967295 134512640 134672761 3221224640 3221223776 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1633 603 41 0 2050 0
vsize: 8364
[startup+400.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1696 0 0 0 39988 15 0 0 25 0 1 0 479004982 8564736 1635 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1635 603 41 0 2050 0
vsize: 8364
[startup+410.008 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1696 0 0 0 40988 15 0 0 25 0 1 0 479004982 8564736 1635 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1635 603 41 0 2050 0
vsize: 8364
[startup+420.008 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1698 0 0 0 41988 15 0 0 25 0 1 0 479004982 8564736 1637 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+430.009 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1698 0 0 0 42988 15 0 0 25 0 1 0 479004982 8564736 1637 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+440.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1699 0 0 0 43988 15 0 0 25 0 1 0 479004982 8564736 1638 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2091 1638 603 41 0 2050 0
vsize: 8364
[startup+450.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1717 0 0 0 44988 15 0 0 25 0 1 0 479004982 8695808 1656 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2123 1656 603 41 0 2082 0
vsize: 8492
[startup+460.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1723 0 0 0 45988 15 0 0 25 0 1 0 479004982 8695808 1662 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2123 1662 603 41 0 2082 0
vsize: 8492
[startup+470.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1729 0 0 0 46988 15 0 0 25 0 1 0 479004982 8695808 1668 4294967295 134512640 134672761 3221224640 3221223824 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+480.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1729 0 0 0 47988 15 0 0 25 0 1 0 479004982 8695808 1668 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+490.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30244
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1729 0 0 0 48989 15 0 0 25 0 1 0 479004982 8695808 1668 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+500.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 49989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+510.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 50989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+520.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 51989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+530.008 s]
Raw data (loadavg): 1.00 0.97 0.91 3/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 52989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+540.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 53989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223840 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+550.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 54989 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+560.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 55990 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223744 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+570.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 56990 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+580.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1741 0 0 0 57990 15 0 0 25 0 1 0 479004982 8859648 1680 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1680 603 41 0 2122 0
vsize: 8652
[startup+590.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1748 0 0 0 58990 15 0 0 25 0 1 0 479004982 8859648 1687 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1687 603 41 0 2122 0
vsize: 8652
[startup+600.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1756 0 0 0 59990 15 0 0 25 0 1 0 479004982 8859648 1695 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+610.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1756 0 0 0 60991 15 0 0 25 0 1 0 479004982 8859648 1695 4294967295 134512640 134672761 3221224640 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+620.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1756 0 0 0 61991 15 0 0 25 0 1 0 479004982 8859648 1695 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+630.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1756 0 0 0 62991 15 0 0 25 0 1 0 479004982 8859648 1695 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+640.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1756 0 0 0 63991 15 0 0 25 0 1 0 479004982 8859648 1695 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+650.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1757 0 0 0 64991 15 0 0 25 0 1 0 479004982 8859648 1696 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1696 603 41 0 2122 0
vsize: 8652
[startup+660.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1757 0 0 0 65991 15 0 0 25 0 1 0 479004982 8859648 1696 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1696 603 41 0 2122 0
vsize: 8652
[startup+670.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1757 0 0 0 66991 15 0 0 25 0 1 0 479004982 8859648 1696 4294967295 134512640 134672761 3221224640 3221223808 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1696 603 41 0 2122 0
vsize: 8652
[startup+680.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1757 0 0 0 67991 15 0 0 25 0 1 0 479004982 8859648 1696 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1696 603 41 0 2122 0
vsize: 8652
[startup+690.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1769 0 0 0 68991 15 0 0 25 0 1 0 479004982 9023488 1708 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1708 603 41 0 2162 0
vsize: 8812
[startup+700.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1769 0 0 0 69992 15 0 0 25 0 1 0 479004982 9023488 1708 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1708 603 41 0 2162 0
vsize: 8812
[startup+710.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1771 0 0 0 70991 16 0 0 25 0 1 0 479004982 9023488 1710 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1710 603 41 0 2162 0
vsize: 8812
[startup+720.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 71991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+730.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 72991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223776 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+740.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 73991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+750.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 74991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+760.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 75991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+770.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1782 0 0 0 76991 16 0 0 25 0 1 0 479004982 9023488 1721 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1721 603 41 0 2162 0
vsize: 8812
[startup+780.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1783 0 0 0 77992 16 0 0 25 0 1 0 479004982 9023488 1722 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1722 603 41 0 2162 0
vsize: 8812
[startup+790.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1783 0 0 0 78992 16 0 0 25 0 1 0 479004982 9023488 1722 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1722 603 41 0 2162 0
vsize: 8812
[startup+800.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1783 0 0 0 79992 16 0 0 25 0 1 0 479004982 9023488 1722 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1722 603 41 0 2162 0
vsize: 8812
[startup+810.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1794 0 0 0 80992 16 0 0 25 0 1 0 479004982 9023488 1733 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1733 603 41 0 2162 0
vsize: 8812
[startup+820.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1794 0 0 0 81992 16 0 0 25 0 1 0 479004982 9023488 1733 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1733 603 41 0 2162 0
vsize: 8812
[startup+830.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1794 0 0 0 82993 16 0 0 25 0 1 0 479004982 9023488 1733 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1733 603 41 0 2162 0
vsize: 8812
[startup+840.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1794 0 0 0 83993 16 0 0 25 0 1 0 479004982 9023488 1733 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1733 603 41 0 2162 0
vsize: 8812
[startup+850.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1794 0 0 0 84993 16 0 0 25 0 1 0 479004982 9023488 1733 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1733 603 41 0 2162 0
vsize: 8812
[startup+860.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1795 0 0 0 85993 16 0 0 25 0 1 0 479004982 9023488 1734 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1734 603 41 0 2162 0
vsize: 8812
[startup+870.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1803 0 0 0 86993 16 0 0 25 0 1 0 479004982 9187328 1742 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1742 603 41 0 2202 0
vsize: 8972
[startup+880.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1803 0 0 0 87994 16 0 0 25 0 1 0 479004982 9187328 1742 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1742 603 41 0 2202 0
vsize: 8972
[startup+890.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1805 0 0 0 88994 16 0 0 25 0 1 0 479004982 9187328 1744 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+900.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1805 0 0 0 89994 16 0 0 25 0 1 0 479004982 9187328 1744 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+910.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1811 0 0 0 90994 16 0 0 25 0 1 0 479004982 9187328 1750 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1750 603 41 0 2202 0
vsize: 8972
[startup+920.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1813 0 0 0 91994 16 0 0 25 0 1 0 479004982 9187328 1752 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1752 603 41 0 2202 0
vsize: 8972
[startup+930.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1813 0 0 0 92994 16 0 0 25 0 1 0 479004982 9187328 1752 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1752 603 41 0 2202 0
vsize: 8972
[startup+940.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1815 0 0 0 93995 16 0 0 25 0 1 0 479004982 9187328 1754 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1754 603 41 0 2202 0
vsize: 8972
[startup+950.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1826 0 0 0 94995 16 0 0 25 0 1 0 479004982 9187328 1765 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1765 603 41 0 2202 0
vsize: 8972
[startup+960.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1827 0 0 0 95995 16 0 0 25 0 1 0 479004982 9187328 1766 4294967295 134512640 134672761 3221224640 3221223808 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1766 603 41 0 2202 0
vsize: 8972
[startup+970.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1837 0 0 0 96995 16 0 0 25 0 1 0 479004982 9351168 1776 4294967295 134512640 134672761 3221224640 3221223776 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1776 603 41 0 2242 0
vsize: 9132
[startup+980.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1837 0 0 0 97995 16 0 0 25 0 1 0 479004982 9351168 1776 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1776 603 41 0 2242 0
vsize: 9132
[startup+990.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1845 0 0 0 98995 16 0 0 25 0 1 0 479004982 9351168 1784 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1784 603 41 0 2242 0
vsize: 9132
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1897 0 0 0 99995 16 0 0 25 0 1 0 479004982 9482240 1836 4294967295 134512640 134672761 3221224640 3221223824 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2315 1836 603 41 0 2274 0
vsize: 9260
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1902 0 0 0 100995 16 0 0 25 0 1 0 479004982 9621504 1841 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1841 603 41 0 2308 0
vsize: 9396
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1912 0 0 0 101995 16 0 0 25 0 1 0 479004982 9621504 1851 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1851 603 41 0 2308 0
vsize: 9396
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1916 0 0 0 102996 16 0 0 25 0 1 0 479004982 9621504 1855 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1855 603 41 0 2308 0
vsize: 9396
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1917 0 0 0 103996 16 0 0 25 0 1 0 479004982 9621504 1856 4294967295 134512640 134672761 3221224640 3221223808 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1856 603 41 0 2308 0
vsize: 9396
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1923 0 0 0 104996 16 0 0 25 0 1 0 479004982 9621504 1862 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1862 603 41 0 2308 0
vsize: 9396
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1923 0 0 0 105996 16 0 0 25 0 1 0 479004982 9621504 1862 4294967295 134512640 134672761 3221224640 3221223764 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1862 603 41 0 2308 0
vsize: 9396
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1923 0 0 0 106996 16 0 0 25 0 1 0 479004982 9621504 1862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1862 603 41 0 2308 0
vsize: 9396
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1928 0 0 0 107996 16 0 0 25 0 1 0 479004982 9621504 1867 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1867 603 41 0 2308 0
vsize: 9396
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1928 0 0 0 108997 16 0 0 25 0 1 0 479004982 9621504 1867 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1867 603 41 0 2308 0
vsize: 9396
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1928 0 0 0 109997 16 0 0 25 0 1 0 479004982 9621504 1867 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1867 603 41 0 2308 0
vsize: 9396
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1928 0 0 0 110997 16 0 0 25 0 1 0 479004982 9621504 1867 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1867 603 41 0 2308 0
vsize: 9396
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1929 0 0 0 111997 16 0 0 25 0 1 0 479004982 9621504 1868 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1929 0 0 0 112997 16 0 0 25 0 1 0 479004982 9621504 1868 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1935 0 0 0 113998 16 0 0 25 0 1 0 479004982 9752576 1874 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1874 603 41 0 2340 0
vsize: 9524
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1935 0 0 0 114998 16 0 0 25 0 1 0 479004982 9752576 1874 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1874 603 41 0 2340 0
vsize: 9524
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1946 0 0 0 115998 16 0 0 25 0 1 0 479004982 9752576 1885 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1885 603 41 0 2340 0
vsize: 9524
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1946 0 0 0 116998 16 0 0 25 0 1 0 479004982 9752576 1885 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1885 603 41 0 2340 0
vsize: 9524
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1946 0 0 0 117998 16 0 0 25 0 1 0 479004982 9752576 1885 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1885 603 41 0 2340 0
vsize: 9524
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1946 0 0 0 118999 16 0 0 25 0 1 0 479004982 9752576 1885 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1885 603 41 0 2340 0
vsize: 9524
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 30246
Raw data (stat): 30189 (minisat+) R 30188 27222 27221 0 -1 0 1946 0 0 0 119999 16 0 0 25 0 1 0 479004982 9752576 1885 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1885 603 41 0 2340 0
vsize: 9524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 30246
Raw data (stat): 30189 (minisat+) Z 30188 27222 27221 0 -1 12 1948 0 0 0 119999 17 0 0 25 0 1 0 479004982 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.17
CPU user time (s): 1199.99
CPU system time (s): 0.171973
CPU usage (%): 100.012
Max. virtual memory (Kb): 9524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####