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-f600.opb
MD5SUM	4fdec182582ed31d1ae371090f6cc5c1
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	1200
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	1200
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	1200
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	1200
Total number of constraints	3150
Number of constraints which are clauses	3150
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 5434

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907312 kB
Buffers:         35016 kB
Cached:          53740 kB
SwapCached:        392 kB
Active:          50352 kB
Inactive:        41540 kB
HighTotal:      131008 kB
HighFree:        73612 kB
LowTotal:       903652 kB
LowFree:        833700 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29880 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:17:14 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3889 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3150     8850 |     944       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1197          
c   -- var.elim.:  1197/1197          
c |         0 |    3150     8850 |    1260       0        0     nan |  0.000 % |
c |       101 |    3150     8850 |    1386     101     2734    27.1 |  0.000 % |
c |       252 |    3150     8850 |    1524     252     8050    31.9 |#### 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.50 0.78 0.85 1/54 28322
Raw data (stat): 28322 (runsolver) R 28321 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480071915 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.57 0.79 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 765 0 0 0 997 1 0 0 25 0 1 0 480071915 4583424 743 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1119 743 603 41 0 1078 0
vsize: 4476
[startup+20.0003 s]
Raw data (loadavg): 0.64 0.80 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 858 0 0 0 1997 2 0 0 25 0 1 0 480071915 5070848 836 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1238 836 603 41 0 1197 0
vsize: 4952
[startup+30.0012 s]
Raw data (loadavg): 0.69 0.80 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 905 0 0 0 2997 2 0 0 25 0 1 0 480071915 5181440 883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1265 883 603 41 0 1224 0
vsize: 5060
[startup+40.0009 s]
Raw data (loadavg): 0.74 0.81 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 928 0 0 0 3996 2 0 0 25 0 1 0 480071915 5292032 906 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1292 906 603 41 0 1251 0
vsize: 5168
[startup+50.0011 s]
Raw data (loadavg): 0.78 0.81 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 998 0 0 0 4997 2 0 0 25 0 1 0 480071915 5558272 976 4294967295 134512640 134672761 3221224576 3221223616 134612975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1357 976 603 41 0 1316 0
vsize: 5428
[startup+60.002 s]
Raw data (loadavg): 0.81 0.82 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1018 0 0 0 5997 2 0 0 25 0 1 0 480071915 5693440 996 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1390 996 603 41 0 1349 0
vsize: 5560
[startup+70.0027 s]
Raw data (loadavg): 0.84 0.83 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1080 0 0 0 6997 3 0 0 25 0 1 0 480071915 5947392 1058 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1452 1058 603 41 0 1411 0
vsize: 5808
[startup+80.0039 s]
Raw data (loadavg): 0.87 0.83 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1086 0 0 0 7997 3 0 0 25 0 1 0 480071915 5947392 1064 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1452 1064 603 41 0 1411 0
vsize: 5808
[startup+90.0038 s]
Raw data (loadavg): 0.89 0.84 0.85 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1123 0 0 0 8997 3 0 0 25 0 1 0 480071915 6152192 1101 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1502 1101 603 41 0 1461 0
vsize: 6008
[startup+100.003 s]
Raw data (loadavg): 0.90 0.84 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1130 0 0 0 9997 3 0 0 25 0 1 0 480071915 6152192 1108 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1502 1108 603 41 0 1461 0
vsize: 6008
[startup+110.005 s]
Raw data (loadavg): 0.92 0.85 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1160 0 0 0 10997 3 0 0 25 0 1 0 480071915 6279168 1138 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1533 1138 603 41 0 1492 0
vsize: 6132
[startup+120.006 s]
Raw data (loadavg): 0.93 0.85 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1170 0 0 0 11998 3 0 0 25 0 1 0 480071915 6279168 1148 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1533 1148 603 41 0 1492 0
vsize: 6132
[startup+130.007 s]
Raw data (loadavg): 0.94 0.85 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1187 0 0 0 12998 3 0 0 25 0 1 0 480071915 6393856 1165 4294967295 134512640 134672761 3221224576 3221223616 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1561 1165 603 41 0 1520 0
vsize: 6244
[startup+140.007 s]
Raw data (loadavg): 0.95 0.86 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1205 0 0 0 13998 3 0 0 25 0 1 0 480071915 6393856 1183 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1561 1183 603 41 0 1520 0
vsize: 6244
[startup+150.006 s]
Raw data (loadavg): 0.96 0.86 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1220 0 0 0 14998 3 0 0 25 0 1 0 480071915 6496256 1198 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1586 1198 603 41 0 1545 0
vsize: 6344
[startup+160.007 s]
Raw data (loadavg): 0.96 0.87 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1232 0 0 0 15998 3 0 0 25 0 1 0 480071915 6496256 1210 4294967295 134512640 134672761 3221224576 3221223564 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1586 1210 603 41 0 1545 0
vsize: 6344
[startup+170.037 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 28322
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1286 0 0 0 17001 3 0 0 25 0 1 0 480071915 6754304 1264 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1264 603 41 0 1608 0
vsize: 6596
[startup+180.037 s]
Raw data (loadavg): 1.05 0.89 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1302 0 0 0 18001 4 0 0 25 0 1 0 480071915 6860800 1280 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1280 603 41 0 1634 0
vsize: 6700
[startup+190.038 s]
Raw data (loadavg): 1.04 0.89 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1310 0 0 0 19001 4 0 0 25 0 1 0 480071915 6860800 1288 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1288 603 41 0 1634 0
vsize: 6700
[startup+200.038 s]
Raw data (loadavg): 1.04 0.90 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1329 0 0 0 20001 4 0 0 25 0 1 0 480071915 6971392 1307 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1702 1307 603 41 0 1661 0
vsize: 6808
[startup+210.039 s]
Raw data (loadavg): 1.03 0.90 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1340 0 0 0 21002 4 0 0 25 0 1 0 480071915 6971392 1318 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1702 1318 603 41 0 1661 0
vsize: 6808
[startup+220.04 s]
Raw data (loadavg): 1.03 0.90 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1355 0 0 0 22002 4 0 0 25 0 1 0 480071915 7073792 1333 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1727 1333 603 41 0 1686 0
vsize: 6908
[startup+230.04 s]
Raw data (loadavg): 1.02 0.91 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1360 0 0 0 23002 4 0 0 25 0 1 0 480071915 7073792 1338 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1727 1338 603 41 0 1686 0
vsize: 6908
[startup+240.04 s]
Raw data (loadavg): 1.02 0.91 0.87 2/54 28375
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1363 0 0 0 24002 4 0 0 25 0 1 0 480071915 7073792 1341 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1727 1341 603 41 0 1686 0
vsize: 6908
[startup+250.04 s]
Raw data (loadavg): 1.01 0.91 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1370 0 0 0 25002 4 0 0 25 0 1 0 480071915 7073792 1348 4294967295 134512640 134672761 3221224576 3221223760 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1727 1348 603 41 0 1686 0
vsize: 6908
[startup+260.041 s]
Raw data (loadavg): 1.01 0.91 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1391 0 0 0 26002 4 0 0 25 0 1 0 480071915 7204864 1369 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1759 1369 603 41 0 1718 0
vsize: 7036
[startup+270.04 s]
Raw data (loadavg): 1.01 0.92 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1403 0 0 0 27002 4 0 0 25 0 1 0 480071915 7204864 1381 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1759 1381 603 41 0 1718 0
vsize: 7036
[startup+280.041 s]
Raw data (loadavg): 1.01 0.92 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1411 0 0 0 28003 4 0 0 25 0 1 0 480071915 7307264 1389 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1784 1389 603 41 0 1743 0
vsize: 7136
[startup+290.041 s]
Raw data (loadavg): 1.01 0.92 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1430 0 0 0 29003 4 0 0 25 0 1 0 480071915 7307264 1408 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1784 1408 603 41 0 1743 0
vsize: 7136
[startup+300.041 s]
Raw data (loadavg): 1.00 0.92 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1440 0 0 0 30003 4 0 0 25 0 1 0 480071915 7409664 1418 4294967295 134512640 134672761 3221224576 3221223616 134612694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1809 1418 603 41 0 1768 0
vsize: 7236
[startup+310.042 s]
Raw data (loadavg): 1.00 0.92 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1445 0 0 0 31003 4 0 0 25 0 1 0 480071915 7409664 1423 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1809 1423 603 41 0 1768 0
vsize: 7236
[startup+320.042 s]
Raw data (loadavg): 1.00 0.93 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1459 0 0 0 32003 4 0 0 25 0 1 0 480071915 7516160 1437 4294967295 134512640 134672761 3221224576 3221223760 134615951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1437 603 41 0 1794 0
vsize: 7340
[startup+330.043 s]
Raw data (loadavg): 1.00 0.93 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1467 0 0 0 33003 4 0 0 25 0 1 0 480071915 7516160 1445 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1445 603 41 0 1794 0
vsize: 7340
[startup+340.043 s]
Raw data (loadavg): 1.00 0.93 0.88 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1477 0 0 0 34003 4 0 0 25 0 1 0 480071915 7516160 1455 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1455 603 41 0 1794 0
vsize: 7340
[startup+350.043 s]
Raw data (loadavg): 1.00 0.93 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1484 0 0 0 35004 4 0 0 25 0 1 0 480071915 7618560 1462 4294967295 134512640 134672761 3221224576 3221223616 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1860 1462 603 41 0 1819 0
vsize: 7440
[startup+360.044 s]
Raw data (loadavg): 1.00 0.93 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1484 0 0 0 36004 4 0 0 25 0 1 0 480071915 7618560 1462 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1860 1462 603 41 0 1819 0
vsize: 7440
[startup+370.044 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1494 0 0 0 37004 4 0 0 25 0 1 0 480071915 7618560 1472 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1860 1472 603 41 0 1819 0
vsize: 7440
[startup+380.045 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1506 0 0 0 38004 4 0 0 25 0 1 0 480071915 7618560 1484 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1860 1484 603 41 0 1819 0
vsize: 7440
[startup+390.045 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1506 0 0 0 39004 4 0 0 25 0 1 0 480071915 7618560 1484 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1860 1484 603 41 0 1819 0
vsize: 7440
[startup+400.044 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1573 0 0 0 40004 4 0 0 25 0 1 0 480071915 7987200 1551 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1551 603 41 0 1909 0
vsize: 7800
[startup+410.045 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1580 0 0 0 41005 4 0 0 25 0 1 0 480071915 7987200 1558 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1558 603 41 0 1909 0
vsize: 7800
[startup+420.044 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1580 0 0 0 42005 4 0 0 25 0 1 0 480071915 7987200 1558 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1558 603 41 0 1909 0
vsize: 7800
[startup+430.046 s]
Raw data (loadavg): 1.00 0.94 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1582 0 0 0 43005 4 0 0 25 0 1 0 480071915 7987200 1560 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1560 603 41 0 1909 0
vsize: 7800
[startup+440.045 s]
Raw data (loadavg): 1.00 0.95 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1582 0 0 0 44005 4 0 0 25 0 1 0 480071915 7987200 1560 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1560 603 41 0 1909 0
vsize: 7800
[startup+450.045 s]
Raw data (loadavg): 1.00 0.95 0.89 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1600 0 0 0 45005 4 0 0 25 0 1 0 480071915 8060928 1578 4294967295 134512640 134672761 3221224576 3221223616 134613815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1968 1578 603 41 0 1927 0
vsize: 7872
[startup+460.045 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1611 0 0 0 46005 4 0 0 25 0 1 0 480071915 8130560 1589 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1985 1589 603 41 0 1944 0
vsize: 7940
[startup+470.045 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1620 0 0 0 47006 4 0 0 25 0 1 0 480071915 8130560 1598 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1985 1598 603 41 0 1944 0
vsize: 7940
[startup+480.046 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28377
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1633 0 0 0 48006 4 0 0 25 0 1 0 480071915 8245248 1611 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2013 1611 603 41 0 1972 0
vsize: 8052
[startup+490.046 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1641 0 0 0 49006 4 0 0 25 0 1 0 480071915 8245248 1619 4294967295 134512640 134672761 3221224576 3221223652 1075347030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2013 1619 603 41 0 1972 0
vsize: 8052
[startup+500.046 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1641 0 0 0 50006 4 0 0 25 0 1 0 480071915 8245248 1619 4294967295 134512640 134672761 3221224576 3221223616 134612992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2013 1619 603 41 0 1972 0
vsize: 8052
[startup+510.047 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1650 0 0 0 51006 4 0 0 25 0 1 0 480071915 8245248 1628 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2013 1628 603 41 0 1972 0
vsize: 8052
[startup+520.047 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1668 0 0 0 52006 5 0 0 25 0 1 0 480071915 8331264 1646 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2034 1646 603 41 0 1993 0
vsize: 8136
[startup+530.048 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1674 0 0 0 53006 5 0 0 25 0 1 0 480071915 8409088 1652 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1652 603 41 0 2012 0
vsize: 8212
[startup+540.048 s]
Raw data (loadavg): 1.00 0.95 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1674 0 0 0 54006 5 0 0 25 0 1 0 480071915 8409088 1652 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1652 603 41 0 2012 0
vsize: 8212
[startup+550.048 s]
Raw data (loadavg): 1.00 0.96 0.90 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1677 0 0 0 55007 5 0 0 25 0 1 0 480071915 8409088 1655 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1655 603 41 0 2012 0
vsize: 8212
[startup+560.049 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1679 0 0 0 56007 5 0 0 25 0 1 0 480071915 8409088 1657 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1657 603 41 0 2012 0
vsize: 8212
[startup+570.049 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1679 0 0 0 57007 5 0 0 25 0 1 0 480071915 8409088 1657 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1657 603 41 0 2012 0
vsize: 8212
[startup+580.05 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1682 0 0 0 58007 5 0 0 25 0 1 0 480071915 8409088 1660 4294967295 134512640 134672761 3221224576 3221223712 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1660 603 41 0 2012 0
vsize: 8212
[startup+590.05 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1688 0 0 0 59008 5 0 0 25 0 1 0 480071915 8409088 1666 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1666 603 41 0 2012 0
vsize: 8212
[startup+600.05 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1689 0 0 0 60008 5 0 0 25 0 1 0 480071915 8409088 1667 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1667 603 41 0 2012 0
vsize: 8212
[startup+610.05 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1690 0 0 0 61008 5 0 0 25 0 1 0 480071915 8409088 1668 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1668 603 41 0 2012 0
vsize: 8212
[startup+620.05 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1702 0 0 0 62008 5 0 0 25 0 1 0 480071915 8523776 1680 4294967295 134512640 134672761 3221224576 3221223616 134614182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2081 1680 603 41 0 2040 0
vsize: 8324
[startup+630.051 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1724 0 0 0 63008 5 0 0 25 0 1 0 480071915 8609792 1702 4294967295 134512640 134672761 3221224576 3221223712 134614524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2102 1702 603 41 0 2061 0
vsize: 8408
[startup+640.051 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1747 0 0 0 64008 5 0 0 25 0 1 0 480071915 8679424 1725 4294967295 134512640 134672761 3221224576 3221223760 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2119 1725 603 41 0 2078 0
vsize: 8476
[startup+650.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1763 0 0 0 65008 5 0 0 25 0 1 0 480071915 8757248 1741 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2138 1741 603 41 0 2097 0
vsize: 8552
[startup+660.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1766 0 0 0 66008 5 0 0 25 0 1 0 480071915 8757248 1744 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2138 1744 603 41 0 2097 0
vsize: 8552
[startup+670.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1778 0 0 0 67008 5 0 0 25 0 1 0 480071915 8830976 1756 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1756 603 41 0 2115 0
vsize: 8624
[startup+680.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1778 0 0 0 68009 5 0 0 25 0 1 0 480071915 8830976 1756 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1756 603 41 0 2115 0
vsize: 8624
[startup+690.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1778 0 0 0 69009 5 0 0 25 0 1 0 480071915 8830976 1756 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1756 603 41 0 2115 0
vsize: 8624
[startup+700.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1778 0 0 0 70009 5 0 0 25 0 1 0 480071915 8830976 1756 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1756 603 41 0 2115 0
vsize: 8624
[startup+710.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1781 0 0 0 71009 5 0 0 25 0 1 0 480071915 8830976 1759 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1759 603 41 0 2115 0
vsize: 8624
[startup+720.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1794 0 0 0 72009 5 0 0 25 0 1 0 480071915 8830976 1772 4294967295 134512640 134672761 3221224576 3221223672 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1772 603 41 0 2115 0
vsize: 8624
[startup+730.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1794 0 0 0 73009 5 0 0 25 0 1 0 480071915 8830976 1772 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2156 1772 603 41 0 2115 0
vsize: 8624
[startup+740.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1816 0 0 0 74010 5 0 0 25 0 1 0 480071915 8933376 1794 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2181 1794 603 41 0 2140 0
vsize: 8724
[startup+750.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1848 0 0 0 75010 5 0 0 25 0 1 0 480071915 9064448 1826 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2213 1826 603 41 0 2172 0
vsize: 8852
[startup+760.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1848 0 0 0 76010 5 0 0 25 0 1 0 480071915 9064448 1826 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2213 1826 603 41 0 2172 0
vsize: 8852
[startup+770.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1848 0 0 0 77010 5 0 0 25 0 1 0 480071915 9064448 1826 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2213 1826 603 41 0 2172 0
vsize: 8852
[startup+780.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1848 0 0 0 78010 5 0 0 25 0 1 0 480071915 9064448 1826 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2213 1826 603 41 0 2172 0
vsize: 8852
[startup+790.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1854 0 0 0 79010 5 0 0 25 0 1 0 480071915 9142272 1832 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1832 603 41 0 2191 0
vsize: 8928
[startup+800.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1854 0 0 0 80011 5 0 0 25 0 1 0 480071915 9142272 1832 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1832 603 41 0 2191 0
vsize: 8928
[startup+810.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1854 0 0 0 81011 5 0 0 25 0 1 0 480071915 9142272 1832 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1832 603 41 0 2191 0
vsize: 8928
[startup+820.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1854 0 0 0 82011 5 0 0 25 0 1 0 480071915 9142272 1832 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1832 603 41 0 2191 0
vsize: 8928
[startup+830.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1854 0 0 0 83011 5 0 0 25 0 1 0 480071915 9142272 1832 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1832 603 41 0 2191 0
vsize: 8928
[startup+840.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1868 0 0 0 84011 6 0 0 25 0 1 0 480071915 9142272 1846 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2232 1846 603 41 0 2191 0
vsize: 8928
[startup+850.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1872 0 0 0 85011 6 0 0 25 0 1 0 480071915 9216000 1850 4294967295 134512640 134672761 3221224576 3221223760 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1850 603 41 0 2209 0
vsize: 9000
[startup+860.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1876 0 0 0 86011 6 0 0 25 0 1 0 480071915 9216000 1854 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1854 603 41 0 2209 0
vsize: 9000
[startup+870.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1876 0 0 0 87012 6 0 0 25 0 1 0 480071915 9216000 1854 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1854 603 41 0 2209 0
vsize: 9000
[startup+880.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1876 0 0 0 88012 6 0 0 25 0 1 0 480071915 9216000 1854 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1854 603 41 0 2209 0
vsize: 9000
[startup+890.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1876 0 0 0 89012 6 0 0 25 0 1 0 480071915 9216000 1854 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1854 603 41 0 2209 0
vsize: 9000
[startup+900.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1876 0 0 0 90012 6 0 0 25 0 1 0 480071915 9216000 1854 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1854 603 41 0 2209 0
vsize: 9000
[startup+910.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1883 0 0 0 91012 6 0 0 25 0 1 0 480071915 9216000 1861 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2250 1861 603 41 0 2209 0
vsize: 9000
[startup+920.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1898 0 0 0 92013 6 0 0 25 0 1 0 480071915 9318400 1876 4294967295 134512640 134672761 3221224576 3221223632 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2275 1876 603 41 0 2234 0
vsize: 9100
[startup+930.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1911 0 0 0 93013 6 0 0 25 0 1 0 480071915 9318400 1889 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2275 1889 603 41 0 2234 0
vsize: 9100
[startup+940.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1912 0 0 0 94013 6 0 0 25 0 1 0 480071915 9318400 1890 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2275 1890 603 41 0 2234 0
vsize: 9100
[startup+950.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1912 0 0 0 95013 6 0 0 25 0 1 0 480071915 9318400 1890 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2275 1890 603 41 0 2234 0
vsize: 9100
[startup+960.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1941 0 0 0 96013 6 0 0 25 0 1 0 480071915 9498624 1919 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2319 1919 603 41 0 2278 0
vsize: 9276
[startup+970.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1957 0 0 0 97014 6 0 0 25 0 1 0 480071915 9498624 1935 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2319 1935 603 41 0 2278 0
vsize: 9276
[startup+980.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1965 0 0 0 98014 6 0 0 25 0 1 0 480071915 9584640 1943 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2340 1943 603 41 0 2299 0
vsize: 9360
[startup+990.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1976 0 0 0 99014 6 0 0 25 0 1 0 480071915 9584640 1954 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2340 1954 603 41 0 2299 0
vsize: 9360
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1981 0 0 0 100014 6 0 0 25 0 1 0 480071915 9658368 1959 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1959 603 41 0 2317 0
vsize: 9432
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1981 0 0 0 101014 6 0 0 25 0 1 0 480071915 9658368 1959 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1959 603 41 0 2317 0
vsize: 9432
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1981 0 0 0 102014 6 0 0 25 0 1 0 480071915 9658368 1959 4294967295 134512640 134672761 3221224576 3221223588 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1959 603 41 0 2317 0
vsize: 9432
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1981 0 0 0 103015 6 0 0 25 0 1 0 480071915 9658368 1959 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1959 603 41 0 2317 0
vsize: 9432
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1988 0 0 0 104015 6 0 0 25 0 1 0 480071915 9658368 1966 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1966 603 41 0 2317 0
vsize: 9432
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1988 0 0 0 105015 6 0 0 25 0 1 0 480071915 9658368 1966 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1966 603 41 0 2317 0
vsize: 9432
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1988 0 0 0 106015 6 0 0 25 0 1 0 480071915 9658368 1966 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1966 603 41 0 2317 0
vsize: 9432
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1992 0 0 0 107015 6 0 0 25 0 1 0 480071915 9658368 1970 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1970 603 41 0 2317 0
vsize: 9432
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 1996 0 0 0 108016 6 0 0 25 0 1 0 480071915 9658368 1974 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2358 1974 603 41 0 2317 0
vsize: 9432
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2001 0 0 0 109016 6 0 0 25 0 1 0 480071915 9740288 1979 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2378 1979 603 41 0 2337 0
vsize: 9512
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2005 0 0 0 110016 6 0 0 25 0 1 0 480071915 9740288 1983 4294967295 134512640 134672761 3221224576 3221223760 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2378 1983 603 41 0 2337 0
vsize: 9512
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2007 0 0 0 111016 6 0 0 25 0 1 0 480071915 9740288 1985 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2378 1985 603 41 0 2337 0
vsize: 9512
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2018 0 0 0 112016 6 0 0 25 0 1 0 480071915 9809920 1996 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2395 1996 603 41 0 2354 0
vsize: 9580
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2037 0 0 0 113017 6 0 0 25 0 1 0 480071915 9887744 2015 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2015 603 41 0 2373 0
vsize: 9656
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2037 0 0 0 114017 6 0 0 25 0 1 0 480071915 9887744 2015 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2015 603 41 0 2373 0
vsize: 9656
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2041 0 0 0 115017 6 0 0 25 0 1 0 480071915 9887744 2019 4294967295 134512640 134672761 3221224576 3221223760 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2019 603 41 0 2373 0
vsize: 9656
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2050 0 0 0 116017 6 0 0 25 0 1 0 480071915 9887744 2028 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2414 2028 603 41 0 2373 0
vsize: 9656
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2054 0 0 0 117017 6 0 0 25 0 1 0 480071915 9957376 2032 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2431 2032 603 41 0 2390 0
vsize: 9724
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2063 0 0 0 118017 6 0 0 25 0 1 0 480071915 9957376 2041 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2431 2041 603 41 0 2390 0
vsize: 9724
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2065 0 0 0 119018 6 0 0 25 0 1 0 480071915 9957376 2043 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2431 2043 603 41 0 2390 0
vsize: 9724
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28379
Raw data (stat): 28322 (minisat+) R 28321 23176 23175 0 -1 0 2068 0 0 0 120018 6 0 0 25 0 1 0 480071915 9957376 2046 4294967295 134512640 134672761 3221224576 3221223568 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2431 2046 603 41 0 2390 0
vsize: 9724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 28379
Raw data (stat): 28322 (minisat+) Z 28321 23176 23175 0 -1 12 2068 0 0 0 120018 7 0 0 25 0 1 0 480071915 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.26
CPU user time (s): 1200.18
CPU system time (s): 0.072988
CPU usage (%): 100.015
Max. virtual memory (Kb): 9724
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####