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-4.opb
MD5SUM	4ad922a0ad53056b410be6ab5caa6b5b
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	13489
Number of constraints which are clauses	13489
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 5553

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 00:26:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3970 boxname=wulflinc6 idbench=210 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ad922a0ad53056b410be6ab5caa6b5b  /oldhome/oroussel/tmp/wulflinc6/normalized-par32-4.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-par32-4.opb /oldhome/oroussel/tmp/wulflinc6/normalized-par32-4.opb
IDLAUNCH: 3970
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        907748 kB
Buffers:         35620 kB
Cached:          69244 kB
SwapCached:       2644 kB
Active:          52432 kB
Inactive:        57932 kB
HighTotal:      131008 kB
HighFree:        57876 kB
LowTotal:       903652 kB
LowFree:        849872 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11040 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:46:41 (client local time) WITH STATUS 0 IN 1200.41 SECONDS
stats: 3970 7 1200.41 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13075 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9693    24218 |    2907       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4770          
c   -- var.elim.:  2000/4770          
c   -- var.elim.:  3000/4770          
c   -- var.elim.:  4000/4770          
c   -- var.elim.:  4770/4770          
c |         0 |    9693    24218 |    3877       0        0     nan |  0.000 % |
c |       100 |    9693    24218 |    4264     100      950     9.5 | 24.906 % |
c |       251 |    9693    24218 |    4691     251     4680    18.6 | 24.906 % |
c |       476 |    9693    24218 |    5160     476    13028    27.4 | 24.906 % |
c |       815 |    969#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 976
Raw data (stat): 976 (runsolver) R 975 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422039641 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 1559 0 0 0 995 3 0 0 25 0 1 0 422039641 7946240 1499 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1940 1499 603 41 0 1899 0
vsize: 7760
[startup+19.9997 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 1761 0 0 0 1995 4 0 0 25 0 1 0 422039641 8790016 1701 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2146 1701 603 41 0 2105 0
vsize: 8584
[startup+30.0001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 1798 0 0 0 2994 4 0 0 25 0 1 0 422039641 8925184 1738 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2179 1738 603 41 0 2138 0
vsize: 8716
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 1855 0 0 0 3994 4 0 0 25 0 1 0 422039641 9039872 1795 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2207 1795 603 41 0 2166 0
vsize: 8828
[startup+50 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 1958 0 0 0 4994 5 0 0 25 0 1 0 422039641 9609216 1898 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1898 603 41 0 2289 0
vsize: 9384
[startup+59.9994 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2017 0 0 0 5995 5 0 0 25 0 1 0 422039641 9809920 1957 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2395 1957 603 41 0 2354 0
vsize: 9580
[startup+69.9996 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2057 0 0 0 6995 5 0 0 25 0 1 0 422039641 9940992 1997 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2427 1997 603 41 0 2386 0
vsize: 9708
[startup+79.9998 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2075 0 0 0 7995 5 0 0 25 0 1 0 422039641 10022912 2015 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2447 2015 603 41 0 2406 0
vsize: 9788
[startup+89.9999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2118 0 0 0 8996 5 0 0 25 0 1 0 422039641 10153984 2058 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2479 2058 603 41 0 2438 0
vsize: 9916
[startup+100 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2132 0 0 0 9996 5 0 0 25 0 1 0 422039641 10252288 2072 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2503 2072 603 41 0 2462 0
vsize: 10012
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2143 0 0 0 10996 5 0 0 25 0 1 0 422039641 10252288 2083 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2503 2083 603 41 0 2462 0
vsize: 10012
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2144 0 0 0 11996 5 0 0 25 0 1 0 422039641 10252288 2084 4294967295 134512640 134672761 3221224576 3221223776 134610652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2503 2084 603 41 0 2462 0
vsize: 10012
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2162 0 0 0 12997 5 0 0 25 0 1 0 422039641 10366976 2102 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2531 2102 603 41 0 2490 0
vsize: 10124
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2286 0 0 0 13997 5 0 0 25 0 1 0 422039641 10924032 2226 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2667 2226 603 41 0 2626 0
vsize: 10668
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2311 0 0 0 14997 5 0 0 25 0 1 0 422039641 11026432 2251 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2692 2251 603 41 0 2651 0
vsize: 10768
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2311 0 0 0 15998 5 0 0 25 0 1 0 422039641 11026432 2251 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2692 2251 603 41 0 2651 0
vsize: 10768
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2334 0 0 0 16998 5 0 0 25 0 1 0 422039641 11141120 2274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2720 2274 603 41 0 2679 0
vsize: 10880
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2334 0 0 0 17998 5 0 0 25 0 1 0 422039641 11141120 2274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2720 2274 603 41 0 2679 0
vsize: 10880
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2334 0 0 0 18999 5 0 0 25 0 1 0 422039641 11141120 2274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2720 2274 603 41 0 2679 0
vsize: 10880
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2344 0 0 0 19999 5 0 0 25 0 1 0 422039641 11173888 2283 4294967295 134512640 134672761 3221224576 3221223724 134614482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2283 603 41 0 2687 0
vsize: 10912
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2347 0 0 0 20999 5 0 0 25 0 1 0 422039641 11173888 2286 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2286 603 41 0 2687 0
vsize: 10912
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2347 0 0 0 22000 5 0 0 25 0 1 0 422039641 11173888 2286 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2286 603 41 0 2687 0
vsize: 10912
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2347 0 0 0 23000 5 0 0 25 0 1 0 422039641 11173888 2286 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2286 603 41 0 2687 0
vsize: 10912
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2402 0 0 0 24000 5 0 0 25 0 1 0 422039641 11403264 2341 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2784 2341 603 41 0 2743 0
vsize: 11136
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2440 0 0 0 25000 6 0 0 25 0 1 0 422039641 11534336 2379 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2816 2379 603 41 0 2775 0
vsize: 11264
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2510 0 0 0 26000 6 0 0 25 0 1 0 422039641 11841536 2448 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2891 2448 603 41 0 2850 0
vsize: 11564
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2617 0 0 0 27000 6 0 0 25 0 1 0 422039641 12275712 2554 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2554 603 41 0 2956 0
vsize: 11988
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2617 0 0 0 28001 6 0 0 25 0 1 0 422039641 12275712 2554 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2997 2554 603 41 0 2956 0
vsize: 11988
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2688 0 0 0 29001 6 0 0 25 0 1 0 422039641 12562432 2624 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3067 2624 603 41 0 3026 0
vsize: 12268
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2766 0 0 0 30001 7 0 0 25 0 1 0 422039641 12877824 2701 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2701 603 41 0 3103 0
vsize: 12576
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2766 0 0 0 31001 7 0 0 25 0 1 0 422039641 12877824 2701 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2701 603 41 0 3103 0
vsize: 12576
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2851 0 0 0 32001 7 0 0 25 0 1 0 422039641 13205504 2785 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3224 2785 603 41 0 3183 0
vsize: 12896
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2851 0 0 0 33001 7 0 0 25 0 1 0 422039641 13205504 2785 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3224 2785 603 41 0 3183 0
vsize: 12896
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2868 0 0 0 34002 7 0 0 25 0 1 0 422039641 13266944 2801 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2801 603 41 0 3198 0
vsize: 12956
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2868 0 0 0 35002 7 0 0 25 0 1 0 422039641 13266944 2801 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2801 603 41 0 3198 0
vsize: 12956
[startup+359.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2881 0 0 0 36002 7 0 0 25 0 1 0 422039641 13316096 2813 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3251 2813 603 41 0 3210 0
vsize: 13004
[startup+369.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2890 0 0 0 37002 7 0 0 25 0 1 0 422039641 13479936 2822 4294967295 134512640 134672761 3221224576 3221223672 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2822 603 41 0 3250 0
vsize: 13164
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2890 0 0 0 38003 7 0 0 25 0 1 0 422039641 13348864 2821 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3259 2821 603 41 0 3218 0
vsize: 13036
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2891 0 0 0 39003 7 0 0 25 0 1 0 422039641 13348864 2822 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3259 2822 603 41 0 3218 0
vsize: 13036
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2891 0 0 0 40004 7 0 0 25 0 1 0 422039641 13348864 2822 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3259 2822 603 41 0 3218 0
vsize: 13036
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2900 0 0 0 41004 7 0 0 25 0 1 0 422039641 13381632 2830 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2830 603 41 0 3226 0
vsize: 13068
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2901 0 0 0 42004 7 0 0 25 0 1 0 422039641 13381632 2831 4294967295 134512640 134672761 3221224576 3221223760 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2831 603 41 0 3226 0
vsize: 13068
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2901 0 0 0 43004 7 0 0 25 0 1 0 422039641 13381632 2831 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2831 603 41 0 3226 0
vsize: 13068
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2901 0 0 0 44005 7 0 0 25 0 1 0 422039641 13381632 2831 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2831 603 41 0 3226 0
vsize: 13068
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2901 0 0 0 45005 7 0 0 25 0 1 0 422039641 13381632 2831 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2831 603 41 0 3226 0
vsize: 13068
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2910 0 0 0 46005 7 0 0 25 0 1 0 422039641 13414400 2839 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3275 2839 603 41 0 3234 0
vsize: 13100
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2910 0 0 0 47006 7 0 0 25 0 1 0 422039641 13414400 2839 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3275 2839 603 41 0 3234 0
vsize: 13100
[startup+479.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2911 0 0 0 48006 7 0 0 25 0 1 0 422039641 13414400 2840 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3275 2840 603 41 0 3234 0
vsize: 13100
[startup+489.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 49006 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+499.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 50006 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+509.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 51007 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+519.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 52007 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+529.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 53008 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 54008 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 55008 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 56009 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+569.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2930 0 0 0 57009 7 0 0 25 0 1 0 422039641 13578240 2859 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3315 2859 603 41 0 3274 0
vsize: 13260
[startup+579.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 58009 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+589.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 59010 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+599.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 60010 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+609.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 61010 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+619.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 62011 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+629.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 63011 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+639.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 64011 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+649.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 65012 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+659.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 66012 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 67012 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+679.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 68012 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+689.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2954 0 0 0 69013 7 0 0 25 0 1 0 422039641 13643776 2883 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2883 603 41 0 3290 0
vsize: 13324
[startup+699.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2955 0 0 0 70013 7 0 0 25 0 1 0 422039641 13643776 2884 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2884 603 41 0 3290 0
vsize: 13324
[startup+709.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2955 0 0 0 71013 7 0 0 25 0 1 0 422039641 13643776 2884 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2884 603 41 0 3290 0
vsize: 13324
[startup+719.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2955 0 0 0 72014 7 0 0 25 0 1 0 422039641 13643776 2884 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2884 603 41 0 3290 0
vsize: 13324
[startup+729.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2955 0 0 0 73014 7 0 0 25 0 1 0 422039641 13643776 2884 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2884 603 41 0 3290 0
vsize: 13324
[startup+739.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2955 0 0 0 74014 7 0 0 25 0 1 0 422039641 13643776 2884 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3331 2884 603 41 0 3290 0
vsize: 13324
[startup+749.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 2992 0 0 0 75015 7 0 0 25 0 1 0 422039641 13774848 2921 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2921 603 41 0 3322 0
vsize: 13452
[startup+759.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3073 0 0 0 76014 8 0 0 25 0 1 0 422039641 14077952 3001 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3001 603 41 0 3396 0
vsize: 13748
[startup+769.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3073 0 0 0 77015 8 0 0 25 0 1 0 422039641 14077952 3001 4294967295 134512640 134672761 3221224576 3221223744 134614551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3001 603 41 0 3396 0
vsize: 13748
[startup+779.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3073 0 0 0 78015 8 0 0 25 0 1 0 422039641 14077952 3001 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3001 603 41 0 3396 0
vsize: 13748
[startup+789.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3074 0 0 0 79015 8 0 0 25 0 1 0 422039641 14077952 3002 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3002 603 41 0 3396 0
vsize: 13748
[startup+799.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3074 0 0 0 80016 8 0 0 25 0 1 0 422039641 14077952 3002 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3002 603 41 0 3396 0
vsize: 13748
[startup+809.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3074 0 0 0 81016 8 0 0 25 0 1 0 422039641 14077952 3002 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3437 3002 603 41 0 3396 0
vsize: 13748
[startup+819.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3095 0 0 0 82017 8 0 0 25 0 1 0 422039641 14159872 3023 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3457 3023 603 41 0 3416 0
vsize: 13828
[startup+829.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3095 0 0 0 83017 8 0 0 25 0 1 0 422039641 14159872 3023 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3457 3023 603 41 0 3416 0
vsize: 13828
[startup+839.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3095 0 0 0 84017 8 0 0 25 0 1 0 422039641 14159872 3023 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3457 3023 603 41 0 3416 0
vsize: 13828
[startup+849.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3103 0 0 0 85018 8 0 0 25 0 1 0 422039641 14192640 3030 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 3030 603 41 0 3424 0
vsize: 13860
[startup+859.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3103 0 0 0 86018 8 0 0 25 0 1 0 422039641 14192640 3030 4294967295 134512640 134672761 3221224576 3221223760 134615544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 3030 603 41 0 3424 0
vsize: 13860
[startup+869.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3104 0 0 0 87018 8 0 0 25 0 1 0 422039641 14192640 3031 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 3031 603 41 0 3424 0
vsize: 13860
[startup+879.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3104 0 0 0 88019 8 0 0 25 0 1 0 422039641 14192640 3031 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 3031 603 41 0 3424 0
vsize: 13860
[startup+889.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3104 0 0 0 89019 8 0 0 25 0 1 0 422039641 14192640 3031 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3465 3031 603 41 0 3424 0
vsize: 13860
[startup+899.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3120 0 0 0 90019 8 0 0 25 0 1 0 422039641 14258176 3046 4294967295 134512640 134672761 3221224576 3221223568 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3046 603 41 0 3440 0
vsize: 13924
[startup+909.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3120 0 0 0 91020 8 0 0 25 0 1 0 422039641 14258176 3046 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3046 603 41 0 3440 0
vsize: 13924
[startup+919.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3120 0 0 0 92020 8 0 0 25 0 1 0 422039641 14258176 3046 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3481 3046 603 41 0 3440 0
vsize: 13924
[startup+929.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3130 0 0 0 93020 8 0 0 25 0 1 0 422039641 14290944 3055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3055 603 41 0 3448 0
vsize: 13956
[startup+939.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3130 0 0 0 94021 8 0 0 25 0 1 0 422039641 14290944 3055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3055 603 41 0 3448 0
vsize: 13956
[startup+949.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3130 0 0 0 95021 8 0 0 25 0 1 0 422039641 14290944 3055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3055 603 41 0 3448 0
vsize: 13956
[startup+959.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3131 0 0 0 96021 8 0 0 25 0 1 0 422039641 14290944 3056 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3056 603 41 0 3448 0
vsize: 13956
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3131 0 0 0 97022 8 0 0 25 0 1 0 422039641 14290944 3056 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3056 603 41 0 3448 0
vsize: 13956
[startup+979.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3131 0 0 0 98022 8 0 0 25 0 1 0 422039641 14290944 3056 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3056 603 41 0 3448 0
vsize: 13956
[startup+989.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3131 0 0 0 99022 8 0 0 25 0 1 0 422039641 14290944 3056 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3056 603 41 0 3448 0
vsize: 13956
[startup+999.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3131 0 0 0 100023 8 0 0 25 0 1 0 422039641 14290944 3056 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3489 3056 603 41 0 3448 0
vsize: 13956
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3139 0 0 0 101023 8 0 0 25 0 1 0 422039641 14323712 3063 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3497 3063 603 41 0 3456 0
vsize: 13988
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3139 0 0 0 102023 8 0 0 25 0 1 0 422039641 14323712 3063 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3497 3063 603 41 0 3456 0
vsize: 13988
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3139 0 0 0 103024 8 0 0 25 0 1 0 422039641 14323712 3063 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3497 3063 603 41 0 3456 0
vsize: 13988
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3148 0 0 0 104024 8 0 0 25 0 1 0 422039641 14356480 3071 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3505 3071 603 41 0 3464 0
vsize: 14020
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3148 0 0 0 105024 8 0 0 25 0 1 0 422039641 14356480 3071 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3505 3071 603 41 0 3464 0
vsize: 14020
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3185 0 0 0 106024 8 0 0 25 0 1 0 422039641 14503936 3107 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3541 3107 603 41 0 3500 0
vsize: 14164
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3185 0 0 0 107025 8 0 0 25 0 1 0 422039641 14503936 3107 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3541 3107 603 41 0 3500 0
vsize: 14164
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3185 0 0 0 108025 8 0 0 25 0 1 0 422039641 14503936 3107 4294967295 134512640 134672761 3221224576 3221223712 134614516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3541 3107 603 41 0 3500 0
vsize: 14164
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3238 0 0 0 109025 8 0 0 25 0 1 0 422039641 14716928 3160 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3160 603 41 0 3552 0
vsize: 14372
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3238 0 0 0 110026 8 0 0 25 0 1 0 422039641 14716928 3160 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3593 3160 603 41 0 3552 0
vsize: 14372
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3254 0 0 0 111026 8 0 0 25 0 1 0 422039641 14782464 3175 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3609 3175 603 41 0 3568 0
vsize: 14436
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3254 0 0 0 112027 8 0 0 25 0 1 0 422039641 14782464 3175 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3609 3175 603 41 0 3568 0
vsize: 14436
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3254 0 0 0 113028 8 0 0 25 0 1 0 422039641 14782464 3175 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3609 3175 603 41 0 3568 0
vsize: 14436
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3271 0 0 0 114028 9 0 0 25 0 1 0 422039641 14848000 3191 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3625 3191 603 41 0 3584 0
vsize: 14500
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3271 0 0 0 115029 9 0 0 25 0 1 0 422039641 14848000 3191 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3625 3191 603 41 0 3584 0
vsize: 14500
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3271 0 0 0 116029 9 0 0 25 0 1 0 422039641 14848000 3191 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3625 3191 603 41 0 3584 0
vsize: 14500
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3285 0 0 0 117029 9 0 0 25 0 1 0 422039641 14880768 3204 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3204 603 41 0 3592 0
vsize: 14532
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3285 0 0 0 118030 9 0 0 25 0 1 0 422039641 14880768 3204 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3204 603 41 0 3592 0
vsize: 14532
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3285 0 0 0 119030 9 0 0 25 0 1 0 422039641 14880768 3204 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3204 603 41 0 3592 0
vsize: 14532
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 976
Raw data (stat): 976 (minisat+) R 975 29653 29652 0 -1 0 3285 0 0 0 120031 9 0 0 25 0 1 0 422039641 14880768 3204 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3204 603 41 0 3592 0
vsize: 14532
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 976
Raw data (stat): 976 (minisat+) Z 975 29653 29652 0 -1 12 3285 0 0 0 120031 9 0 0 25 0 1 0 422039641 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.41
CPU user time (s): 1200.31
CPU system time (s): 0.096985
CPU usage (%): 100.032
Max. virtual memory (Kb): 14532
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####