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-2.opb
MD5SUM	48ed39004ec868a1cad026c865b17eb2
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	13429
Number of constraints which are clauses	13429
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 5542

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 00:25:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3966 boxname=wulflinc18 idbench=206 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48ed39004ec868a1cad026c865b17eb2  /oldhome/oroussel/tmp/wulflinc18/normalized-par32-2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-par32-2.opb /oldhome/oroussel/tmp/wulflinc18/normalized-par32-2.opb
IDLAUNCH: 3966
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        885844 kB
Buffers:         34480 kB
Cached:          78488 kB
SwapCached:        320 kB
Active:          55032 kB
Inactive:        61120 kB
HighTotal:      131008 kB
HighFree:        48580 kB
LowTotal:       903652 kB
LowFree:        837264 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27196 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:45:05 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 3966 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13025 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9654    24020 |    2896       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4784          
c   -- var.elim.:  2000/4784          
c   -- var.elim.:  3000/4784          
c   -- var.elim.:  4000/4784          
c   -- var.elim.:  4784/4784          
c |         0 |    9654    24020 |    3861       0        0     nan |  0.000 % |
c |       101 |    9654    24020 |    4247     101      973     9.6 | 24.686 % |
c |       252 |    9654    24020 |    4672     252     6469    25.7 | 24.685 % |
c |       478 |    9654    24020 |    5139     478    13468    28.2 | 24.685 % |
c |       815 |    9654    24020 |    5653     815    27675    34.0 | 24.68#### 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.91 0.94 0.90 2/55 25314
Raw data (stat): 25314 (runsolver) R 25313 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480244336 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.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1563 0 0 0 993 5 0 0 25 0 1 0 480244336 7823360 1503 4294967295 134512640 134672761 3221224560 3221223744 134615629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1910 1503 603 41 0 1869 0
vsize: 7640
[startup+20.001 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1684 0 0 0 1993 5 0 0 25 0 1 0 480244336 8404992 1624 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2052 1624 603 41 0 2011 0
vsize: 8208
[startup+30.0013 s]
Raw data (loadavg): 0.94 0.94 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1756 0 0 0 2993 5 0 0 25 0 1 0 480244336 8671232 1696 4294967295 134512640 134672761 3221224560 3221223600 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2117 1696 603 41 0 2076 0
vsize: 8468
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1810 0 0 0 3993 6 0 0 25 0 1 0 480244336 8929280 1750 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2180 1750 603 41 0 2139 0
vsize: 8720
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1873 0 0 0 4993 6 0 0 25 0 1 0 480244336 9228288 1813 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1813 603 41 0 2212 0
vsize: 9012
[startup+60.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1889 0 0 0 5993 6 0 0 25 0 1 0 480244336 9228288 1829 4294967295 134512640 134672761 3221224560 3221223696 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2253 1829 603 41 0 2212 0
vsize: 9012
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1956 0 0 0 6994 6 0 0 25 0 1 0 480244336 9490432 1896 4294967295 134512640 134672761 3221224560 3221223556 1075346557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2317 1896 603 41 0 2276 0
vsize: 9268
[startup+80.0025 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 1983 0 0 0 7994 6 0 0 25 0 1 0 480244336 9621504 1923 4294967295 134512640 134672761 3221224560 3221223600 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1923 603 41 0 2308 0
vsize: 9396
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2001 0 0 0 8994 6 0 0 25 0 1 0 480244336 9756672 1941 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2382 1941 603 41 0 2341 0
vsize: 9528
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2060 0 0 0 9994 6 0 0 25 0 1 0 480244336 9887744 2000 4294967295 134512640 134672761 3221224560 3221223600 134612642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2000 603 41 0 2373 0
vsize: 9656
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2075 0 0 0 10994 6 0 0 25 0 1 0 480244336 10010624 2015 4294967295 134512640 134672761 3221224560 3221223696 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 2015 603 41 0 2403 0
vsize: 9776
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2083 0 0 0 11994 6 0 0 25 0 1 0 480244336 10010624 2023 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 2023 603 41 0 2403 0
vsize: 9776
[startup+130.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2083 0 0 0 12994 6 0 0 25 0 1 0 480244336 10010624 2023 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 2023 603 41 0 2403 0
vsize: 9776
[startup+140.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2091 0 0 0 13995 6 0 0 25 0 1 0 480244336 10010624 2031 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 2031 603 41 0 2403 0
vsize: 9776
[startup+150.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2188 0 0 0 14995 6 0 0 25 0 1 0 480244336 10407936 2128 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2541 2128 603 41 0 2500 0
vsize: 10164
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2208 0 0 0 15995 6 0 0 25 0 1 0 480244336 10543104 2148 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2574 2148 603 41 0 2533 0
vsize: 10296
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2208 0 0 0 16995 6 0 0 25 0 1 0 480244336 10543104 2148 4294967295 134512640 134672761 3221224560 3221223744 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2574 2148 603 41 0 2533 0
vsize: 10296
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2230 0 0 0 17995 7 0 0 25 0 1 0 480244336 10645504 2170 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2599 2170 603 41 0 2558 0
vsize: 10396
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2230 0 0 0 18995 7 0 0 25 0 1 0 480244336 10645504 2170 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2599 2170 603 41 0 2558 0
vsize: 10396
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2230 0 0 0 19995 7 0 0 25 0 1 0 480244336 10645504 2170 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2599 2170 603 41 0 2558 0
vsize: 10396
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2230 0 0 0 20995 7 0 0 25 0 1 0 480244336 10645504 2170 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2599 2170 603 41 0 2558 0
vsize: 10396
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2300 0 0 0 21995 7 0 0 25 0 1 0 480244336 11112448 2240 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2240 603 41 0 2672 0
vsize: 10852
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2300 0 0 0 22996 7 0 0 25 0 1 0 480244336 10981376 2239 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2681 2239 603 41 0 2640 0
vsize: 10724
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2318 0 0 0 23996 7 0 0 25 0 1 0 480244336 11055104 2257 4294967295 134512640 134672761 3221224560 3221223740 134615849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2699 2257 603 41 0 2658 0
vsize: 10796
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2336 0 0 0 24996 7 0 0 25 0 1 0 480244336 11137024 2275 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2719 2275 603 41 0 2678 0
vsize: 10876
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2337 0 0 0 25996 7 0 0 25 0 1 0 480244336 11137024 2276 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2719 2276 603 41 0 2678 0
vsize: 10876
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2342 0 0 0 26996 7 0 0 25 0 1 0 480244336 11149312 2280 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2722 2280 603 41 0 2681 0
vsize: 10888
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2343 0 0 0 27996 7 0 0 25 0 1 0 480244336 11149312 2281 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2722 2281 603 41 0 2681 0
vsize: 10888
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2343 0 0 0 28997 7 0 0 25 0 1 0 480244336 11149312 2281 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2722 2281 603 41 0 2681 0
vsize: 10888
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2352 0 0 0 29997 7 0 0 25 0 1 0 480244336 11182080 2289 4294967295 134512640 134672761 3221224560 3221223696 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2730 2289 603 41 0 2689 0
vsize: 10920
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2364 0 0 0 30997 7 0 0 25 0 1 0 480244336 11231232 2300 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2300 603 41 0 2701 0
vsize: 10968
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2364 0 0 0 31997 7 0 0 25 0 1 0 480244336 11231232 2300 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2742 2300 603 41 0 2701 0
vsize: 10968
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2449 0 0 0 32997 7 0 0 25 0 1 0 480244336 11558912 2384 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2384 603 41 0 2781 0
vsize: 11288
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2449 0 0 0 33997 7 0 0 25 0 1 0 480244336 11558912 2384 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2384 603 41 0 2781 0
vsize: 11288
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2463 0 0 0 34997 7 0 0 25 0 1 0 480244336 11608064 2397 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2397 603 41 0 2793 0
vsize: 11336
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2463 0 0 0 35997 7 0 0 25 0 1 0 480244336 11608064 2397 4294967295 134512640 134672761 3221224560 3221223600 134612578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2397 603 41 0 2793 0
vsize: 11336
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2473 0 0 0 36997 7 0 0 25 0 1 0 480244336 11640832 2406 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2406 603 41 0 2801 0
vsize: 11368
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2473 0 0 0 37997 7 0 0 25 0 1 0 480244336 11640832 2406 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2406 603 41 0 2801 0
vsize: 11368
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2473 0 0 0 38998 7 0 0 25 0 1 0 480244336 11640832 2406 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2406 603 41 0 2801 0
vsize: 11368
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2473 0 0 0 39998 7 0 0 25 0 1 0 480244336 11640832 2406 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2406 603 41 0 2801 0
vsize: 11368
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2482 0 0 0 40998 7 0 0 25 0 1 0 480244336 11673600 2414 4294967295 134512640 134672761 3221224560 3221223696 134614674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2850 2414 603 41 0 2809 0
vsize: 11400
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2491 0 0 0 41998 7 0 0 25 0 1 0 480244336 11706368 2422 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2858 2422 603 41 0 2817 0
vsize: 11432
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2491 0 0 0 42998 7 0 0 25 0 1 0 480244336 11706368 2422 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2858 2422 603 41 0 2817 0
vsize: 11432
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2500 0 0 0 43999 7 0 0 25 0 1 0 480244336 11739136 2430 4294967295 134512640 134672761 3221224560 3221223744 134615514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2866 2430 603 41 0 2825 0
vsize: 11464
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2500 0 0 0 44999 7 0 0 25 0 1 0 480244336 11739136 2430 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2866 2430 603 41 0 2825 0
vsize: 11464
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2509 0 0 0 45999 7 0 0 25 0 1 0 480244336 11771904 2438 4294967295 134512640 134672761 3221224560 3221223552 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2874 2438 603 41 0 2833 0
vsize: 11496
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2509 0 0 0 46999 7 0 0 25 0 1 0 480244336 11771904 2438 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2874 2438 603 41 0 2833 0
vsize: 11496
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2547 0 0 0 47999 7 0 0 25 0 1 0 480244336 11927552 2475 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2912 2475 603 41 0 2871 0
vsize: 11648
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2547 0 0 0 49000 7 0 0 25 0 1 0 480244336 11927552 2475 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2912 2475 603 41 0 2871 0
vsize: 11648
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2564 0 0 0 50000 7 0 0 25 0 1 0 480244336 11993088 2491 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2928 2491 603 41 0 2887 0
vsize: 11712
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2599 0 0 0 51000 7 0 0 25 0 1 0 480244336 12124160 2526 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2526 603 41 0 2919 0
vsize: 11840
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2646 0 0 0 52000 8 0 0 25 0 1 0 480244336 12410880 2573 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3030 2573 603 41 0 2989 0
vsize: 12120
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2646 0 0 0 53000 8 0 0 25 0 1 0 480244336 12410880 2573 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3030 2573 603 41 0 2989 0
vsize: 12120
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2646 0 0 0 54000 8 0 0 25 0 1 0 480244336 12410880 2573 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3030 2573 603 41 0 2989 0
vsize: 12120
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2646 0 0 0 55000 8 0 0 25 0 1 0 480244336 12410880 2573 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3030 2573 603 41 0 2989 0
vsize: 12120
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2671 0 0 0 56000 8 0 0 25 0 1 0 480244336 12476416 2598 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2598 603 41 0 3005 0
vsize: 12184
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2671 0 0 0 57001 8 0 0 25 0 1 0 480244336 12476416 2598 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2598 603 41 0 3005 0
vsize: 12184
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2672 0 0 0 58001 8 0 0 25 0 1 0 480244336 12476416 2599 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2599 603 41 0 3005 0
vsize: 12184
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2672 0 0 0 59001 8 0 0 25 0 1 0 480244336 12476416 2599 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2599 603 41 0 3005 0
vsize: 12184
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 60001 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 61001 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 62002 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 63002 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 64002 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 65002 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 66002 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 67003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 68003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 69003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 70003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 71003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2679 0 0 0 72003 8 0 0 25 0 1 0 480244336 12476416 2606 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3046 2606 603 41 0 3005 0
vsize: 12184
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2689 0 0 0 73003 8 0 0 25 0 1 0 480244336 12509184 2615 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2615 603 41 0 3013 0
vsize: 12216
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2689 0 0 0 74003 8 0 0 25 0 1 0 480244336 12509184 2615 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2615 603 41 0 3013 0
vsize: 12216
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2689 0 0 0 75004 8 0 0 25 0 1 0 480244336 12509184 2615 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2615 603 41 0 3013 0
vsize: 12216
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2689 0 0 0 76004 8 0 0 25 0 1 0 480244336 12509184 2615 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2615 603 41 0 3013 0
vsize: 12216
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2689 0 0 0 77004 8 0 0 25 0 1 0 480244336 12509184 2615 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2615 603 41 0 3013 0
vsize: 12216
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2754 0 0 0 78004 8 0 0 25 0 1 0 480244336 12754944 2680 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2680 603 41 0 3073 0
vsize: 12456
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2754 0 0 0 79004 8 0 0 25 0 1 0 480244336 12754944 2680 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2680 603 41 0 3073 0
vsize: 12456
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2755 0 0 0 80004 8 0 0 25 0 1 0 480244336 12754944 2681 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2681 603 41 0 3073 0
vsize: 12456
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2785 0 0 0 81004 8 0 0 25 0 1 0 480244336 12890112 2711 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2711 603 41 0 3106 0
vsize: 12588
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2785 0 0 0 82005 8 0 0 25 0 1 0 480244336 12890112 2711 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2711 603 41 0 3106 0
vsize: 12588
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2802 0 0 0 83005 8 0 0 25 0 1 0 480244336 12955648 2727 4294967295 134512640 134672761 3221224560 3221223744 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3163 2727 603 41 0 3122 0
vsize: 12652
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2802 0 0 0 84005 8 0 0 25 0 1 0 480244336 12955648 2727 4294967295 134512640 134672761 3221224560 3221223584 134612939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3163 2727 603 41 0 3122 0
vsize: 12652
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2802 0 0 0 85005 8 0 0 25 0 1 0 480244336 12955648 2727 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3163 2727 603 41 0 3122 0
vsize: 12652
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2819 0 0 0 86005 8 0 0 25 0 1 0 480244336 13021184 2743 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2743 603 41 0 3138 0
vsize: 12716
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2819 0 0 0 87005 8 0 0 25 0 1 0 480244336 13021184 2743 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2743 603 41 0 3138 0
vsize: 12716
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2819 0 0 0 88005 8 0 0 25 0 1 0 480244336 13021184 2743 4294967295 134512640 134672761 3221224560 3221223736 134615853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2743 603 41 0 3138 0
vsize: 12716
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2833 0 0 0 89006 8 0 0 25 0 1 0 480244336 13070336 2756 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3191 2756 603 41 0 3150 0
vsize: 12764
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2833 0 0 0 90005 8 0 0 25 0 1 0 480244336 13070336 2756 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3191 2756 603 41 0 3150 0
vsize: 12764
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2852 0 0 0 91005 8 0 0 25 0 1 0 480244336 13201408 2775 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2775 603 41 0 3182 0
vsize: 12892
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2882 0 0 0 92006 9 0 0 25 0 1 0 480244336 13266944 2804 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2804 603 41 0 3198 0
vsize: 12956
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2882 0 0 0 93006 9 0 0 25 0 1 0 480244336 13266944 2804 4294967295 134512640 134672761 3221224560 3221223744 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2804 603 41 0 3198 0
vsize: 12956
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2905 0 0 0 94006 9 0 0 25 0 1 0 480244336 13357056 2827 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3261 2827 603 41 0 3220 0
vsize: 13044
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2905 0 0 0 95006 9 0 0 25 0 1 0 480244336 13357056 2827 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3261 2827 603 41 0 3220 0
vsize: 13044
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2905 0 0 0 96006 9 0 0 25 0 1 0 480244336 13357056 2827 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3261 2827 603 41 0 3220 0
vsize: 13044
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2914 0 0 0 97006 9 0 0 25 0 1 0 480244336 13389824 2835 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2835 603 41 0 3228 0
vsize: 13076
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2914 0 0 0 98007 9 0 0 25 0 1 0 480244336 13389824 2835 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2835 603 41 0 3228 0
vsize: 13076
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2914 0 0 0 99007 9 0 0 25 0 1 0 480244336 13389824 2835 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2835 603 41 0 3228 0
vsize: 13076
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2914 0 0 0 100007 9 0 0 25 0 1 0 480244336 13389824 2835 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2835 603 41 0 3228 0
vsize: 13076
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2914 0 0 0 101007 9 0 0 25 0 1 0 480244336 13389824 2835 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2835 603 41 0 3228 0
vsize: 13076
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2915 0 0 0 102007 9 0 0 25 0 1 0 480244336 13389824 2836 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2836 603 41 0 3228 0
vsize: 13076
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2915 0 0 0 103008 9 0 0 25 0 1 0 480244336 13389824 2836 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2836 603 41 0 3228 0
vsize: 13076
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2915 0 0 0 104008 9 0 0 25 0 1 0 480244336 13389824 2836 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2836 603 41 0 3228 0
vsize: 13076
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2915 0 0 0 105008 9 0 0 25 0 1 0 480244336 13389824 2836 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2836 603 41 0 3228 0
vsize: 13076
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2915 0 0 0 106008 9 0 0 25 0 1 0 480244336 13389824 2836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2836 603 41 0 3228 0
vsize: 13076
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2924 0 0 0 107008 9 0 0 25 0 1 0 480244336 13422592 2844 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2844 603 41 0 3236 0
vsize: 13108
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2924 0 0 0 108008 9 0 0 25 0 1 0 480244336 13422592 2844 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2844 603 41 0 3236 0
vsize: 13108
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2924 0 0 0 109009 9 0 0 25 0 1 0 480244336 13422592 2844 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2844 603 41 0 3236 0
vsize: 13108
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2924 0 0 0 110009 9 0 0 25 0 1 0 480244336 13422592 2844 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2844 603 41 0 3236 0
vsize: 13108
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2924 0 0 0 111009 9 0 0 25 0 1 0 480244336 13422592 2844 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2844 603 41 0 3236 0
vsize: 13108
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2926 0 0 0 112009 9 0 0 25 0 1 0 480244336 13422592 2846 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2846 603 41 0 3236 0
vsize: 13108
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2942 0 0 0 113009 9 0 0 25 0 1 0 480244336 13488128 2861 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3293 2861 603 41 0 3252 0
vsize: 13172
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2942 0 0 0 114009 9 0 0 25 0 1 0 480244336 13488128 2861 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3293 2861 603 41 0 3252 0
vsize: 13172
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2943 0 0 0 115010 9 0 0 25 0 1 0 480244336 13488128 2862 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3293 2862 603 41 0 3252 0
vsize: 13172
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2987 0 0 0 116010 9 0 0 25 0 1 0 480244336 13656064 2905 4294967295 134512640 134672761 3221224560 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3334 2905 603 41 0 3293 0
vsize: 13336
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2987 0 0 0 117010 9 0 0 25 0 1 0 480244336 13656064 2905 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3334 2905 603 41 0 3293 0
vsize: 13336
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 2987 0 0 0 118010 9 0 0 25 0 1 0 480244336 13656064 2905 4294967295 134512640 134672761 3221224560 3221223724 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3334 2905 603 41 0 3293 0
vsize: 13336
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 3004 0 0 0 119010 9 0 0 25 0 1 0 480244336 13721600 2921 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3350 2921 603 41 0 3309 0
vsize: 13400
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20024 20023 0 -1 0 3004 0 0 0 120010 9 0 0 25 0 1 0 480244336 13721600 2921 4294967295 134512640 134672761 3221224560 3221223744 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3350 2921 603 41 0 3309 0
vsize: 13400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 25322
Raw data (stat): 25314 (minisat+) Z 25313 20024 20023 0 -1 12 3004 0 0 0 120010 10 0 0 25 0 1 0 480244336 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.04
CPU time (s): 1200.21
CPU user time (s): 1200.11
CPU system time (s): 0.101984
CPU usage (%): 100.014
Max. virtual memory (Kb): 13400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####