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-f1000.opb
MD5SUM	3b740c03d309134e8e181ea08fc4a1e3
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	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 numbers	11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2000
Total number of constraints	5250
Number of constraints which are clauses	5250
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 4851

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 20:34:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1139 boxname=wulflinc3 idbench=127 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc3/normalized-f1000.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc3/normalized-f1000.opb
IDLAUNCH: 1139
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        915688 kB
Buffers:         35164 kB
Cached:          60704 kB
SwapCached:       3276 kB
Active:          67548 kB
Inactive:        34464 kB
HighTotal:      131008 kB
HighFree:        66360 kB
LowTotal:       903652 kB
LowFree:        849328 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11348 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:55:00 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 1139 7 1200.18 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.29 0.58 0.75 2/54 16015
Raw data (stat): 16015 (runsolver) R 16014 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420646105 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.40 0.59 0.75 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 821 0 0 0 996 1 0 0 25 0 1 0 420646105 4943872 799 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1207 799 603 41 0 1166 0
vsize: 4828
[startup+20.0016 s]
Raw data (loadavg): 0.49 0.61 0.76 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 906 0 0 0 1996 2 0 0 25 0 1 0 420646105 5214208 884 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1273 884 603 41 0 1232 0
vsize: 5092
[startup+30.0021 s]
Raw data (loadavg): 0.57 0.62 0.76 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 981 0 0 0 2996 2 0 0 25 0 1 0 420646105 5488640 959 4294967295 134512640 134672761 3221224640 3221223808 134560903 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.002 s]
Raw data (loadavg): 0.63 0.63 0.76 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1049 0 0 0 3995 3 0 0 25 0 1 0 420646105 5758976 1027 4294967295 134512640 134672761 3221224640 3221223840 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1406 1027 603 41 0 1365 0
vsize: 5624
[startup+50.0031 s]
Raw data (loadavg): 0.69 0.64 0.76 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1067 0 0 0 4995 3 0 0 25 0 1 0 420646105 5898240 1045 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1440 1045 603 41 0 1399 0
vsize: 5760
[startup+60.0026 s]
Raw data (loadavg): 0.74 0.65 0.76 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1138 0 0 0 5995 3 0 0 25 0 1 0 420646105 6168576 1116 4294967295 134512640 134672761 3221224640 3221223824 134559354 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.0038 s]
Raw data (loadavg): 0.78 0.66 0.77 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1144 0 0 0 6995 3 0 0 25 0 1 0 420646105 6168576 1122 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.0046 s]
Raw data (loadavg): 0.81 0.68 0.77 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1203 0 0 0 7995 3 0 0 25 0 1 0 420646105 6438912 1181 4294967295 134512640 134672761 3221224640 3221223808 134560988 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.0041 s]
Raw data (loadavg): 0.84 0.69 0.77 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1230 0 0 0 8995 3 0 0 25 0 1 0 420646105 6574080 1208 4294967295 134512640 134672761 3221224640 3221223808 134561115 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.86 0.70 0.77 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1270 0 0 0 9995 3 0 0 25 0 1 0 420646105 6709248 1248 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1638 1248 603 41 0 1597 0
vsize: 6552
[startup+110.004 s]
Raw data (loadavg): 0.88 0.71 0.77 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1276 0 0 0 10995 3 0 0 25 0 1 0 420646105 6844416 1254 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.005 s]
Raw data (loadavg): 0.90 0.71 0.78 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1322 0 0 0 11995 4 0 0 25 0 1 0 420646105 6975488 1300 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1703 1300 603 41 0 1662 0
vsize: 6812
[startup+130.005 s]
Raw data (loadavg): 0.92 0.72 0.78 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1372 0 0 0 12995 4 0 0 25 0 1 0 420646105 7245824 1350 4294967295 134512640 134672761 3221224640 3221223824 134559581 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.005 s]
Raw data (loadavg): 0.93 0.73 0.78 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1392 0 0 0 13995 4 0 0 25 0 1 0 420646105 7245824 1370 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.005 s]
Raw data (loadavg): 0.94 0.74 0.78 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1408 0 0 0 14995 4 0 0 25 0 1 0 420646105 7393280 1386 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.005 s]
Raw data (loadavg): 0.95 0.75 0.78 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1420 0 0 0 15996 4 0 0 25 0 1 0 420646105 7393280 1398 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.95 0.76 0.79 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1434 0 0 0 16996 4 0 0 25 0 1 0 420646105 7393280 1412 4294967295 134512640 134672761 3221224640 3221223824 134559405 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.005 s]
Raw data (loadavg): 0.96 0.76 0.79 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1442 0 0 0 17996 4 0 0 25 0 1 0 420646105 7536640 1420 4294967295 134512640 134672761 3221224640 3221223776 134560566 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.005 s]
Raw data (loadavg): 0.97 0.77 0.79 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1490 0 0 0 18996 5 0 0 25 0 1 0 420646105 7671808 1468 4294967295 134512640 134672761 3221224640 3221223808 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.006 s]
Raw data (loadavg): 0.97 0.78 0.79 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1542 0 0 0 19996 5 0 0 25 0 1 0 420646105 7942144 1520 4294967295 134512640 134672761 3221224640 3221223840 134557911 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.98 0.79 0.79 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1563 0 0 0 20996 5 0 0 25 0 1 0 420646105 7942144 1541 4294967295 134512640 134672761 3221224640 3221223824 134559336 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.006 s]
Raw data (loadavg): 0.98 0.79 0.80 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1576 0 0 0 21996 5 0 0 25 0 1 0 420646105 8081408 1554 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1554 603 41 0 1932 0
vsize: 7892
[startup+230.006 s]
Raw data (loadavg): 0.98 0.80 0.80 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1584 0 0 0 22996 5 0 0 25 0 1 0 420646105 8081408 1562 4294967295 134512640 134672761 3221224640 3221223640 1075349712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1562 603 41 0 1932 0
vsize: 7892
[startup+240.006 s]
Raw data (loadavg): 0.98 0.80 0.80 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1588 0 0 0 23997 5 0 0 25 0 1 0 420646105 8081408 1566 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1566 603 41 0 1932 0
vsize: 7892
[startup+250.006 s]
Raw data (loadavg): 0.99 0.81 0.80 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1596 0 0 0 24997 5 0 0 25 0 1 0 420646105 8081408 1574 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1574 603 41 0 1932 0
vsize: 7892
[startup+260.007 s]
Raw data (loadavg): 0.99 0.82 0.80 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1607 0 0 0 25997 5 0 0 25 0 1 0 420646105 8220672 1585 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1585 603 41 0 1966 0
vsize: 8028
[startup+270.007 s]
Raw data (loadavg): 0.99 0.82 0.81 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1627 0 0 0 26997 5 0 0 25 0 1 0 420646105 8220672 1605 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1605 603 41 0 1966 0
vsize: 8028
[startup+280.007 s]
Raw data (loadavg): 0.99 0.83 0.81 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1634 0 0 0 27997 5 0 0 25 0 1 0 420646105 8355840 1612 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1612 603 41 0 1999 0
vsize: 8160
[startup+290.007 s]
Raw data (loadavg): 0.99 0.83 0.81 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1663 0 0 0 28997 5 0 0 25 0 1 0 420646105 8491008 1641 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1641 603 41 0 2032 0
vsize: 8292
[startup+300.008 s]
Raw data (loadavg): 0.99 0.84 0.81 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1715 0 0 0 29997 5 0 0 25 0 1 0 420646105 8626176 1693 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1693 603 41 0 2065 0
vsize: 8424
[startup+310.008 s]
Raw data (loadavg): 0.99 0.84 0.81 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1744 0 0 0 30997 5 0 0 25 0 1 0 420646105 8769536 1722 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1722 603 41 0 2100 0
vsize: 8564
[startup+320.009 s]
Raw data (loadavg): 0.99 0.85 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1760 0 0 0 31997 5 0 0 25 0 1 0 420646105 8904704 1738 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1738 603 41 0 2133 0
vsize: 8696
[startup+330.009 s]
Raw data (loadavg): 0.99 0.85 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1764 0 0 0 32997 5 0 0 25 0 1 0 420646105 8904704 1742 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1742 603 41 0 2133 0
vsize: 8696
[startup+340.009 s]
Raw data (loadavg): 0.99 0.86 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1774 0 0 0 33998 5 0 0 25 0 1 0 420646105 8904704 1752 4294967295 134512640 134672761 3221224640 3221223824 134558324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1752 603 41 0 2133 0
vsize: 8696
[startup+350.009 s]
Raw data (loadavg): 0.99 0.86 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1774 0 0 0 34998 5 0 0 25 0 1 0 420646105 8904704 1752 4294967295 134512640 134672761 3221224640 3221223840 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1752 603 41 0 2133 0
vsize: 8696
[startup+360.01 s]
Raw data (loadavg): 0.99 0.86 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1787 0 0 0 35998 5 0 0 25 0 1 0 420646105 8904704 1765 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1765 603 41 0 2133 0
vsize: 8696
[startup+370.01 s]
Raw data (loadavg): 0.99 0.87 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1826 0 0 0 36998 5 0 0 25 0 1 0 420646105 9175040 1804 4294967295 134512640 134672761 3221224640 3221223808 134561375 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.01 s]
Raw data (loadavg): 0.99 0.87 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1829 0 0 0 37998 5 0 0 25 0 1 0 420646105 9175040 1807 4294967295 134512640 134672761 3221224640 3221223808 134560942 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.88 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1834 0 0 0 38998 6 0 0 25 0 1 0 420646105 9175040 1812 4294967295 134512640 134672761 3221224640 3221223808 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.88 0.82 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1847 0 0 0 39998 6 0 0 25 0 1 0 420646105 9175040 1825 4294967295 134512640 134672761 3221224640 3221223776 134560673 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.88 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1863 0 0 0 40998 6 0 0 25 0 1 0 420646105 9306112 1841 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.89 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1869 0 0 0 41999 6 0 0 25 0 1 0 420646105 9306112 1847 4294967295 134512640 134672761 3221224640 3221223808 134560903 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.012 s]
Raw data (loadavg): 0.99 0.89 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1874 0 0 0 42999 6 0 0 25 0 1 0 420646105 9306112 1852 4294967295 134512640 134672761 3221224640 3221223824 134558654 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.89 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1884 0 0 0 43999 6 0 0 25 0 1 0 420646105 9441280 1862 4294967295 134512640 134672761 3221224640 3221223808 134561021 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.012 s]
Raw data (loadavg): 0.99 0.89 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1884 0 0 0 44999 6 0 0 25 0 1 0 420646105 9441280 1862 4294967295 134512640 134672761 3221224640 3221223744 134560196 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.90 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1941 0 0 0 45999 6 0 0 25 0 1 0 420646105 9576448 1919 4294967295 134512640 134672761 3221224640 3221223776 134565098 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.013 s]
Raw data (loadavg): 0.99 0.90 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1956 0 0 0 46999 6 0 0 25 0 1 0 420646105 9723904 1934 4294967295 134512640 134672761 3221224640 3221223824 134559405 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.013 s]
Raw data (loadavg): 0.99 0.90 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1962 0 0 0 47999 6 0 0 25 0 1 0 420646105 9723904 1940 4294967295 134512640 134672761 3221224640 3221223808 134561201 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.91 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1990 0 0 0 48999 6 0 0 25 0 1 0 420646105 9863168 1968 4294967295 134512640 134672761 3221224640 3221223808 134561151 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.91 0.83 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 1996 0 0 0 49999 6 0 0 25 0 1 0 420646105 9863168 1974 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1974 603 41 0 2367 0
vsize: 9632
[startup+510.013 s]
Raw data (loadavg): 0.99 0.91 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2001 0 0 0 50999 6 0 0 25 0 1 0 420646105 9863168 1979 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1979 603 41 0 2367 0
vsize: 9632
[startup+520.013 s]
Raw data (loadavg): 0.99 0.91 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2010 0 0 0 51999 6 0 0 25 0 1 0 420646105 9863168 1988 4294967295 134512640 134672761 3221224640 3221223764 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1988 603 41 0 2367 0
vsize: 9632
[startup+530.013 s]
Raw data (loadavg): 0.99 0.92 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2020 0 0 0 52999 6 0 0 25 0 1 0 420646105 10002432 1998 4294967295 134512640 134672761 3221224640 3221223824 134558754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 1998 603 41 0 2401 0
vsize: 9768
[startup+540.013 s]
Raw data (loadavg): 0.99 0.92 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2031 0 0 0 54000 6 0 0 25 0 1 0 420646105 10002432 2009 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 2009 603 41 0 2401 0
vsize: 9768
[startup+550.013 s]
Raw data (loadavg): 0.99 0.92 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2037 0 0 0 55000 6 0 0 25 0 1 0 420646105 10002432 2015 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 2015 603 41 0 2401 0
vsize: 9768
[startup+560.013 s]
Raw data (loadavg): 0.99 0.92 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2048 0 0 0 56000 6 0 0 25 0 1 0 420646105 10137600 2026 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2026 603 41 0 2434 0
vsize: 9900
[startup+570.013 s]
Raw data (loadavg): 0.99 0.92 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2052 0 0 0 57000 6 0 0 25 0 1 0 420646105 10137600 2030 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2030 603 41 0 2434 0
vsize: 9900
[startup+580.013 s]
Raw data (loadavg): 0.99 0.93 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2052 0 0 0 58000 6 0 0 25 0 1 0 420646105 10137600 2030 4294967295 134512640 134672761 3221224640 3221223856 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2030 603 41 0 2434 0
vsize: 9900
[startup+590.013 s]
Raw data (loadavg): 0.99 0.93 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2058 0 0 0 59000 6 0 0 25 0 1 0 420646105 10137600 2036 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2036 603 41 0 2434 0
vsize: 9900
[startup+600.014 s]
Raw data (loadavg): 0.99 0.93 0.84 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2079 0 0 0 60001 6 0 0 25 0 1 0 420646105 10137600 2057 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2057 603 41 0 2434 0
vsize: 9900
[startup+610.014 s]
Raw data (loadavg): 0.99 0.93 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2087 0 0 0 61001 6 0 0 25 0 1 0 420646105 10268672 2065 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2065 603 41 0 2466 0
vsize: 10028
[startup+620.015 s]
Raw data (loadavg): 0.99 0.93 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2101 0 0 0 62001 6 0 0 25 0 1 0 420646105 10268672 2079 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2079 603 41 0 2466 0
vsize: 10028
[startup+630.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2101 0 0 0 63001 6 0 0 25 0 1 0 420646105 10268672 2079 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2079 603 41 0 2466 0
vsize: 10028
[startup+640.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2101 0 0 0 64001 6 0 0 25 0 1 0 420646105 10268672 2079 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2079 603 41 0 2466 0
vsize: 10028
[startup+650.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2104 0 0 0 65002 6 0 0 25 0 1 0 420646105 10268672 2082 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2082 603 41 0 2466 0
vsize: 10028
[startup+660.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2116 0 0 0 66002 6 0 0 25 0 1 0 420646105 10412032 2094 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2094 603 41 0 2501 0
vsize: 10168
[startup+670.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2119 0 0 0 67002 6 0 0 25 0 1 0 420646105 10412032 2097 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2097 603 41 0 2501 0
vsize: 10168
[startup+680.015 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2124 0 0 0 68002 6 0 0 25 0 1 0 420646105 10412032 2102 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2102 603 41 0 2501 0
vsize: 10168
[startup+690.014 s]
Raw data (loadavg): 0.99 0.94 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2136 0 0 0 69002 6 0 0 25 0 1 0 420646105 10412032 2114 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2114 603 41 0 2501 0
vsize: 10168
[startup+700.014 s]
Raw data (loadavg): 0.99 0.95 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2136 0 0 0 70002 6 0 0 25 0 1 0 420646105 10412032 2114 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2542 2114 603 41 0 2501 0
vsize: 10168
[startup+710.014 s]
Raw data (loadavg): 0.99 0.95 0.85 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2140 0 0 0 71002 6 0 0 25 0 1 0 420646105 10551296 2118 4294967295 134512640 134672761 3221224640 3221223808 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.015 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2143 0 0 0 72002 7 0 0 25 0 1 0 420646105 10551296 2121 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2576 2121 603 41 0 2535 0
vsize: 10304
[startup+730.015 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2211 0 0 0 73001 7 0 0 25 0 1 0 420646105 10821632 2189 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2189 603 41 0 2601 0
vsize: 10568
[startup+740.015 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2216 0 0 0 74001 7 0 0 25 0 1 0 420646105 10821632 2194 4294967295 134512640 134672761 3221224640 3221223744 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2194 603 41 0 2601 0
vsize: 10568
[startup+750.015 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2230 0 0 0 75002 7 0 0 25 0 1 0 420646105 10821632 2208 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2208 603 41 0 2601 0
vsize: 10568
[startup+760.015 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2236 0 0 0 76002 7 0 0 25 0 1 0 420646105 10821632 2214 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2642 2214 603 41 0 2601 0
vsize: 10568
[startup+770.016 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2277 0 0 0 77002 7 0 0 25 0 1 0 420646105 11091968 2255 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2255 603 41 0 2667 0
vsize: 10832
[startup+780.017 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2286 0 0 0 78002 7 0 0 25 0 1 0 420646105 11091968 2264 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2264 603 41 0 2667 0
vsize: 10832
[startup+790.017 s]
Raw data (loadavg): 0.99 0.95 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2286 0 0 0 79002 7 0 0 25 0 1 0 420646105 11091968 2264 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2264 603 41 0 2667 0
vsize: 10832
[startup+800.018 s]
Raw data (loadavg): 0.99 0.96 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2286 0 0 0 80002 7 0 0 25 0 1 0 420646105 11091968 2264 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2264 603 41 0 2667 0
vsize: 10832
[startup+810.018 s]
Raw data (loadavg): 0.99 0.96 0.86 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2288 0 0 0 81003 7 0 0 25 0 1 0 420646105 11091968 2266 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2708 2266 603 41 0 2667 0
vsize: 10832
[startup+820.018 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2296 0 0 0 82003 7 0 0 25 0 1 0 420646105 11227136 2274 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2274 603 41 0 2700 0
vsize: 10964
[startup+830.018 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2297 0 0 0 83003 7 0 0 25 0 1 0 420646105 11227136 2275 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2275 603 41 0 2700 0
vsize: 10964
[startup+840.018 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2300 0 0 0 84003 7 0 0 25 0 1 0 420646105 11227136 2278 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2278 603 41 0 2700 0
vsize: 10964
[startup+850.019 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2307 0 0 0 85003 7 0 0 25 0 1 0 420646105 11227136 2285 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2285 603 41 0 2700 0
vsize: 10964
[startup+860.019 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2311 0 0 0 86003 7 0 0 25 0 1 0 420646105 11227136 2289 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2289 603 41 0 2700 0
vsize: 10964
[startup+870.019 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2315 0 0 0 87004 7 0 0 25 0 1 0 420646105 11227136 2293 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2741 2293 603 41 0 2700 0
vsize: 10964
[startup+880.02 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2320 0 0 0 88004 7 0 0 25 0 1 0 420646105 11227136 2298 4294967295 134512640 134672761 3221224640 3221223808 134561193 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.02 s]
Raw data (loadavg): 0.99 0.96 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2324 0 0 0 89004 7 0 0 25 0 1 0 420646105 11227136 2302 4294967295 134512640 134672761 3221224640 3221223776 134560718 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.021 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2324 0 0 0 90004 7 0 0 25 0 1 0 420646105 11227136 2302 4294967295 134512640 134672761 3221224640 3221223808 134561151 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.021 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2337 0 0 0 91004 7 0 0 25 0 1 0 420646105 11370496 2315 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2776 2315 603 41 0 2735 0
vsize: 11104
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2343 0 0 0 92005 7 0 0 25 0 1 0 420646105 11370496 2321 4294967295 134512640 134672761 3221224640 3221223808 134561229 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.021 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2364 0 0 0 93005 7 0 0 25 0 1 0 420646105 11505664 2342 4294967295 134512640 134672761 3221224640 3221223808 134561229 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.021 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2365 0 0 0 94005 7 0 0 25 0 1 0 420646105 11505664 2343 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2809 2343 603 41 0 2768 0
vsize: 11236
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2369 0 0 0 95005 7 0 0 25 0 1 0 420646105 11505664 2347 4294967295 134512640 134672761 3221224640 3221223808 134561021 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.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2369 0 0 0 96005 7 0 0 25 0 1 0 420646105 11505664 2347 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.023 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2373 0 0 0 97006 7 0 0 25 0 1 0 420646105 11505664 2351 4294967295 134512640 134672761 3221224640 3221223808 134560892 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.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2376 0 0 0 98006 7 0 0 25 0 1 0 420646105 11505664 2354 4294967295 134512640 134672761 3221224640 3221223808 134561164 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.023 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2397 0 0 0 99006 7 0 0 25 0 1 0 420646105 11640832 2375 4294967295 134512640 134672761 3221224640 3221223824 134559116 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.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2397 0 0 0 100006 7 0 0 25 0 1 0 420646105 11640832 2375 4294967295 134512640 134672761 3221224640 3221223808 134560906 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.02 s]
Raw data (loadavg): 0.99 0.97 0.88 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2400 0 0 0 101006 7 0 0 25 0 1 0 420646105 11640832 2378 4294967295 134512640 134672761 3221224640 3221223808 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.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2400 0 0 0 102006 7 0 0 25 0 1 0 420646105 11640832 2378 4294967295 134512640 134672761 3221224640 3221223824 134558423 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.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2441 0 0 0 103006 8 0 0 25 0 1 0 420646105 11776000 2419 4294967295 134512640 134672761 3221224640 3221223808 134560867 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.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2445 0 0 0 104006 8 0 0 25 0 1 0 420646105 11776000 2423 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2449 0 0 0 105007 8 0 0 25 0 1 0 420646105 11776000 2427 4294967295 134512640 134672761 3221224640 3221223808 134561164 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.02 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2449 0 0 0 106007 8 0 0 25 0 1 0 420646105 11776000 2427 4294967295 134512640 134672761 3221224640 3221223808 134561151 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2450 0 0 0 107007 8 0 0 25 0 1 0 420646105 11776000 2428 4294967295 134512640 134672761 3221224640 3221223824 134558662 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2450 0 0 0 108007 8 0 0 25 0 1 0 420646105 11776000 2428 4294967295 134512640 134672761 3221224640 3221223776 134560577 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2450 0 0 0 109007 8 0 0 25 0 1 0 420646105 11776000 2428 4294967295 134512640 134672761 3221224640 3221223776 134556427 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2450 0 0 0 110008 8 0 0 25 0 1 0 420646105 11776000 2428 4294967295 134512640 134672761 3221224640 3221223808 134560980 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2456 0 0 0 111008 8 0 0 25 0 1 0 420646105 11776000 2434 4294967295 134512640 134672761 3221224640 3221223808 134561193 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.89 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2465 0 0 0 112008 8 0 0 25 0 1 0 420646105 11915264 2443 4294967295 134512640 134672761 3221224640 3221223808 134561193 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2471 0 0 0 113008 8 0 0 25 0 1 0 420646105 11915264 2449 4294967295 134512640 134672761 3221224640 3221223808 134560828 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2478 0 0 0 114008 8 0 0 25 0 1 0 420646105 11915264 2456 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2456 603 41 0 2868 0
vsize: 11636
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2503 0 0 0 115008 8 0 0 25 0 1 0 420646105 12050432 2481 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2481 603 41 0 2901 0
vsize: 11768
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2508 0 0 0 116008 8 0 0 25 0 1 0 420646105 12050432 2486 4294967295 134512640 134672761 3221224640 3221223808 134561188 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2515 0 0 0 117008 8 0 0 25 0 1 0 420646105 12050432 2493 4294967295 134512640 134672761 3221224640 3221223824 134559332 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2518 0 0 0 118008 8 0 0 25 0 1 0 420646105 12050432 2496 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2519 0 0 0 119008 8 0 0 25 0 1 0 420646105 12050432 2497 4294967295 134512640 134672761 3221224640 3221223808 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.90 2/54 16015
Raw data (stat): 16015 (minisat+) R 16014 10720 10719 0 -1 0 2519 0 0 0 120008 8 0 0 25 0 1 0 420646105 12050432 2497 4294967295 134512640 134672761 3221224640 3221223824 134559415 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.90 1/54 16015
Raw data (stat): 16015 (minisat+) Z 16014 10720 10719 0 -1 12 2521 0 0 0 120008 9 0 0 25 0 1 0 420646105 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.18
CPU user time (s): 1200.09
CPU system time (s): 0.093985
CPU usage (%): 100.012
Max. virtual memory (Kb): 11768
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####