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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-f1000.opb
MD5SUM3b740c03d309134e8e181ea08fc4a1e3
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
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 2000
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 2000
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2000
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2000
Total number of constraints5250
Number of constraints which are clauses5250
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 5816 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 01:59:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4263 boxname=wulflinc4 idbench=127 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc4/normalized-f1000.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-f1000.opb /oldhome/oroussel/tmp/wulflinc4/normalized-f1000.opb
IDLAUNCH: 4263
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        897688 kB
Buffers:         36160 kB
Cached:          80868 kB
SwapCached:          0 kB
Active:          55012 kB
Inactive:        64848 kB
HighTotal:      131008 kB
HighFree:        46424 kB
LowTotal:       903652 kB
LowFree:        851264 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11548 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:19:25 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 4263 7 1200.15 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5250 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5250    14750 |    1750       0        0     nan |  0.000 % |
c |       100 |    5250    14750 |    1925     100     3875    38.8 |  0.000 % |
c |       250 |    5250    14750 |    2117     250    10126    40.5 |  0.000 % |
c |       475 |    5250    14750 |    2329     475    18401    38.7 |  0.000 % |
c |       813 |    5250    14750 |    2562     813    31625    38.9 |  0.000 % |
c |      1319 |    5250    14750 |    2818    1319    51895    39.3 |  0.000 % |
c |      2079 |    5250    14750 |    3100    2079    83376    40.1 |  0.000 % |
c |      3219 |    5250    14750 |    3410    3219   133390    41.4 |  0.000 % |
c |      4927 |    5250    14750 |    3751    3134   136512    43.6 |  0.000 % |
c |      7489 |    5250    14750 |    4126    3713   163080    43.9 |  0.000 % |
c |     11335 |    5250    14750 |    4539    3280   139769    42.6 |  0.000 % |
c |     17102 |    5250    14750 |    4992    4323   194018    44.9 |  0.000 % |
c |     25751 |    5250    14750 |    5492    2626   104281    39.7 |  0.000 % |
c |     38725 |    5250    14750 |    6041    4250   177931    41.9 |  0.000 % |
c |     58186 |    5250    14750 |    6645    5028   218270    43.4 |  0.000 % |
c |     87378 |    5250    14750 |    7310    3492   135818    38.9 |  0.000 % |
c |    131170 |    5250    14750 |    8041    6015   241026    40.1 |  0.000 % |
c |    196855 |    5250    14750 |    8845    5979   238890    40.0 |  0.000 % |
c |    295382 |    5250    14750 |    9729    5160   195623    37.9 |  0.000 % |
c |    443172 |    5250    14750 |   10702    9137   375254    41.1 |  0.000 % |
c |    664860 |    5250    14750 |   11773    8065   328188    40.7 |  0.000 % |
c |    997386 |    5250    14750 |   12950    6081   232085    38.2 |  0.000 % |
c |   1496176 |    5250    14750 |   14245   12487   501590    40.2 |  0.000 % |
#### 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.58 0.88 0.91 2/54 11722
Raw data (stat): 11722 (runsolver) R 11721 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422592782 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.65 0.88 0.91 2/54 11722
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 821 0 0 0 996 2 0 0 25 0 1 0 422592782 4943872 799 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1207 799 603 41 0 1166 0
vsize: 4828
[startup+20.0007 s]
Raw data (loadavg): 0.70 0.88 0.91 2/54 11722
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 907 0 0 0 1995 3 0 0 25 0 1 0 422592782 5218304 885 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1274 885 603 41 0 1233 0
vsize: 5096
[startup+30.0014 s]
Raw data (loadavg): 0.75 0.89 0.91 2/54 11722
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 981 0 0 0 2994 3 0 0 25 0 1 0 422592782 5488640 959 4294967295 134512640 134672761 3221224560 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1340 959 603 41 0 1299 0
vsize: 5360
[startup+40.0021 s]
Raw data (loadavg): 0.78 0.89 0.91 2/54 11722
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1049 0 0 0 3993 4 0 0 25 0 1 0 422592782 5758976 1027 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1406 1027 603 41 0 1365 0
vsize: 5624
[startup+50.0023 s]
Raw data (loadavg): 0.89 0.91 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1088 0 0 0 4992 4 0 0 25 0 1 0 422592782 6033408 1066 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1066 603 41 0 1432 0
vsize: 5892
[startup+60.002 s]
Raw data (loadavg): 0.91 0.91 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1138 0 0 0 5991 4 0 0 25 0 1 0 422592782 6168576 1116 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1506 1116 603 41 0 1465 0
vsize: 6024
[startup+70.0031 s]
Raw data (loadavg): 0.92 0.91 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1144 0 0 0 6991 4 0 0 25 0 1 0 422592782 6168576 1122 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1506 1122 603 41 0 1465 0
vsize: 6024
[startup+80.0037 s]
Raw data (loadavg): 0.93 0.92 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1203 0 0 0 7991 4 0 0 25 0 1 0 422592782 6438912 1181 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1572 1181 603 41 0 1531 0
vsize: 6288
[startup+90.0036 s]
Raw data (loadavg): 0.94 0.92 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1230 0 0 0 8991 4 0 0 25 0 1 0 422592782 6574080 1208 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1605 1208 603 41 0 1564 0
vsize: 6420
[startup+100.004 s]
Raw data (loadavg): 0.95 0.92 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1272 0 0 0 9991 4 0 0 25 0 1 0 422592782 6709248 1250 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1638 1250 603 41 0 1597 0
vsize: 6552
[startup+110.003 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 11775
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1276 0 0 0 10991 4 0 0 25 0 1 0 422592782 6844416 1254 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1671 1254 603 41 0 1630 0
vsize: 6684
[startup+120.003 s]
Raw data (loadavg): 0.96 0.92 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1332 0 0 0 11991 5 0 0 25 0 1 0 422592782 6975488 1310 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1703 1310 603 41 0 1662 0
vsize: 6812
[startup+130.003 s]
Raw data (loadavg): 0.97 0.93 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1372 0 0 0 12991 5 0 0 25 0 1 0 422592782 7245824 1350 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1769 1350 603 41 0 1728 0
vsize: 7076
[startup+140.004 s]
Raw data (loadavg): 0.97 0.93 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1392 0 0 0 13991 5 0 0 25 0 1 0 422592782 7245824 1370 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1769 1370 603 41 0 1728 0
vsize: 7076
[startup+150.004 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1408 0 0 0 14991 5 0 0 25 0 1 0 422592782 7393280 1386 4294967295 134512640 134672761 3221224560 3221223732 134559669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1386 603 41 0 1764 0
vsize: 7220
[startup+160.004 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1420 0 0 0 15991 5 0 0 25 0 1 0 422592782 7393280 1398 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1398 603 41 0 1764 0
vsize: 7220
[startup+170.005 s]
Raw data (loadavg): 0.98 0.93 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1434 0 0 0 16991 5 0 0 25 0 1 0 422592782 7393280 1412 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1412 603 41 0 1764 0
vsize: 7220
[startup+180.004 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1442 0 0 0 17991 5 0 0 25 0 1 0 422592782 7536640 1420 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1840 1420 603 41 0 1799 0
vsize: 7360
[startup+190.004 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1490 0 0 0 18991 6 0 0 25 0 1 0 422592782 7671808 1468 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1873 1468 603 41 0 1832 0
vsize: 7492
[startup+200.005 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1542 0 0 0 19991 6 0 0 25 0 1 0 422592782 7942144 1520 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1520 603 41 0 1898 0
vsize: 7756
[startup+210.005 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1563 0 0 0 20991 6 0 0 25 0 1 0 422592782 7942144 1541 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1541 603 41 0 1898 0
vsize: 7756
[startup+220.005 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1577 0 0 0 21991 6 0 0 25 0 1 0 422592782 8081408 1555 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1555 603 41 0 1932 0
vsize: 7892
[startup+230.006 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1585 0 0 0 22992 6 0 0 25 0 1 0 422592782 8081408 1563 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1563 603 41 0 1932 0
vsize: 7892
[startup+240.006 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1589 0 0 0 23992 6 0 0 25 0 1 0 422592782 8081408 1567 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1567 603 41 0 1932 0
vsize: 7892
[startup+250.007 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1597 0 0 0 24992 6 0 0 25 0 1 0 422592782 8081408 1575 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1575 603 41 0 1932 0
vsize: 7892
[startup+260.006 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1608 0 0 0 25992 6 0 0 25 0 1 0 422592782 8220672 1586 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1586 603 41 0 1966 0
vsize: 8028
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1628 0 0 0 26992 6 0 0 25 0 1 0 422592782 8220672 1606 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1606 603 41 0 1966 0
vsize: 8028
[startup+280.007 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1635 0 0 0 27993 6 0 0 25 0 1 0 422592782 8355840 1613 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1613 603 41 0 1999 0
vsize: 8160
[startup+290.008 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1664 0 0 0 28993 6 0 0 25 0 1 0 422592782 8491008 1642 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1642 603 41 0 2032 0
vsize: 8292
[startup+300.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1716 0 0 0 29993 6 0 0 25 0 1 0 422592782 8626176 1694 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1694 603 41 0 2065 0
vsize: 8424
[startup+310.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1745 0 0 0 30993 6 0 0 25 0 1 0 422592782 8769536 1723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1723 603 41 0 2100 0
vsize: 8564
[startup+320.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1761 0 0 0 31993 6 0 0 25 0 1 0 422592782 8904704 1739 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1739 603 41 0 2133 0
vsize: 8696
[startup+330.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1765 0 0 0 32993 6 0 0 25 0 1 0 422592782 8904704 1743 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1743 603 41 0 2133 0
vsize: 8696
[startup+340.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1775 0 0 0 33993 6 0 0 25 0 1 0 422592782 8904704 1753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1753 603 41 0 2133 0
vsize: 8696
[startup+350.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1775 0 0 0 34993 6 0 0 25 0 1 0 422592782 8904704 1753 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1753 603 41 0 2133 0
vsize: 8696
[startup+360.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1788 0 0 0 35993 6 0 0 25 0 1 0 422592782 8904704 1766 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1766 603 41 0 2133 0
vsize: 8696
[startup+370.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1826 0 0 0 36993 7 0 0 25 0 1 0 422592782 9175040 1804 4294967295 134512640 134672761 3221224560 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1804 603 41 0 2199 0
vsize: 8960
[startup+380.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1829 0 0 0 37994 7 0 0 25 0 1 0 422592782 9175040 1807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1807 603 41 0 2199 0
vsize: 8960
[startup+390.009 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1834 0 0 0 38994 7 0 0 25 0 1 0 422592782 9175040 1812 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1812 603 41 0 2199 0
vsize: 8960
[startup+400.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1847 0 0 0 39994 7 0 0 25 0 1 0 422592782 9175040 1825 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1825 603 41 0 2199 0
vsize: 8960
[startup+410.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11777
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1863 0 0 0 40994 7 0 0 25 0 1 0 422592782 9306112 1841 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1841 603 41 0 2231 0
vsize: 9088
[startup+420.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1869 0 0 0 41994 7 0 0 25 0 1 0 422592782 9306112 1847 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1847 603 41 0 2231 0
vsize: 9088
[startup+430.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1874 0 0 0 42994 7 0 0 25 0 1 0 422592782 9306112 1852 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1852 603 41 0 2231 0
vsize: 9088
[startup+440.012 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1884 0 0 0 43995 7 0 0 25 0 1 0 422592782 9441280 1862 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+450.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1884 0 0 0 44995 7 0 0 25 0 1 0 422592782 9441280 1862 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1941 0 0 0 45995 7 0 0 25 0 1 0 422592782 9576448 1919 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2338 1919 603 41 0 2297 0
vsize: 9352
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1956 0 0 0 46994 7 0 0 25 0 1 0 422592782 9723904 1934 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2374 1934 603 41 0 2333 0
vsize: 9496
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1962 0 0 0 47994 7 0 0 25 0 1 0 422592782 9723904 1940 4294967295 134512640 134672761 3221224560 3221223744 134558563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2374 1940 603 41 0 2333 0
vsize: 9496
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1990 0 0 0 48994 7 0 0 25 0 1 0 422592782 9863168 1968 4294967295 134512640 134672761 3221224560 3221223760 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1968 603 41 0 2367 0
vsize: 9632
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 1997 0 0 0 49995 7 0 0 25 0 1 0 422592782 9863168 1975 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1975 603 41 0 2367 0
vsize: 9632
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2002 0 0 0 50995 7 0 0 25 0 1 0 422592782 9863168 1980 4294967295 134512640 134672761 3221224560 3221223560 1075350014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1980 603 41 0 2367 0
vsize: 9632
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2011 0 0 0 51995 7 0 0 25 0 1 0 422592782 9863168 1989 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1989 603 41 0 2367 0
vsize: 9632
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2021 0 0 0 52995 8 0 0 25 0 1 0 422592782 10002432 1999 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 1999 603 41 0 2401 0
vsize: 9768
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2032 0 0 0 53995 8 0 0 25 0 1 0 422592782 10002432 2010 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 2010 603 41 0 2401 0
vsize: 9768
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2038 0 0 0 54995 8 0 0 25 0 1 0 422592782 10002432 2016 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 2016 603 41 0 2401 0
vsize: 9768
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2049 0 0 0 55995 8 0 0 25 0 1 0 422592782 10137600 2027 4294967295 134512640 134672761 3221224560 3221223576 1075352732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2027 603 41 0 2434 0
vsize: 9900
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2053 0 0 0 56996 8 0 0 25 0 1 0 422592782 10137600 2031 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2053 0 0 0 57996 8 0 0 25 0 1 0 422592782 10137600 2031 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2059 0 0 0 58996 8 0 0 25 0 1 0 422592782 10137600 2037 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2037 603 41 0 2434 0
vsize: 9900
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2080 0 0 0 59996 8 0 0 25 0 1 0 422592782 10137600 2058 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2058 603 41 0 2434 0
vsize: 9900
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2088 0 0 0 60996 8 0 0 25 0 1 0 422592782 10268672 2066 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2066 603 41 0 2466 0
vsize: 10028
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2102 0 0 0 61996 8 0 0 25 0 1 0 422592782 10268672 2080 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2102 0 0 0 62996 8 0 0 25 0 1 0 422592782 10268672 2080 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2102 0 0 0 63997 8 0 0 25 0 1 0 422592782 10268672 2080 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2105 0 0 0 64997 8 0 0 25 0 1 0 422592782 10268672 2083 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2083 603 41 0 2466 0
vsize: 10028
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2117 0 0 0 65997 8 0 0 25 0 1 0 422592782 10412032 2095 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2095 603 41 0 2501 0
vsize: 10168
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2120 0 0 0 66997 8 0 0 25 0 1 0 422592782 10412032 2098 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2098 603 41 0 2501 0
vsize: 10168
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2125 0 0 0 67997 8 0 0 25 0 1 0 422592782 10412032 2103 4294967295 134512640 134672761 3221224560 3221223776 134557531 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2103 603 41 0 2501 0
vsize: 10168
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2137 0 0 0 68998 8 0 0 25 0 1 0 422592782 10412032 2115 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2115 603 41 0 2501 0
vsize: 10168
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2137 0 0 0 69998 8 0 0 25 0 1 0 422592782 10412032 2115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2115 603 41 0 2501 0
vsize: 10168
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2140 0 0 0 70998 8 0 0 25 0 1 0 422592782 10551296 2118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2576 2118 603 41 0 2535 0
vsize: 10304
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2144 0 0 0 71997 8 0 0 25 0 1 0 422592782 10551296 2122 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2576 2122 603 41 0 2535 0
vsize: 10304
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2212 0 0 0 72996 8 0 0 25 0 1 0 422592782 10821632 2190 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2190 603 41 0 2601 0
vsize: 10568
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2217 0 0 0 73996 8 0 0 25 0 1 0 422592782 10821632 2195 4294967295 134512640 134672761 3221224560 3221223760 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2195 603 41 0 2601 0
vsize: 10568
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2231 0 0 0 74996 9 0 0 25 0 1 0 422592782 10821632 2209 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2209 603 41 0 2601 0
vsize: 10568
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2237 0 0 0 75996 9 0 0 25 0 1 0 422592782 10821632 2215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2215 603 41 0 2601 0
vsize: 10568
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2278 0 0 0 76997 9 0 0 25 0 1 0 422592782 11091968 2256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2256 603 41 0 2667 0
vsize: 10832
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2284 0 0 0 77997 9 0 0 25 0 1 0 422592782 11091968 2262 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2262 603 41 0 2667 0
vsize: 10832
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2287 0 0 0 78997 9 0 0 25 0 1 0 422592782 11091968 2265 4294967295 134512640 134672761 3221224560 3221223736 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2287 0 0 0 79997 9 0 0 25 0 1 0 422592782 11091968 2265 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2289 0 0 0 80997 9 0 0 25 0 1 0 422592782 11091968 2267 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2267 603 41 0 2667 0
vsize: 10832
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2297 0 0 0 81997 9 0 0 25 0 1 0 422592782 11227136 2275 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2275 603 41 0 2700 0
vsize: 10964
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2298 0 0 0 82997 9 0 0 25 0 1 0 422592782 11227136 2276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2276 603 41 0 2700 0
vsize: 10964
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2301 0 0 0 83998 9 0 0 25 0 1 0 422592782 11227136 2279 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2279 603 41 0 2700 0
vsize: 10964
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2308 0 0 0 84998 9 0 0 25 0 1 0 422592782 11227136 2286 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2286 603 41 0 2700 0
vsize: 10964
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2312 0 0 0 85998 9 0 0 25 0 1 0 422592782 11227136 2290 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2290 603 41 0 2700 0
vsize: 10964
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2316 0 0 0 86998 9 0 0 25 0 1 0 422592782 11227136 2294 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2294 603 41 0 2700 0
vsize: 10964
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2320 0 0 0 87998 9 0 0 25 0 1 0 422592782 11227136 2298 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2298 603 41 0 2700 0
vsize: 10964
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2324 0 0 0 88998 9 0 0 25 0 1 0 422592782 11227136 2302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2324 0 0 0 89999 9 0 0 25 0 1 0 422592782 11227136 2302 4294967295 134512640 134672761 3221224560 3221223620 1075346603 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2336 0 0 0 90999 9 0 0 25 0 1 0 422592782 11370496 2314 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2776 2314 603 41 0 2735 0
vsize: 11104
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2343 0 0 0 91999 9 0 0 25 0 1 0 422592782 11370496 2321 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2776 2321 603 41 0 2735 0
vsize: 11104
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2364 0 0 0 92999 9 0 0 25 0 1 0 422592782 11505664 2342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2342 603 41 0 2768 0
vsize: 11236
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2364 0 0 0 93999 9 0 0 25 0 1 0 422592782 11505664 2342 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2342 603 41 0 2768 0
vsize: 11236
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2369 0 0 0 94999 9 0 0 25 0 1 0 422592782 11505664 2347 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2369 0 0 0 96000 9 0 0 25 0 1 0 422592782 11505664 2347 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2373 0 0 0 97000 9 0 0 25 0 1 0 422592782 11505664 2351 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2351 603 41 0 2768 0
vsize: 11236
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2376 0 0 0 98000 9 0 0 25 0 1 0 422592782 11505664 2354 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2354 603 41 0 2768 0
vsize: 11236
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2397 0 0 0 99000 9 0 0 25 0 1 0 422592782 11640832 2375 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2397 0 0 0 100000 9 0 0 25 0 1 0 422592782 11640832 2375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2400 0 0 0 101000 9 0 0 25 0 1 0 422592782 11640832 2378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2842 2378 603 41 0 2801 0
vsize: 11368
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2400 0 0 0 102001 9 0 0 25 0 1 0 422592782 11640832 2378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2842 2378 603 41 0 2801 0
vsize: 11368
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2441 0 0 0 103001 9 0 0 25 0 1 0 422592782 11776000 2419 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2419 603 41 0 2834 0
vsize: 11500
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2445 0 0 0 104001 9 0 0 25 0 1 0 422592782 11776000 2423 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2423 603 41 0 2834 0
vsize: 11500
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2449 0 0 0 105001 9 0 0 25 0 1 0 422592782 11776000 2427 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2449 0 0 0 106001 9 0 0 25 0 1 0 422592782 11776000 2427 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2450 0 0 0 107002 9 0 0 25 0 1 0 422592782 11776000 2428 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2450 0 0 0 108002 9 0 0 25 0 1 0 422592782 11776000 2428 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2450 0 0 0 109002 9 0 0 25 0 1 0 422592782 11776000 2428 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2450 0 0 0 110002 9 0 0 25 0 1 0 422592782 11776000 2428 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2456 0 0 0 111002 9 0 0 25 0 1 0 422592782 11776000 2434 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2434 603 41 0 2834 0
vsize: 11500
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2465 0 0 0 112002 9 0 0 25 0 1 0 422592782 11915264 2443 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2909 2443 603 41 0 2868 0
vsize: 11636
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2471 0 0 0 113002 10 0 0 25 0 1 0 422592782 11915264 2449 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2909 2449 603 41 0 2868 0
vsize: 11636
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2477 0 0 0 114003 10 0 0 25 0 1 0 422592782 11915264 2455 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2455 603 41 0 2868 0
vsize: 11636
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2500 0 0 0 115002 10 0 0 25 0 1 0 422592782 12050432 2478 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2478 603 41 0 2901 0
vsize: 11768
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2508 0 0 0 116002 10 0 0 25 0 1 0 422592782 12050432 2486 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2486 603 41 0 2901 0
vsize: 11768
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2515 0 0 0 117003 10 0 0 25 0 1 0 422592782 12050432 2493 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2493 603 41 0 2901 0
vsize: 11768
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2518 0 0 0 118003 10 0 0 25 0 1 0 422592782 12050432 2496 4294967295 134512640 134672761 3221224560 3221223744 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2496 603 41 0 2901 0
vsize: 11768
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2519 0 0 0 119003 10 0 0 25 0 1 0 422592782 12050432 2497 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11779
Raw data (stat): 11722 (minisat+) R 11721 5897 5896 0 -1 0 2519 0 0 0 120003 10 0 0 25 0 1 0 422592782 12050432 2497 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 11779
Raw data (stat): 11722 (minisat+) Z 11721 5897 5896 0 -1 12 2521 0 0 0 120003 10 0 0 25 0 1 0 422592782 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.04
CPU time (s): 1200.15
CPU user time (s): 1200.04
CPU system time (s): 0.109983
CPU usage (%): 100.009
Max. virtual memory (Kb): 11768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####