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 18800

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        553944 kB
Buffers:         20476 kB
Cached:         439408 kB
SwapCached:        544 kB
Active:          45068 kB
Inactive:       416836 kB
HighTotal:      131008 kB
HighFree:         3276 kB
LowTotal:       903652 kB
LowFree:        550668 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13276 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:57:52 (client local time) WITH STATUS 0 IN 1200.42 SECONDS
stats: 18127 7 1200.42 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  165709   413697 |   55236       0        0     nan |  0.000 % |
c |       100 |  165495   413208 |   60759      94      947    10.1 |  5.418 % |
c |       251 |  165314   412790 |   66835     226     2224     9.8 |  5.480 % |
c |       477 |  165314   412790 |   73519     452     3967     8.8 |  5.480 % |
c |       816 |  165234   412605 |   80871     788    11063    14.0 |  5.517 % |
c |      1322 |  164860   411732 |   88958    1280    20626    16.1 |  5.697 % |
c |      2082 |  164610   411172 |   97853    2026    32599    16.1 |  5.813 % |
c |      3221 |  164537   410996 |  107639    3162    52546    16.6 |  5.843 % |
c |      4929 |  163933   409623 |  118403    4818    80663    16.7 |  6.149 % |
c |      7491 |  163725   409156 |  130243    7366   135555    18.4 |  6.251 % |
c |     11337 |  163121   407793 |  143267   11144   248488    22.3 |  6.537 % |
c |     17104 |  162877   407028 |  157594   16896   384219    22.7 |  6.597 % |
c |     25753 |  162591   406266 |  173354   25528   603572    23.6 |  6.703 % |
c |     38729 |  162352   405711 |  190689   38435   884284    23.0 |  6.828 % |
c |     58190 |  161153   402950 |  209758   57788  1410528    24.4 |  7.403 % |
c |     87385 |  160609   401700 |  230734   86947  2606297    30.0 |  7.677 % |
c |    131174 |  159617   399421 |  253807  130619  3892752    29.8 |  8.165 % |
c |    196859 |  158407   396645 |  279188  196231  6193520    31.6 |  8.781 % |
c |    295385 |  157849   395376 |  307107   39157  1312286    33.5 |  9.069 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 19769
Raw data (stat): 19769 (runsolver) R 19768 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488355570 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 5220 0 0 0 985 13 0 0 25 0 1 0 488355570 24674304 5047 4294967295 134512640 134672761 3221224624 3221223808 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6024 5047 603 41 0 5983 0
vsize: 24096
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 5522 0 0 0 1984 14 0 0 25 0 1 0 488355570 25870336 5349 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6316 5349 603 41 0 6275 0
vsize: 25264
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 5829 0 0 0 2983 15 0 0 25 0 1 0 488355570 27197440 5656 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6640 5656 603 41 0 6599 0
vsize: 26560
[startup+39.9998 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 6113 0 0 0 3982 16 0 0 25 0 1 0 488355570 28266496 5940 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 5940 603 41 0 6860 0
vsize: 27604
[startup+50.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 6347 0 0 0 4981 17 0 0 25 0 1 0 488355570 29327360 6174 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7160 6174 603 41 0 7119 0
vsize: 28640
[startup+60.0001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 6583 0 0 0 5980 18 0 0 25 0 1 0 488355570 30265344 6410 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7389 6410 603 41 0 7348 0
vsize: 29556
[startup+70.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 6801 0 0 0 6980 18 0 0 25 0 1 0 488355570 31207424 6628 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7619 6628 603 41 0 7578 0
vsize: 30476
[startup+80.0007 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 6980 0 0 0 7979 19 0 0 25 0 1 0 488355570 31879168 6807 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7783 6807 603 41 0 7742 0
vsize: 31132
[startup+90.0005 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 7159 0 0 0 8979 20 0 0 25 0 1 0 488355570 32571392 6986 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7952 6986 603 41 0 7911 0
vsize: 31808
[startup+99.9997 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 7357 0 0 0 9979 21 0 0 25 0 1 0 488355570 33386496 7184 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8151 7184 603 41 0 8110 0
vsize: 32604
[startup+110 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 7573 0 0 0 10978 21 0 0 25 0 1 0 488355570 34586624 7400 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8444 7400 603 41 0 8403 0
vsize: 33776
[startup+120 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 7843 0 0 0 11978 22 0 0 25 0 1 0 488355570 35667968 7670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8708 7670 603 41 0 8667 0
vsize: 34832
[startup+130 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8139 0 0 0 12977 23 0 0 25 0 1 0 488355570 36896768 7966 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9008 7966 603 41 0 8967 0
vsize: 36032
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8267 0 0 0 13977 24 0 0 25 0 1 0 488355570 37437440 8094 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9140 8094 603 41 0 9099 0
vsize: 36560
[startup+150 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8414 0 0 0 14977 24 0 0 25 0 1 0 488355570 37990400 8241 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9275 8241 603 41 0 9234 0
vsize: 37100
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8573 0 0 0 15976 25 0 0 25 0 1 0 488355570 38678528 8400 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9443 8400 603 41 0 9402 0
vsize: 37772
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8706 0 0 0 16976 26 0 0 25 0 1 0 488355570 39211008 8533 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9573 8533 603 41 0 9532 0
vsize: 38292
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8840 0 0 0 17976 26 0 0 25 0 1 0 488355570 39743488 8667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9703 8667 603 41 0 9662 0
vsize: 38812
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 8977 0 0 0 18975 27 0 0 25 0 1 0 488355570 40280064 8804 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 8804 603 41 0 9793 0
vsize: 39336
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9073 0 0 0 19975 27 0 0 25 0 1 0 488355570 40693760 8900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8900 603 41 0 9894 0
vsize: 39740
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9166 0 0 0 20975 28 0 0 25 0 1 0 488355570 41103360 8993 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10035 8993 603 41 0 9994 0
vsize: 40140
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9303 0 0 0 21975 28 0 0 25 0 1 0 488355570 41644032 9130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10167 9130 603 41 0 10126 0
vsize: 40668
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9427 0 0 0 22974 29 0 0 25 0 1 0 488355570 42106880 9254 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10280 9254 603 41 0 10239 0
vsize: 41120
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9551 0 0 0 23974 30 0 0 25 0 1 0 488355570 42643456 9378 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9378 603 41 0 10370 0
vsize: 41644
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9640 0 0 0 24974 30 0 0 25 0 1 0 488355570 43040768 9467 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10508 9467 603 41 0 10467 0
vsize: 42032
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 9891 0 0 0 25974 31 0 0 25 0 1 0 488355570 43974656 9718 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10736 9718 603 41 0 10695 0
vsize: 42944
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10103 0 0 0 26973 31 0 0 25 0 1 0 488355570 44908544 9930 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10964 9930 603 41 0 10923 0
vsize: 43856
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10185 0 0 0 27974 32 0 0 25 0 1 0 488355570 45174784 10012 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11029 10012 603 41 0 10988 0
vsize: 44116
[startup+290.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10278 0 0 0 28974 32 0 0 25 0 1 0 488355570 45592576 10105 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10105 603 41 0 11090 0
vsize: 44524
[startup+300.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10421 0 0 0 29973 33 0 0 25 0 1 0 488355570 46649344 10248 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10248 603 41 0 11348 0
vsize: 45556
[startup+310.003 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10642 0 0 0 30973 33 0 0 25 0 1 0 488355570 47583232 10469 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 10469 603 41 0 11576 0
vsize: 46468
[startup+320.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10791 0 0 0 31973 34 0 0 25 0 1 0 488355570 48115712 10618 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11747 10618 603 41 0 11706 0
vsize: 46988
[startup+330.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 10887 0 0 0 32973 34 0 0 25 0 1 0 488355570 48521216 10714 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11846 10714 603 41 0 11805 0
vsize: 47384
[startup+340.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11037 0 0 0 33973 34 0 0 25 0 1 0 488355570 49111040 10864 4294967295 134512640 134672761 3221224624 3221223760 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11990 10864 603 41 0 11949 0
vsize: 47960
[startup+350.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11185 0 0 0 34973 35 0 0 25 0 1 0 488355570 49786880 11012 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12155 11012 603 41 0 12114 0
vsize: 48620
[startup+360.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11357 0 0 0 35973 35 0 0 25 0 1 0 488355570 50450432 11184 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12317 11184 603 41 0 12276 0
vsize: 49268
[startup+370.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11530 0 0 0 36972 36 0 0 25 0 1 0 488355570 51122176 11357 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12481 11357 603 41 0 12440 0
vsize: 49924
[startup+380.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11610 0 0 0 37972 36 0 0 25 0 1 0 488355570 51576832 11437 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12592 11437 603 41 0 12551 0
vsize: 50368
[startup+390.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11691 0 0 0 38972 36 0 0 25 0 1 0 488355570 51896320 11518 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 11518 603 41 0 12629 0
vsize: 50680
[startup+400.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11763 0 0 0 39973 36 0 0 25 0 1 0 488355570 52162560 11590 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 11590 603 41 0 12694 0
vsize: 50940
[startup+410.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11857 0 0 0 40973 37 0 0 25 0 1 0 488355570 52559872 11684 4294967295 134512640 134672761 3221224624 3221223716 1075351154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12832 11684 603 41 0 12791 0
vsize: 51328
[startup+420.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 11923 0 0 0 41973 37 0 0 25 0 1 0 488355570 52822016 11750 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12896 11750 603 41 0 12855 0
vsize: 51584
[startup+430.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12018 0 0 0 42973 37 0 0 25 0 1 0 488355570 53215232 11845 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12992 11845 603 41 0 12951 0
vsize: 51968
[startup+440.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12188 0 0 0 43973 38 0 0 25 0 1 0 488355570 53878784 12015 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13154 12015 603 41 0 13113 0
vsize: 52616
[startup+450.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12355 0 0 0 44973 38 0 0 25 0 1 0 488355570 54542336 12182 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13316 12182 603 41 0 13275 0
vsize: 53264
[startup+460.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12455 0 0 0 45973 38 0 0 25 0 1 0 488355570 55136256 12282 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13461 12282 603 41 0 13420 0
vsize: 53844
[startup+470.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12544 0 0 0 46973 39 0 0 25 0 1 0 488355570 55402496 12371 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13526 12371 603 41 0 13485 0
vsize: 54104
[startup+480.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12624 0 0 0 47973 39 0 0 25 0 1 0 488355570 55676928 12451 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13593 12451 603 41 0 13552 0
vsize: 54372
[startup+490.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12797 0 0 0 48973 39 0 0 25 0 1 0 488355570 56467456 12624 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13786 12624 603 41 0 13745 0
vsize: 55144
[startup+500.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12880 0 0 0 49973 39 0 0 25 0 1 0 488355570 56733696 12707 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13851 12707 603 41 0 13810 0
vsize: 55404
[startup+510.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 12967 0 0 0 50973 40 0 0 25 0 1 0 488355570 57131008 12794 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13948 12794 603 41 0 13907 0
vsize: 55792
[startup+520.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13049 0 0 0 51973 40 0 0 25 0 1 0 488355570 57397248 12876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14013 12876 603 41 0 13972 0
vsize: 56052
[startup+530.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13136 0 0 0 52974 40 0 0 25 0 1 0 488355570 57802752 12963 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14112 12963 603 41 0 14071 0
vsize: 56448
[startup+540.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13214 0 0 0 53974 40 0 0 25 0 1 0 488355570 58077184 13041 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14179 13041 603 41 0 14138 0
vsize: 56716
[startup+550.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13276 0 0 0 54974 41 0 0 25 0 1 0 488355570 58343424 13103 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14244 13103 603 41 0 14203 0
vsize: 56976
[startup+560.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13331 0 0 0 55974 41 0 0 25 0 1 0 488355570 58474496 13158 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14276 13158 603 41 0 14235 0
vsize: 57104
[startup+570.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13469 0 0 0 56973 42 0 0 25 0 1 0 488355570 59011072 13296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13296 603 41 0 14366 0
vsize: 57628
[startup+580.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13583 0 0 0 57973 42 0 0 25 0 1 0 488355570 59555840 13410 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14540 13410 603 41 0 14499 0
vsize: 58160
[startup+590.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13653 0 0 0 58974 42 0 0 25 0 1 0 488355570 59826176 13480 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14606 13480 603 41 0 14565 0
vsize: 58424
[startup+600.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13785 0 0 0 59974 43 0 0 25 0 1 0 488355570 60370944 13612 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14739 13612 603 41 0 14698 0
vsize: 58956
[startup+610.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13855 0 0 0 60974 43 0 0 25 0 1 0 488355570 60637184 13682 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14804 13682 603 41 0 14763 0
vsize: 59216
[startup+620.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13914 0 0 0 61974 43 0 0 25 0 1 0 488355570 60903424 13741 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14869 13741 603 41 0 14828 0
vsize: 59476
[startup+630.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 13962 0 0 0 62974 44 0 0 25 0 1 0 488355570 61034496 13789 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14901 13789 603 41 0 14860 0
vsize: 59604
[startup+640.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14038 0 0 0 63974 44 0 0 25 0 1 0 488355570 61317120 13865 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14970 13865 603 41 0 14929 0
vsize: 59880
[startup+650.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14116 0 0 0 64974 45 0 0 25 0 1 0 488355570 61710336 13943 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15066 13943 603 41 0 15025 0
vsize: 60264
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14189 0 0 0 65974 45 0 0 25 0 1 0 488355570 61992960 14016 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15135 14016 603 41 0 15094 0
vsize: 60540
[startup+670.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14269 0 0 0 66974 45 0 0 25 0 1 0 488355570 62406656 14096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15236 14096 603 41 0 15195 0
vsize: 60944
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14329 0 0 0 67974 45 0 0 25 0 1 0 488355570 62676992 14156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15302 14156 603 41 0 15261 0
vsize: 61208
[startup+690.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14464 0 0 0 68974 46 0 0 25 0 1 0 488355570 63213568 14291 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15433 14291 603 41 0 15392 0
vsize: 61732
[startup+700.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14639 0 0 0 69974 46 0 0 25 0 1 0 488355570 63877120 14466 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15595 14466 603 41 0 15554 0
vsize: 62380
[startup+710.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14794 0 0 0 70973 47 0 0 25 0 1 0 488355570 64540672 14621 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15757 14621 603 41 0 15716 0
vsize: 63028
[startup+720.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14837 0 0 0 71973 47 0 0 25 0 1 0 488355570 64679936 14664 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15791 14664 603 41 0 15750 0
vsize: 63164
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14873 0 0 0 72974 47 0 0 25 0 1 0 488355570 64811008 14700 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15823 14700 603 41 0 15782 0
vsize: 63292
[startup+740.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14922 0 0 0 73974 47 0 0 25 0 1 0 488355570 64942080 14749 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 14749 603 41 0 15814 0
vsize: 63420
[startup+750.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 14967 0 0 0 74974 47 0 0 25 0 1 0 488355570 65208320 14794 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15920 14794 603 41 0 15879 0
vsize: 63680
[startup+760.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15015 0 0 0 75975 48 0 0 25 0 1 0 488355570 65343488 14842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15953 14842 603 41 0 15912 0
vsize: 63812
[startup+770.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15073 0 0 0 76975 48 0 0 25 0 1 0 488355570 65748992 14900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16052 14900 603 41 0 16011 0
vsize: 64208
[startup+780.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15125 0 0 0 77975 48 0 0 25 0 1 0 488355570 65880064 14952 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16084 14952 603 41 0 16043 0
vsize: 64336
[startup+790.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15175 0 0 0 78975 48 0 0 25 0 1 0 488355570 66015232 15002 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16117 15002 603 41 0 16076 0
vsize: 64468
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15231 0 0 0 79975 48 0 0 25 0 1 0 488355570 66277376 15058 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16181 15058 603 41 0 16140 0
vsize: 64724
[startup+810.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15292 0 0 0 80975 49 0 0 25 0 1 0 488355570 66695168 15119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16283 15119 603 41 0 16242 0
vsize: 65132
[startup+820.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15346 0 0 0 81976 49 0 0 25 0 1 0 488355570 66826240 15173 4294967295 134512640 134672761 3221224624 3221223792 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16315 15173 603 41 0 16274 0
vsize: 65260
[startup+830.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15462 0 0 0 82976 49 0 0 25 0 1 0 488355570 67350528 15289 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16443 15289 603 41 0 16402 0
vsize: 65772
[startup+840.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15551 0 0 0 83976 49 0 0 25 0 1 0 488355570 67645440 15378 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16515 15378 603 41 0 16474 0
vsize: 66060
[startup+850.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15662 0 0 0 84976 50 0 0 25 0 1 0 488355570 68046848 15489 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16613 15489 603 41 0 16572 0
vsize: 66452
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15800 0 0 0 85976 50 0 0 25 0 1 0 488355570 68698112 15627 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16772 15627 603 41 0 16731 0
vsize: 67088
[startup+870.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15846 0 0 0 86976 50 0 0 25 0 1 0 488355570 68837376 15673 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16806 15673 603 41 0 16765 0
vsize: 67224
[startup+880.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15892 0 0 0 87976 50 0 0 25 0 1 0 488355570 68968448 15719 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16838 15719 603 41 0 16797 0
vsize: 67352
[startup+890.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 15969 0 0 0 88976 51 0 0 25 0 1 0 488355570 69427200 15796 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 15796 603 41 0 16909 0
vsize: 67800
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16052 0 0 0 89976 51 0 0 25 0 1 0 488355570 69795840 15879 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17040 15879 603 41 0 16999 0
vsize: 68160
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16180 0 0 0 90977 51 0 0 25 0 1 0 488355570 71372800 16007 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17425 16007 603 41 0 17384 0
vsize: 69700
[startup+920.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16293 0 0 0 91977 51 0 0 25 0 1 0 488355570 71790592 16120 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17527 16120 603 41 0 17486 0
vsize: 70108
[startup+930.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16352 0 0 0 92977 51 0 0 25 0 1 0 488355570 72089600 16179 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17600 16179 603 41 0 17559 0
vsize: 70400
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16420 0 0 0 93977 51 0 0 25 0 1 0 488355570 72396800 16247 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17675 16247 603 41 0 17634 0
vsize: 70700
[startup+950.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16458 0 0 0 94977 52 0 0 25 0 1 0 488355570 72527872 16285 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17707 16285 603 41 0 17666 0
vsize: 70828
[startup+960.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 16610 0 0 0 95977 52 0 0 25 0 1 0 488355570 73199616 16437 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17871 16437 603 41 0 17830 0
vsize: 71484
[startup+970.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17002 0 0 0 96976 54 0 0 25 0 1 0 488355570 74801152 16829 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18262 16829 603 41 0 18221 0
vsize: 73048
[startup+980.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17226 0 0 0 97976 54 0 0 25 0 1 0 488355570 75608064 17053 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18459 17053 603 41 0 18418 0
vsize: 73836
[startup+990.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17268 0 0 0 98976 54 0 0 25 0 1 0 488355570 75870208 17095 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18523 17095 603 41 0 18482 0
vsize: 74092
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17310 0 0 0 99976 54 0 0 25 0 1 0 488355570 76001280 17137 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18555 17137 603 41 0 18514 0
vsize: 74220
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17385 0 0 0 100976 55 0 0 25 0 1 0 488355570 76267520 17212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18620 17212 603 41 0 18579 0
vsize: 74480
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17476 0 0 0 101976 55 0 0 25 0 1 0 488355570 76673024 17303 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17303 603 41 0 18678 0
vsize: 74876
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 102977 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 103977 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223728 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 104977 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223728 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 105977 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 106977 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 107978 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 108978 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 109978 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 110979 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 111979 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 112980 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 113980 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 114980 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 115981 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223808 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 116981 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 117981 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 118982 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 19769
Raw data (stat): 19769 (minisat+) R 19768 29653 29652 0 -1 0 17495 0 0 0 119982 55 0 0 25 0 1 0 488355570 76673024 17322 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 17322 603 41 0 18678 0
vsize: 74876
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 19769
Raw data (stat): 19769 (minisat+) Z 19768 29653 29652 0 -1 12 17497 0 0 0 119982 59 0 0 25 0 1 0 488355570 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.06
CPU time (s): 1200.42
CPU user time (s): 1199.83
CPU system time (s): 0.59191
CPU usage (%): 100.029
Max. virtual memory (Kb): 74876
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####