PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-par32-3-c.opb
MD5SUM	b552ff39062b6c42ea64365c815cbd78
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	2650
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	2650
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2650
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2650
Total number of constraints	6619
Number of constraints which are clauses	6619
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3
Trace number 5544

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 00:25:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3967 boxname=wulflinc21 idbench=207 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b552ff39062b6c42ea64365c815cbd78  /oldhome/oroussel/tmp/wulflinc21/normalized-par32-3-c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-par32-3-c.opb /oldhome/oroussel/tmp/wulflinc21/normalized-par32-3-c.opb
IDLAUNCH: 3967
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        902092 kB
Buffers:         27232 kB
Cached:          85580 kB
SwapCached:          0 kB
Active:          34400 kB
Inactive:        81276 kB
HighTotal:      131008 kB
HighFree:        41832 kB
LowTotal:       903652 kB
LowFree:        860260 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11400 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:45:17 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3967 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6619 PB-constraints to clauses...
c   -- Unit propagations: (none)
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 |    6619    18160 |    1985       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2650          
c   -- var.elim.:  2000/2650          
c   -- var.elim.:  2650/2650          
c |         0 |    6497    17794 |      --       0       --      -- |     --   | -122/-366
c |         0 |    6497    17794 |    2598       0        0     nan |  0.000 % |
c |       101 |    6497    17794 |    2858     101     3036    30.1 |  0.004 % |
c |       253 |    6497    17794 |    3144     253     8505    33.6 |  0.000 % |
c |       479 |    6490    17774 |    3455     478    16458    34.4 |  0.075 % |
c |       816 |    6490    17774 |    3800     815    29275    35.9 |  0.075 % |
c |      1323 |    6490    17774 |    4180    1322    50665    38.3 |  0.075 % |
c |      2085 |    6490    17774 |    4598    2084    79616    38.2 |  0.075 % |
c |      3225 |    6490    17774 |    5058    3224   127290    39.5 |  0.075 % |
c |      4934 |    6490    17774 |    5564    4933   210092    42.6 |  0.075 % |#### 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.98 0.91 2/55 2884
Raw data (stat): 2884 (runsolver) R 2883 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 357516343 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+9.99992 s]
Raw data (loadavg): 0.93 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1128 0 0 0 996 3 0 0 25 0 1 0 357516343 6156288 1106 4294967295 134512640 134672761 3221224560 3221223744 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1503 1106 603 41 0 1462 0
vsize: 6012
[startup+19.9996 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1197 0 0 0 1996 3 0 0 25 0 1 0 357516343 6430720 1175 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1570 1175 603 41 0 1529 0
vsize: 6280
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1352 0 0 0 2995 4 0 0 25 0 1 0 357516343 7163904 1330 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1749 1330 603 41 0 1708 0
vsize: 6996
[startup+40.0004 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1433 0 0 0 3995 4 0 0 25 0 1 0 357516343 7503872 1411 4294967295 134512640 134672761 3221224560 3221223552 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1832 1411 603 41 0 1791 0
vsize: 7328
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1464 0 0 0 4995 4 0 0 25 0 1 0 357516343 7622656 1442 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1861 1442 603 41 0 1820 0
vsize: 7444
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1480 0 0 0 5995 4 0 0 25 0 1 0 357516343 7622656 1458 4294967295 134512640 134672761 3221224560 3221223760 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1861 1458 603 41 0 1820 0
vsize: 7444
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1580 0 0 0 6995 5 0 0 25 0 1 0 357516343 8089600 1558 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1558 603 41 0 1934 0
vsize: 7900
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1651 0 0 0 7995 5 0 0 25 0 1 0 357516343 8355840 1629 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1629 603 41 0 1999 0
vsize: 8160
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1659 0 0 0 8995 5 0 0 25 0 1 0 357516343 8355840 1637 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1637 603 41 0 1999 0
vsize: 8160
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1659 0 0 0 9995 5 0 0 25 0 1 0 357516343 8355840 1637 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1637 603 41 0 1999 0
vsize: 8160
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1660 0 0 0 10995 5 0 0 25 0 1 0 357516343 8355840 1638 4294967295 134512640 134672761 3221224560 3221223744 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1638 603 41 0 1999 0
vsize: 8160
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1661 0 0 0 11995 5 0 0 25 0 1 0 357516343 8355840 1639 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1639 603 41 0 1999 0
vsize: 8160
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1664 0 0 0 12995 5 0 0 25 0 1 0 357516343 8355840 1642 4294967295 134512640 134672761 3221224560 3221223600 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1642 603 41 0 1999 0
vsize: 8160
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1687 0 0 0 13995 5 0 0 25 0 1 0 357516343 8478720 1665 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2070 1665 603 41 0 2029 0
vsize: 8280
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1697 0 0 0 14995 5 0 0 25 0 1 0 357516343 8552448 1675 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1675 603 41 0 2047 0
vsize: 8352
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1741 0 0 0 15995 5 0 0 25 0 1 0 357516343 8683520 1719 4294967295 134512640 134672761 3221224560 3221223696 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2120 1719 603 41 0 2079 0
vsize: 8480
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1786 0 0 0 16995 5 0 0 25 0 1 0 357516343 8908800 1764 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2175 1764 603 41 0 2134 0
vsize: 8700
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1913 0 0 0 17995 6 0 0 25 0 1 0 357516343 9449472 1891 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1891 603 41 0 2266 0
vsize: 9228
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1976 0 0 0 18995 6 0 0 25 0 1 0 357516343 9707520 1954 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2370 1954 603 41 0 2329 0
vsize: 9480
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1980 0 0 0 19995 6 0 0 25 0 1 0 357516343 9707520 1958 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2370 1958 603 41 0 2329 0
vsize: 9480
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 1984 0 0 0 20995 6 0 0 25 0 1 0 357516343 9707520 1962 4294967295 134512640 134672761 3221224560 3221223600 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2370 1962 603 41 0 2329 0
vsize: 9480
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2001 0 0 0 21995 6 0 0 25 0 1 0 357516343 9805824 1979 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1979 603 41 0 2353 0
vsize: 9576
[startup+230.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2001 0 0 0 22996 6 0 0 25 0 1 0 357516343 9805824 1979 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1979 603 41 0 2353 0
vsize: 9576
[startup+240.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2001 0 0 0 23996 6 0 0 25 0 1 0 357516343 9805824 1979 4294967295 134512640 134672761 3221224560 3221223744 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1979 603 41 0 2353 0
vsize: 9576
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2071 0 0 0 24996 6 0 0 25 0 1 0 357516343 10055680 2049 4294967295 134512640 134672761 3221224560 3221223636 1075347048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2455 2049 603 41 0 2414 0
vsize: 9820
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2079 0 0 0 25996 6 0 0 25 0 1 0 357516343 10055680 2057 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2455 2057 603 41 0 2414 0
vsize: 9820
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2091 0 0 0 26996 6 0 0 25 0 1 0 357516343 10153984 2069 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2479 2069 603 41 0 2438 0
vsize: 9916
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2124 0 0 0 27996 6 0 0 25 0 1 0 357516343 10289152 2102 4294967295 134512640 134672761 3221224560 3221223408 134645469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2512 2102 603 41 0 2471 0
vsize: 10048
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2133 0 0 0 28996 6 0 0 25 0 1 0 357516343 10289152 2111 4294967295 134512640 134672761 3221224560 3221223600 134612616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2512 2111 603 41 0 2471 0
vsize: 10048
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2133 0 0 0 29997 6 0 0 25 0 1 0 357516343 10289152 2111 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2512 2111 603 41 0 2471 0
vsize: 10048
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2142 0 0 0 30997 6 0 0 25 0 1 0 357516343 10379264 2120 4294967295 134512640 134672761 3221224560 3221223552 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2120 603 41 0 2493 0
vsize: 10136
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2142 0 0 0 31997 6 0 0 25 0 1 0 357516343 10379264 2120 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2120 603 41 0 2493 0
vsize: 10136
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2142 0 0 0 32997 6 0 0 25 0 1 0 357516343 10379264 2120 4294967295 134512640 134672761 3221224560 3221223616 134644272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2120 603 41 0 2493 0
vsize: 10136
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2142 0 0 0 33997 6 0 0 25 0 1 0 357516343 10379264 2120 4294967295 134512640 134672761 3221224560 3221223600 134612983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2120 603 41 0 2493 0
vsize: 10136
[startup+350.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2142 0 0 0 34997 6 0 0 25 0 1 0 357516343 10379264 2120 4294967295 134512640 134672761 3221224560 3221223600 134612670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2120 603 41 0 2493 0
vsize: 10136
[startup+360.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2153 0 0 0 35998 6 0 0 25 0 1 0 357516343 10379264 2131 4294967295 134512640 134672761 3221224560 3221223696 134614661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2131 603 41 0 2493 0
vsize: 10136
[startup+370.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2192 0 0 0 36998 7 0 0 25 0 1 0 357516343 10584064 2170 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2584 2170 603 41 0 2543 0
vsize: 10336
[startup+380.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2250 0 0 0 37997 7 0 0 25 0 1 0 357516343 10813440 2228 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2228 603 41 0 2599 0
vsize: 10560
[startup+390.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2250 0 0 0 38998 7 0 0 25 0 1 0 357516343 10813440 2228 4294967295 134512640 134672761 3221224560 3221223552 134565036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2228 603 41 0 2599 0
vsize: 10560
[startup+400.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2257 0 0 0 39998 7 0 0 25 0 1 0 357516343 10813440 2235 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2235 603 41 0 2599 0
vsize: 10560
[startup+410.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2257 0 0 0 40998 7 0 0 25 0 1 0 357516343 10813440 2235 4294967295 134512640 134672761 3221224560 3221223372 1075349878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2235 603 41 0 2599 0
vsize: 10560
[startup+420.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2265 0 0 0 41998 7 0 0 25 0 1 0 357516343 10813440 2243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2243 603 41 0 2599 0
vsize: 10560
[startup+430.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2265 0 0 0 42998 7 0 0 25 0 1 0 357516343 10813440 2243 4294967295 134512640 134672761 3221224560 3221223600 134613022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2243 603 41 0 2599 0
vsize: 10560
[startup+440.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2266 0 0 0 43998 7 0 0 25 0 1 0 357516343 10813440 2244 4294967295 134512640 134672761 3221224560 3221223724 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2244 603 41 0 2599 0
vsize: 10560
[startup+450.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2266 0 0 0 44998 7 0 0 25 0 1 0 357516343 10813440 2244 4294967295 134512640 134672761 3221224560 3221223600 134612975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2640 2244 603 41 0 2599 0
vsize: 10560
[startup+460.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2274 0 0 0 45999 7 0 0 25 0 1 0 357516343 10911744 2252 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2252 603 41 0 2623 0
vsize: 10656
[startup+470 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2274 0 0 0 46999 7 0 0 25 0 1 0 357516343 10911744 2252 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2252 603 41 0 2623 0
vsize: 10656
[startup+480 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 47999 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223728 134564732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+490.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 48999 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+500 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 49999 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+510 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 50999 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+520 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 52000 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+530 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 53000 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+540 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 54000 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+550 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 55000 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+560 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2288 0 0 0 56000 7 0 0 25 0 1 0 357516343 10911744 2266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2266 603 41 0 2623 0
vsize: 10656
[startup+570 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2349 0 0 0 57000 7 0 0 25 0 1 0 357516343 11177984 2327 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2729 2327 603 41 0 2688 0
vsize: 10916
[startup+580 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2349 0 0 0 58000 7 0 0 25 0 1 0 357516343 11177984 2327 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2729 2327 603 41 0 2688 0
vsize: 10916
[startup+590 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2358 0 0 0 59001 7 0 0 25 0 1 0 357516343 11251712 2336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2747 2336 603 41 0 2706 0
vsize: 10988
[startup+600 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2388 0 0 0 60001 7 0 0 25 0 1 0 357516343 11378688 2366 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2778 2366 603 41 0 2737 0
vsize: 11112
[startup+610.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2388 0 0 0 61001 7 0 0 25 0 1 0 357516343 11378688 2366 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2778 2366 603 41 0 2737 0
vsize: 11112
[startup+620 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2388 0 0 0 62001 7 0 0 25 0 1 0 357516343 11362304 2366 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2774 2366 603 41 0 2733 0
vsize: 11096
[startup+630.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2388 0 0 0 63002 7 0 0 25 0 1 0 357516343 11341824 2366 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2366 603 41 0 2728 0
vsize: 11076
[startup+640.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2395 0 0 0 64002 7 0 0 25 0 1 0 357516343 11341824 2373 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2373 603 41 0 2728 0
vsize: 11076
[startup+650.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2404 0 0 0 65002 7 0 0 25 0 1 0 357516343 11444224 2382 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2794 2382 603 41 0 2753 0
vsize: 11176
[startup+660.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2475 0 0 0 66001 8 0 0 25 0 1 0 357516343 11702272 2453 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2857 2453 603 41 0 2816 0
vsize: 11428
[startup+670.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 67001 8 0 0 25 0 1 0 357516343 11829248 2476 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2888 2476 603 41 0 2847 0
vsize: 11552
[startup+680.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 68002 8 0 0 25 0 1 0 357516343 11829248 2476 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2888 2476 603 41 0 2847 0
vsize: 11552
[startup+690.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 69002 8 0 0 25 0 1 0 357516343 11829248 2476 4294967295 134512640 134672761 3221224560 3221223744 134615538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2888 2476 603 41 0 2847 0
vsize: 11552
[startup+700.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 70002 8 0 0 25 0 1 0 357516343 11829248 2476 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2888 2476 603 41 0 2847 0
vsize: 11552
[startup+710.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 71002 8 0 0 25 0 1 0 357516343 11816960 2476 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2476 603 41 0 2844 0
vsize: 11540
[startup+720.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 72002 8 0 0 25 0 1 0 357516343 11816960 2476 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2476 603 41 0 2844 0
vsize: 11540
[startup+730.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 73002 8 0 0 25 0 1 0 357516343 11816960 2476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2476 603 41 0 2844 0
vsize: 11540
[startup+740.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 74001 8 0 0 25 0 1 0 357516343 11816960 2476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2476 603 41 0 2844 0
vsize: 11540
[startup+750.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2498 0 0 0 75001 9 0 0 25 0 1 0 357516343 11816960 2476 4294967295 134512640 134672761 3221224560 3221223712 134616479 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2476 603 41 0 2844 0
vsize: 11540
[startup+760.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 76001 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+770.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 77001 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+780.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 78001 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+790.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 79001 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+800.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 80002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+810.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 81002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+820.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 82002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+830.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 83002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+840.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 84002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+850.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 85002 9 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+860.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2499 0 0 0 86001 10 0 0 25 0 1 0 357516343 11816960 2477 4294967295 134512640 134672761 3221224560 3221223600 134612632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2477 603 41 0 2844 0
vsize: 11540
[startup+870.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2500 0 0 0 87001 10 0 0 25 0 1 0 357516343 11816960 2478 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2478 603 41 0 2844 0
vsize: 11540
[startup+880.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2500 0 0 0 88002 10 0 0 25 0 1 0 357516343 11816960 2478 4294967295 134512640 134672761 3221224560 3221223496 1075349923 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2478 603 41 0 2844 0
vsize: 11540
[startup+890.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 89001 10 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+900.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 90001 10 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+910.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 91001 10 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+920.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 92001 10 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+930.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 93001 11 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+940.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 94002 11 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+950.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 95001 11 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223520 134645493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+960.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2519 0 0 0 96002 11 0 0 25 0 1 0 357516343 11948032 2497 4294967295 134512640 134672761 3221224560 3221223744 134615945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2497 603 41 0 2876 0
vsize: 11668
[startup+970.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2523 0 0 0 97002 11 0 0 25 0 1 0 357516343 11956224 2500 4294967295 134512640 134672761 3221224560 3221223760 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2500 603 41 0 2878 0
vsize: 11676
[startup+980.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 98002 11 0 0 25 0 1 0 357516343 11956224 2501 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2501 603 41 0 2878 0
vsize: 11676
[startup+990.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 99002 11 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 100002 11 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 101002 11 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 102002 11 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223600 134612927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 103002 11 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2524 0 0 0 104002 12 0 0 25 0 1 0 357516343 11948032 2500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2917 2500 603 41 0 2876 0
vsize: 11668
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2551 0 0 0 105002 12 0 0 25 0 1 0 357516343 12083200 2527 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2950 2527 603 41 0 2909 0
vsize: 11800
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2589 0 0 0 106001 12 0 0 25 0 1 0 357516343 12218368 2564 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2983 2564 603 41 0 2942 0
vsize: 11932
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2589 0 0 0 107001 12 0 0 25 0 1 0 357516343 12218368 2564 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2983 2564 603 41 0 2942 0
vsize: 11932
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2589 0 0 0 108002 12 0 0 25 0 1 0 357516343 12214272 2563 4294967295 134512640 134672761 3221224560 3221223744 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2563 603 41 0 2941 0
vsize: 11928
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 109002 12 0 0 25 0 1 0 357516343 12132352 2557 4294967295 134512640 134672761 3221224560 3221223584 134612944 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2962 2557 603 41 0 2921 0
vsize: 11848
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 110001 13 0 0 25 0 1 0 357516343 12128256 2556 4294967295 134512640 134672761 3221224560 3221223696 134614688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2961 2556 603 41 0 2920 0
vsize: 11844
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 111001 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 112001 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 113001 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 114001 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 115002 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223696 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 116002 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 117002 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2590 0 0 0 118002 13 0 0 25 0 1 0 357516343 12099584 2549 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2549 603 41 0 2913 0
vsize: 11816
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2591 0 0 0 119002 13 0 0 25 0 1 0 357516343 12099584 2550 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2550 603 41 0 2913 0
vsize: 11816
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 2884
Raw data (stat): 2884 (minisat+) R 2883 30927 30926 0 -1 0 2591 0 0 0 120002 13 0 0 25 0 1 0 357516343 12099584 2550 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2550 603 41 0 2913 0
vsize: 11816
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.91 1/55 2884
Raw data (stat): 2884 (minisat+) Z 2883 30927 30926 0 -1 12 2591 0 0 0 120003 14 0 0 25 0 1 0 357516343 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.02
CPU time (s): 1200.17
CPU user time (s): 1200.03
CPU system time (s): 0.142978
CPU usage (%): 100.013
Max. virtual memory (Kb): 11932
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####