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/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb
MD5SUM	8c44064d4224b1d41c28f152218dd39f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	98
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05084
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 15260

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 03:35:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18133 boxname=wulflinc3 idbench=1395 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c44064d4224b1d41c28f152218dd39f  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18133
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        518568 kB
Buffers:         33820 kB
Cached:         458920 kB
SwapCached:         56 kB
Active:          30428 kB
Inactive:       465144 kB
HighTotal:      131008 kB
HighFree:        43092 kB
LowTotal:       903652 kB
LowFree:        475476 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            14844 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:55:45 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 18133 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 272]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    7
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    6
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    6
c ---[ 229]---> BDD-cost:    7
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    6
c ---[ 224]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    7
c ---[ 212]---> Sorter-cost: 1902     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    6
c ---[ 164]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    6
c ---[ 162]---> BDD-cost:    6
c ---[ 161]---> BDD-cost:    6
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    7
c ---[ 158]---> BDD-cost:    6
c ---[ 157]---> BDD-cost:    6
c ---[ 156]---> BDD-cost:    6
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 150]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 149]---> BDD-cost:    7
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    5
c ---[ 146]---> BDD-cost:    5
c ---[ 145]---> BDD-cost:    5
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    7
c ---[ 142]---> BDD-cost:    5
c ---[ 141]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    7
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    6
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    6
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:    6
c ---[ 114]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:    5
c ---[ 107]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 105]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 103]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 101]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  99]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  97]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  95]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  91]---> Sorter-cost: 1881     Base: 2 2 2 2 5 5 2 2 2 5
c ---[  89]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[  87]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  85]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  83]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  81]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[  73]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  136
c ---[  65]---> BDD-cost:  283
c ---[  64]---> BDD-cost:  282
c ---[  63]---> BDD-cost:  470
c ---[  62]---> BDD-cost:  579
c ---[  61]---> BDD-cost:  572
c ---[  60]---> Sorter-cost:  306     Base: 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[  57]---> Sorter-cost:  801     Base: 2 2 2 2 2 5 2
c ---[  56]---> Sorter-cost:  819     Base: 2 2 2 2 2 5 2
c ---[  55]---> Sorter-cost: 1035     Base: 5 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1285     Base: 5 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1289     Base: 5 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[  48]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[  46]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[  44]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[  42]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[  40]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1063     Base: 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    7
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  171966   430214 |   51589       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/53660          
c   -- var.elim.:  2000/53660          
c   -- var.elim.:  3000/53660          
c   -- var.elim.:  4000/53660          
c   -- var.elim.:  5000/53660          
c   -- var.elim.:  6000/53660          
c   -- var.elim.:  7000/53660          
c   -- var.elim.:  8000/53660          
c   -- var.elim.:  9000/53660          
c   -- var.elim.:  10000/53660          
c   -- var.elim.:  11000/53660          
c   -- var.elim.:  12000/53660          
c   -- var.elim.:  13000/53660          
c   -- var.elim.:  14000/53660          
c   -- var.elim.:  15000/53660          
c   -- var.elim.:  16000/53660          
c   -- var.elim.:  17000/53660          
c   -- var.elim.:  18000/53660          
c   -- var.elim.:  19000/53660          
c   -- var.elim.:  20000/53660          
c   -- var.elim.:  21000/53660          
c   -- var.elim.:  22000/53660          
c   -- var.elim.:  23000/53660          
c   -- var.elim.:  24000/53660          
c   -- var.elim.:  25000/53660          
c   -- var.elim.:  26000/53660          
c   -- var.elim.:  27000/53660          
c   -- var.elim.:  28000/53660          
c   -- var.elim.:  29000/53660          
c   -- var.elim.:  30000/53660          
c   -- var.elim.:  31000/53660          
c   -- var.elim.:  32000/53660          
c   -- var.elim.:  33000/53660          
c   -- var.elim.:  34000/53660          
c   -- var.elim.:  35000/53660          
c   -- var.elim.:  36000/53660          
c   -- var.elim.:  37000/53660          
c   -- var.elim.:  38000/53660          
c   -- var.elim.:  39000/53660          
c   -- var.elim.:  40000/53660          
c   -- var.elim.:  41000/53660          
c   -- var.elim.:  42000/53660          
c   -- var.elim.:  43000/53660          
c   -- var.elim.:  44000/53660          
c   -- var.elim.:  45000/53660          
c   -- var.elim.:  46000/53660          
c   -- var.elim.:  47000/53660          
c   -- var.elim.:  48000/53660          
c   -- var.elim.:  49000/53660          
c   -- var.elim.:  50000/53660          
c   -- var.elim.:  51000/53660          
c   -- var.elim.:  52000/53660          
c   -- var.elim.:  53000/53660          
c   -- var.elim.:  53660/53660          
c   -- var.elim.:  1000/27395          
c   -- var.elim.:  2000/27395          
c   -- var.elim.:  3000/27395          
c   -- var.elim.:  4000/27395          
c   -- var.elim.:  5000/27395          
c   -- var.elim.:  6000/27395          
c   -- var.elim.:  7000/27395          
c   -- var.elim.:  8000/27395          
c   -- var.elim.:  9000/27395          
c   -- var.elim.:  10000/27395          
c   -- var.elim.:  11000/27395          
c   -- var.elim.:  12000/27395          
c   -- var.elim.:  13000/27395          
c   -- var.elim.:  14000/27395          
c   -- var.elim.:  15000/27395          
c   -- var.elim.:  16000/27395          
c   -- var.elim.:  17000/27395          
c   -- var.elim.:  18000/27395          
c   -- var.elim.:  19000/27395          
c   -- var.elim.:  20000/27395          
c   -- var.elim.:  21000/27395          
c   -- var.elim.:  22000/27395          
c   -- var.elim.:  23000/27395          
c   -- var.elim.:  24000/27395          
c   -- var.elim.:  25000/27395          
c   -- var.elim.:  26000/27395          
c   -- var.elim.:  27000/27395          
c   -- var.elim.:  27395/27395          
c   -- var.elim.:  357/357          
c   -- var.elim.:  17/17          
c   -- subsuming                       
c   -- var.elim.:  1000/5228          
c   -- var.elim.:  2000/5228          
c   -- var.elim.:  3000/5228          
c   -- var.elim.:  4000/5228          
c   -- var.elim.:  5000/5228          
c   -- var.elim.:  5228/5228          
c   -- var.elim.:  1000/2136          
c   -- var.elim.:  2000/2136          
c   -- var.elim.:  2136/2136          
c   -- var.elim.:  185/185          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  816/816          
c   -- var.elim.:  216/216          
c   -- var.elim.:  54/54          
c   -- subsuming                       
c   -- var.elim.:  76/76          
c   -- var.elim.:  73/73          
c |         0 |  145733   450954 |      --       0       --      -- |     --   | -19923/39478
c |         0 |  145733   450954 |   58293       0        0     nan |  0.000 % |
c |       100 |  145725   450926 |   64119      99      510     5.2 |  9.193 % |
c |       251 |  145725   450926 |   70530     250     1731     6.9 |  9.193 % |
c |       477 |  145582   450357 |   77507     474     5710    12.0 |  9.237 % |
c |       814 |  145582   450357 |   85258     811    15056    18.6 |  9.237 % |
c |      1322 |  145546   450236 |   93761    1318    24114    18.3 |  9.252 % |
c |      2082 |  144991   448127 |  102744    2056    35486    17.3 |  9.437 % |
c |      3221 |  144991   448127 |  113018    3195    97383    30.5 |  9.437 % |
c |      4929 |  144976   448069 |  124307    4896   188722    38.5 |  9.443 % |
c |      7493 |  144427   446005 |  136220    7433   271407    36.5 |  9.652 % |
c |     11337 |  144353   445708 |  149765   11257   413122    36.7 |  9.679 % |
c |     17104 |  143927   444155 |  164256   17011   960285    56.5 |  9.828 % |
c |     25753 |  143417   441991 |  180041   25545  1601773    62.7 |  9.975 % |
c |     38727 |  143119   440953 |  197634   38497  2914293    75.7 | 10.094 % |
c |     58189 |  141847   436339 |  215465   57916  3772341    65.1 | 10.566 % |
c |     87382 |  141564   435289 |  236539   87022  5094397    58.5 | 10.685 % |
c |    131173 |  141514   435115 |  260101  130806  8135856    62.2 | 10.703 % |
c |    196857 |  140943   433114 |  284956  196448 13333385    67.9 | 10.939 % |
c |    295383 |  140407   431056 |  312260   268#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 4235
Raw data (stat): 4235 (runsolver) R 4234 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483658466 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 9964 0 0 0 964 33 0 0 25 0 1 0 483658466 40316928 8582 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 8582 603 41 0 9802 0
vsize: 39372
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 10230 0 0 0 1963 34 0 0 25 0 1 0 483658466 41496576 8848 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10131 8848 603 41 0 10090 0
vsize: 40524
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 10715 0 0 0 2961 37 0 0 25 0 1 0 483658466 43606016 9333 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10646 9333 603 41 0 10605 0
vsize: 42584
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 11169 0 0 0 3959 38 0 0 25 0 1 0 483658466 45318144 9787 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11064 9787 603 41 0 11023 0
vsize: 44256
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 11921 0 0 0 4958 40 0 0 25 0 1 0 483658466 48480256 10539 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 10539 603 41 0 11795 0
vsize: 47344
[startup+60.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 12928 0 0 0 5955 43 0 0 25 0 1 0 483658466 52695040 11546 4294967295 134512640 134672761 3221224560 3221223744 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12865 11546 603 41 0 12824 0
vsize: 51460
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 13344 0 0 0 6954 44 0 0 25 0 1 0 483658466 54272000 11962 4294967295 134512640 134672761 3221224560 3221223600 134612670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13250 11962 603 41 0 13209 0
vsize: 53000
[startup+80.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 13679 0 0 0 7953 45 0 0 25 0 1 0 483658466 55599104 12297 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13574 12297 603 41 0 13533 0
vsize: 54296
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 14011 0 0 0 8953 46 0 0 25 0 1 0 483658466 56938496 12629 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13901 12629 603 41 0 13860 0
vsize: 55604
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 14329 0 0 0 9952 46 0 0 25 0 1 0 483658466 58535936 12947 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14291 12947 603 41 0 14250 0
vsize: 57164
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 14627 0 0 0 10951 48 0 0 25 0 1 0 483658466 59727872 13245 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14582 13245 603 41 0 14541 0
vsize: 58328
[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 14913 0 0 0 11952 48 0 0 25 0 1 0 483658466 60923904 13531 4294967295 134512640 134672761 3221224560 3221223760 134610614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14874 13531 603 41 0 14833 0
vsize: 59496
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 15238 0 0 0 12951 49 0 0 25 0 1 0 483658466 62242816 13856 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15196 13856 603 41 0 15155 0
vsize: 60784
[startup+140.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 15496 0 0 0 13951 50 0 0 25 0 1 0 483658466 63299584 14114 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15454 14114 603 41 0 15413 0
vsize: 61816
[startup+150.03 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 15745 0 0 0 14951 51 0 0 25 0 1 0 483658466 64237568 14363 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15683 14363 603 41 0 15642 0
vsize: 62732
[startup+160.03 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 16016 0 0 0 15951 52 0 0 25 0 1 0 483658466 65298432 14634 4294967295 134512640 134672761 3221224560 3221223696 134614656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15942 14634 603 41 0 15901 0
vsize: 63768
[startup+170.029 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 16291 0 0 0 16950 52 0 0 25 0 1 0 483658466 66494464 14909 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16234 14909 603 41 0 16193 0
vsize: 64936
[startup+180.029 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 16501 0 0 0 17950 53 0 0 25 0 1 0 483658466 67284992 15119 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16427 15119 603 41 0 16386 0
vsize: 65708
[startup+190.039 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 16756 0 0 0 18950 54 0 0 25 0 1 0 483658466 68345856 15374 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16686 15374 603 41 0 16645 0
vsize: 66744
[startup+200.039 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 17157 0 0 0 19948 55 0 0 25 0 1 0 483658466 70090752 15775 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17112 15775 603 41 0 17071 0
vsize: 68448
[startup+210.04 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 17323 0 0 0 20948 56 0 0 25 0 1 0 483658466 70762496 15941 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17276 15941 603 41 0 17235 0
vsize: 69104
[startup+220.041 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 17771 0 0 0 21947 58 0 0 25 0 1 0 483658466 72474624 16389 4294967295 134512640 134672761 3221224560 3221223664 134604522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17694 16389 603 41 0 17653 0
vsize: 70776
[startup+230.041 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 18374 0 0 0 22945 59 0 0 25 0 1 0 483658466 74973184 16992 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18304 16992 603 41 0 18263 0
vsize: 73216
[startup+240.041 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 18629 0 0 0 23945 60 0 0 25 0 1 0 483658466 76025856 17247 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18561 17247 603 41 0 18520 0
vsize: 74244
[startup+250.041 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 18860 0 0 0 24944 61 0 0 25 0 1 0 483658466 76980224 17478 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18794 17478 603 41 0 18753 0
vsize: 75176
[startup+260.042 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 19123 0 0 0 25944 61 0 0 25 0 1 0 483658466 78028800 17741 4294967295 134512640 134672761 3221224560 3221223936 134620485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19050 17741 603 41 0 19009 0
vsize: 76200
[startup+270.042 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 19275 0 0 0 26943 62 0 0 25 0 1 0 483658466 79097856 17893 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19311 17893 603 41 0 19270 0
vsize: 77244
[startup+280.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 19451 0 0 0 27943 63 0 0 25 0 1 0 483658466 79888384 18069 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19504 18069 603 41 0 19463 0
vsize: 78016
[startup+290.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 19717 0 0 0 28942 64 0 0 25 0 1 0 483658466 80949248 18335 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 18335 603 41 0 19722 0
vsize: 79052
[startup+300.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 19909 0 0 0 29942 64 0 0 25 0 1 0 483658466 81653760 18527 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19935 18527 603 41 0 19894 0
vsize: 79740
[startup+310.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 20544 0 0 0 30940 66 0 0 25 0 1 0 483658466 84287488 19162 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20578 19162 603 41 0 20537 0
vsize: 82312
[startup+320.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 21242 0 0 0 31938 68 0 0 25 0 1 0 483658466 87175168 19860 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21283 19860 603 41 0 21242 0
vsize: 85132
[startup+330.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 21493 0 0 0 32938 69 0 0 25 0 1 0 483658466 88227840 20111 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21540 20111 603 41 0 21499 0
vsize: 86160
[startup+340.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 21660 0 0 0 33937 69 0 0 25 0 1 0 483658466 88911872 20278 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21707 20278 603 41 0 21666 0
vsize: 86828
[startup+350.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 21846 0 0 0 34938 70 0 0 25 0 1 0 483658466 89718784 20464 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21904 20464 603 41 0 21863 0
vsize: 87616
[startup+360.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 22038 0 0 0 35938 70 0 0 25 0 1 0 483658466 90517504 20656 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22099 20656 603 41 0 22058 0
vsize: 88396
[startup+370.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 22214 0 0 0 36938 71 0 0 25 0 1 0 483658466 91181056 20832 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22261 20832 603 41 0 22220 0
vsize: 89044
[startup+380.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 22433 0 0 0 37937 71 0 0 25 0 1 0 483658466 92135424 21051 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22494 21051 603 41 0 22453 0
vsize: 89976
[startup+390.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 22638 0 0 0 38937 71 0 0 25 0 1 0 483658466 92921856 21256 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22686 21256 603 41 0 22645 0
vsize: 90744
[startup+400.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 22831 0 0 0 39937 72 0 0 25 0 1 0 483658466 93753344 21449 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22889 21449 603 41 0 22848 0
vsize: 91556
[startup+410.057 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23008 0 0 0 40936 73 0 0 25 0 1 0 483658466 94543872 21626 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23082 21626 603 41 0 23041 0
vsize: 92328
[startup+420.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23197 0 0 0 41935 74 0 0 25 0 1 0 483658466 95203328 21815 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23243 21815 603 41 0 23202 0
vsize: 92972
[startup+430.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23313 0 0 0 42935 74 0 0 25 0 1 0 483658466 95731712 21931 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23372 21931 603 41 0 23331 0
vsize: 93488
[startup+440.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23444 0 0 0 43937 74 0 0 25 0 1 0 483658466 96272384 22062 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23504 22062 603 41 0 23463 0
vsize: 94016
[startup+450.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23606 0 0 0 44936 75 0 0 25 0 1 0 483658466 96944128 22224 4294967295 134512640 134672761 3221224560 3221223704 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23668 22224 603 41 0 23627 0
vsize: 94672
[startup+460.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23754 0 0 0 45936 76 0 0 25 0 1 0 483658466 97603584 22372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23829 22372 603 41 0 23788 0
vsize: 95316
[startup+470.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23850 0 0 0 46936 76 0 0 25 0 1 0 483658466 97865728 22468 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23893 22468 603 41 0 23852 0
vsize: 95572
[startup+480.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 23978 0 0 0 47936 77 0 0 25 0 1 0 483658466 98398208 22596 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24023 22596 603 41 0 23982 0
vsize: 96092
[startup+490.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24125 0 0 0 48935 78 0 0 25 0 1 0 483658466 99057664 22743 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24184 22743 603 41 0 24143 0
vsize: 96736
[startup+500.087 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24276 0 0 0 49935 78 0 0 25 0 1 0 483658466 99586048 22894 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24313 22894 603 41 0 24272 0
vsize: 97252
[startup+510.095 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24533 0 0 0 50936 79 0 0 25 0 1 0 483658466 100638720 23151 4294967295 134512640 134672761 3221224560 3221223600 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24570 23151 603 41 0 24529 0
vsize: 98280
[startup+520.113 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24749 0 0 0 51937 80 0 0 25 0 1 0 483658466 101576704 23367 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24799 23367 603 41 0 24758 0
vsize: 99196
[startup+530.121 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24879 0 0 0 52937 80 0 0 25 0 1 0 483658466 102100992 23497 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24927 23497 603 41 0 24886 0
vsize: 99708
[startup+540.121 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 24995 0 0 0 53937 81 0 0 25 0 1 0 483658466 102625280 23613 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25055 23613 603 41 0 25014 0
vsize: 100220
[startup+550.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25089 0 0 0 54938 81 0 0 25 0 1 0 483658466 102887424 23707 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25119 23707 603 41 0 25078 0
vsize: 100476
[startup+560.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25304 0 0 0 55937 81 0 0 25 0 1 0 483658466 103813120 23922 4294967295 134512640 134672761 3221224560 3221223744 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25345 23922 603 41 0 25304 0
vsize: 101380
[startup+570.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25450 0 0 0 56937 82 0 0 25 0 1 0 483658466 104341504 24068 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25474 24068 603 41 0 25433 0
vsize: 101896
[startup+580.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25574 0 0 0 57937 82 0 0 25 0 1 0 483658466 104894464 24192 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25609 24192 603 41 0 25568 0
vsize: 102436
[startup+590.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25700 0 0 0 58936 83 0 0 25 0 1 0 483658466 105426944 24318 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25739 24318 603 41 0 25698 0
vsize: 102956
[startup+600.129 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 25862 0 0 0 59936 83 0 0 25 0 1 0 483658466 106090496 24480 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25901 24480 603 41 0 25860 0
vsize: 103604
[startup+610.129 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 26400 0 0 0 60935 84 0 0 25 0 1 0 483658466 108199936 25018 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26416 25018 603 41 0 26375 0
vsize: 105664
[startup+620.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 26915 0 0 0 61934 86 0 0 25 0 1 0 483658466 110301184 25533 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26929 25533 603 41 0 26888 0
vsize: 107716
[startup+630.13 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 27426 0 0 0 62933 87 0 0 25 0 1 0 483658466 112398336 26044 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27441 26044 603 41 0 27400 0
vsize: 109764
[startup+640.131 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 27847 0 0 0 63931 89 0 0 25 0 1 0 483658466 114102272 26465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27857 26465 603 41 0 27816 0
vsize: 111428
[startup+650.131 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 28208 0 0 0 64930 90 0 0 25 0 1 0 483658466 115675136 26826 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28241 26826 603 41 0 28200 0
vsize: 112964
[startup+660.131 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 28327 0 0 0 65930 90 0 0 25 0 1 0 483658466 116207616 26945 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26945 603 41 0 28330 0
vsize: 113484
[startup+670.131 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 28447 0 0 0 66930 91 0 0 25 0 1 0 483658466 116604928 27065 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28468 27065 603 41 0 28427 0
vsize: 113872
[startup+680.131 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 28579 0 0 0 67930 91 0 0 25 0 1 0 483658466 117129216 27197 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28596 27197 603 41 0 28555 0
vsize: 114384
[startup+690.132 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 28703 0 0 0 68930 91 0 0 25 0 1 0 483658466 117661696 27321 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28726 27321 603 41 0 28685 0
vsize: 114904
[startup+700.132 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 29089 0 0 0 69929 92 0 0 25 0 1 0 483658466 119259136 27707 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29116 27707 603 41 0 29075 0
vsize: 116464
[startup+710.132 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 29630 0 0 0 70928 93 0 0 25 0 1 0 483658466 121376768 28248 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29633 28248 603 41 0 29592 0
vsize: 118532
[startup+720.133 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30127 0 0 0 71927 95 0 0 25 0 1 0 483658466 123490304 28745 4294967295 134512640 134672761 3221224560 3221223704 134616356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30149 28745 603 41 0 30108 0
vsize: 120596
[startup+730.132 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30263 0 0 0 72927 95 0 0 25 0 1 0 483658466 124043264 28881 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30284 28881 603 41 0 30243 0
vsize: 121136
[startup+740.132 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30486 0 0 0 73926 96 0 0 25 0 1 0 483658466 124981248 29104 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30513 29104 603 41 0 30472 0
vsize: 122052
[startup+750.133 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30637 0 0 0 74926 96 0 0 25 0 1 0 483658466 125665280 29255 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30680 29255 603 41 0 30639 0
vsize: 122720
[startup+760.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30722 0 0 0 75926 96 0 0 25 0 1 0 483658466 125947904 29340 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30749 29340 603 41 0 30708 0
vsize: 122996
[startup+770.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30839 0 0 0 76926 96 0 0 25 0 1 0 483658466 126480384 29457 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30879 29457 603 41 0 30838 0
vsize: 123516
[startup+780.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 30950 0 0 0 77926 97 0 0 25 0 1 0 483658466 126877696 29568 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30976 29568 603 41 0 30935 0
vsize: 123904
[startup+790.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 31063 0 0 0 78926 97 0 0 25 0 1 0 483658466 127328256 29681 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31086 29681 603 41 0 31045 0
vsize: 124344
[startup+800.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 31329 0 0 0 79926 97 0 0 25 0 1 0 483658466 128499712 29947 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31372 29947 603 41 0 31331 0
vsize: 125488
[startup+810.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 31672 0 0 0 80925 98 0 0 25 0 1 0 483658466 129961984 30290 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31729 30290 603 41 0 31688 0
vsize: 126916
[startup+820.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 31816 0 0 0 81925 99 0 0 25 0 1 0 483658466 130490368 30434 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31858 30434 603 41 0 31817 0
vsize: 127432
[startup+830.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 31915 0 0 0 82925 99 0 0 25 0 1 0 483658466 130887680 30533 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31955 30533 603 41 0 31914 0
vsize: 127820
[startup+840.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 32092 0 0 0 83925 99 0 0 25 0 1 0 483658466 132726784 30710 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32404 30710 603 41 0 32363 0
vsize: 129616
[startup+850.134 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 32287 0 0 0 84924 100 0 0 25 0 1 0 483658466 133517312 30905 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32597 30905 603 41 0 32556 0
vsize: 130388
[startup+860.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 32624 0 0 0 85924 100 0 0 25 0 1 0 483658466 134836224 31242 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32919 31242 603 41 0 32878 0
vsize: 131676
[startup+870.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33095 0 0 0 86923 102 0 0 25 0 1 0 483658466 136794112 31713 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33397 31713 603 41 0 33356 0
vsize: 133588
[startup+880.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33464 0 0 0 87922 103 0 0 25 0 1 0 483658466 138240000 32082 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33750 32082 603 41 0 33709 0
vsize: 135000
[startup+890.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33551 0 0 0 88922 103 0 0 25 0 1 0 483658466 138637312 32169 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33847 32169 603 41 0 33806 0
vsize: 135388
[startup+900.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33683 0 0 0 89921 104 0 0 25 0 1 0 483658466 139173888 32301 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33978 32301 603 41 0 33937 0
vsize: 135912
[startup+910.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33801 0 0 0 90921 104 0 0 25 0 1 0 483658466 139571200 32419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34075 32419 603 41 0 34034 0
vsize: 136300
[startup+920.135 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 33928 0 0 0 91921 104 0 0 25 0 1 0 483658466 140103680 32546 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34205 32546 603 41 0 34164 0
vsize: 136820
[startup+930.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34065 0 0 0 92921 104 0 0 25 0 1 0 483658466 140627968 32683 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34333 32683 603 41 0 34292 0
vsize: 137332
[startup+940.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34162 0 0 0 93921 104 0 0 25 0 1 0 483658466 141021184 32780 4294967295 134512640 134672761 3221224560 3221223704 134616256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34429 32780 603 41 0 34388 0
vsize: 137716
[startup+950.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34493 0 0 0 94921 105 0 0 25 0 1 0 483658466 142340096 33111 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34751 33111 603 41 0 34710 0
vsize: 139004
[startup+960.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34564 0 0 0 95921 105 0 0 25 0 1 0 483658466 142606336 33182 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34816 33182 603 41 0 34775 0
vsize: 139264
[startup+970.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34640 0 0 0 96921 106 0 0 25 0 1 0 483658466 143052800 33258 4294967295 134512640 134672761 3221224560 3221223600 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34925 33258 603 41 0 34884 0
vsize: 139700
[startup+980.136 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34712 0 0 0 97921 106 0 0 25 0 1 0 483658466 143335424 33330 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34994 33330 603 41 0 34953 0
vsize: 139976
[startup+990.137 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34788 0 0 0 98921 106 0 0 25 0 1 0 483658466 143601664 33406 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35059 33406 603 41 0 35018 0
vsize: 140236
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34875 0 0 0 99921 106 0 0 25 0 1 0 483658466 143867904 33493 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35124 33493 603 41 0 35083 0
vsize: 140496
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 34958 0 0 0 100920 107 0 0 25 0 1 0 483658466 144269312 33576 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35222 33576 603 41 0 35181 0
vsize: 140888
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35050 0 0 0 101921 107 0 0 25 0 1 0 483658466 144560128 33668 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35293 33668 603 41 0 35252 0
vsize: 141172
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35544 0 0 0 102920 108 0 0 25 0 1 0 483658466 147980288 34162 4294967295 134512640 134672761 3221224560 3221223616 134644229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36128 34162 603 41 0 36087 0
vsize: 144512
[startup+1040.14 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 103919 108 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1050.14 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 104918 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1060.15 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 105918 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1070.15 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 106919 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1080.15 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 107919 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1090.16 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 108920 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1100.16 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 109920 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1110.17 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 110921 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1120.17 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 111921 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1130.17 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35666 0 0 0 112922 109 0 0 25 0 1 0 483658466 146931712 33996 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35872 33996 603 41 0 35831 0
vsize: 143488
[startup+1140.17 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 113922 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1150.17 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 114921 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1160.17 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 115921 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1170.18 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 116922 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1180.19 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 117923 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1190.19 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 118923 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
[startup+1200.19 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 4235
Raw data (stat): 4235 (minisat+) R 4234 10720 10719 0 -1 0 35699 0 0 0 119923 109 0 0 25 0 1 0 483658466 147193856 34029 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35936 34029 603 41 0 35895 0
vsize: 143744
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.01 1.01 0.93 1/54 4235
Raw data (stat): 4235 (minisat+) Z 4234 10720 10719 0 -1 12 35699 0 0 0 119924 116 0 0 24 0 1 0 483658466 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.28
CPU time (s): 1200.4
CPU user time (s): 1199.24
CPU system time (s): 1.16182
CPU usage (%): 100.011
Max. virtual memory (Kb): 144512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####