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-c.opb
MD5SUM	40e47c460002545cc2670ca84fd53082
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	2606
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	2606
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	2606
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	2606
Total number of constraints	6509
Number of constraints which are clauses	6509
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 5535

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 00:24:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3965 boxname=wulflinc8 idbench=205 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  40e47c460002545cc2670ca84fd53082  /oldhome/oroussel/tmp/wulflinc8/normalized-par32-2-c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc8/normalized-par32-2-c.opb /oldhome/oroussel/tmp/wulflinc8/normalized-par32-2-c.opb
IDLAUNCH: 3965
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        903032 kB
Buffers:         36980 kB
Cached:          75424 kB
SwapCached:          0 kB
Active:          73112 kB
Inactive:        42120 kB
HighTotal:      131008 kB
HighFree:        51660 kB
LowTotal:       903652 kB
LowFree:        851372 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            10904 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:44:38 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 3965 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6509 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 |    6509    17852 |    1952       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2606          
c   -- var.elim.:  2000/2606          
c   -- var.elim.:  2606/2606          
c |         0 |    6387    17486 |      --       0       --      -- |     --   | -122/-366
c |         0 |    6387    17486 |    2554       0        0     nan |  0.000 % |
c |       102 |    6387    17486 |    2810     102     4492    44.0 |  0.004 % |
c |       252 |    6387    17486 |    3091     252    10875    43.2 |  0.000 % |
c |       477 |    6387    17486 |    3400     477    19037    39.9 |  0.000 % |
c |       814 |    6387    17486 |    3740     814    31480    38.7 |  0.000 % |
c |      1320 |    6387    17486 |    4114    1320    50856    38.5 |  0.000 % |
c |      2079 |    6387    17486 |    4525    2079    79296    38.1 |  0.000 % |
c |      3218 |    6387    17486 |    4978    3218   122343    38.0 |  0.000 % |
c |      4927 |    6387    17486 |    5476    4927   210169    42.7 |  0.000 % |
c |      7489 |    6387    17486 |    6024    5557   258429    46.5 |  0.000 % |
c |     11333 |    6380    1#### 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.85 0.97 0.91 2/54 30929
Raw data (stat): 30929 (runsolver) R 30928 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 408463316 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1125 0 0 0 995 3 0 0 25 0 1 0 408463316 6123520 1103 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1495 1103 603 41 0 1454 0
vsize: 5980
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1285 0 0 0 1995 3 0 0 25 0 1 0 408463316 6787072 1263 4294967295 134512640 134672761 3221224560 3221223780 134603692 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1657 1263 603 41 0 1616 0
vsize: 6628
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1331 0 0 0 2995 3 0 0 25 0 1 0 408463316 7053312 1309 4294967295 134512640 134672761 3221224560 3221223712 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1722 1309 603 41 0 1681 0
vsize: 6888
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1399 0 0 0 3995 3 0 0 25 0 1 0 408463316 7356416 1377 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1796 1377 603 41 0 1755 0
vsize: 7184
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1407 0 0 0 4995 3 0 0 25 0 1 0 408463316 7356416 1385 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1796 1385 603 41 0 1755 0
vsize: 7184
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1519 0 0 0 5995 4 0 0 25 0 1 0 408463316 7856128 1497 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1918 1497 603 41 0 1877 0
vsize: 7672
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1547 0 0 0 6995 4 0 0 25 0 1 0 408463316 7970816 1525 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1946 1525 603 41 0 1905 0
vsize: 7784
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1577 0 0 0 7995 4 0 0 25 0 1 0 408463316 8073216 1555 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1971 1555 603 41 0 1930 0
vsize: 7884
[startup+90.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1581 0 0 0 8995 4 0 0 25 0 1 0 408463316 8073216 1559 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1971 1559 603 41 0 1930 0
vsize: 7884
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1581 0 0 0 9995 4 0 0 25 0 1 0 408463316 8073216 1559 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1971 1559 603 41 0 1930 0
vsize: 7884
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1626 0 0 0 10995 4 0 0 25 0 1 0 408463316 8208384 1604 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2004 1604 603 41 0 1963 0
vsize: 8016
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1654 0 0 0 11996 5 0 0 25 0 1 0 408463316 8339456 1632 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2036 1632 603 41 0 1995 0
vsize: 8144
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1659 0 0 0 12996 5 0 0 25 0 1 0 408463316 8409088 1637 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1637 603 41 0 2012 0
vsize: 8212
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1663 0 0 0 13996 5 0 0 25 0 1 0 408463316 8409088 1641 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1641 603 41 0 2012 0
vsize: 8212
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1667 0 0 0 14996 5 0 0 25 0 1 0 408463316 8409088 1645 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1645 603 41 0 2012 0
vsize: 8212
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1674 0 0 0 15996 5 0 0 25 0 1 0 408463316 8409088 1652 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1652 603 41 0 2012 0
vsize: 8212
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1674 0 0 0 16996 5 0 0 25 0 1 0 408463316 8409088 1652 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1652 603 41 0 2012 0
vsize: 8212
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1676 0 0 0 17997 5 0 0 25 0 1 0 408463316 8409088 1654 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1654 603 41 0 2012 0
vsize: 8212
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1685 0 0 0 18997 5 0 0 25 0 1 0 408463316 8507392 1663 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1663 603 41 0 2036 0
vsize: 8308
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1692 0 0 0 19997 5 0 0 25 0 1 0 408463316 8507392 1670 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1670 603 41 0 2036 0
vsize: 8308
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1692 0 0 0 20997 5 0 0 25 0 1 0 408463316 8507392 1670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1670 603 41 0 2036 0
vsize: 8308
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1738 0 0 0 21997 5 0 0 25 0 1 0 408463316 8769536 1716 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1716 603 41 0 2100 0
vsize: 8564
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1874 0 0 0 22997 5 0 0 25 0 1 0 408463316 9265152 1852 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2262 1852 603 41 0 2221 0
vsize: 9048
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1882 0 0 0 23997 5 0 0 25 0 1 0 408463316 9265152 1860 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2262 1860 603 41 0 2221 0
vsize: 9048
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1883 0 0 0 24997 5 0 0 25 0 1 0 408463316 9265152 1861 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2262 1861 603 41 0 2221 0
vsize: 9048
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1883 0 0 0 25997 5 0 0 25 0 1 0 408463316 9265152 1861 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2262 1861 603 41 0 2221 0
vsize: 9048
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1883 0 0 0 26997 5 0 0 25 0 1 0 408463316 9265152 1861 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2262 1861 603 41 0 2221 0
vsize: 9048
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1895 0 0 0 27998 5 0 0 25 0 1 0 408463316 9428992 1873 4294967295 134512640 134672761 3221224560 3221223656 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1873 603 41 0 2261 0
vsize: 9208
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1944 0 0 0 28998 5 0 0 25 0 1 0 408463316 9498624 1922 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2319 1922 603 41 0 2278 0
vsize: 9276
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1980 0 0 0 29998 5 0 0 25 0 1 0 408463316 9707520 1958 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2370 1958 603 41 0 2329 0
vsize: 9480
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1993 0 0 0 30998 6 0 0 25 0 1 0 408463316 9707520 1971 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2370 1971 603 41 0 2329 0
vsize: 9480
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 1993 0 0 0 31998 6 0 0 25 0 1 0 408463316 9707520 1971 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2370 1971 603 41 0 2329 0
vsize: 9480
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2002 0 0 0 32998 6 0 0 25 0 1 0 408463316 9797632 1980 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2392 1980 603 41 0 2351 0
vsize: 9568
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2030 0 0 0 33998 6 0 0 25 0 1 0 408463316 9916416 2008 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 2008 603 41 0 2380 0
vsize: 9684
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2030 0 0 0 34998 6 0 0 25 0 1 0 408463316 9916416 2008 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 2008 603 41 0 2380 0
vsize: 9684
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2037 0 0 0 35998 6 0 0 25 0 1 0 408463316 9916416 2015 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 2015 603 41 0 2380 0
vsize: 9684
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2045 0 0 0 36999 6 0 0 25 0 1 0 408463316 9916416 2023 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 2023 603 41 0 2380 0
vsize: 9684
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2057 0 0 0 37999 6 0 0 25 0 1 0 408463316 10014720 2035 4294967295 134512640 134672761 3221224560 3221223552 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2035 603 41 0 2404 0
vsize: 9780
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2064 0 0 0 38999 6 0 0 25 0 1 0 408463316 10014720 2042 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2042 603 41 0 2404 0
vsize: 9780
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2064 0 0 0 39999 6 0 0 25 0 1 0 408463316 10014720 2042 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2042 603 41 0 2404 0
vsize: 9780
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2064 0 0 0 40999 6 0 0 25 0 1 0 408463316 10014720 2042 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2042 603 41 0 2404 0
vsize: 9780
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2072 0 0 0 41999 6 0 0 25 0 1 0 408463316 10014720 2050 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2050 603 41 0 2404 0
vsize: 9780
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2072 0 0 0 43000 6 0 0 25 0 1 0 408463316 10014720 2050 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2050 603 41 0 2404 0
vsize: 9780
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2072 0 0 0 44000 6 0 0 25 0 1 0 408463316 10014720 2050 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2050 603 41 0 2404 0
vsize: 9780
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2072 0 0 0 45000 6 0 0 25 0 1 0 408463316 10014720 2050 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2050 603 41 0 2404 0
vsize: 9780
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2072 0 0 0 46000 6 0 0 25 0 1 0 408463316 10014720 2050 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2445 2050 603 41 0 2404 0
vsize: 9780
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2104 0 0 0 47000 6 0 0 25 0 1 0 408463316 10145792 2082 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2477 2082 603 41 0 2436 0
vsize: 9908
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2111 0 0 0 48000 6 0 0 25 0 1 0 408463316 10235904 2089 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2499 2089 603 41 0 2458 0
vsize: 9996
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2134 0 0 0 49000 6 0 0 25 0 1 0 408463316 10313728 2112 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2112 603 41 0 2477 0
vsize: 10072
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2142 0 0 0 50001 6 0 0 25 0 1 0 408463316 10313728 2120 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2120 603 41 0 2477 0
vsize: 10072
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2142 0 0 0 51001 6 0 0 25 0 1 0 408463316 10313728 2120 4294967295 134512640 134672761 3221224560 3221223600 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2120 603 41 0 2477 0
vsize: 10072
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2142 0 0 0 52001 6 0 0 25 0 1 0 408463316 10313728 2120 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2518 2120 603 41 0 2477 0
vsize: 10072
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2165 0 0 0 53001 6 0 0 25 0 1 0 408463316 10448896 2143 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2143 603 41 0 2510 0
vsize: 10204
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2165 0 0 0 54001 6 0 0 25 0 1 0 408463316 10448896 2143 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2143 603 41 0 2510 0
vsize: 10204
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2165 0 0 0 55002 6 0 0 25 0 1 0 408463316 10448896 2143 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2143 603 41 0 2510 0
vsize: 10204
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2165 0 0 0 56002 6 0 0 25 0 1 0 408463316 10448896 2143 4294967295 134512640 134672761 3221224560 3221223744 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2143 603 41 0 2510 0
vsize: 10204
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2167 0 0 0 57002 6 0 0 25 0 1 0 408463316 10448896 2145 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2145 603 41 0 2510 0
vsize: 10204
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2167 0 0 0 58002 6 0 0 25 0 1 0 408463316 10448896 2145 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2145 603 41 0 2510 0
vsize: 10204
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2167 0 0 0 59002 6 0 0 25 0 1 0 408463316 10448896 2145 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2145 603 41 0 2510 0
vsize: 10204
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2221 0 0 0 60002 6 0 0 25 0 1 0 408463316 10743808 2199 4294967295 134512640 134672761 3221224560 3221223504 134645620 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2623 2199 603 41 0 2582 0
vsize: 10492
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2239 0 0 0 61003 6 0 0 25 0 1 0 408463316 10752000 2217 4294967295 134512640 134672761 3221224560 3221223600 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2625 2217 603 41 0 2584 0
vsize: 10500
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2239 0 0 0 62003 6 0 0 25 0 1 0 408463316 10752000 2217 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2625 2217 603 41 0 2584 0
vsize: 10500
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2240 0 0 0 63003 6 0 0 25 0 1 0 408463316 10747904 2218 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2218 603 41 0 2583 0
vsize: 10496
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2240 0 0 0 64003 6 0 0 25 0 1 0 408463316 10747904 2218 4294967295 134512640 134672761 3221224560 3221223552 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2218 603 41 0 2583 0
vsize: 10496
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2240 0 0 0 65003 6 0 0 25 0 1 0 408463316 10747904 2218 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2218 603 41 0 2583 0
vsize: 10496
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 66003 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 67004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 68004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223760 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 69004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 70004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 71004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2247 0 0 0 72004 7 0 0 25 0 1 0 408463316 10747904 2225 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2225 603 41 0 2583 0
vsize: 10496
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 73005 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 74005 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 75005 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 76005 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 77005 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223600 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 78006 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 79006 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2254 0 0 0 80006 7 0 0 25 0 1 0 408463316 10747904 2232 4294967295 134512640 134672761 3221224560 3221223580 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2624 2232 603 41 0 2583 0
vsize: 10496
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 81006 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 82006 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 83006 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 84007 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 85007 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 86007 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223760 134610688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2309 0 0 0 87007 7 0 0 25 0 1 0 408463316 10973184 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2287 603 41 0 2638 0
vsize: 10716
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2357 0 0 0 88007 7 0 0 25 0 1 0 408463316 11259904 2335 4294967295 134512640 134672761 3221224560 3221223600 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2749 2335 603 41 0 2708 0
vsize: 10996
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2357 0 0 0 89007 7 0 0 25 0 1 0 408463316 11259904 2335 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2749 2335 603 41 0 2708 0
vsize: 10996
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2357 0 0 0 90007 7 0 0 25 0 1 0 408463316 11255808 2334 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2748 2334 603 41 0 2707 0
vsize: 10992
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2378 0 0 0 91008 7 0 0 25 0 1 0 408463316 11337728 2355 4294967295 134512640 134672761 3221224560 3221223744 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2768 2355 603 41 0 2727 0
vsize: 11072
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2420 0 0 0 92008 7 0 0 25 0 1 0 408463316 11509760 2396 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2810 2396 603 41 0 2769 0
vsize: 11240
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2477 0 0 0 93008 7 0 0 25 0 1 0 408463316 11735040 2451 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2865 2451 603 41 0 2824 0
vsize: 11460
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2494 0 0 0 94008 7 0 0 25 0 1 0 408463316 11800576 2467 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2881 2467 603 41 0 2840 0
vsize: 11524
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2500 0 0 0 95008 7 0 0 25 0 1 0 408463316 11816960 2472 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2472 603 41 0 2844 0
vsize: 11540
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2500 0 0 0 96008 7 0 0 25 0 1 0 408463316 11816960 2472 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2885 2472 603 41 0 2844 0
vsize: 11540
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2500 0 0 0 97009 7 0 0 25 0 1 0 408463316 11812864 2471 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2884 2471 603 41 0 2843 0
vsize: 11536
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2501 0 0 0 98009 7 0 0 25 0 1 0 408463316 11812864 2472 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2884 2472 603 41 0 2843 0
vsize: 11536
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2515 0 0 0 99009 7 0 0 25 0 1 0 408463316 11874304 2485 4294967295 134512640 134672761 3221224560 3221223696 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2899 2485 603 41 0 2858 0
vsize: 11596
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2515 0 0 0 100009 7 0 0 25 0 1 0 408463316 11874304 2485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2899 2485 603 41 0 2858 0
vsize: 11596
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2515 0 0 0 101009 7 0 0 25 0 1 0 408463316 11870208 2484 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2484 603 41 0 2857 0
vsize: 11592
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 102009 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223760 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 103009 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 104010 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 105010 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 106010 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 107010 7 0 0 25 0 1 0 408463316 11870208 2485 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2898 2485 603 41 0 2857 0
vsize: 11592
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2516 0 0 0 108010 7 0 0 25 0 1 0 408463316 11866112 2484 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2484 603 41 0 2856 0
vsize: 11588
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2546 0 0 0 109010 8 0 0 25 0 1 0 408463316 11988992 2513 4294967295 134512640 134672761 3221224560 3221223744 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2927 2513 603 41 0 2886 0
vsize: 11708
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 110010 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 111011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 112011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 113011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 114011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 115011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223552 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 116011 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 117012 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223696 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2569 0 0 0 118012 8 0 0 25 0 1 0 408463316 12079104 2536 4294967295 134512640 134672761 3221224560 3221223696 134614715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2949 2536 603 41 0 2908 0
vsize: 11796
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2570 0 0 0 119012 8 0 0 25 0 1 0 408463316 12075008 2536 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2948 2536 603 41 0 2907 0
vsize: 11792
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30929
Raw data (stat): 30929 (minisat+) R 30928 26667 26666 0 -1 0 2570 0 0 0 120012 8 0 0 25 0 1 0 408463316 12075008 2536 4294967295 134512640 134672761 3221224560 3221223760 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2948 2536 603 41 0 2907 0
vsize: 11792
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30929
Raw data (stat): 30929 (minisat+) Z 30928 26667 26666 0 -1 12 2570 0 0 0 120012 8 0 0 25 0 1 0 408463316 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.22
CPU user time (s): 1200.13
CPU system time (s): 0.087986
CPU usage (%): 100.016
Max. virtual memory (Kb): 11796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####