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 5703 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 01:30:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4142 boxname=wulflinc15 idbench=6 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ce39bf71367df072c91f9b7587480c93  /oldhome/oroussel/tmp/wulflinc15/normalized-chnl15_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-chnl15_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc15/normalized-chnl15_20_pb.cnf.cr.opb
IDLAUNCH: 4142
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        899600 kB
Buffers:         36364 kB
Cached:          77160 kB
SwapCached:       2144 kB
Active:          63660 kB
Inactive:        54776 kB
HighTotal:      131008 kB
HighFree:        50092 kB
LowTotal:       903652 kB
LowFree:        849508 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11152 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:50:18 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4142 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 % |
#### 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.91 0.97 0.92 2/54 3427
Raw data (stat): 3427 (runsolver) R 3426 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422418951 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 891 0 0 0 996 2 0 0 25 0 1 0 422418951 5255168 869 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1283 869 603 41 0 1242 0
vsize: 5132
[startup+19.9997 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1054 0 0 0 1995 2 0 0 25 0 1 0 422418951 5795840 1032 4294967295 134512640 134672761 3221224528 3221223696 134559131 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.0002 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1205 0 0 0 2995 3 0 0 25 0 1 0 422418951 6467584 1183 4294967295 134512640 134672761 3221224528 3221223696 134561188 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.0004 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1273 0 0 0 3995 3 0 0 25 0 1 0 422418951 6742016 1251 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1646 1251 603 41 0 1605 0
vsize: 6584
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1273 0 0 0 4995 3 0 0 25 0 1 0 422418951 6742016 1251 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1646 1251 603 41 0 1605 0
vsize: 6584
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1362 0 0 0 5995 3 0 0 25 0 1 0 422418951 7159808 1340 4294967295 134512640 134672761 3221224528 3221223696 134560983 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.0009 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1388 0 0 0 6995 3 0 0 25 0 1 0 422418951 7294976 1366 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1781 1366 603 41 0 1740 0
vsize: 7124
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1398 0 0 0 7995 3 0 0 25 0 1 0 422418951 7294976 1376 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1781 1376 603 41 0 1740 0
vsize: 7124
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1471 0 0 0 8995 4 0 0 25 0 1 0 422418951 7565312 1449 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1847 1449 603 41 0 1806 0
vsize: 7388
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1579 0 0 0 9995 4 0 0 25 0 1 0 422418951 7970816 1557 4294967295 134512640 134672761 3221224528 3221223712 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1946 1557 603 41 0 1905 0
vsize: 7784
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1579 0 0 0 10995 4 0 0 25 0 1 0 422418951 7970816 1557 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1946 1557 603 41 0 1905 0
vsize: 7784
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1601 0 0 0 11995 4 0 0 25 0 1 0 422418951 8105984 1579 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1579 603 41 0 1938 0
vsize: 7916
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1609 0 0 0 12995 4 0 0 25 0 1 0 422418951 8241152 1587 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2012 1587 603 41 0 1971 0
vsize: 8048
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1618 0 0 0 13995 4 0 0 25 0 1 0 422418951 8241152 1596 4294967295 134512640 134672761 3221224528 3221223700 134559060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2012 1596 603 41 0 1971 0
vsize: 8048
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1645 0 0 0 14995 4 0 0 25 0 1 0 422418951 8376320 1623 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2045 1623 603 41 0 2004 0
vsize: 8180
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1677 0 0 0 15996 4 0 0 25 0 1 0 422418951 8515584 1655 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2079 1655 603 41 0 2038 0
vsize: 8316
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1747 0 0 0 16995 5 0 0 25 0 1 0 422418951 8785920 1725 4294967295 134512640 134672761 3221224528 3221222156 134566343 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2145 1725 603 41 0 2104 0
vsize: 8580
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1768 0 0 0 17995 5 0 0 25 0 1 0 422418951 8785920 1746 4294967295 134512640 134672761 3221224528 3221223712 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2145 1746 603 41 0 2104 0
vsize: 8580
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1777 0 0 0 18995 5 0 0 25 0 1 0 422418951 8929280 1755 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2180 1755 603 41 0 2139 0
vsize: 8720
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1810 0 0 0 19996 5 0 0 25 0 1 0 422418951 9039872 1788 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2207 1788 603 41 0 2166 0
vsize: 8828
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1827 0 0 0 20996 5 0 0 25 0 1 0 422418951 9179136 1805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2241 1805 603 41 0 2200 0
vsize: 8964
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1872 0 0 0 21996 5 0 0 25 0 1 0 422418951 9326592 1850 4294967295 134512640 134672761 3221224528 3221223712 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2277 1850 603 41 0 2236 0
vsize: 9108
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1873 0 0 0 22996 5 0 0 25 0 1 0 422418951 9326592 1851 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2277 1851 603 41 0 2236 0
vsize: 9108
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1878 0 0 0 23996 5 0 0 25 0 1 0 422418951 9326592 1856 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2277 1856 603 41 0 2236 0
vsize: 9108
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1933 0 0 0 24996 5 0 0 25 0 1 0 422418951 9601024 1911 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2344 1911 603 41 0 2303 0
vsize: 9376
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 1980 0 0 0 25996 5 0 0 25 0 1 0 422418951 9736192 1958 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2377 1958 603 41 0 2336 0
vsize: 9508
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2005 0 0 0 26996 5 0 0 25 0 1 0 422418951 9871360 1983 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2410 1983 603 41 0 2369 0
vsize: 9640
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2015 0 0 0 27996 5 0 0 25 0 1 0 422418951 9871360 1993 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2410 1993 603 41 0 2369 0
vsize: 9640
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2018 0 0 0 28997 6 0 0 25 0 1 0 422418951 10006528 1996 4294967295 134512640 134672761 3221224528 3221223708 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2443 1996 603 41 0 2402 0
vsize: 9772
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2056 0 0 0 29997 6 0 0 25 0 1 0 422418951 10137600 2034 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2475 2034 603 41 0 2434 0
vsize: 9900
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2093 0 0 0 30997 6 0 0 25 0 1 0 422418951 10272768 2071 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2508 2071 603 41 0 2467 0
vsize: 10032
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2096 0 0 0 31997 6 0 0 25 0 1 0 422418951 10272768 2074 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2508 2074 603 41 0 2467 0
vsize: 10032
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2111 0 0 0 32996 6 0 0 25 0 1 0 422418951 10420224 2089 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2544 2089 603 41 0 2503 0
vsize: 10176
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2147 0 0 0 33996 6 0 0 25 0 1 0 422418951 10567680 2125 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2125 603 41 0 2539 0
vsize: 10320
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2185 0 0 0 34996 6 0 0 25 0 1 0 422418951 10702848 2163 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2613 2163 603 41 0 2572 0
vsize: 10452
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2190 0 0 0 35997 6 0 0 25 0 1 0 422418951 10702848 2168 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2613 2168 603 41 0 2572 0
vsize: 10452
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2218 0 0 0 36997 6 0 0 25 0 1 0 422418951 10838016 2196 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2646 2196 603 41 0 2605 0
vsize: 10584
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2236 0 0 0 37997 6 0 0 25 0 1 0 422418951 10838016 2214 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2646 2214 603 41 0 2605 0
vsize: 10584
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2237 0 0 0 38997 6 0 0 25 0 1 0 422418951 10838016 2215 4294967295 134512640 134672761 3221224528 3221223712 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2646 2215 603 41 0 2605 0
vsize: 10584
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2339 0 0 0 39997 7 0 0 25 0 1 0 422418951 11255808 2317 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2748 2317 603 41 0 2707 0
vsize: 10992
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2361 0 0 0 40997 7 0 0 25 0 1 0 422418951 11390976 2339 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2781 2339 603 41 0 2740 0
vsize: 11124
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2361 0 0 0 41997 7 0 0 25 0 1 0 422418951 11390976 2339 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2781 2339 603 41 0 2740 0
vsize: 11124
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2362 0 0 0 42997 7 0 0 25 0 1 0 422418951 11390976 2340 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2362 0 0 0 43998 7 0 0 25 0 1 0 422418951 11390976 2340 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2362 0 0 0 44998 7 0 0 25 0 1 0 422418951 11390976 2340 4294967295 134512640 134672761 3221224528 3221223712 134559550 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2781 2340 603 41 0 2740 0
vsize: 11124
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2382 0 0 0 45998 7 0 0 25 0 1 0 422418951 11542528 2360 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2818 2360 603 41 0 2777 0
vsize: 11272
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2396 0 0 0 46998 7 0 0 25 0 1 0 422418951 11542528 2374 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2818 2374 603 41 0 2777 0
vsize: 11272
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2396 0 0 0 47998 7 0 0 25 0 1 0 422418951 11542528 2374 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2818 2374 603 41 0 2777 0
vsize: 11272
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2396 0 0 0 48998 7 0 0 25 0 1 0 422418951 11542528 2374 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2818 2374 603 41 0 2777 0
vsize: 11272
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2396 0 0 0 49999 7 0 0 25 0 1 0 422418951 11542528 2374 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2818 2374 603 41 0 2777 0
vsize: 11272
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2400 0 0 0 50998 7 0 0 25 0 1 0 422418951 11542528 2378 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2818 2378 603 41 0 2777 0
vsize: 11272
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2412 0 0 0 51998 7 0 0 25 0 1 0 422418951 11689984 2390 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2854 2390 603 41 0 2813 0
vsize: 11416
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2422 0 0 0 52998 7 0 0 25 0 1 0 422418951 11689984 2400 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2854 2400 603 41 0 2813 0
vsize: 11416
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2428 0 0 0 53999 7 0 0 25 0 1 0 422418951 11689984 2406 4294967295 134512640 134672761 3221224528 3221223632 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2854 2406 603 41 0 2813 0
vsize: 11416
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2451 0 0 0 54999 7 0 0 25 0 1 0 422418951 11821056 2429 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2886 2429 603 41 0 2845 0
vsize: 11544
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2475 0 0 0 55999 7 0 0 25 0 1 0 422418951 11956224 2453 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2453 603 41 0 2878 0
vsize: 11676
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2476 0 0 0 56999 7 0 0 25 0 1 0 422418951 11956224 2454 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2454 603 41 0 2878 0
vsize: 11676
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2478 0 0 0 57999 7 0 0 25 0 1 0 422418951 11956224 2456 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2456 603 41 0 2878 0
vsize: 11676
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2525 0 0 0 58999 7 0 0 25 0 1 0 422418951 12091392 2503 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2952 2503 603 41 0 2911 0
vsize: 11808
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2525 0 0 0 60000 7 0 0 25 0 1 0 422418951 12091392 2503 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2952 2503 603 41 0 2911 0
vsize: 11808
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2643 0 0 0 60999 8 0 0 25 0 1 0 422418951 12632064 2621 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2621 603 41 0 3043 0
vsize: 12336
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2643 0 0 0 61999 8 0 0 25 0 1 0 422418951 12632064 2621 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2621 603 41 0 3043 0
vsize: 12336
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2660 0 0 0 63000 8 0 0 25 0 1 0 422418951 12632064 2638 4294967295 134512640 134672761 3221224528 3221223696 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2638 603 41 0 3043 0
vsize: 12336
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2660 0 0 0 64000 8 0 0 25 0 1 0 422418951 12632064 2638 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3084 2638 603 41 0 3043 0
vsize: 12336
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2666 0 0 0 65000 8 0 0 25 0 1 0 422418951 12767232 2644 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3117 2644 603 41 0 3076 0
vsize: 12468
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2666 0 0 0 66000 8 0 0 25 0 1 0 422418951 12763136 2644 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2644 603 41 0 3075 0
vsize: 12464
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 67000 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223680 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 68000 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 69001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223704 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 70001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 71001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 72001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 73001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 74001 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 75002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 76002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 77002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 78002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 79002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2670 0 0 0 80002 8 0 0 25 0 1 0 422418951 12763136 2648 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2648 603 41 0 3075 0
vsize: 12464
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2671 0 0 0 81001 8 0 0 25 0 1 0 422418951 12763136 2649 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2671 0 0 0 82001 8 0 0 25 0 1 0 422418951 12763136 2649 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2649 603 41 0 3075 0
vsize: 12464
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2675 0 0 0 83001 8 0 0 25 0 1 0 422418951 12763136 2653 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2653 603 41 0 3075 0
vsize: 12464
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2676 0 0 0 84001 8 0 0 25 0 1 0 422418951 12763136 2654 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2654 603 41 0 3075 0
vsize: 12464
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2688 0 0 0 85001 8 0 0 25 0 1 0 422418951 12763136 2666 4294967295 134512640 134672761 3221224528 3221223544 1075352757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2666 603 41 0 3075 0
vsize: 12464
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2721 0 0 0 86001 8 0 0 25 0 1 0 422418951 12910592 2699 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2699 603 41 0 3111 0
vsize: 12608
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2736 0 0 0 87001 8 0 0 25 0 1 0 422418951 13058048 2714 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3188 2714 603 41 0 3147 0
vsize: 12752
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2765 0 0 0 88001 8 0 0 25 0 1 0 422418951 13221888 2743 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3228 2743 603 41 0 3187 0
vsize: 12912
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2793 0 0 0 89001 9 0 0 25 0 1 0 422418951 13385728 2771 4294967295 134512640 134672761 3221224528 3221223696 134561188 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.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2793 0 0 0 90001 9 0 0 25 0 1 0 422418951 13385728 2771 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3268 2771 603 41 0 3227 0
vsize: 13072
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2811 0 0 0 91001 9 0 0 25 0 1 0 422418951 13549568 2789 4294967295 134512640 134672761 3221224528 3221223632 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2789 603 41 0 3267 0
vsize: 13232
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2817 0 0 0 92001 9 0 0 25 0 1 0 422418951 13549568 2795 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2795 603 41 0 3267 0
vsize: 13232
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2823 0 0 0 93002 9 0 0 25 0 1 0 422418951 13549568 2801 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2801 603 41 0 3267 0
vsize: 13232
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2829 0 0 0 94002 9 0 0 25 0 1 0 422418951 13549568 2807 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2807 603 41 0 3267 0
vsize: 13232
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2836 0 0 0 95002 9 0 0 25 0 1 0 422418951 13549568 2814 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2814 603 41 0 3267 0
vsize: 13232
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2841 0 0 0 96002 9 0 0 25 0 1 0 422418951 13713408 2819 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2819 603 41 0 3307 0
vsize: 13392
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2843 0 0 0 97002 9 0 0 25 0 1 0 422418951 13713408 2821 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2821 603 41 0 3307 0
vsize: 13392
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2849 0 0 0 98003 9 0 0 25 0 1 0 422418951 13713408 2827 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2827 603 41 0 3307 0
vsize: 13392
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2855 0 0 0 99003 9 0 0 25 0 1 0 422418951 13713408 2833 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2833 603 41 0 3307 0
vsize: 13392
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2855 0 0 0 100003 9 0 0 25 0 1 0 422418951 13713408 2833 4294967295 134512640 134672761 3221224528 3221223680 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2833 603 41 0 3307 0
vsize: 13392
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2881 0 0 0 101003 9 0 0 25 0 1 0 422418951 13848576 2859 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2859 603 41 0 3340 0
vsize: 13524
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2881 0 0 0 102003 9 0 0 25 0 1 0 422418951 13848576 2859 4294967295 134512640 134672761 3221224528 3221223524 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2859 603 41 0 3340 0
vsize: 13524
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2883 0 0 0 103004 9 0 0 25 0 1 0 422418951 13848576 2861 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2861 603 41 0 3340 0
vsize: 13524
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2893 0 0 0 104004 9 0 0 25 0 1 0 422418951 13848576 2871 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2871 603 41 0 3340 0
vsize: 13524
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 105004 9 0 0 25 0 1 0 422418951 14118912 2929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 106004 9 0 0 25 0 1 0 422418951 14118912 2929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 107004 9 0 0 25 0 1 0 422418951 14118912 2929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3447 2929 603 41 0 3406 0
vsize: 13788
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 108005 9 0 0 25 0 1 0 422418951 14098432 2929 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3442 2929 603 41 0 3401 0
vsize: 13768
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 109005 9 0 0 25 0 1 0 422418951 14086144 2929 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 110005 9 0 0 25 0 1 0 422418951 14086144 2929 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 111005 9 0 0 25 0 1 0 422418951 14086144 2929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 112005 9 0 0 25 0 1 0 422418951 14086144 2929 4294967295 134512640 134672761 3221224528 3221223712 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 2929 603 41 0 3398 0
vsize: 13756
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 113006 9 0 0 25 0 1 0 422418951 14082048 2929 4294967295 134512640 134672761 3221224528 3221223712 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 114006 9 0 0 25 0 1 0 422418951 14082048 2929 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2951 0 0 0 115006 9 0 0 25 0 1 0 422418951 14082048 2929 4294967295 134512640 134672761 3221224528 3221223684 134560075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2929 603 41 0 3397 0
vsize: 13752
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2952 0 0 0 116006 9 0 0 25 0 1 0 422418951 14082048 2930 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2930 603 41 0 3397 0
vsize: 13752
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 2952 0 0 0 117006 9 0 0 25 0 1 0 422418951 14082048 2930 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3438 2930 603 41 0 3397 0
vsize: 13752
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 3014 0 0 0 118006 9 0 0 25 0 1 0 422418951 14352384 2992 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 2992 603 41 0 3463 0
vsize: 14016
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 3014 0 0 0 119007 9 0 0 25 0 1 0 422418951 14352384 2992 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 2992 603 41 0 3463 0
vsize: 14016
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3427
Raw data (stat): 3427 (minisat+) R 3426 29151 29150 0 -1 0 3015 0 0 0 120007 9 0 0 25 0 1 0 422418951 14352384 2993 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 2993 603 41 0 3463 0
vsize: 14016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 3427
Raw data (stat): 3427 (minisat+) Z 3426 29151 29150 0 -1 12 3017 0 0 0 120007 10 0 0 25 0 1 0 422418951 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.18
CPU user time (s): 1200.07
CPU system time (s): 0.101984
CPU usage (%): 100.011
Max. virtual memory (Kb): 14016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####