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 6454

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 05:02:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4869 boxname=wulflinc22 idbench=357 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  77c89bda49ebcdc0428e1292512864a9  /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-3.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-3.opb /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-3.opb
IDLAUNCH: 4869
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        826928 kB
Buffers:         33488 kB
Cached:         131024 kB
SwapCached:        524 kB
Active:          52124 kB
Inactive:       115756 kB
HighTotal:      131008 kB
HighFree:         6216 kB
LowTotal:       903652 kB
LowFree:        820712 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34192 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:22:40 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 4869 7 1200.25 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 |   69823   231374 |   23274       0        0     nan |  0.000 % |
c |       102 |   69823   231374 |   25601     102     2640    25.9 |  4.579 % |
c |       252 |   69776   231215 |   28161     248     4421    17.8 |  4.645 % |
c |       478 |   69704   230975 |   30977     467     6770    14.5 |  4.743 % |
c |       815 |   69622   230704 |   34075     797     8354    10.5 |  4.854 % |
c |      1321 |   69531   230406 |   37483    1289    11787     9.1 |  4.966 % |
c |      2083 |   69505   230323 |   41231    2045    20454    10.0 |  4.998 % |
c |      3222 |   69472   230217 |   45354    3177    35419    11.1 |  5.038 % |
c |      4930 |   69455   230163 |   49889    4883    51737    10.6 |  5.057 % |
c |      7493 |   69423   230063 |   54878    7440    76276    10.3 |  5.097 % |
c |     11338 |   69423   230063 |   60366   11285   135331    12.0 |  5.097 % |
c |     17104 |   69395   229969 |   66403   17049   226228    13.3 |  5.136 % |
c |     25753 |   69307   229678 |   73043   25517   325288    12.7 |  5.247 % |
c |     38729 |   69281   229595 |   80348   38489   628765    16.3 |  5.280 % |
c |     58190 |   69264   229541 |   88382   57947  1255059    21.7 |  5.300 % |
c |     87383 |   69264   229541 |   97221   87140  3401578    39.0 |  5.300 % |
c |    131172 |   69258   229524 |  106943   44251  3143087    71.0 |  5.306 % |
c |    196857 |   69258   229524 |  117637   20434  1599193    78.3 |  5.306 % |
c |    295383 |   69254   229508 |  129401  118956 13798271   116.0 |  5.313 % |
c |    443172 |   69229   229429 |  142341   34291  6499084   189.5 |  5.352 % |
#### 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.82 0.95 0.90 2/54 32457
Raw data (stat): 32457 (runsolver) R 32456 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481915792 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0005 s]
Raw data (loadavg): 0.84 0.95 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 2208 0 0 0 992 6 0 0 25 0 1 0 481915792 10821632 2179 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2179 603 41 0 2601 0
vsize: 10568
[startup+20.0006 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 2650 0 0 0 1991 7 0 0 25 0 1 0 481915792 12570624 2621 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2621 603 41 0 3028 0
vsize: 12276
[startup+30.0022 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 3059 0 0 0 2990 8 0 0 25 0 1 0 481915792 14315520 3030 4294967295 134512640 134672761 3221224576 3221223760 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3495 3030 603 41 0 3454 0
vsize: 13980
[startup+40.0024 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 3749 0 0 0 3987 11 0 0 25 0 1 0 481915792 17154048 3720 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4188 3720 603 41 0 4147 0
vsize: 16752
[startup+50.0028 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 4931 0 0 0 4984 13 0 0 25 0 1 0 481915792 22130688 4902 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5403 4902 603 41 0 5362 0
vsize: 21612
[startup+60.0027 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 6138 0 0 0 5980 17 0 0 25 0 1 0 481915792 27115520 6109 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6620 6109 603 41 0 6579 0
vsize: 26480
[startup+70.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 6939 0 0 0 6978 19 0 0 25 0 1 0 481915792 30359552 6910 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7412 6910 603 41 0 7371 0
vsize: 29648
[startup+80.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 6939 0 0 0 7978 20 0 0 25 0 1 0 481915792 30359552 6910 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7412 6910 603 41 0 7371 0
vsize: 29648
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 6939 0 0 0 8978 20 0 0 25 0 1 0 481915792 30359552 6910 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7412 6910 603 41 0 7371 0
vsize: 29648
[startup+100.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 6939 0 0 0 9978 20 0 0 25 0 1 0 481915792 30359552 6910 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7412 6910 603 41 0 7371 0
vsize: 29648
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 7405 0 0 0 10976 22 0 0 25 0 1 0 481915792 32235520 7376 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7870 7376 603 41 0 7829 0
vsize: 31480
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 8048 0 0 0 11975 23 0 0 25 0 1 0 481915792 34926592 8019 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8527 8019 603 41 0 8486 0
vsize: 34108
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 8596 0 0 0 12974 25 0 0 25 0 1 0 481915792 37228544 8567 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9089 8567 603 41 0 9048 0
vsize: 36356
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 9064 0 0 0 13972 27 0 0 25 0 1 0 481915792 39108608 9035 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9548 9036 603 41 0 9507 0
vsize: 38192
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 9508 0 0 0 14971 28 0 0 25 0 1 0 481915792 40890368 9479 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9983 9479 603 41 0 9942 0
vsize: 39932
[startup+160.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 9896 0 0 0 15970 29 0 0 25 0 1 0 481915792 42577920 9867 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10395 9867 603 41 0 10354 0
vsize: 41580
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 10240 0 0 0 16969 30 0 0 25 0 1 0 481915792 44040192 10211 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10752 10211 603 41 0 10711 0
vsize: 43008
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 10565 0 0 0 17968 31 0 0 25 0 1 0 481915792 45383680 10536 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11080 10536 603 41 0 11039 0
vsize: 44320
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 10857 0 0 0 18968 32 0 0 25 0 1 0 481915792 46592000 10828 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11375 10828 603 41 0 11334 0
vsize: 45500
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 11152 0 0 0 19968 32 0 0 25 0 1 0 481915792 47812608 11123 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11673 11123 603 41 0 11632 0
vsize: 46692
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32457
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 11460 0 0 0 20966 34 0 0 25 0 1 0 481915792 49106944 11431 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11989 11431 603 41 0 11948 0
vsize: 47956
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 11800 0 0 0 21965 35 0 0 25 0 1 0 481915792 50597888 11771 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12353 11771 603 41 0 12312 0
vsize: 49412
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12070 0 0 0 22964 37 0 0 25 0 1 0 481915792 51679232 12041 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12617 12041 603 41 0 12576 0
vsize: 50468
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12353 0 0 0 23964 37 0 0 25 0 1 0 481915792 52764672 12324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12882 12324 603 41 0 12841 0
vsize: 51528
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 24963 37 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 25963 37 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 26964 37 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 27964 37 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 28964 38 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 29964 38 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12375 0 0 0 30964 38 0 0 25 0 1 0 481915792 52899840 12346 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12915 12346 603 41 0 12874 0
vsize: 51660
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12385 0 0 0 31964 38 0 0 25 0 1 0 481915792 53047296 12356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12951 12356 603 41 0 12910 0
vsize: 51804
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12386 0 0 0 32964 38 0 0 25 0 1 0 481915792 53047296 12357 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12951 12357 603 41 0 12910 0
vsize: 51804
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12388 0 0 0 33964 38 0 0 25 0 1 0 481915792 53047296 12359 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12951 12359 603 41 0 12910 0
vsize: 51804
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12474 0 0 0 34964 38 0 0 25 0 1 0 481915792 53313536 12445 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13016 12445 603 41 0 12975 0
vsize: 52064
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 12958 0 0 0 35964 39 0 0 25 0 1 0 481915792 55332864 12929 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13509 12929 603 41 0 13468 0
vsize: 54036
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 13467 0 0 0 36962 41 0 0 25 0 1 0 481915792 57475072 13438 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14032 13438 603 41 0 13991 0
vsize: 56128
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 13994 0 0 0 37961 43 0 0 25 0 1 0 481915792 59621376 13965 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14556 13965 603 41 0 14515 0
vsize: 58224
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 14399 0 0 0 38960 44 0 0 25 0 1 0 481915792 61227008 14370 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14948 14370 603 41 0 14907 0
vsize: 59792
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 14834 0 0 0 39959 45 0 0 25 0 1 0 481915792 63107072 14805 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15407 14805 603 41 0 15366 0
vsize: 61628
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 15233 0 0 0 40958 46 0 0 25 0 1 0 481915792 64708608 15204 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15798 15204 603 41 0 15757 0
vsize: 63192
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 15586 0 0 0 41957 47 0 0 25 0 1 0 481915792 66179072 15557 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16157 15557 603 41 0 16116 0
vsize: 64628
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 15951 0 0 0 42956 49 0 0 25 0 1 0 481915792 67653632 15922 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16517 15923 603 41 0 16476 0
vsize: 66068
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 16276 0 0 0 43955 49 0 0 25 0 1 0 481915792 69058560 16247 4294967295 134512640 134672761 3221224576 3221223664 134555602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16860 16247 603 41 0 16819 0
vsize: 67440
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 16607 0 0 0 44955 50 0 0 25 0 1 0 481915792 70389760 16578 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17185 16578 603 41 0 17144 0
vsize: 68740
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 16927 0 0 0 45954 51 0 0 25 0 1 0 481915792 71741440 16898 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17515 16898 603 41 0 17474 0
vsize: 70060
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 17247 0 0 0 46954 51 0 0 25 0 1 0 481915792 73089024 17218 4294967295 134512640 134672761 3221224576 3221223744 134561086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17844 17218 603 41 0 17803 0
vsize: 71376
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 17586 0 0 0 47953 52 0 0 25 0 1 0 481915792 74424320 17557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18170 17557 603 41 0 18129 0
vsize: 72680
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 18022 0 0 0 48951 54 0 0 25 0 1 0 481915792 76185600 17993 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18600 17993 603 41 0 18559 0
vsize: 74400
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 18308 0 0 0 49950 55 0 0 25 0 1 0 481915792 77406208 18279 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18898 18279 603 41 0 18857 0
vsize: 75592
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 18608 0 0 0 50949 56 0 0 25 0 1 0 481915792 78610432 18579 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19192 18579 603 41 0 19151 0
vsize: 76768
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 18856 0 0 0 51949 57 0 0 25 0 1 0 481915792 79548416 18827 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19421 18827 603 41 0 19380 0
vsize: 77684
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 52948 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 53948 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 54949 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 55949 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 56949 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 57949 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 58949 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223680 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 59950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 60950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 61950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 62950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 63950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 64950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 65950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 66950 58 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19032 0 0 0 67950 59 0 0 25 0 1 0 481915792 80883712 19003 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19747 19003 603 41 0 19706 0
vsize: 78988
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19247 0 0 0 68950 59 0 0 25 0 1 0 481915792 81678336 19218 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19941 19218 603 41 0 19900 0
vsize: 79764
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 19857 0 0 0 69948 61 0 0 25 0 1 0 481915792 84230144 19828 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20564 19828 603 41 0 20523 0
vsize: 82256
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 20448 0 0 0 70946 63 0 0 25 0 1 0 481915792 86638592 20419 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21152 20419 603 41 0 21111 0
vsize: 84608
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 21124 0 0 0 71945 65 0 0 25 0 1 0 481915792 89456640 21095 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21840 21095 603 41 0 21799 0
vsize: 87360
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 21647 0 0 0 72943 67 0 0 25 0 1 0 481915792 91615232 21618 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22367 21618 603 41 0 22326 0
vsize: 89468
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22194 0 0 0 73941 69 0 0 25 0 1 0 481915792 93765632 22165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22892 22165 603 41 0 22851 0
vsize: 91568
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22778 0 0 0 74940 71 0 0 25 0 1 0 481915792 96194560 22749 4294967295 134512640 134672761 3221224576 3221223728 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23485 22749 603 41 0 23444 0
vsize: 93940
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22974 0 0 0 75939 71 0 0 25 0 1 0 481915792 97001472 22945 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22945 603 41 0 23641 0
vsize: 94728
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22975 0 0 0 76939 72 0 0 25 0 1 0 481915792 97001472 22946 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22946 603 41 0 23641 0
vsize: 94728
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22975 0 0 0 77939 72 0 0 25 0 1 0 481915792 97001472 22946 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22946 603 41 0 23641 0
vsize: 94728
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22975 0 0 0 78939 72 0 0 25 0 1 0 481915792 97001472 22946 4294967295 134512640 134672761 3221224576 3221223760 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22946 603 41 0 23641 0
vsize: 94728
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 79939 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 80939 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 81939 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 82939 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 83940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 84940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 85940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 86940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 87940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22976 0 0 0 88940 72 0 0 25 0 1 0 481915792 97001472 22947 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22947 603 41 0 23641 0
vsize: 94728
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22977 0 0 0 89940 72 0 0 25 0 1 0 481915792 97001472 22948 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22948 603 41 0 23641 0
vsize: 94728
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22977 0 0 0 90940 73 0 0 25 0 1 0 481915792 97001472 22948 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22948 603 41 0 23641 0
vsize: 94728
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22977 0 0 0 91940 73 0 0 25 0 1 0 481915792 97001472 22948 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22948 603 41 0 23641 0
vsize: 94728
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22977 0 0 0 92940 73 0 0 25 0 1 0 481915792 97001472 22948 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22948 603 41 0 23641 0
vsize: 94728
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 22977 0 0 0 93941 73 0 0 25 0 1 0 481915792 97001472 22948 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23682 22948 603 41 0 23641 0
vsize: 94728
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 23070 0 0 0 94940 73 0 0 25 0 1 0 481915792 97406976 23041 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23781 23041 603 41 0 23740 0
vsize: 95124
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 23630 0 0 0 95939 75 0 0 25 0 1 0 481915792 99704832 23601 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24342 23601 603 41 0 24301 0
vsize: 97368
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 24189 0 0 0 96937 77 0 0 25 0 1 0 481915792 102006784 24160 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24904 24160 603 41 0 24863 0
vsize: 99616
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 24757 0 0 0 97935 79 0 0 25 0 1 0 481915792 104296448 24728 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25463 24728 603 41 0 25422 0
vsize: 101852
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 25260 0 0 0 98933 81 0 0 25 0 1 0 481915792 106438656 25231 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25986 25231 603 41 0 25945 0
vsize: 103944
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 25737 0 0 0 99932 83 0 0 25 0 1 0 481915792 108318720 25708 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26445 25708 603 41 0 26404 0
vsize: 105780
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 26197 0 0 0 100931 83 0 0 25 0 1 0 481915792 110198784 26168 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26904 26169 603 41 0 26863 0
vsize: 107616
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 26701 0 0 0 101930 85 0 0 25 0 1 0 481915792 112353280 26672 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27430 26672 603 41 0 27389 0
vsize: 109720
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 27159 0 0 0 102928 87 0 0 25 0 1 0 481915792 114237440 27130 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27890 27130 603 41 0 27849 0
vsize: 111560
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 27703 0 0 0 103926 89 0 0 25 0 1 0 481915792 116383744 27674 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28414 27674 603 41 0 28373 0
vsize: 113656
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 28190 0 0 0 104925 90 0 0 25 0 1 0 481915792 118390784 28161 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28904 28161 603 41 0 28863 0
vsize: 115616
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 28652 0 0 0 105924 91 0 0 25 0 1 0 481915792 120270848 28623 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29363 28623 603 41 0 29322 0
vsize: 117452
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29147 0 0 0 106923 93 0 0 25 0 1 0 481915792 122318848 29118 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29863 29118 603 41 0 29822 0
vsize: 119452
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29545 0 0 0 107922 94 0 0 25 0 1 0 481915792 123932672 29516 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30257 29516 603 41 0 30216 0
vsize: 121028
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 108922 94 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 109922 94 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 110922 94 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 111922 94 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 112922 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 113922 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 114923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 115923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 116923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 117923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 118923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32459
Raw data (stat): 32457 (minisat+) R 32456 26298 26297 0 -1 0 29660 0 0 0 119923 95 0 0 25 0 1 0 481915792 124469248 29631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30388 29631 603 41 0 30347 0
vsize: 121552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32459
Raw data (stat): 32457 (minisat+) Z 32456 26298 26297 0 -1 12 29662 0 0 0 119923 100 0 0 25 0 1 0 481915792 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.25
CPU user time (s): 1199.24
CPU system time (s): 1.00685
CPU usage (%): 100.014
Max. virtual memory (Kb): 121552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####