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_20_pb.cnf.cr.opb
MD5SUMce39bf71367df072c91f9b7587480c93
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 21
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.017996
Number of variables600
Total number of constraints70
Number of constraints which are clauses40
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 constraint20

Trace number 4742 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 20:09:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=50 boxname=wulflinc2 idbench=6 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ce39bf71367df072c91f9b7587480c93  /oldhome/oroussel/tmp/wulflinc2/normalized-chnl15_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-chnl15_20_pb.cnf.cr.opb
IDLAUNCH: 50
/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:        912992 kB
Buffers:         33144 kB
Cached:          68308 kB
SwapCached:          4 kB
Active:          52656 kB
Inactive:        51624 kB
HighTotal:      131008 kB
HighFree:        58940 kB
LowTotal:       903652 kB
LowFree:        854052 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11832 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:29:22 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 50 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 70 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2770     7710 |     923       0        0     nan |  0.000 % |
c |       100 |    2770     7710 |    1015     100     4995    50.0 |  1.754 % |
c |       250 |    2770     7710 |    1116     250    15405    61.6 |  1.754 % |
c |       475 |    2770     7710 |    1228     475    29678    62.5 |  1.754 % |
c |       813 |    2770     7710 |    1351     813    60708    74.7 |  1.754 % |
c |      1321 |    2770     7710 |    1486    1321    96881    73.3 |  1.754 % |
c |      2081 |    2770     7710 |    1635    1212    77160    63.7 |  1.754 % |
c |      3220 |    2770     7710 |    1798    1329    97111    73.1 |  1.754 % |
c |      4931 |    2770     7710 |    1978    1906   183476    96.3 |  1.754 % |
c |      7493 |    2770     7710 |    2176    2046   198314    96.9 |  1.754 % |
c |     11338 |    2770     7710 |    2394    2183   218158    99.9 |  1.754 % |
c |     17104 |    2770     7710 |    2633    2466   275809   111.8 |  1.754 % |
c |     25754 |    2770     7710 |    2896    1984   192143    96.8 |  1.754 % |
c |     38728 |    2770     7710 |    3186    1896   207649   109.5 |  1.754 % |
c |     58192 |    2770     7710 |    3505    1948   255353   131.1 |  1.754 % |
c |     87385 |    2770     7710 |    3855    2206   267107   121.1 |  1.754 % |
c |    131175 |    2770     7710 |    4241    4025   528667   131.3 |  1.754 % |
c |    196859 |    2770     7710 |    4665    3236   437395   135.2 |  1.754 % |
c |    295385 |    2770     7710 |    5131    4002   477975   119.4 |  1.754 % |
c |    443174 |    2770     7710 |    5644    3155   376760   119.4 |  1.754 % |
c |    664858 |    2770     7710 |    6209    3354   390492   116.4 |  1.754 % |
c |    997385 |    2770     7710 |    6830    5823   703796   120.9 |  1.754 % |
c |   1496173 |    2770     7710 |    7513    4813   546647   113.6 |  1.754 % |
#### 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.85 0.95 0.87 2/54 22499
Raw data (stat): 22499 (runsolver) R 22498 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420497910 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.87 0.95 0.87 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 891 0 0 0 996 2 0 0 25 0 1 0 420497910 5255168 869 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1283 869 603 41 0 1242 0
vsize: 5132
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.96 0.87 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1054 0 0 0 1994 2 0 0 25 0 1 0 420497910 5795840 1032 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1415 1032 603 41 0 1374 0
vsize: 5660
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1205 0 0 0 2993 3 0 0 25 0 1 0 420497910 6467584 1183 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1579 1183 603 41 0 1538 0
vsize: 6316
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1273 0 0 0 3992 4 0 0 25 0 1 0 420497910 6742016 1251 4294967295 134512640 134672761 3221224624 3221223808 134559390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1646 1251 603 41 0 1605 0
vsize: 6584
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1273 0 0 0 4993 4 0 0 25 0 1 0 420497910 6742016 1251 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1646 1251 603 41 0 1605 0
vsize: 6584
[startup+60.002 s]
Raw data (loadavg): 0.94 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1362 0 0 0 5992 4 0 0 25 0 1 0 420497910 7159808 1340 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1748 1340 603 41 0 1707 0
vsize: 6992
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1388 0 0 0 6992 4 0 0 25 0 1 0 420497910 7294976 1366 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1781 1366 603 41 0 1740 0
vsize: 7124
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1398 0 0 0 7992 4 0 0 25 0 1 0 420497910 7294976 1376 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1781 1376 603 41 0 1740 0
vsize: 7124
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1492 0 0 0 8992 5 0 0 25 0 1 0 420497910 7700480 1470 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1880 1470 603 41 0 1839 0
vsize: 7520
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1580 0 0 0 9991 5 0 0 25 0 1 0 420497910 7970816 1558 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1946 1558 603 41 0 1905 0
vsize: 7784
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1580 0 0 0 10992 5 0 0 25 0 1 0 420497910 7970816 1558 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1946 1558 603 41 0 1905 0
vsize: 7784
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.88 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1605 0 0 0 11992 5 0 0 25 0 1 0 420497910 8105984 1583 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1979 1583 603 41 0 1938 0
vsize: 7916
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1616 0 0 0 12992 5 0 0 25 0 1 0 420497910 8241152 1594 4294967295 134512640 134672761 3221224624 3221223728 134559821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2012 1594 603 41 0 1971 0
vsize: 8048
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1619 0 0 0 13992 5 0 0 25 0 1 0 420497910 8241152 1597 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2012 1597 603 41 0 1971 0
vsize: 8048
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1646 0 0 0 14992 5 0 0 25 0 1 0 420497910 8376320 1624 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2045 1624 603 41 0 2004 0
vsize: 8180
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1678 0 0 0 15992 5 0 0 25 0 1 0 420497910 8515584 1656 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2079 1656 603 41 0 2038 0
vsize: 8316
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1748 0 0 0 16992 5 0 0 25 0 1 0 420497910 8785920 1726 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1726 603 41 0 2104 0
vsize: 8580
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1772 0 0 0 17993 5 0 0 25 0 1 0 420497910 8929280 1750 4294967295 134512640 134672761 3221224624 3221223800 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2180 1750 603 41 0 2139 0
vsize: 8720
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1778 0 0 0 18993 5 0 0 25 0 1 0 420497910 8929280 1756 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2180 1756 603 41 0 2139 0
vsize: 8720
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1811 0 0 0 19993 5 0 0 25 0 1 0 420497910 9039872 1789 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2207 1789 603 41 0 2166 0
vsize: 8828
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1831 0 0 0 20993 5 0 0 25 0 1 0 420497910 9179136 1809 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1809 603 41 0 2200 0
vsize: 8964
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1873 0 0 0 21993 6 0 0 25 0 1 0 420497910 9326592 1851 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2277 1851 603 41 0 2236 0
vsize: 9108
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1874 0 0 0 22993 6 0 0 25 0 1 0 420497910 9326592 1852 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2277 1852 603 41 0 2236 0
vsize: 9108
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1930 0 0 0 23993 6 0 0 25 0 1 0 420497910 9601024 1908 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2344 1908 603 41 0 2303 0
vsize: 9376
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1934 0 0 0 24993 6 0 0 25 0 1 0 420497910 9601024 1912 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2344 1912 603 41 0 2303 0
vsize: 9376
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 1981 0 0 0 25993 6 0 0 25 0 1 0 420497910 9736192 1959 4294967295 134512640 134672761 3221224624 3221223808 134559482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2377 1959 603 41 0 2336 0
vsize: 9508
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2016 0 0 0 26993 6 0 0 25 0 1 0 420497910 9871360 1994 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2410 1994 603 41 0 2369 0
vsize: 9640
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2016 0 0 0 27994 6 0 0 25 0 1 0 420497910 9871360 1994 4294967295 134512640 134672761 3221224624 3221223776 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2410 1994 603 41 0 2369 0
vsize: 9640
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2036 0 0 0 28994 6 0 0 25 0 1 0 420497910 10006528 2014 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2443 2014 603 41 0 2402 0
vsize: 9772
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2085 0 0 0 29994 6 0 0 25 0 1 0 420497910 10272768 2063 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2508 2063 603 41 0 2467 0
vsize: 10032
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2095 0 0 0 30994 6 0 0 25 0 1 0 420497910 10272768 2073 4294967295 134512640 134672761 3221224624 3221223728 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2508 2073 603 41 0 2467 0
vsize: 10032
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2103 0 0 0 31994 6 0 0 25 0 1 0 420497910 10272768 2081 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2508 2081 603 41 0 2467 0
vsize: 10032
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2112 0 0 0 32994 6 0 0 25 0 1 0 420497910 10420224 2090 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2544 2090 603 41 0 2503 0
vsize: 10176
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2185 0 0 0 33994 6 0 0 25 0 1 0 420497910 10702848 2163 4294967295 134512640 134672761 3221224624 3221223728 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2613 2163 603 41 0 2572 0
vsize: 10452
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2186 0 0 0 34994 6 0 0 25 0 1 0 420497910 10702848 2164 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2613 2164 603 41 0 2572 0
vsize: 10452
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2194 0 0 0 35995 6 0 0 25 0 1 0 420497910 10702848 2172 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2613 2172 603 41 0 2572 0
vsize: 10452
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2233 0 0 0 36995 6 0 0 25 0 1 0 420497910 10838016 2211 4294967295 134512640 134672761 3221224624 3221223808 134559596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2646 2211 603 41 0 2605 0
vsize: 10584
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2237 0 0 0 37995 6 0 0 25 0 1 0 420497910 10838016 2215 4294967295 134512640 134672761 3221224624 3221223788 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2646 2215 603 41 0 2605 0
vsize: 10584
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2237 0 0 0 38995 6 0 0 25 0 1 0 420497910 10838016 2215 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2646 2215 603 41 0 2605 0
vsize: 10584
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2362 0 0 0 39995 7 0 0 25 0 1 0 420497910 11390976 2340 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2362 0 0 0 40995 7 0 0 25 0 1 0 420497910 11390976 2340 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2362 0 0 0 41995 7 0 0 25 0 1 0 420497910 11390976 2340 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2363 0 0 0 42995 7 0 0 25 0 1 0 420497910 11390976 2341 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2341 603 41 0 2740 0
vsize: 11124
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2363 0 0 0 43996 7 0 0 25 0 1 0 420497910 11390976 2341 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2341 603 41 0 2740 0
vsize: 11124
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2364 0 0 0 44996 7 0 0 25 0 1 0 420497910 11390976 2342 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2781 2342 603 41 0 2740 0
vsize: 11124
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2392 0 0 0 45996 7 0 0 25 0 1 0 420497910 11542528 2370 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2370 603 41 0 2777 0
vsize: 11272
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2397 0 0 0 46996 7 0 0 25 0 1 0 420497910 11542528 2375 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2375 603 41 0 2777 0
vsize: 11272
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2397 0 0 0 47996 7 0 0 25 0 1 0 420497910 11542528 2375 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2375 603 41 0 2777 0
vsize: 11272
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2397 0 0 0 48996 7 0 0 25 0 1 0 420497910 11542528 2375 4294967295 134512640 134672761 3221224624 3221223728 134555205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2375 603 41 0 2777 0
vsize: 11272
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2400 0 0 0 49997 7 0 0 25 0 1 0 420497910 11542528 2378 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2378 603 41 0 2777 0
vsize: 11272
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2401 0 0 0 50996 7 0 0 25 0 1 0 420497910 11542528 2379 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2379 603 41 0 2777 0
vsize: 11272
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2422 0 0 0 51996 7 0 0 25 0 1 0 420497910 11689984 2400 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2854 2400 603 41 0 2813 0
vsize: 11416
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2426 0 0 0 52996 7 0 0 25 0 1 0 420497910 11689984 2404 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2854 2404 603 41 0 2813 0
vsize: 11416
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2445 0 0 0 53996 7 0 0 25 0 1 0 420497910 11821056 2423 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2886 2423 603 41 0 2845 0
vsize: 11544
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2458 0 0 0 54997 7 0 0 25 0 1 0 420497910 11821056 2436 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2886 2436 603 41 0 2845 0
vsize: 11544
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2477 0 0 0 55997 7 0 0 25 0 1 0 420497910 11956224 2455 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2919 2455 603 41 0 2878 0
vsize: 11676
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2479 0 0 0 56997 7 0 0 25 0 1 0 420497910 11956224 2457 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2919 2457 603 41 0 2878 0
vsize: 11676
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2509 0 0 0 57997 7 0 0 25 0 1 0 420497910 12091392 2487 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2952 2487 603 41 0 2911 0
vsize: 11808
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2526 0 0 0 58997 7 0 0 25 0 1 0 420497910 12091392 2504 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2952 2504 603 41 0 2911 0
vsize: 11808
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2625 0 0 0 59997 8 0 0 25 0 1 0 420497910 12496896 2603 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3051 2603 603 41 0 3010 0
vsize: 12204
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2644 0 0 0 60997 8 0 0 25 0 1 0 420497910 12632064 2622 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3084 2622 603 41 0 3043 0
vsize: 12336
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2657 0 0 0 61997 8 0 0 25 0 1 0 420497910 12632064 2635 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3084 2635 603 41 0 3043 0
vsize: 12336
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2661 0 0 0 62997 8 0 0 25 0 1 0 420497910 12632064 2639 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3084 2639 603 41 0 3043 0
vsize: 12336
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2667 0 0 0 63998 8 0 0 25 0 1 0 420497910 12767232 2645 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3117 2645 603 41 0 3076 0
vsize: 12468
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2667 0 0 0 64998 8 0 0 25 0 1 0 420497910 12763136 2645 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2645 603 41 0 3075 0
vsize: 12464
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 65998 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 66998 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 67998 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223720 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 68998 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 69999 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 70999 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 71999 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 72999 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 73999 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 75000 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 76000 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 77000 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 78000 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2671 0 0 0 79000 8 0 0 25 0 1 0 420497910 12763136 2649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2672 0 0 0 80000 8 0 0 25 0 1 0 420497910 12763136 2650 4294967295 134512640 134672761 3221224624 3221223728 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2650 603 41 0 3075 0
vsize: 12464
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2672 0 0 0 81001 8 0 0 25 0 1 0 420497910 12763136 2650 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2650 603 41 0 3075 0
vsize: 12464
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2676 0 0 0 82001 8 0 0 25 0 1 0 420497910 12763136 2654 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2654 603 41 0 3075 0
vsize: 12464
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2677 0 0 0 83001 8 0 0 25 0 1 0 420497910 12763136 2655 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2655 603 41 0 3075 0
vsize: 12464
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2689 0 0 0 84002 9 0 0 25 0 1 0 420497910 12763136 2667 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2667 603 41 0 3075 0
vsize: 12464
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2707 0 0 0 85002 9 0 0 25 0 1 0 420497910 12910592 2685 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2685 603 41 0 3111 0
vsize: 12608
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2736 0 0 0 86002 9 0 0 25 0 1 0 420497910 13058048 2714 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3188 2714 603 41 0 3147 0
vsize: 12752
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2765 0 0 0 87002 9 0 0 25 0 1 0 420497910 13221888 2743 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3228 2743 603 41 0 3187 0
vsize: 12912
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2793 0 0 0 88002 9 0 0 25 0 1 0 420497910 13385728 2771 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3268 2771 603 41 0 3227 0
vsize: 13072
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2793 0 0 0 89002 9 0 0 25 0 1 0 420497910 13385728 2771 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3268 2771 603 41 0 3227 0
vsize: 13072
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2811 0 0 0 90002 9 0 0 25 0 1 0 420497910 13549568 2789 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2789 603 41 0 3267 0
vsize: 13232
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2817 0 0 0 91003 9 0 0 25 0 1 0 420497910 13549568 2795 4294967295 134512640 134672761 3221224624 3221223728 134555096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2795 603 41 0 3267 0
vsize: 13232
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2818 0 0 0 92003 9 0 0 25 0 1 0 420497910 13549568 2796 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2796 603 41 0 3267 0
vsize: 13232
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2829 0 0 0 93003 9 0 0 25 0 1 0 420497910 13549568 2807 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2807 603 41 0 3267 0
vsize: 13232
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2836 0 0 0 94003 9 0 0 25 0 1 0 420497910 13549568 2814 4294967295 134512640 134672761 3221224624 3221223376 134565845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2814 603 41 0 3267 0
vsize: 13232
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2836 0 0 0 95003 9 0 0 25 0 1 0 420497910 13549568 2814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3308 2814 603 41 0 3267 0
vsize: 13232
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2843 0 0 0 96004 9 0 0 25 0 1 0 420497910 13713408 2821 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2821 603 41 0 3307 0
vsize: 13392
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2849 0 0 0 97004 9 0 0 25 0 1 0 420497910 13713408 2827 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2827 603 41 0 3307 0
vsize: 13392
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2855 0 0 0 98004 9 0 0 25 0 1 0 420497910 13713408 2833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2833 603 41 0 3307 0
vsize: 13392
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2855 0 0 0 99004 9 0 0 25 0 1 0 420497910 13713408 2833 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3348 2833 603 41 0 3307 0
vsize: 13392
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2881 0 0 0 100004 9 0 0 25 0 1 0 420497910 13848576 2859 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3381 2859 603 41 0 3340 0
vsize: 13524
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2881 0 0 0 101005 9 0 0 25 0 1 0 420497910 13848576 2859 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3381 2859 603 41 0 3340 0
vsize: 13524
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2883 0 0 0 102005 9 0 0 25 0 1 0 420497910 13848576 2861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3381 2861 603 41 0 3340 0
vsize: 13524
[startup+1030.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2893 0 0 0 103005 9 0 0 25 0 1 0 420497910 13848576 2871 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3381 2871 603 41 0 3340 0
vsize: 13524
[startup+1040.02 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 104005 9 0 0 25 0 1 0 420497910 14118912 2929 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1050.02 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 105005 9 0 0 25 0 1 0 420497910 14118912 2929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1060.02 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 106005 9 0 0 25 0 1 0 420497910 14118912 2929 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1070.02 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 107005 9 0 0 25 0 1 0 420497910 14098432 2929 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3442 2929 603 41 0 3401 0
vsize: 13768
[startup+1080.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 108005 9 0 0 25 0 1 0 420497910 14086144 2929 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1090.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 109006 9 0 0 25 0 1 0 420497910 14086144 2929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1100.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 110006 9 0 0 25 0 1 0 420497910 14086144 2929 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1110.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 111006 9 0 0 25 0 1 0 420497910 14086144 2929 4294967295 134512640 134672761 3221224624 3221223728 134555105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1120.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 112006 9 0 0 25 0 1 0 420497910 14082048 2929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1130.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 113006 9 0 0 25 0 1 0 420497910 14082048 2929 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1140.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2951 0 0 0 114007 9 0 0 25 0 1 0 420497910 14082048 2929 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1150.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2952 0 0 0 115007 9 0 0 25 0 1 0 420497910 14082048 2930 4294967295 134512640 134672761 3221224624 3221223808 134559516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2930 603 41 0 3397 0
vsize: 13752
[startup+1160.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 2952 0 0 0 116007 9 0 0 25 0 1 0 420497910 14082048 2930 4294967295 134512640 134672761 3221224624 3221223808 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2930 603 41 0 3397 0
vsize: 13752
[startup+1170.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 3014 0 0 0 117007 9 0 0 25 0 1 0 420497910 14352384 2992 4294967295 134512640 134672761 3221224624 3221223728 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3504 2992 603 41 0 3463 0
vsize: 14016
[startup+1180.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 3014 0 0 0 118007 9 0 0 25 0 1 0 420497910 14352384 2992 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3504 2992 603 41 0 3463 0
vsize: 14016
[startup+1190.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 3015 0 0 0 119008 9 0 0 25 0 1 0 420497910 14352384 2993 4294967295 134512640 134672761 3221224624 3221223808 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3504 2993 603 41 0 3463 0
vsize: 14016
[startup+1200.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 22499
Raw data (stat): 22499 (minisat+) R 22498 20937 20936 0 -1 0 3015 0 0 0 120007 9 0 0 25 0 1 0 420497910 14352384 2993 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3504 2993 603 41 0 3463 0
vsize: 14016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 22499
Raw data (stat): 22499 (minisat+) Z 22498 20937 20936 0 -1 12 3017 0 0 0 120007 10 0 0 25 0 1 0 420497910 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.03
CPU time (s): 1200.18
CPU user time (s): 1200.08
CPU system time (s): 0.103984
CPU usage (%): 100.012
Max. virtual memory (Kb): 14016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####