PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-3.opb
MD5SUM	77c89bda49ebcdc0428e1292512864a9
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3080
Optimality of the best value was proved	NO
Number of terms in the objective function	2792
Biggest coefficient in the objective function	1000
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	1385986
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1000
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	1385986
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07184
Number of variables	3300
Total number of constraints	5284
Number of constraints which are clauses	1364
Number of constraints which are cardinality constraints (but not clauses)	3920
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	220
Trace number 5072

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 21:52:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3209 boxname=wulflinc20 idbench=357 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  77c89bda49ebcdc0428e1292512864a9  /oldhome/oroussel/tmp/wulflinc20/normalized-ws97-3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-ws97-3.opb
IDLAUNCH: 3209
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893868 kB
Buffers:         33692 kB
Cached:          71656 kB
SwapCached:       2636 kB
Active:          45588 kB
Inactive:        65256 kB
HighTotal:      131008 kB
HighFree:        55608 kB
LowTotal:       903652 kB
LowFree:        838260 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24464 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:12:53 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3209 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2572 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2571]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2570]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2569]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2568]---> Adder-cost: 418   maxlim: 156   bits: 8/8
c ---[2567]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2566]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2565]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2564]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2563]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2562]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2561]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2560]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2559]---> Adder-cost: 430   maxlim: 193   bits: 8/8
c ---[2558]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2557]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2556]---> Adder-cost: 298   maxlim: 96   bits: 8/7
c ---[2555]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2554]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2553]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2552]---> Adder-cost: 11   maxlim: 41   bits: 7/6
c ---[2551]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2550]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2549]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2548]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2547]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2546]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2545]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2544]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2543]---> Adder-cost: 58   maxlim: 18   bits: 6/5
c ---[2542]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2541]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2540]---> Adder-cost: 28   maxlim: 39   bits: 7/6
c ---[2538]---> BDD-cost:    5
c ---[2536]---> BDD-cost:   15
c ---[2534]---> BDD-cost:    3
c ---[2532]---> BDD-cost:    5
c ---[2530]---> BDD-cost:   15
c ---[2528]---> BDD-cost:    3
c ---[2526]---> BDD-cost:    5
c ---[2524]---> BDD-cost:   15
c ---[2522]---> BDD-cost:    5
c ---[2520]---> BDD-cost:   15
c ---[2518]---> BDD-cost:    3
c ---[2516]---> BDD-cost:    5
c ---[2514]---> BDD-cost:   15
c ---[2512]---> BDD-cost:    3
c ---[2510]---> BDD-cost:    5
c ---[2508]---> BDD-cost:   15
c ---[2506]---> BDD-cost:    3
c ---[2504]---> BDD-cost:    5
c ---[2502]---> BDD-cost:   15
c ---[2500]---> BDD-cost:    3
c ---[2498]---> BDD-cost:    5
c ---[2496]---> BDD-cost:   15
c ---[2494]---> BDD-cost:    3
c ---[2492]---> BDD-cost:   15
c ---[2490]---> BDD-cost:    3
c ---[2488]---> BDD-cost:    5
c ---[2486]---> BDD-cost:   15
c ---[2484]---> BDD-cost:    5
c ---[2482]---> BDD-cost:   15
c ---[2480]---> BDD-cost:    3
c ---[2478]---> BDD-cost:    5
c ---[2476]---> BDD-cost:   15
c ---[2474]---> BDD-cost:    3
c ---[2472]---> BDD-cost:    5
c ---[2470]---> BDD-cost:   15
c ---[2468]---> BDD-cost:    3
c ---[2466]---> BDD-cost:    5
c ---[2464]---> BDD-cost:   15
c ---[2462]---> BDD-cost:    3
c ---[2460]---> BDD-cost:    5
c ---[2458]---> BDD-cost:   15
c ---[2456]---> BDD-cost:    5
c ---[2454]---> BDD-cost:   15
c ---[2452]---> BDD-cost:    3
c ---[2450]---> BDD-cost:    5
c ---[2448]---> BDD-cost:   15
c ---[2446]---> BDD-cost:    3
c ---[2444]---> BDD-cost:   15
c ---[2442]---> BDD-cost:    5
c ---[2440]---> BDD-cost:   15
c ---[2438]---> BDD-cost:    3
c ---[2436]---> BDD-cost:    5
c ---[2434]---> BDD-cost:   15
c ---[2432]---> BDD-cost:    3
c ---[2430]---> BDD-cost:    5
c ---[2428]---> BDD-cost:   15
c ---[2426]---> BDD-cost:    3
c ---[2424]---> BDD-cost:    5
c ---[2422]---> BDD-cost:   15
c ---[2420]---> BDD-cost:    5
c ---[2418]---> BDD-cost:   15
c ---[2416]---> BDD-cost:    3
c ---[2414]---> BDD-cost:    5
c ---[2412]---> BDD-cost:   15
c ---[2410]---> BDD-cost:    3
c ---[2408]---> BDD-cost:    5
c ---[2406]---> BDD-cost:   15
c ---[2404]---> BDD-cost:    5
c ---[2402]---> BDD-cost:   15
c ---[2400]---> BDD-cost:    3
c ---[2398]---> BDD-cost:    5
c ---[2396]---> BDD-cost:   15
c ---[2394]---> BDD-cost:    5
c ---[2392]---> BDD-cost:   15
c ---[2390]---> BDD-cost:    5
c ---[2388]---> BDD-cost:   15
c ---[2386]---> BDD-cost:    3
c ---[2384]---> BDD-cost:    5
c ---[2382]---> BDD-cost:   15
c ---[2380]---> BDD-cost:    3
c ---[2378]---> BDD-cost:    5
c ---[2376]---> BDD-cost:   15
c ---[2374]---> BDD-cost:    3
c ---[2372]---> BDD-cost:    5
c ---[2370]---> BDD-cost:   15
c ---[2368]---> BDD-cost:    3
c ---[2366]---> BDD-cost:    5
c ---[2364]---> BDD-cost:   15
c ---[2362]---> BDD-cost:    5
c ---[2360]---> BDD-cost:   15
c ---[2358]---> BDD-cost:    5
c ---[2356]---> BDD-cost:   15
c ---[2354]---> BDD-cost:    5
c ---[2352]---> BDD-cost:   15
c ---[2350]---> BDD-cost:    3
c ---[2348]---> BDD-cost:    5
c ---[2346]---> BDD-cost:   15
c ---[2344]---> BDD-cost:    5
c ---[2342]---> BDD-cost:   15
c ---[2340]---> BDD-cost:    3
c ---[2338]---> BDD-cost:    5
c ---[2336]---> BDD-cost:   15
c ---[2334]---> BDD-cost:    5
c ---[2332]---> BDD-cost:   15
c ---[2330]---> BDD-cost:    3
c ---[2328]---> BDD-cost:    5
c ---[2326]---> BDD-cost:   15
c ---[2324]---> BDD-cost:    3
c ---[2322]---> BDD-cost:    5
c ---[2320]---> BDD-cost:   15
c ---[2318]---> BDD-cost:    5
c ---[2316]---> BDD-cost:   15
c ---[2314]---> BDD-cost:    3
c ---[2312]---> BDD-cost:    5
c ---[2310]---> BDD-cost:   15
c ---[2308]---> BDD-cost:    3
c ---[2306]---> BDD-cost:    5
c ---[2304]---> BDD-cost:   15
c ---[2302]---> BDD-cost:    5
c ---[2300]---> BDD-cost:   15
c ---[2298]---> BDD-cost:    5
c ---[2296]---> BDD-cost:   15
c ---[2294]---> BDD-cost:    3
c ---[2292]---> BDD-cost:    5
c ---[2290]---> BDD-cost:   15
c ---[2288]---> BDD-cost:    5
c ---[2286]---> BDD-cost:   15
c ---[2284]---> BDD-cost:    5
c ---[2282]---> BDD-cost:   15
c ---[2280]---> BDD-cost:    5
c ---[2278]---> BDD-cost:   15
c ---[2276]---> BDD-cost:    3
c ---[2274]---> BDD-cost:    5
c ---[2272]---> BDD-cost:   15
c ---[2270]---> BDD-cost:    3
c ---[2268]---> BDD-cost:    5
c ---[2266]---> BDD-cost:   15
c ---[2264]---> BDD-cost:    5
c ---[2262]---> BDD-cost:   15
c ---[2260]---> BDD-cost:    5
c ---[2258]---> BDD-cost:   15
c ---[2256]---> BDD-cost:    5
c ---[2254]---> BDD-cost:   15
c ---[2252]---> BDD-cost:    3
c ---[2250]---> BDD-cost:    5
c ---[2248]---> BDD-cost:   15
c ---[2246]---> BDD-cost:    3
c ---[2244]---> BDD-cost:    5
c ---[2242]---> BDD-cost:   15
c ---[2240]---> BDD-cost:    3
c ---[2238]---> BDD-cost:    5
c ---[2236]---> BDD-cost:   15
c ---[2234]---> BDD-cost:    5
c ---[2232]---> BDD-cost:   15
c ---[2230]---> BDD-cost:    3
c ---[2228]---> BDD-cost:    5
c ---[2226]---> BDD-cost:   15
c ---[2224]---> BDD-cost:    5
c ---[2222]---> BDD-cost:   15
c ---[2220]---> BDD-cost:    3
c ---[2218]---> BDD-cost:    5
c ---[2216]---> BDD-cost:   15
c ---[2214]---> BDD-cost:    3
c ---[2212]---> BDD-cost:    5
c ---[2210]---> BDD-cost:   15
c ---[2208]---> BDD-cost:    3
c ---[2206]---> BDD-cost:    5
c ---[2204]---> BDD-cost:   15
c ---[2202]---> BDD-cost:    3
c ---[2200]---> BDD-cost:    5
c ---[2198]---> BDD-cost:   15
c ---[2196]---> BDD-cost:    5
c ---[2194]---> BDD-cost:   15
c ---[2192]---> BDD-cost:    3
c ---[2190]---> BDD-cost:   15
c ---[2188]---> BDD-cost:    3
c ---[2186]---> BDD-cost:    5
c ---[2184]---> BDD-cost:   15
c ---[2182]---> BDD-cost:    3
c ---[2180]---> BDD-cost:    5
c ---[2178]---> BDD-cost:   15
c ---[2176]---> BDD-cost:    3
c ---[2174]---> BDD-cost:    5
c ---[2172]---> BDD-cost:   15
c ---[2170]---> BDD-cost:    3
c ---[2168]---> BDD-cost:    5
c ---[2166]---> BDD-cost:   15
c ---[2164]---> BDD-cost:    3
c ---[2162]---> BDD-cost:    5
c ---[2160]---> BDD-cost:   15
c ---[2158]---> BDD-cost:    3
c ---[2156]---> BDD-cost:    5
c ---[2154]---> BDD-cost:   15
c ---[2152]---> BDD-cost:    3
c ---[2150]---> BDD-cost:    5
c ---[2148]---> BDD-cost:   15
c ---[2146]---> BDD-cost:    3
c ---[2144]---> BDD-cost:    5
c ---[2142]---> BDD-cost:   15
c ---[2140]---> BDD-cost:    3
c ---[2138]---> BDD-cost:    5
c ---[2136]---> BDD-cost:   15
c ---[2134]---> BDD-cost:    3
c ---[2132]---> BDD-cost:    5
c ---[2130]---> BDD-cost:   15
c ---[2128]---> BDD-cost:    3
c ---[2126]---> BDD-cost:    5
c ---[2124]---> BDD-cost:   15
c ---[2122]---> BDD-cost:    3
c ---[2120]---> BDD-cost:    5
c ---[2118]---> BDD-cost:   15
c ---[2116]---> BDD-cost:    3
c ---[2114]---> BDD-cost:    5
c ---[2112]---> BDD-cost:   15
c ---[2110]---> BDD-cost:    3
c ---[2108]---> BDD-cost:    5
c ---[2106]---> BDD-cost:   15
c ---[2104]---> BDD-cost:   15
c ---[2102]---> BDD-cost:    3
c ---[2100]---> BDD-cost:    5
c ---[2098]---> BDD-cost:   15
c ---[2096]---> BDD-cost:    3
c ---[2094]---> BDD-cost:    5
c ---[2092]---> BDD-cost:   15
c ---[2090]---> BDD-cost:    5
c ---[2088]---> BDD-cost:   15
c ---[2086]---> BDD-cost:    3
c ---[2084]---> BDD-cost:    5
c ---[2082]---> BDD-cost:   15
c ---[2080]---> BDD-cost:    5
c ---[2078]---> BDD-cost:   15
c ---[2076]---> BDD-cost:    3
c ---[2074]---> BDD-cost:    5
c ---[2072]---> BDD-cost:   15
c ---[2070]---> BDD-cost:    3
c ---[2068]---> BDD-cost:    5
c ---[2066]---> BDD-cost:   15
c ---[2064]---> BDD-cost:    5
c ---[2062]---> BDD-cost:   15
c ---[2060]---> BDD-cost:    3
c ---[2058]---> BDD-cost:    5
c ---[2056]---> BDD-cost:   15
c ---[2054]---> BDD-cost:    5
c ---[2052]---> BDD-cost:   15
c ---[2050]---> BDD-cost:    5
c ---[2048]---> BDD-cost:   15
c ---[2046]---> BDD-cost:    5
c ---[2044]---> BDD-cost:   15
c ---[2042]---> BDD-cost:    3
c ---[2040]---> BDD-cost:    5
c ---[2038]---> BDD-cost:   15
c ---[2036]---> BDD-cost:    3
c ---[2034]---> BDD-cost:    5
c ---[2032]---> BDD-cost:   15
c ---[2030]---> BDD-cost:    3
c ---[2028]---> BDD-cost:    5
c ---[2026]---> BDD-cost:   15
c ---[2024]---> BDD-cost:    3
c ---[2022]---> BDD-cost:    5
c ---[2020]---> BDD-cost:   15
c ---[2018]---> BDD-cost:    3
c ---[2016]---> BDD-cost:    5
c ---[2014]---> BDD-cost:   15
c ---[2012]---> BDD-cost:    3
c ---[2010]---> BDD-cost:    5
c ---[2008]---> BDD-cost:   15
c ---[2006]---> BDD-cost:    3
c ---[2004]---> BDD-cost:    5
c ---[2002]---> BDD-cost:   15
c ---[2000]---> BDD-cost:    5
c ---[1998]---> BDD-cost:   15
c ---[1996]---> BDD-cost:    3
c ---[1994]---> BDD-cost:    5
c ---[1992]---> BDD-cost:   15
c ---[1990]---> BDD-cost:    3
c ---[1988]---> BDD-cost:    5
c ---[1986]---> BDD-cost:   15
c ---[1984]---> BDD-cost:    3
c ---[1982]---> BDD-cost:    5
c ---[1980]---> BDD-cost:   15
c ---[1978]---> BDD-cost:    3
c ---[1976]---> BDD-cost:    5
c ---[1974]---> BDD-cost:   15
c ---[1972]---> BDD-cost:    3
c ---[1970]---> BDD-cost:    5
c ---[1968]---> BDD-cost:   15
c ---[1966]---> BDD-cost:    3
c ---[1964]---> BDD-cost:    5
c ---[1962]---> BDD-cost:   15
c ---[1960]---> BDD-cost:    5
c ---[1958]---> BDD-cost:   15
c ---[1956]---> BDD-cost:    5
c ---[1954]---> BDD-cost:   15
c ---[1952]---> BDD-cost:    3
c ---[1950]---> BDD-cost:    5
c ---[1948]---> BDD-cost:   15
c ---[1946]---> BDD-cost:    5
c ---[1944]---> BDD-cost:   15
c ---[1942]---> BDD-cost:    3
c ---[1940]---> BDD-cost:    5
c ---[1938]---> BDD-cost:   15
c ---[1936]---> BDD-cost:    5
c ---[1934]---> BDD-cost:   15
c ---[1932]---> BDD-cost:    3
c ---[1930]---> BDD-cost:    5
c ---[1928]---> BDD-cost:   15
c ---[1926]---> BDD-cost:    3
c ---[1924]---> BDD-cost:    5
c ---[1922]---> BDD-cost:   15
c ---[1920]---> BDD-cost:    5
c ---[1918]---> BDD-cost:   15
c ---[1916]---> BDD-cost:    3
c ---[1914]---> BDD-cost:    5
c ---[1912]---> BDD-cost:   15
c ---[1910]---> BDD-cost:    3
c ---[1908]---> BDD-cost:    5
c ---[1906]---> BDD-cost:   15
c ---[1904]---> BDD-cost:    3
c ---[1902]---> BDD-cost:    5
c ---[1900]---> BDD-cost:   15
c ---[1898]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    5
c ---[1894]---> BDD-cost:   15
c ---[1892]---> BDD-cost:    5
c ---[1890]---> BDD-cost:   15
c ---[1888]---> BDD-cost:    3
c ---[1886]---> BDD-cost:    5
c ---[1884]---> BDD-cost:   15
c ---[1882]---> BDD-cost:    3
c ---[1880]---> BDD-cost:    5
c ---[1878]---> BDD-cost:   15
c ---[1876]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    5
c ---[1872]---> BDD-cost:   15
c ---[1870]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    5
c ---[1866]---> BDD-cost:   15
c ---[1864]---> BDD-cost:    3
c ---[1862]---> BDD-cost:    5
c ---[1860]---> BDD-cost:   15
c ---[1858]---> BDD-cost:    3
c ---[1856]---> BDD-cost:    5
c ---[1854]---> BDD-cost:   15
c ---[1852]---> BDD-cost:    3
c ---[1850]---> BDD-cost:    5
c ---[1848]---> BDD-cost:   15
c ---[1846]---> BDD-cost:    3
c ---[1844]---> BDD-cost:    5
c ---[1842]---> BDD-cost:   15
c ---[1840]---> BDD-cost:    3
c ---[1838]---> BDD-cost:    5
c ---[1836]---> BDD-cost:   15
c ---[1834]---> BDD-cost:    3
c ---[1832]---> BDD-cost:    5
c ---[1830]---> BDD-cost:   15
c ---[1828]---> BDD-cost:    3
c ---[1826]---> BDD-cost:    5
c ---[1824]---> BDD-cost:   15
c ---[1822]---> BDD-cost:    3
c ---[1820]---> BDD-cost:    5
c ---[1818]---> BDD-cost:   15
c ---[1816]---> BDD-cost:    3
c ---[1814]---> BDD-cost:    5
c ---[1812]---> BDD-cost:   15
c ---[1810]---> BDD-cost:    5
c ---[1808]---> BDD-cost:   15
c ---[1806]---> BDD-cost:    5
c ---[1804]---> BDD-cost:   15
c ---[1802]---> BDD-cost:    3
c ---[1800]---> BDD-cost:    5
c ---[1798]---> BDD-cost:   15
c ---[1796]---> BDD-cost:    3
c ---[1794]---> BDD-cost:    5
c ---[1792]---> BDD-cost:   15
c ---[1790]---> BDD-cost:    3
c ---[1788]---> BDD-cost:    5
c ---[1786]---> BDD-cost:   15
c ---[1784]---> BDD-cost:    3
c ---[1782]---> BDD-cost:    5
c ---[1780]---> BDD-cost:   15
c ---[1778]---> BDD-cost:    5
c ---[1776]---> BDD-cost:   15
c ---[1774]---> BDD-cost:    5
c ---[1772]---> BDD-cost:   15
c ---[1770]---> BDD-cost:    5
c ---[1768]---> BDD-cost:   15
c ---[1766]---> BDD-cost:    5
c ---[1764]---> BDD-cost:   15
c ---[1762]---> BDD-cost:    3
c ---[1760]---> BDD-cost:    5
c ---[1758]---> BDD-cost:   15
c ---[1756]---> BDD-cost:    3
c ---[1754]---> BDD-cost:    5
c ---[1752]---> BDD-cost:   15
c ---[1750]---> BDD-cost:    5
c ---[1748]---> BDD-cost:   15
c ---[1746]---> BDD-cost:    3
c ---[1744]---> BDD-cost:    5
c ---[1742]---> BDD-cost:   15
c ---[1740]---> BDD-cost:    3
c ---[1738]---> BDD-cost:    5
c ---[1736]---> BDD-cost:   15
c ---[1734]---> BDD-cost:    3
c ---[1732]---> BDD-cost:    5
c ---[1730]---> BDD-cost:   15
c ---[1728]---> BDD-cost:    3
c ---[1726]---> BDD-cost:   15
c ---[1724]---> BDD-cost:    5
c ---[1722]---> BDD-cost:   15
c ---[1720]---> BDD-cost:    3
c ---[1718]---> BDD-cost:    5
c ---[1716]---> BDD-cost:   15
c ---[1714]---> BDD-cost:    3
c ---[1712]---> BDD-cost:   15
c ---[1710]---> BDD-cost:   15
c ---[1708]---> BDD-cost:    5
c ---[1706]---> BDD-cost:    5
c ---[1704]---> BDD-cost:   15
c ---[1702]---> BDD-cost:    3
c ---[1700]---> BDD-cost:    5
c ---[1698]---> BDD-cost:   15
c ---[1696]---> BDD-cost:    5
c ---[1694]---> BDD-cost:   15
c ---[1692]---> BDD-cost:    5
c ---[1690]---> BDD-cost:   15
c ---[1688]---> BDD-cost:    5
c ---[1686]---> BDD-cost:   15
c ---[1684]---> BDD-cost:    3
c ---[1682]---> BDD-cost:    5
c ---[1680]---> BDD-cost:   15
c ---[1678]---> BDD-cost:    3
c ---[1676]---> BDD-cost:    5
c ---[1674]---> BDD-cost:   15
c ---[1672]---> BDD-cost:    3
c ---[1670]---> BDD-cost:    5
c ---[1668]---> BDD-cost:   15
c ---[1666]---> BDD-cost:    5
c ---[1664]---> BDD-cost:   15
c ---[1662]---> BDD-cost:    3
c ---[1660]---> BDD-cost:    5
c ---[1658]---> BDD-cost:   15
c ---[1656]---> BDD-cost:    3
c ---[1654]---> BDD-cost:    5
c ---[1652]---> BDD-cost:   15
c ---[1650]---> BDD-cost:    3
c ---[1648]---> BDD-cost:    5
c ---[1646]---> BDD-cost:   15
c ---[1644]---> BDD-cost:    3
c ---[1642]---> BDD-cost:    5
c ---[1640]---> BDD-cost:   15
c ---[1638]---> BDD-cost:    3
c ---[1636]---> BDD-cost:    5
c ---[1634]---> BDD-cost:   15
c ---[1632]---> BDD-cost:    3
c ---[1630]---> BDD-cost:   15
c ---[1628]---> BDD-cost:    5
c ---[1626]---> BDD-cost:   15
c ---[1624]---> BDD-cost:    3
c ---[1622]---> BDD-cost:    5
c ---[1620]---> BDD-cost:   15
c ---[1618]---> BDD-cost:    3
c ---[1616]---> BDD-cost:    5
c ---[1614]---> BDD-cost:   15
c ---[1612]---> BDD-cost:    5
c ---[1610]---> BDD-cost:   15
c ---[1608]---> BDD-cost:    3
c ---[1606]---> BDD-cost:    5
c ---[1604]---> BDD-cost:   15
c ---[1602]---> BDD-cost:    5
c ---[1600]---> BDD-cost:   15
c ---[1598]---> BDD-cost:    3
c ---[1596]---> BDD-cost:    5
c ---[1594]---> BDD-cost:   15
c ---[1592]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    5
c ---[1588]---> BDD-cost:   15
c ---[1586]---> BDD-cost:    3
c ---[1584]---> BDD-cost:    5
c ---[1582]---> BDD-cost:   15
c ---[1580]---> BDD-cost:    5
c ---[1578]---> BDD-cost:   15
c ---[1576]---> BDD-cost:    5
c ---[1574]---> BDD-cost:   15
c ---[1572]---> BDD-cost:    3
c ---[1570]---> BDD-cost:    5
c ---[1568]---> BDD-cost:   15
c ---[1566]---> BDD-cost:   15
c ---[1564]---> BDD-cost:    5
c ---[1562]---> BDD-cost:   15
c ---[1560]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    5
c ---[1556]---> BDD-cost:   15
c ---[1554]---> BDD-cost:    3
c ---[1552]---> BDD-cost:    5
c ---[1550]---> BDD-cost:   15
c ---[1548]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    5
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:    3
c ---[1540]---> BDD-cost:    5
c ---[1538]---> BDD-cost:   15
c ---[1536]---> BDD-cost:    5
c ---[1534]---> BDD-cost:   15
c ---[1532]---> BDD-cost:    5
c ---[1530]---> BDD-cost:   15
c ---[1528]---> BDD-cost:    5
c ---[1526]---> BDD-cost:   15
c ---[1524]---> BDD-cost:    3
c ---[1522]---> BDD-cost:    5
c ---[1520]---> BDD-cost:   15
c ---[1518]---> BDD-cost:    3
c ---[1516]---> BDD-cost:    5
c ---[1514]---> BDD-cost:   15
c ---[1512]---> BDD-cost:    5
c ---[1510]---> BDD-cost:   15
c ---[1508]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    5
c ---[1504]---> BDD-cost:   15
c ---[1502]---> BDD-cost:    5
c ---[1500]---> BDD-cost:   15
c ---[1498]---> BDD-cost:    3
c ---[1496]---> BDD-cost:    5
c ---[1494]---> BDD-cost:   15
c ---[1492]---> BDD-cost:    3
c ---[1490]---> BDD-cost:    5
c ---[1488]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    5
c ---[1484]---> BDD-cost:   15
c ---[1482]---> BDD-cost:    3
c ---[1480]---> BDD-cost:    5
c ---[1478]---> BDD-cost:   15
c ---[1476]---> BDD-cost:    3
c ---[1474]---> BDD-cost:    5
c ---[1472]---> BDD-cost:   15
c ---[1470]---> BDD-cost:   15
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:   15
c ---[1464]---> BDD-cost:    5
c ---[1462]---> BDD-cost:   15
c ---[1460]---> BDD-cost:    3
c ---[1458]---> BDD-cost:    5
c ---[1456]---> BDD-cost:   15
c ---[1454]---> BDD-cost:    3
c ---[1452]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    3
c ---[1448]---> BDD-cost:    5
c ---[1446]---> BDD-cost:   15
c ---[1444]---> BDD-cost:    3
c ---[1442]---> BDD-cost:    5
c ---[1440]---> BDD-cost:   15
c ---[1438]---> BDD-cost:    3
c ---[1436]---> BDD-cost:    5
c ---[1434]---> BDD-cost:   15
c ---[1432]---> BDD-cost:    3
c ---[1430]---> BDD-cost:    5
c ---[1428]---> BDD-cost:   15
c ---[1426]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    5
c ---[1422]---> BDD-cost:   15
c ---[1420]---> BDD-cost:    3
c ---[1418]---> BDD-cost:    5
c ---[1416]---> BDD-cost:   15
c ---[1414]---> BDD-cost:    5
c ---[1412]---> BDD-cost:   15
c ---[1410]---> BDD-cost:   15
c ---[1408]---> BDD-cost:    3
c ---[1406]---> BDD-cost:    5
c ---[1404]---> BDD-cost:   15
c ---[1402]---> BDD-cost:    3
c ---[1400]---> BDD-cost:    5
c ---[1398]---> BDD-cost:   15
c ---[1396]---> BDD-cost:    3
c ---[1394]---> BDD-cost:   15
c ---[1392]---> BDD-cost:    5
c ---[1390]---> BDD-cost:   15
c ---[1388]---> BDD-cost:    3
c ---[1386]---> BDD-cost:    5
c ---[1384]---> BDD-cost:    5
c ---[1382]---> BDD-cost:    3
c ---[1380]---> BDD-cost:    5
c ---[1378]---> BDD-cost:    5
c ---[1376]---> BDD-cost:   15
c ---[1374]---> BDD-cost:    3
c ---[1372]---> BDD-cost:    5
c ---[1370]---> BDD-cost:   15
c ---[1368]---> BDD-cost:    3
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   61319   205646 |   20439       0        0     nan |  0.000 % |
c |       100 |   61319   205646 |   22482     100     2264    22.6 |  4.579 % |
c |       251 |   61260   205447 |   24731     245     3093    12.6 |  4.664 % |
c |       476 |   61218   205307 |   27204     466     4223     9.1 |  4.723 % |
c |       814 |   61152   205085 |   29924     795     6238     7.8 |  4.815 % |
c |      1321 |   61152   205085 |   32917    1302     9324     7.2 |  4.815 % |
c |      2080 |   61046   204737 |   36208    2045    14953     7.3 |  4.953 % |
c |      3219 |   60995   204568 |   39829    3174    31814    10.0 |  5.025 % |
c |      4928 |   60982   204523 |   43812    4810    47925    10.0 |  5.044 % |
c |      7491 |   60982   204523 |   48194    7373    89050    12.1 |  5.044 % |
c |     11335 |   60982   204523 |   53013   11217   150664    13.4 |  5.044 % |
c |     17102 |   60976   204506 |   58314   16982   235337    13.9 |  5.051 % |
c |     25753 |   60929   204356 |   64146   25627   354236    13.8 |  5.110 % |
c |     38729 |   60789   203888 |   70560   38457   543667    14.1 |  5.300 % |
c |     58190 |   60773   203836 |   77617   57914   922406    15.9 |  5.319 % |
c |     87382 |   60769   203820 |   85378   24184   454151    18.8 |  5.326 % |
c |    131172 |   60765   203804 |   93916   67835  2572645    37.9 |  5.332 % |
c |    196857 |   60747   203735 |  103308   44026  2703276    61.4 |  5.365 % |
c |    295383 |   60747   203735 |  113639   50081 14716642   293.9 |  5.365 % |
c |    443175 |   60743   203719 |  125003   95032 22163034   233.2 |  5.372 % |
#### 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.86 0.94 0.90 2/54 31057
Raw data (stat): 31057 (runsolver) R 31056 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479337820 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 2208 0 0 0 993 5 0 0 25 0 1 0 479337820 10633216 2179 4294967295 134512640 134672761 3221224640 3221223764 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2596 2179 603 41 0 2555 0
vsize: 10384
[startup+20.0016 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 2698 0 0 0 1990 7 0 0 25 0 1 0 479337820 12779520 2669 4294967295 134512640 134672761 3221224640 3221223808 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3120 2669 603 41 0 3079 0
vsize: 12480
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 3196 0 0 0 2989 8 0 0 25 0 1 0 479337820 14655488 3167 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3578 3167 603 41 0 3537 0
vsize: 14312
[startup+40.0023 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 3795 0 0 0 3986 10 0 0 25 0 1 0 479337820 17383424 3766 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4244 3766 603 41 0 4203 0
vsize: 16976
[startup+50.0018 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 4064 0 0 0 4986 11 0 0 25 0 1 0 479337820 18464768 4035 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4508 4035 603 41 0 4467 0
vsize: 18032
[startup+60.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 4064 0 0 0 5986 11 0 0 25 0 1 0 479337820 18464768 4035 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4508 4035 603 41 0 4467 0
vsize: 18032
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 4345 0 0 0 6985 12 0 0 25 0 1 0 479337820 19677184 4316 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4804 4316 603 41 0 4763 0
vsize: 19216
[startup+80.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 5481 0 0 0 7983 14 0 0 25 0 1 0 479337820 24272896 5452 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5926 5452 603 41 0 5885 0
vsize: 23704
[startup+90.0019 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 6716 0 0 0 8979 18 0 0 25 0 1 0 479337820 29401088 6687 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7178 6687 603 41 0 7137 0
vsize: 28712
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 7722 0 0 0 9976 22 0 0 25 0 1 0 479337820 33443840 7693 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8165 7693 603 41 0 8124 0
vsize: 32660
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 8935 0 0 0 10972 26 0 0 25 0 1 0 479337820 38395904 8906 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9374 8906 603 41 0 9333 0
vsize: 37496
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 8991 0 0 0 11971 26 0 0 25 0 1 0 479337820 38666240 8962 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8962 603 41 0 9399 0
vsize: 37760
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 8991 0 0 0 12972 26 0 0 25 0 1 0 479337820 38666240 8962 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8962 603 41 0 9399 0
vsize: 37760
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 8991 0 0 0 13971 27 0 0 25 0 1 0 479337820 38666240 8962 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8962 603 41 0 9399 0
vsize: 37760
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 8991 0 0 0 14971 27 0 0 25 0 1 0 479337820 38666240 8962 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8962 603 41 0 9399 0
vsize: 37760
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 9431 0 0 0 15970 28 0 0 25 0 1 0 479337820 40423424 9402 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9869 9402 603 41 0 9828 0
vsize: 39476
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 10678 0 0 0 16967 31 0 0 25 0 1 0 479337820 45539328 10649 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11118 10649 603 41 0 11077 0
vsize: 44472
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 11910 0 0 0 17965 34 0 0 25 0 1 0 479337820 50536448 11881 4294967295 134512640 134672761 3221224640 3221223656 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12338 11881 603 41 0 12297 0
vsize: 49352
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 13135 0 0 0 18962 37 0 0 25 0 1 0 479337820 55656448 13106 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13588 13106 603 41 0 13547 0
vsize: 54352
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 14239 0 0 0 19959 40 0 0 25 0 1 0 479337820 60096512 14210 4294967295 134512640 134672761 3221224640 3221223744 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14672 14210 603 41 0 14631 0
vsize: 58688
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 15177 0 0 0 20956 43 0 0 25 0 1 0 479337820 64012288 15148 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15628 15148 603 41 0 15587 0
vsize: 62512
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 15988 0 0 0 21954 45 0 0 25 0 1 0 479337820 67244032 15959 4294967295 134512640 134672761 3221224640 3221223744 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16417 15959 603 41 0 16376 0
vsize: 65668
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 16700 0 0 0 22952 47 0 0 25 0 1 0 479337820 70209536 16671 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17141 16671 603 41 0 17100 0
vsize: 68564
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 17398 0 0 0 23950 49 0 0 25 0 1 0 479337820 73043968 17369 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17833 17369 603 41 0 17792 0
vsize: 71332
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 18063 0 0 0 24948 52 0 0 25 0 1 0 479337820 75739136 18034 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18491 18034 603 41 0 18450 0
vsize: 73964
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 18784 0 0 0 25947 53 0 0 25 0 1 0 479337820 78692352 18755 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19212 18755 603 41 0 19171 0
vsize: 76848
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 19458 0 0 0 26945 55 0 0 25 0 1 0 479337820 81518592 19429 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19902 19429 603 41 0 19861 0
vsize: 79608
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20062 0 0 0 27944 57 0 0 25 0 1 0 479337820 83943424 20033 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20494 20033 603 41 0 20453 0
vsize: 81976
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20229 0 0 0 28943 57 0 0 25 0 1 0 479337820 84619264 20200 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20200 603 41 0 20618 0
vsize: 82636
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20229 0 0 0 29944 57 0 0 25 0 1 0 479337820 84619264 20200 4294967295 134512640 134672761 3221224640 3221223744 134560501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20200 603 41 0 20618 0
vsize: 82636
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20230 0 0 0 30944 57 0 0 25 0 1 0 479337820 84619264 20201 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20201 603 41 0 20618 0
vsize: 82636
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20230 0 0 0 31944 57 0 0 25 0 1 0 479337820 84619264 20201 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20201 603 41 0 20618 0
vsize: 82636
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20230 0 0 0 32944 57 0 0 25 0 1 0 479337820 84619264 20201 4294967295 134512640 134672761 3221224640 3221223776 134565113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20201 603 41 0 20618 0
vsize: 82636
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20234 0 0 0 33944 58 0 0 25 0 1 0 479337820 84619264 20205 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20205 603 41 0 20618 0
vsize: 82636
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 34944 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 35944 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 36944 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223824 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 37945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 38945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 39945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 40945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 41945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31057
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 42945 58 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 43942 60 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 20236 0 0 0 44942 60 0 0 25 0 1 0 479337820 84619264 20207 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20659 20207 603 41 0 20618 0
vsize: 82636
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 21121 0 0 0 45941 61 0 0 25 0 1 0 479337820 88252416 21092 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21546 21092 603 41 0 21505 0
vsize: 86184
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 22204 0 0 0 46937 65 0 0 25 0 1 0 479337820 92688384 22175 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22629 22175 603 41 0 22588 0
vsize: 90516
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 23285 0 0 0 47934 68 0 0 25 0 1 0 479337820 97128448 23256 4294967295 134512640 134672761 3221224640 3221223712 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23713 23256 603 41 0 23672 0
vsize: 94852
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 23980 0 0 0 48932 71 0 0 25 0 1 0 479337820 99966976 23951 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24406 23951 603 41 0 24365 0
vsize: 97624
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31110
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 24696 0 0 0 49930 73 0 0 25 0 1 0 479337820 102912000 24667 4294967295 134512640 134672761 3221224640 3221223824 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25125 24667 603 41 0 25084 0
vsize: 100500
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 50927 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 51927 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 52927 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 53928 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 54928 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 55928 76 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 56928 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223744 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 57928 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 58928 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 59928 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223744 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 60929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223744 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 61929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 62929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 63929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223744 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 64929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223824 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 65929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 66929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25711 0 0 0 67929 77 0 0 25 0 1 0 479337820 107081728 25682 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25682 603 41 0 26102 0
vsize: 104572
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 68929 77 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 69930 77 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 70930 78 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 71930 78 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 72930 78 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 73930 78 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 25712 0 0 0 74930 78 0 0 25 0 1 0 479337820 107081728 25683 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26143 25683 603 41 0 26102 0
vsize: 104572
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31112
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 26143 0 0 0 75929 80 0 0 25 0 1 0 479337820 108843008 26114 4294967295 134512640 134672761 3221224640 3221223776 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26573 26114 603 41 0 26532 0
vsize: 106292
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 26415 0 0 0 76928 80 0 0 25 0 1 0 479337820 109920256 26386 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26836 26386 603 41 0 26795 0
vsize: 107344
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 26683 0 0 0 77928 81 0 0 25 0 1 0 479337820 111132672 26654 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27132 26654 603 41 0 27091 0
vsize: 108528
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 27355 0 0 0 78926 83 0 0 25 0 1 0 479337820 113827840 27326 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27790 27326 603 41 0 27749 0
vsize: 111160
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 28326 0 0 0 79924 85 0 0 25 0 1 0 479337820 117743616 28297 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28746 28297 603 41 0 28705 0
vsize: 114984
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 29444 0 0 0 80922 87 0 0 25 0 1 0 479337820 122310656 29415 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29861 29415 603 41 0 29820 0
vsize: 119444
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30423 0 0 0 81919 90 0 0 25 0 1 0 479337820 126865408 30394 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30973 30394 603 41 0 30932 0
vsize: 123892
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 82918 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 83918 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223744 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 84918 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 85918 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 86919 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 87919 91 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30856 0 0 0 88919 92 0 0 25 0 1 0 479337820 128614400 30827 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30827 603 41 0 31359 0
vsize: 125600
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30857 0 0 0 89919 92 0 0 25 0 1 0 479337820 128614400 30828 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30828 603 41 0 31359 0
vsize: 125600
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 90919 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 91919 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223764 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 92919 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223764 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 93920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 94920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 95920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 96920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223824 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 97920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 98920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 99920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 100920 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 101921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 102921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223800 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 103921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 104921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 105921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 106921 92 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 107921 93 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 108922 93 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 30859 0 0 0 109922 93 0 0 25 0 1 0 479337820 128614400 30830 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30830 603 41 0 31359 0
vsize: 125600
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31278 0 0 0 110921 93 0 0 25 0 1 0 479337820 130367488 31249 4294967295 134512640 134672761 3221224640 3221223824 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31828 31249 603 41 0 31787 0
vsize: 127312
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 111920 94 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 112920 94 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 113920 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 114921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 115921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 116921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 117921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 118921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223744 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31114
Raw data (stat): 31057 (minisat+) R 31056 27565 27564 0 -1 0 31543 0 0 0 119921 95 0 0 25 0 1 0 479337820 131444736 31514 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32091 31514 603 41 0 32050 0
vsize: 128364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31114
Raw data (stat): 31057 (minisat+) Z 31056 27565 27564 0 -1 12 31545 0 0 0 119921 101 0 0 25 0 1 0 479337820 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.22
CPU system time (s): 1.01285
CPU usage (%): 100.012
Max. virtual memory (Kb): 128364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####