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 6190

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 03:47:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4639 boxname=wulflinc25 idbench=127 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc25/normalized-f1000.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-f1000.opb /oldhome/oroussel/tmp/wulflinc25/normalized-f1000.opb
IDLAUNCH: 4639
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        870468 kB
Buffers:         35080 kB
Cached:          94220 kB
SwapCached:         36 kB
Active:          50708 kB
Inactive:        81472 kB
HighTotal:      131008 kB
HighFree:        33040 kB
LowTotal:       903652 kB
LowFree:        837428 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26312 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:07:35 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4639 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.49 0.82 0.86 2/54 2475
Raw data (stat): 2475 (runsolver) R 2474 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481476794 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.57 0.83 0.86 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 821 0 0 0 996 2 0 0 25 0 1 0 481476794 4943872 799 4294967295 134512640 134672761 3221224576 3221223760 134558662 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.0007 s]
Raw data (loadavg): 0.63 0.83 0.86 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 906 0 0 0 1994 3 0 0 25 0 1 0 481476794 5214208 884 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1273 884 603 41 0 1232 0
vsize: 5092
[startup+30.0005 s]
Raw data (loadavg): 0.69 0.84 0.86 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 982 0 0 0 2994 3 0 0 25 0 1 0 481476794 5488640 960 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1340 960 603 41 0 1299 0
vsize: 5360
[startup+40.0009 s]
Raw data (loadavg): 0.74 0.84 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1049 0 0 0 3994 3 0 0 25 0 1 0 481476794 5758976 1027 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1406 1027 603 41 0 1365 0
vsize: 5624
[startup+50.0014 s]
Raw data (loadavg): 0.78 0.85 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1099 0 0 0 4994 3 0 0 25 0 1 0 481476794 6033408 1077 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1077 603 41 0 1432 0
vsize: 5892
[startup+60.0013 s]
Raw data (loadavg): 0.81 0.85 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1138 0 0 0 5994 3 0 0 25 0 1 0 481476794 6168576 1116 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1116 603 41 0 1465 0
vsize: 6024
[startup+70.0019 s]
Raw data (loadavg): 0.84 0.86 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1144 0 0 0 6994 3 0 0 25 0 1 0 481476794 6168576 1122 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1122 603 41 0 1465 0
vsize: 6024
[startup+80.0022 s]
Raw data (loadavg): 0.86 0.86 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1206 0 0 0 7994 3 0 0 25 0 1 0 481476794 6438912 1184 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1572 1184 603 41 0 1531 0
vsize: 6288
[startup+90.0031 s]
Raw data (loadavg): 0.88 0.87 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1236 0 0 0 8994 3 0 0 25 0 1 0 481476794 6574080 1214 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1605 1214 603 41 0 1564 0
vsize: 6420
[startup+100.002 s]
Raw data (loadavg): 0.90 0.87 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1272 0 0 0 9994 4 0 0 25 0 1 0 481476794 6709248 1250 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1638 1250 603 41 0 1597 0
vsize: 6552
[startup+110.002 s]
Raw data (loadavg): 0.92 0.87 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1282 0 0 0 10995 4 0 0 25 0 1 0 481476794 6844416 1260 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1671 1260 603 41 0 1630 0
vsize: 6684
[startup+120.003 s]
Raw data (loadavg): 0.93 0.88 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1337 0 0 0 11994 4 0 0 25 0 1 0 481476794 6975488 1315 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1703 1315 603 41 0 1662 0
vsize: 6812
[startup+130.003 s]
Raw data (loadavg): 0.94 0.88 0.87 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1379 0 0 0 12995 4 0 0 25 0 1 0 481476794 7245824 1357 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1769 1357 603 41 0 1728 0
vsize: 7076
[startup+140.002 s]
Raw data (loadavg): 0.95 0.88 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1397 0 0 0 13994 4 0 0 25 0 1 0 481476794 7245824 1375 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1769 1375 603 41 0 1728 0
vsize: 7076
[startup+150.003 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1414 0 0 0 14995 4 0 0 25 0 1 0 481476794 7393280 1392 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1805 1392 603 41 0 1764 0
vsize: 7220
[startup+160.002 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1428 0 0 0 15995 4 0 0 25 0 1 0 481476794 7393280 1406 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1805 1406 603 41 0 1764 0
vsize: 7220
[startup+170.002 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1438 0 0 0 16995 4 0 0 25 0 1 0 481476794 7536640 1416 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1840 1416 603 41 0 1799 0
vsize: 7360
[startup+180.002 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1446 0 0 0 17995 4 0 0 25 0 1 0 481476794 7536640 1424 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1840 1424 603 41 0 1799 0
vsize: 7360
[startup+190.001 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1511 0 0 0 18995 5 0 0 25 0 1 0 481476794 7806976 1489 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1906 1489 603 41 0 1865 0
vsize: 7624
[startup+200 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1546 0 0 0 19995 5 0 0 25 0 1 0 481476794 7942144 1524 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1524 603 41 0 1898 0
vsize: 7756
[startup+210 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1568 0 0 0 20995 5 0 0 25 0 1 0 481476794 7942144 1546 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1546 603 41 0 1898 0
vsize: 7756
[startup+220.001 s]
Raw data (loadavg): 0.98 0.91 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1577 0 0 0 21995 5 0 0 25 0 1 0 481476794 8081408 1555 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1973 1555 603 41 0 1932 0
vsize: 7892
[startup+230.001 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1585 0 0 0 22996 5 0 0 25 0 1 0 481476794 8081408 1563 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1973 1563 603 41 0 1932 0
vsize: 7892
[startup+240 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1593 0 0 0 23996 5 0 0 25 0 1 0 481476794 8081408 1571 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1973 1571 603 41 0 1932 0
vsize: 7892
[startup+250 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1602 0 0 0 24996 5 0 0 25 0 1 0 481476794 8220672 1580 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2007 1580 603 41 0 1966 0
vsize: 8028
[startup+260 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1616 0 0 0 25996 5 0 0 25 0 1 0 481476794 8220672 1594 4294967295 134512640 134672761 3221224576 3221223680 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2007 1594 603 41 0 1966 0
vsize: 8028
[startup+270.001 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1629 0 0 0 26996 5 0 0 25 0 1 0 481476794 8220672 1607 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2007 1607 603 41 0 1966 0
vsize: 8028
[startup+280 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1658 0 0 0 27996 5 0 0 25 0 1 0 481476794 8355840 1636 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2040 1636 603 41 0 1999 0
vsize: 8160
[startup+290 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1705 0 0 0 28996 5 0 0 25 0 1 0 481476794 8626176 1683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1683 603 41 0 2065 0
vsize: 8424
[startup+300.001 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1736 0 0 0 29996 5 0 0 25 0 1 0 481476794 8769536 1714 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2141 1714 603 41 0 2100 0
vsize: 8564
[startup+310 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1761 0 0 0 30996 5 0 0 25 0 1 0 481476794 8904704 1739 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2174 1739 603 41 0 2133 0
vsize: 8696
[startup+320.001 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1761 0 0 0 31996 5 0 0 25 0 1 0 481476794 8904704 1739 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2174 1739 603 41 0 2133 0
vsize: 8696
[startup+330.002 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1775 0 0 0 32996 5 0 0 25 0 1 0 481476794 8904704 1753 4294967295 134512640 134672761 3221224576 3221223424 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2174 1753 603 41 0 2133 0
vsize: 8696
[startup+340.001 s]
Raw data (loadavg): 1.06 0.95 0.90 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1775 0 0 0 33996 5 0 0 25 0 1 0 481476794 8904704 1753 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2174 1753 603 41 0 2133 0
vsize: 8696
[startup+350.001 s]
Raw data (loadavg): 1.05 0.95 0.90 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1785 0 0 0 34996 5 0 0 25 0 1 0 481476794 8904704 1763 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2174 1763 603 41 0 2133 0
vsize: 8696
[startup+360 s]
Raw data (loadavg): 1.04 0.95 0.90 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1824 0 0 0 35996 6 0 0 25 0 1 0 481476794 9175040 1802 4294967295 134512640 134672761 3221224576 3221223712 134565113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1802 603 41 0 2199 0
vsize: 8960
[startup+370.001 s]
Raw data (loadavg): 1.04 0.95 0.90 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1829 0 0 0 36997 6 0 0 25 0 1 0 481476794 9175040 1807 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1807 603 41 0 2199 0
vsize: 8960
[startup+380.001 s]
Raw data (loadavg): 1.03 0.95 0.90 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1834 0 0 0 37997 6 0 0 25 0 1 0 481476794 9175040 1812 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1812 603 41 0 2199 0
vsize: 8960
[startup+390 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1843 0 0 0 38997 6 0 0 25 0 1 0 481476794 9175040 1821 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1821 603 41 0 2199 0
vsize: 8960
[startup+399.999 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1860 0 0 0 39997 6 0 0 25 0 1 0 481476794 9306112 1838 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1838 603 41 0 2231 0
vsize: 9088
[startup+409.999 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1866 0 0 0 40997 6 0 0 25 0 1 0 481476794 9306112 1844 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1844 603 41 0 2231 0
vsize: 9088
[startup+420 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1874 0 0 0 41997 6 0 0 25 0 1 0 481476794 9306112 1852 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1852 603 41 0 2231 0
vsize: 9088
[startup+430.001 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1884 0 0 0 42997 6 0 0 25 0 1 0 481476794 9441280 1862 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+440 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1884 0 0 0 43997 6 0 0 25 0 1 0 481476794 9441280 1862 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+450 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1941 0 0 0 44997 7 0 0 25 0 1 0 481476794 9576448 1919 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2338 1919 603 41 0 2297 0
vsize: 9352
[startup+460 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1956 0 0 0 45996 7 0 0 25 0 1 0 481476794 9723904 1934 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2374 1934 603 41 0 2333 0
vsize: 9496
[startup+470 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1964 0 0 0 46996 7 0 0 25 0 1 0 481476794 9723904 1942 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2374 1942 603 41 0 2333 0
vsize: 9496
[startup+480 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1990 0 0 0 47996 7 0 0 25 0 1 0 481476794 9863168 1968 4294967295 134512640 134672761 3221224576 3221223664 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1968 603 41 0 2367 0
vsize: 9632
[startup+489.999 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 1997 0 0 0 48996 7 0 0 25 0 1 0 481476794 9863168 1975 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1975 603 41 0 2367 0
vsize: 9632
[startup+499.999 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2002 0 0 0 49997 7 0 0 25 0 1 0 481476794 9863168 1980 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1980 603 41 0 2367 0
vsize: 9632
[startup+509.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2011 0 0 0 50997 7 0 0 25 0 1 0 481476794 9863168 1989 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1989 603 41 0 2367 0
vsize: 9632
[startup+519.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2025 0 0 0 51997 7 0 0 25 0 1 0 481476794 10002432 2003 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2003 603 41 0 2401 0
vsize: 9768
[startup+529.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2037 0 0 0 52997 7 0 0 25 0 1 0 481476794 10002432 2015 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2015 603 41 0 2401 0
vsize: 9768
[startup+539.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2038 0 0 0 53997 7 0 0 25 0 1 0 481476794 10002432 2016 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2016 603 41 0 2401 0
vsize: 9768
[startup+549.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2049 0 0 0 54997 7 0 0 25 0 1 0 481476794 10137600 2027 4294967295 134512640 134672761 3221224576 3221223760 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2027 603 41 0 2434 0
vsize: 9900
[startup+559.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2053 0 0 0 55997 7 0 0 25 0 1 0 481476794 10137600 2031 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+569.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2053 0 0 0 56998 7 0 0 25 0 1 0 481476794 10137600 2031 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+579.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2067 0 0 0 57998 7 0 0 25 0 1 0 481476794 10137600 2045 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2045 603 41 0 2434 0
vsize: 9900
[startup+589.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2081 0 0 0 58998 8 0 0 25 0 1 0 481476794 10268672 2059 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2059 603 41 0 2466 0
vsize: 10028
[startup+599.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2088 0 0 0 59998 8 0 0 25 0 1 0 481476794 10268672 2066 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2066 603 41 0 2466 0
vsize: 10028
[startup+609.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2102 0 0 0 60998 8 0 0 25 0 1 0 481476794 10268672 2080 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+619.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2102 0 0 0 61998 8 0 0 25 0 1 0 481476794 10268672 2080 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+630 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2105 0 0 0 62999 8 0 0 25 0 1 0 481476794 10268672 2083 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2083 603 41 0 2466 0
vsize: 10028
[startup+639.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2111 0 0 0 63999 8 0 0 25 0 1 0 481476794 10412032 2089 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2089 603 41 0 2501 0
vsize: 10168
[startup+649.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2118 0 0 0 64999 8 0 0 25 0 1 0 481476794 10412032 2096 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2096 603 41 0 2501 0
vsize: 10168
[startup+659.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2123 0 0 0 65999 8 0 0 25 0 1 0 481476794 10412032 2101 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2101 603 41 0 2501 0
vsize: 10168
[startup+669.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2131 0 0 0 66999 8 0 0 25 0 1 0 481476794 10412032 2109 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2109 603 41 0 2501 0
vsize: 10168
[startup+679.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2137 0 0 0 67999 8 0 0 25 0 1 0 481476794 10412032 2115 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2115 603 41 0 2501 0
vsize: 10168
[startup+689.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2138 0 0 0 69000 8 0 0 25 0 1 0 481476794 10412032 2116 4294967295 134512640 134672761 3221224576 3221223760 134559599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2116 603 41 0 2501 0
vsize: 10168
[startup+699.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2141 0 0 0 70000 8 0 0 25 0 1 0 481476794 10551296 2119 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2576 2119 603 41 0 2535 0
vsize: 10304
[startup+709.998 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2189 0 0 0 70999 8 0 0 25 0 1 0 481476794 10686464 2167 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2609 2167 603 41 0 2568 0
vsize: 10436
[startup+719.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2214 0 0 0 71999 8 0 0 25 0 1 0 481476794 10821632 2192 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2192 603 41 0 2601 0
vsize: 10568
[startup+730 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2220 0 0 0 72999 8 0 0 25 0 1 0 481476794 10821632 2198 4294967295 134512640 134672761 3221224576 3221223760 134558880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2198 603 41 0 2601 0
vsize: 10568
[startup+739.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2233 0 0 0 73999 9 0 0 25 0 1 0 481476794 10821632 2211 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2211 603 41 0 2601 0
vsize: 10568
[startup+750 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 2475
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2278 0 0 0 74999 9 0 0 25 0 1 0 481476794 11091968 2256 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2256 603 41 0 2667 0
vsize: 10832
[startup+759.999 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2281 0 0 0 75999 9 0 0 25 0 1 0 481476794 11091968 2259 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2259 603 41 0 2667 0
vsize: 10832
[startup+770 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2287 0 0 0 76999 9 0 0 25 0 1 0 481476794 11091968 2265 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+780 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2287 0 0 0 77999 9 0 0 25 0 1 0 481476794 11091968 2265 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+789.999 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2287 0 0 0 79000 9 0 0 25 0 1 0 481476794 11091968 2265 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+800 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2297 0 0 0 80000 9 0 0 25 0 1 0 481476794 11227136 2275 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2275 603 41 0 2700 0
vsize: 10964
[startup+809.999 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2298 0 0 0 81000 9 0 0 25 0 1 0 481476794 11227136 2276 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2276 603 41 0 2700 0
vsize: 10964
[startup+819.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2528
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2301 0 0 0 82000 9 0 0 25 0 1 0 481476794 11227136 2279 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2279 603 41 0 2700 0
vsize: 10964
[startup+829.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2305 0 0 0 83000 9 0 0 25 0 1 0 481476794 11227136 2283 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2283 603 41 0 2700 0
vsize: 10964
[startup+839.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2312 0 0 0 84001 9 0 0 25 0 1 0 481476794 11227136 2290 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2290 603 41 0 2700 0
vsize: 10964
[startup+850 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2316 0 0 0 85001 9 0 0 25 0 1 0 481476794 11227136 2294 4294967295 134512640 134672761 3221224576 3221223744 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2294 603 41 0 2700 0
vsize: 10964
[startup+860 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2320 0 0 0 86001 9 0 0 25 0 1 0 481476794 11227136 2298 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2298 603 41 0 2700 0
vsize: 10964
[startup+870 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2324 0 0 0 87001 9 0 0 25 0 1 0 481476794 11227136 2302 4294967295 134512640 134672761 3221224576 3221223584 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+880 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2324 0 0 0 88001 9 0 0 25 0 1 0 481476794 11227136 2302 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+889.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2337 0 0 0 89001 9 0 0 25 0 1 0 481476794 11370496 2315 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2315 603 41 0 2735 0
vsize: 11104
[startup+900 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2343 0 0 0 90002 9 0 0 25 0 1 0 481476794 11370496 2321 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2321 603 41 0 2735 0
vsize: 11104
[startup+910 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2364 0 0 0 91002 9 0 0 25 0 1 0 481476794 11505664 2342 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2342 603 41 0 2768 0
vsize: 11236
[startup+920 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2365 0 0 0 92002 9 0 0 25 0 1 0 481476794 11505664 2343 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2343 603 41 0 2768 0
vsize: 11236
[startup+930.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2369 0 0 0 93002 9 0 0 25 0 1 0 481476794 11505664 2347 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+940 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2369 0 0 0 94002 9 0 0 25 0 1 0 481476794 11505664 2347 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+950 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2373 0 0 0 95003 9 0 0 25 0 1 0 481476794 11505664 2351 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2351 603 41 0 2768 0
vsize: 11236
[startup+960 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2376 0 0 0 96003 9 0 0 25 0 1 0 481476794 11505664 2354 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2354 603 41 0 2768 0
vsize: 11236
[startup+970.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2397 0 0 0 97003 9 0 0 25 0 1 0 481476794 11640832 2375 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+980.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2397 0 0 0 98003 9 0 0 25 0 1 0 481476794 11640832 2375 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+990.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2400 0 0 0 99003 9 0 0 25 0 1 0 481476794 11640832 2378 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2378 603 41 0 2801 0
vsize: 11368
[startup+1000 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2426 0 0 0 100003 9 0 0 25 0 1 0 481476794 11776000 2404 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2404 603 41 0 2834 0
vsize: 11500
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2444 0 0 0 101004 9 0 0 25 0 1 0 481476794 11776000 2422 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2422 603 41 0 2834 0
vsize: 11500
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2445 0 0 0 102004 9 0 0 25 0 1 0 481476794 11776000 2423 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2423 603 41 0 2834 0
vsize: 11500
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2449 0 0 0 103004 9 0 0 25 0 1 0 481476794 11776000 2427 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2449 0 0 0 104004 9 0 0 25 0 1 0 481476794 11776000 2427 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2450 0 0 0 105004 9 0 0 25 0 1 0 481476794 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2450 0 0 0 106004 9 0 0 25 0 1 0 481476794 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2450 0 0 0 107005 9 0 0 25 0 1 0 481476794 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2454 0 0 0 108005 9 0 0 25 0 1 0 481476794 11776000 2432 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2432 603 41 0 2834 0
vsize: 11500
[startup+1090 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2461 0 0 0 109005 9 0 0 25 0 1 0 481476794 11915264 2439 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2439 603 41 0 2868 0
vsize: 11636
[startup+1100 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2530
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2465 0 0 0 110005 9 0 0 25 0 1 0 481476794 11915264 2443 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2443 603 41 0 2868 0
vsize: 11636
[startup+1110 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2475 0 0 0 111005 9 0 0 25 0 1 0 481476794 11915264 2453 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2453 603 41 0 2868 0
vsize: 11636
[startup+1120 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2497 0 0 0 112005 9 0 0 25 0 1 0 481476794 12050432 2475 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2475 603 41 0 2901 0
vsize: 11768
[startup+1130 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2506 0 0 0 113005 9 0 0 25 0 1 0 481476794 12050432 2484 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2484 603 41 0 2901 0
vsize: 11768
[startup+1140 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2512 0 0 0 114005 9 0 0 25 0 1 0 481476794 12050432 2490 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2490 603 41 0 2901 0
vsize: 11768
[startup+1150 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2518 0 0 0 115006 9 0 0 25 0 1 0 481476794 12050432 2496 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2496 603 41 0 2901 0
vsize: 11768
[startup+1160 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2519 0 0 0 116006 10 0 0 25 0 1 0 481476794 12050432 2497 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
[startup+1170 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2519 0 0 0 117006 10 0 0 25 0 1 0 481476794 12050432 2497 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2527 0 0 0 118006 10 0 0 25 0 1 0 481476794 12189696 2505 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2976 2505 603 41 0 2935 0
vsize: 11904
[startup+1190 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2536 0 0 0 119006 10 0 0 25 0 1 0 481476794 12189696 2514 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2976 2514 603 41 0 2935 0
vsize: 11904
[startup+1200 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2532
Raw data (stat): 2475 (minisat+) R 2474 28099 28098 0 -1 0 2544 0 0 0 120006 10 0 0 25 0 1 0 481476794 12189696 2522 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2522 603 41 0 2935 0
vsize: 11904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2532
Raw data (stat): 2475 (minisat+) Z 2474 28099 28098 0 -1 12 2546 0 0 0 120006 10 0 0 25 0 1 0 481476794 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.01
CPU time (s): 1200.18
CPU user time (s): 1200.07
CPU system time (s): 0.106983
CPU usage (%): 100.014
Max. virtual memory (Kb): 11904
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####