Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_16_pb.cnf.cr.opb
MD5SUM3f8902c4e8af50006f671e2bddb3e9aa
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 17
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.013997
Number of variables480
Total number of constraints62
Number of constraints which are clauses32
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint16

Trace number 6083 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893864 kB
Buffers:         35500 kB
Cached:          84652 kB
SwapCached:          4 kB
Active:          58008 kB
Inactive:        64984 kB
HighTotal:      131008 kB
HighFree:        42588 kB
LowTotal:       903652 kB
LowFree:        851276 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12200 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:40:58 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4517 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 62 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................
c ---[  29]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  27]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  25]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  19]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  17]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  15]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   29
c ---[  12]---> BDD-cost:   29
c ---[  11]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   8]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   6]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   4]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost:   29
c ---[   1]---> BDD-cost:   29
c ---[   0]---> BDD-cost:   29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3812    10920 |    1270       0        0     nan |  0.000 % |
c |       104 |    3812    10920 |    1397     104     5751    55.3 |  2.222 % |
c |       254 |    3767    10785 |    1536     225    13712    60.9 |  2.889 % |
c |       479 |    3752    10740 |    1690     441    34253    77.7 |  3.111 % |
c |       816 |    3742    10710 |    1859     774    59164    76.4 |  3.259 % |
c |      1322 |    3727    10665 |    2045    1274   101292    79.5 |  3.482 % |
c |      2082 |    3717    10635 |    2249    2028   179745    88.6 |  3.630 % |
c |      3221 |    3692    10560 |    2474    1829   170632    93.3 |  4.000 % |
c |      4931 |    3682    10530 |    2722    2190   237517   108.5 |  4.148 % |
c |      7493 |    3657    10455 |    2994    1776   202464   114.0 |  4.519 % |
c |     11337 |    3652    10440 |    3294    2184   248774   113.9 |  4.593 % |
c |     17106 |    3622    10350 |    3623    2452   272522   111.1 |  5.037 % |
c |     25755 |    3572    10200 |    3985    3052   345591   113.2 |  5.778 % |
c |     38730 |    3467     9885 |    4384    2932   272102    92.8 |  7.333 % |
c |     58191 |    3323     9455 |    4822    3250   335612   103.3 |  9.482 % |
c |     87384 |    3078     8720 |    5305    3861   333434    86.4 | 13.111 % |
c |    131173 |    2662     7480 |    5835    4082   414316   101.5 | 19.333 % |
c |    196857 |    2465     6895 |    6419    5973   616395   103.2 | 22.296 % |
c |    295385 |    2257     6275 |    7061    6199   614660    99.2 | 25.407 % |
c |    443174 |    1951     5365 |    7767    7248   676251    93.3 | 30.000 % |
c |    664857 |    1931     5305 |    8543    6162   519332    84.3 | 30.296 % |
c |    997383 |    1754     4800 |    9398    7206   513867    71.3 | 33.111 % |
#### 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.92 0.98 0.92 2/54 26245
Raw data (stat): 26245 (runsolver) R 26244 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423087806 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 973 0 0 0 996 2 0 0 25 0 1 0 423087806 5496832 951 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1342 951 603 41 0 1301 0
vsize: 5368
[startup+20.0029 s]
Raw data (loadavg): 0.94 0.98 0.92 5/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1056 0 0 0 1996 3 0 0 25 0 1 0 423087806 5902336 1034 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1441 1034 603 41 0 1400 0
vsize: 5764
[startup+30.0036 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1159 0 0 0 2996 3 0 0 25 0 1 0 423087806 6303744 1137 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1539 1137 603 41 0 1498 0
vsize: 6156
[startup+40.0037 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1229 0 0 0 3995 4 0 0 25 0 1 0 423087806 6574080 1207 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1605 1207 603 41 0 1564 0
vsize: 6420
[startup+50.004 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1292 0 0 0 4994 4 0 0 25 0 1 0 423087806 6844416 1270 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1671 1270 603 41 0 1630 0
vsize: 6684
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1376 0 0 0 5994 4 0 0 25 0 1 0 423087806 7114752 1354 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1737 1354 603 41 0 1696 0
vsize: 6948
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1398 0 0 0 6994 4 0 0 25 0 1 0 423087806 7254016 1376 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1771 1376 603 41 0 1730 0
vsize: 7084
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1428 0 0 0 7993 5 0 0 25 0 1 0 423087806 7393280 1406 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1406 603 41 0 1764 0
vsize: 7220
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1467 0 0 0 8993 5 0 0 25 0 1 0 423087806 7532544 1445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1445 603 41 0 1798 0
vsize: 7356
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1513 0 0 0 9992 6 0 0 25 0 1 0 423087806 7827456 1491 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1911 1491 603 41 0 1870 0
vsize: 7644
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1582 0 0 0 10993 6 0 0 25 0 1 0 423087806 8093696 1560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1976 1560 603 41 0 1935 0
vsize: 7904
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1598 0 0 0 11992 6 0 0 25 0 1 0 423087806 8241152 1576 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2012 1576 603 41 0 1971 0
vsize: 8048
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1649 0 0 0 12993 6 0 0 25 0 1 0 423087806 8376320 1627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2045 1627 603 41 0 2004 0
vsize: 8180
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1721 0 0 0 13993 6 0 0 25 0 1 0 423087806 8646656 1699 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1699 603 41 0 2070 0
vsize: 8444
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1732 0 0 0 14993 6 0 0 25 0 1 0 423087806 8785920 1710 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1710 603 41 0 2104 0
vsize: 8580
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1769 0 0 0 15993 6 0 0 25 0 1 0 423087806 8921088 1747 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1747 603 41 0 2137 0
vsize: 8712
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1792 0 0 0 16993 6 0 0 25 0 1 0 423087806 9056256 1770 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2211 1770 603 41 0 2170 0
vsize: 8844
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1813 0 0 0 17993 6 0 0 25 0 1 0 423087806 9056256 1791 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2211 1791 603 41 0 2170 0
vsize: 8844
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1865 0 0 0 18993 6 0 0 25 0 1 0 423087806 9326592 1843 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2277 1843 603 41 0 2236 0
vsize: 9108
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1878 0 0 0 19993 6 0 0 25 0 1 0 423087806 9461760 1856 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2310 1856 603 41 0 2269 0
vsize: 9240
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1907 0 0 0 20993 6 0 0 25 0 1 0 423087806 9625600 1885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2350 1885 603 41 0 2309 0
vsize: 9400
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1931 0 0 0 21994 6 0 0 25 0 1 0 423087806 9625600 1909 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2350 1909 603 41 0 2309 0
vsize: 9400
[startup+230.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1936 0 0 0 22994 6 0 0 25 0 1 0 423087806 9773056 1914 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2386 1914 603 41 0 2345 0
vsize: 9544
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2004 0 0 0 23994 6 0 0 25 0 1 0 423087806 10051584 1982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2454 1982 603 41 0 2413 0
vsize: 9816
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2021 0 0 0 24994 6 0 0 25 0 1 0 423087806 10051584 1999 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2454 1999 603 41 0 2413 0
vsize: 9816
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2047 0 0 0 25994 7 0 0 25 0 1 0 423087806 10199040 2025 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2490 2025 603 41 0 2449 0
vsize: 9960
[startup+270.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2096 0 0 0 26994 7 0 0 25 0 1 0 423087806 10346496 2074 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2526 2074 603 41 0 2485 0
vsize: 10104
[startup+280.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2106 0 0 0 27994 7 0 0 25 0 1 0 423087806 10493952 2084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2084 603 41 0 2521 0
vsize: 10248
[startup+290.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2114 0 0 0 28994 7 0 0 25 0 1 0 423087806 10493952 2092 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2092 603 41 0 2521 0
vsize: 10248
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2117 0 0 0 29994 7 0 0 25 0 1 0 423087806 10493952 2095 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2095 603 41 0 2521 0
vsize: 10248
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2118 0 0 0 30995 7 0 0 25 0 1 0 423087806 10493952 2096 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2096 603 41 0 2521 0
vsize: 10248
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2128 0 0 0 31995 7 0 0 25 0 1 0 423087806 10493952 2106 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2106 603 41 0 2521 0
vsize: 10248
[startup+330.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2136 0 0 0 32995 7 0 0 25 0 1 0 423087806 10493952 2114 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2114 603 41 0 2521 0
vsize: 10248
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2142 0 0 0 33995 7 0 0 25 0 1 0 423087806 10657792 2120 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2120 603 41 0 2561 0
vsize: 10408
[startup+350.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2195 0 0 0 34994 7 0 0 25 0 1 0 423087806 10792960 2173 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2635 2173 603 41 0 2594 0
vsize: 10540
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2250 0 0 0 35993 7 0 0 25 0 1 0 423087806 11063296 2228 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2701 2228 603 41 0 2660 0
vsize: 10804
[startup+370.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2251 0 0 0 36994 7 0 0 25 0 1 0 423087806 11063296 2229 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2701 2229 603 41 0 2660 0
vsize: 10804
[startup+380.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2271 0 0 0 37994 7 0 0 25 0 1 0 423087806 11206656 2249 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2736 2249 603 41 0 2695 0
vsize: 10944
[startup+390.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2272 0 0 0 38994 7 0 0 25 0 1 0 423087806 11206656 2250 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2736 2250 603 41 0 2695 0
vsize: 10944
[startup+400.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2338 0 0 0 39994 7 0 0 25 0 1 0 423087806 11341824 2316 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2316 603 41 0 2728 0
vsize: 11076
[startup+410.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2339 0 0 0 40994 7 0 0 25 0 1 0 423087806 11341824 2317 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2317 603 41 0 2728 0
vsize: 11076
[startup+420.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2346 0 0 0 41994 8 0 0 25 0 1 0 423087806 11501568 2324 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2324 603 41 0 2767 0
vsize: 11232
[startup+430.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2351 0 0 0 42994 8 0 0 25 0 1 0 423087806 11501568 2329 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2329 603 41 0 2767 0
vsize: 11232
[startup+440.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2361 0 0 0 43995 8 0 0 25 0 1 0 423087806 11501568 2339 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2339 603 41 0 2767 0
vsize: 11232
[startup+450.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 44995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2345 603 41 0 2767 0
vsize: 11232
[startup+460.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 45995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2345 603 41 0 2767 0
vsize: 11232
[startup+470.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 46995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2345 603 41 0 2767 0
vsize: 11232
[startup+480.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2372 0 0 0 47995 8 0 0 25 0 1 0 423087806 11665408 2350 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2848 2350 603 41 0 2807 0
vsize: 11392
[startup+490.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2373 0 0 0 48995 8 0 0 25 0 1 0 423087806 11665408 2351 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2848 2351 603 41 0 2807 0
vsize: 11392
[startup+500.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2374 0 0 0 49995 8 0 0 25 0 1 0 423087806 11665408 2352 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2848 2352 603 41 0 2807 0
vsize: 11392
[startup+510.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2379 0 0 0 50996 8 0 0 25 0 1 0 423087806 11665408 2357 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2848 2357 603 41 0 2807 0
vsize: 11392
[startup+520.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2424 0 0 0 51995 8 0 0 25 0 1 0 423087806 11800576 2402 4294967295 134512640 134672761 3221224544 3221223776 134541847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2881 2402 603 41 0 2840 0
vsize: 11524
[startup+530.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2427 0 0 0 52995 8 0 0 25 0 1 0 423087806 11800576 2405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2881 2405 603 41 0 2840 0
vsize: 11524
[startup+540.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2432 0 0 0 53995 8 0 0 25 0 1 0 423087806 11964416 2410 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2921 2410 603 41 0 2880 0
vsize: 11684
[startup+550.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2445 0 0 0 54996 8 0 0 25 0 1 0 423087806 11964416 2423 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2921 2423 603 41 0 2880 0
vsize: 11684
[startup+560.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2445 0 0 0 55996 8 0 0 25 0 1 0 423087806 11964416 2423 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2921 2423 603 41 0 2880 0
vsize: 11684
[startup+570.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2464 0 0 0 56996 8 0 0 25 0 1 0 423087806 12099584 2442 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2954 2442 603 41 0 2913 0
vsize: 11816
[startup+580.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2558 0 0 0 57996 8 0 0 25 0 1 0 423087806 12541952 2536 4294967295 134512640 134672761 3221224544 3221223680 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3062 2536 603 41 0 3021 0
vsize: 12248
[startup+590.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2631 0 0 0 58995 9 0 0 25 0 1 0 423087806 12836864 2609 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2609 603 41 0 3093 0
vsize: 12536
[startup+600.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2653 0 0 0 59996 9 0 0 25 0 1 0 423087806 12980224 2631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3169 2631 603 41 0 3128 0
vsize: 12676
[startup+610.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2691 0 0 0 60996 9 0 0 25 0 1 0 423087806 13127680 2669 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3205 2669 603 41 0 3164 0
vsize: 12820
[startup+620.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2719 0 0 0 61996 9 0 0 25 0 1 0 423087806 13262848 2697 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3238 2697 603 41 0 3197 0
vsize: 12952
[startup+630.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2751 0 0 0 62996 9 0 0 25 0 1 0 423087806 13426688 2729 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3278 2729 603 41 0 3237 0
vsize: 13112
[startup+640.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2763 0 0 0 63996 9 0 0 25 0 1 0 423087806 13590528 2741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3318 2741 603 41 0 3277 0
vsize: 13272
[startup+650.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2764 0 0 0 64997 9 0 0 25 0 1 0 423087806 13590528 2742 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3318 2742 603 41 0 3277 0
vsize: 13272
[startup+660.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2788 0 0 0 65997 9 0 0 25 0 1 0 423087806 13590528 2766 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3318 2766 603 41 0 3277 0
vsize: 13272
[startup+670.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2810 0 0 0 66997 9 0 0 25 0 1 0 423087806 13754368 2788 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3358 2788 603 41 0 3317 0
vsize: 13432
[startup+680.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2815 0 0 0 67997 9 0 0 25 0 1 0 423087806 13754368 2793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3358 2793 603 41 0 3317 0
vsize: 13432
[startup+690.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2818 0 0 0 68997 9 0 0 25 0 1 0 423087806 13754368 2796 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3358 2796 603 41 0 3317 0
vsize: 13432
[startup+700.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2840 0 0 0 69997 9 0 0 25 0 1 0 423087806 13918208 2818 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3398 2818 603 41 0 3357 0
vsize: 13592
[startup+710.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2840 0 0 0 70997 9 0 0 25 0 1 0 423087806 13918208 2818 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3398 2818 603 41 0 3357 0
vsize: 13592
[startup+720.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3175 0 0 0 71996 10 0 0 25 0 1 0 423087806 15405056 3153 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3153 603 41 0 3720 0
vsize: 15044
[startup+730.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3217 0 0 0 72996 10 0 0 25 0 1 0 423087806 15540224 3195 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3794 3195 603 41 0 3753 0
vsize: 15176
[startup+740.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3282 0 0 0 73996 10 0 0 25 0 1 0 423087806 15843328 3260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3868 3260 603 41 0 3827 0
vsize: 15472
[startup+750.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3310 0 0 0 74996 10 0 0 25 0 1 0 423087806 15986688 3288 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3288 603 41 0 3862 0
vsize: 15612
[startup+760.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3317 0 0 0 75997 10 0 0 25 0 1 0 423087806 15986688 3295 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3295 603 41 0 3862 0
vsize: 15612
[startup+770.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3357 0 0 0 76997 11 0 0 25 0 1 0 423087806 16257024 3335 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3969 3335 603 41 0 3928 0
vsize: 15876
[startup+780.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3383 0 0 0 77997 11 0 0 25 0 1 0 423087806 16257024 3361 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3969 3361 603 41 0 3928 0
vsize: 15876
[startup+790.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3383 0 0 0 78997 11 0 0 25 0 1 0 423087806 16257024 3361 4294967295 134512640 134672761 3221224544 3221223648 134554647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3969 3361 603 41 0 3928 0
vsize: 15876
[startup+800.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3432 0 0 0 79997 11 0 0 25 0 1 0 423087806 16547840 3410 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4040 3410 603 41 0 3999 0
vsize: 16160
[startup+810.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3444 0 0 0 80997 11 0 0 25 0 1 0 423087806 16547840 3422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4040 3422 603 41 0 3999 0
vsize: 16160
[startup+820.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3445 0 0 0 81997 11 0 0 25 0 1 0 423087806 16547840 3423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4040 3423 603 41 0 3999 0
vsize: 16160
[startup+830.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3463 0 0 0 82998 11 0 0 25 0 1 0 423087806 16711680 3441 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4080 3441 603 41 0 4039 0
vsize: 16320
[startup+840.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3474 0 0 0 83998 11 0 0 25 0 1 0 423087806 16711680 3452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4080 3452 603 41 0 4039 0
vsize: 16320
[startup+850.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3493 0 0 0 84998 11 0 0 25 0 1 0 423087806 16875520 3471 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4120 3471 603 41 0 4079 0
vsize: 16480
[startup+860.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3507 0 0 0 85998 11 0 0 25 0 1 0 423087806 16875520 3485 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4120 3485 603 41 0 4079 0
vsize: 16480
[startup+870.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3523 0 0 0 86998 11 0 0 25 0 1 0 423087806 17010688 3501 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3501 603 41 0 4112 0
vsize: 16612
[startup+880.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3526 0 0 0 87998 11 0 0 25 0 1 0 423087806 17010688 3504 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3504 603 41 0 4112 0
vsize: 16612
[startup+890.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3532 0 0 0 88999 11 0 0 25 0 1 0 423087806 17010688 3510 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3510 603 41 0 4112 0
vsize: 16612
[startup+900.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3541 0 0 0 89999 11 0 0 25 0 1 0 423087806 17010688 3519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3519 603 41 0 4112 0
vsize: 16612
[startup+910.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3541 0 0 0 90999 11 0 0 25 0 1 0 423087806 17010688 3519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3519 603 41 0 4112 0
vsize: 16612
[startup+920.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3549 0 0 0 91999 11 0 0 25 0 1 0 423087806 17010688 3527 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3527 603 41 0 4112 0
vsize: 16612
[startup+930.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3570 0 0 0 92999 11 0 0 25 0 1 0 423087806 17158144 3548 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4189 3548 603 41 0 4148 0
vsize: 16756
[startup+940.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3571 0 0 0 94000 11 0 0 25 0 1 0 423087806 17158144 3549 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4189 3549 603 41 0 4148 0
vsize: 16756
[startup+950.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3571 0 0 0 95000 11 0 0 25 0 1 0 423087806 17158144 3549 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4189 3549 603 41 0 4148 0
vsize: 16756
[startup+960.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3573 0 0 0 96000 11 0 0 25 0 1 0 423087806 17158144 3551 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4189 3551 603 41 0 4148 0
vsize: 16756
[startup+970.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3590 0 0 0 97000 11 0 0 25 0 1 0 423087806 17321984 3568 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4229 3568 603 41 0 4188 0
vsize: 16916
[startup+980.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3602 0 0 0 98000 11 0 0 25 0 1 0 423087806 17321984 3580 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4229 3580 603 41 0 4188 0
vsize: 16916
[startup+990.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3618 0 0 0 99001 11 0 0 25 0 1 0 423087806 17469440 3596 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3596 603 41 0 4224 0
vsize: 17060
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3624 0 0 0 100001 11 0 0 25 0 1 0 423087806 17469440 3602 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3602 603 41 0 4224 0
vsize: 17060
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3648 0 0 0 101001 11 0 0 25 0 1 0 423087806 17633280 3626 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4305 3626 603 41 0 4264 0
vsize: 17220
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3651 0 0 0 102001 11 0 0 25 0 1 0 423087806 17633280 3629 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4305 3629 603 41 0 4264 0
vsize: 17220
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3657 0 0 0 103001 11 0 0 25 0 1 0 423087806 17633280 3635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4305 3635 603 41 0 4264 0
vsize: 17220
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3668 0 0 0 104001 11 0 0 25 0 1 0 423087806 17633280 3646 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4305 3646 603 41 0 4264 0
vsize: 17220
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3668 0 0 0 105002 11 0 0 25 0 1 0 423087806 17633280 3646 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4305 3646 603 41 0 4264 0
vsize: 17220
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3680 0 0 0 106002 11 0 0 25 0 1 0 423087806 17797120 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3658 603 41 0 4304 0
vsize: 17380
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3680 0 0 0 107002 11 0 0 25 0 1 0 423087806 17797120 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3658 603 41 0 4304 0
vsize: 17380
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3690 0 0 0 108002 11 0 0 25 0 1 0 423087806 17797120 3668 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3668 603 41 0 4304 0
vsize: 17380
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3692 0 0 0 109002 11 0 0 25 0 1 0 423087806 17797120 3670 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3670 603 41 0 4304 0
vsize: 17380
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3692 0 0 0 110003 11 0 0 25 0 1 0 423087806 17797120 3670 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3670 603 41 0 4304 0
vsize: 17380
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3700 0 0 0 111002 11 0 0 25 0 1 0 423087806 17797120 3678 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4345 3678 603 41 0 4304 0
vsize: 17380
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3783 0 0 0 112002 11 0 0 25 0 1 0 423087806 18194432 3761 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4442 3761 603 41 0 4401 0
vsize: 17768
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3788 0 0 0 113003 11 0 0 25 0 1 0 423087806 18194432 3766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4442 3766 603 41 0 4401 0
vsize: 17768
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3789 0 0 0 114003 11 0 0 25 0 1 0 423087806 18194432 3767 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4442 3767 603 41 0 4401 0
vsize: 17768
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3801 0 0 0 115003 11 0 0 25 0 1 0 423087806 18345984 3779 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4479 3779 603 41 0 4438 0
vsize: 17916
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 116003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3810 603 41 0 4474 0
vsize: 18060
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 117003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3810 603 41 0 4474 0
vsize: 18060
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 118003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3810 603 41 0 4474 0
vsize: 18060
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3842 0 0 0 119003 12 0 0 25 0 1 0 423087806 18493440 3820 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4515 3820 603 41 0 4474 0
vsize: 18060
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26245
Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3859 0 0 0 120004 12 0 0 25 0 1 0 423087806 18657280 3837 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4555 3837 603 41 0 4514 0
vsize: 18220
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 26245
Raw data (stat): 26245 (minisat+) Z 26244 20937 20936 0 -1 12 3861 0 0 0 120004 13 0 0 25 0 1 0 423087806 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.02
CPU time (s): 1200.17
CPU user time (s): 1200.04
CPU system time (s): 0.13098
CPU usage (%): 100.012
Max. virtual memory (Kb): 18220
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####