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/miplib3/normalized-mps-v2-13-7-l152lav.opb
MD5SUM	9d4ce12b138a2bef65a1f401ec9d1f01
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.69
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 15156

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        810096 kB
Buffers:         21556 kB
Cached:         175240 kB
SwapCached:        540 kB
Active:          91372 kB
Inactive:       107500 kB
HighTotal:      131008 kB
HighFree:         5236 kB
LowTotal:       903652 kB
LowFree:        804860 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20208 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:22:08 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 18484 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   97126   314221 |   29137       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24129          
c   -- var.elim.:  2000/24129          
c   -- var.elim.:  3000/24129          
c   -- var.elim.:  4000/24129          
c   -- var.elim.:  5000/24129          
c   -- var.elim.:  6000/24129          
c   -- var.elim.:  7000/24129          
c   -- var.eli#### 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 20460
Raw data (stat): 20460 (runsolver) R 20459 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541668466 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 6473 0 0 0 983 15 0 0 25 0 1 0 541668466 27369472 5572 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 5572 603 41 0 6641 0
vsize: 26728
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 6845 0 0 0 1983 15 0 0 25 0 1 0 541668466 28823552 5944 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 5944 603 41 0 6996 0
vsize: 28148
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 7270 0 0 0 2982 17 0 0 25 0 1 0 541668466 30556160 6369 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7460 6369 603 41 0 7419 0
vsize: 29840
[startup+40.001 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 7829 0 0 0 3981 18 0 0 25 0 1 0 541668466 32927744 6928 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8039 6928 603 41 0 7998 0
vsize: 32156
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 8348 0 0 0 4980 19 0 0 25 0 1 0 541668466 35041280 7447 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8555 7447 603 41 0 8514 0
vsize: 34220
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 9033 0 0 0 5977 22 0 0 25 0 1 0 541668466 37789696 8132 4294967295 134512640 134672761 3221224544 3221223536 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9226 8132 603 41 0 9185 0
vsize: 36904
[startup+70.0022 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 9826 0 0 0 6976 24 0 0 25 0 1 0 541668466 41074688 8925 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10028 8925 603 41 0 9987 0
vsize: 40112
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 11343 0 0 0 7970 29 0 0 25 0 1 0 541668466 47362048 10442 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11563 10442 603 41 0 11522 0
vsize: 46252
[startup+90.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 12313 0 0 0 8968 32 0 0 25 0 1 0 541668466 51331072 11412 4294967295 134512640 134672761 3221224544 3221223552 134522555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12532 11412 603 41 0 12491 0
vsize: 50128
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 13108 0 0 0 9965 35 0 0 25 0 1 0 541668466 54628352 12207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13337 12207 603 41 0 13296 0
vsize: 53348
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 13836 0 0 0 10963 37 0 0 25 0 1 0 541668466 57544704 12935 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14049 12935 603 41 0 14008 0
vsize: 56196
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 14524 0 0 0 11960 40 0 0 25 0 1 0 541668466 60334080 13623 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14730 13623 603 41 0 14689 0
vsize: 58920
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 15555 0 0 0 12957 43 0 0 25 0 1 0 541668466 64552960 14654 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15760 14654 603 41 0 15719 0
vsize: 63040
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 16748 0 0 0 13954 47 0 0 25 0 1 0 541668466 69419008 15847 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16948 15847 603 41 0 16907 0
vsize: 67792
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 18083 0 0 0 14950 50 0 0 25 0 1 0 541668466 74940416 17182 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18296 17182 603 41 0 18255 0
vsize: 73184
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 18875 0 0 0 15948 53 0 0 25 0 1 0 541668466 78110720 17974 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19070 17974 603 41 0 19029 0
vsize: 76280
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 19906 0 0 0 16946 55 0 0 25 0 1 0 541668466 82313216 19005 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20096 19005 603 41 0 20055 0
vsize: 80384
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 20953 0 0 0 17943 58 0 0 25 0 1 0 541668466 86900736 20052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21216 20052 603 41 0 21175 0
vsize: 84864
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20460
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 22193 0 0 0 18939 63 0 0 25 0 1 0 541668466 91918336 21292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22441 21292 603 41 0 22400 0
vsize: 89764
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 23369 0 0 0 19936 66 0 0 25 0 1 0 541668466 96792576 22468 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23631 22468 603 41 0 23590 0
vsize: 94524
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 24230 0 0 0 20934 68 0 0 25 0 1 0 541668466 100237312 23329 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24472 23329 603 41 0 24431 0
vsize: 97888
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 25494 0 0 0 21931 71 0 0 25 0 1 0 541668466 105472000 24593 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25750 24593 603 41 0 25709 0
vsize: 103000
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 27411 0 0 0 22927 75 0 0 25 0 1 0 541668466 113336320 26510 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27670 26510 603 41 0 27629 0
vsize: 110680
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 27869 0 0 0 23926 76 0 0 25 0 1 0 541668466 115163136 26968 4294967295 134512640 134672761 3221224544 3221223536 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28116 26968 603 41 0 28075 0
vsize: 112464
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 28928 0 0 0 24924 79 0 0 25 0 1 0 541668466 119492608 28027 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29173 28028 603 41 0 29132 0
vsize: 116692
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 30178 0 0 0 25921 82 0 0 25 0 1 0 541668466 124559360 29277 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30410 29277 603 41 0 30369 0
vsize: 121640
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 31084 0 0 0 26919 84 0 0 25 0 1 0 541668466 128348160 30183 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31335 30183 603 41 0 31294 0
vsize: 125340
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 32051 0 0 0 27917 86 0 0 25 0 1 0 541668466 132177920 31150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32270 31150 603 41 0 32229 0
vsize: 129080
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 32817 0 0 0 28915 88 0 0 25 0 1 0 541668466 135340032 31916 4294967295 134512640 134672761 3221224544 3221223416 1075352691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33042 31916 603 41 0 33001 0
vsize: 132168
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 33859 0 0 0 29913 91 0 0 25 0 1 0 541668466 139669504 32958 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34099 32958 603 41 0 34058 0
vsize: 136396
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 34602 0 0 0 30911 93 0 0 25 0 1 0 541668466 142708736 33701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34841 33701 603 41 0 34800 0
vsize: 139364
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 35570 0 0 0 31907 97 0 0 25 0 1 0 541668466 146673664 34669 4294967295 134512640 134672761 3221224544 3221223584 134614246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35809 34669 603 41 0 35768 0
vsize: 143236
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 36638 0 0 0 32905 99 0 0 25 0 1 0 541668466 151015424 35737 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36869 35737 603 41 0 36828 0
vsize: 147476
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 37459 0 0 0 33903 101 0 0 25 0 1 0 541668466 154284032 36558 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37667 36558 603 41 0 37626 0
vsize: 150668
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 38429 0 0 0 34901 104 0 0 25 0 1 0 541668466 158248960 37528 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38635 37528 603 41 0 38594 0
vsize: 154540
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 39383 0 0 0 35898 106 0 0 25 0 1 0 541668466 162193408 38482 4294967295 134512640 134672761 3221224544 3221223648 134604323 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39598 38482 603 41 0 39557 0
vsize: 158392
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 40497 0 0 0 36895 109 0 0 25 0 1 0 541668466 166764544 39596 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40714 39596 603 41 0 40673 0
vsize: 162856
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 41438 0 0 0 37892 112 0 0 25 0 1 0 541668466 170553344 40537 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41639 40537 603 41 0 41598 0
vsize: 166556
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 41928 0 0 0 38891 113 0 0 25 0 1 0 541668466 172625920 41027 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42145 41027 603 41 0 42104 0
vsize: 168580
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 42705 0 0 0 39890 115 0 0 25 0 1 0 541668466 175779840 41804 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42915 41804 603 41 0 42874 0
vsize: 171660
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 43049 0 0 0 40889 116 0 0 25 0 1 0 541668466 177238016 42148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43271 42148 603 41 0 43230 0
vsize: 173084
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 43615 0 0 0 41888 117 0 0 25 0 1 0 541668466 179486720 42714 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 42714 603 41 0 43779 0
vsize: 175280
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 43972 0 0 0 42887 118 0 0 25 0 1 0 541668466 180944896 43071 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44176 43071 603 41 0 44135 0
vsize: 176704
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 44311 0 0 0 43885 120 0 0 25 0 1 0 541668466 182378496 43410 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44526 43410 603 41 0 44485 0
vsize: 178104
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 44639 0 0 0 44884 121 0 0 25 0 1 0 541668466 183693312 43738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44847 43738 603 41 0 44806 0
vsize: 179388
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 45455 0 0 0 45882 123 0 0 25 0 1 0 541668466 187015168 44554 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45658 44554 603 41 0 45617 0
vsize: 182632
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 46499 0 0 0 46880 126 0 0 25 0 1 0 541668466 191336448 45598 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46713 45598 603 41 0 46672 0
vsize: 186852
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 46887 0 0 0 47879 127 0 0 25 0 1 0 541668466 192798720 45986 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47070 45986 603 41 0 47029 0
vsize: 188280
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 47547 0 0 0 48877 129 0 0 25 0 1 0 541668466 196087808 46646 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47873 46646 603 41 0 47832 0
vsize: 191492
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 48186 0 0 0 49875 131 0 0 25 0 1 0 541668466 198680576 47285 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48506 47285 603 41 0 48465 0
vsize: 194024
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 48716 0 0 0 50874 133 0 0 25 0 1 0 541668466 200794112 47815 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49022 47815 603 41 0 48981 0
vsize: 196088
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 49448 0 0 0 51871 135 0 0 25 0 1 0 541668466 203816960 48547 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49760 48547 603 41 0 49719 0
vsize: 199040
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 50512 0 0 0 52868 138 0 0 25 0 1 0 541668466 208166912 49611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50822 49611 603 41 0 50781 0
vsize: 203288
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 51142 0 0 0 53866 141 0 0 25 0 1 0 541668466 210817024 50241 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51469 50241 603 41 0 51428 0
vsize: 205876
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 51903 0 0 0 54864 143 0 0 25 0 1 0 541668466 213852160 51002 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52210 51002 603 41 0 52169 0
vsize: 208840
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 52533 0 0 0 55863 144 0 0 25 0 1 0 541668466 216485888 51632 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52853 51632 603 41 0 52812 0
vsize: 211412
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 53130 0 0 0 56862 146 0 0 25 0 1 0 541668466 218832896 52229 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53426 52229 603 41 0 53385 0
vsize: 213704
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 53812 0 0 0 57860 147 0 0 25 0 1 0 541668466 221614080 52911 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54105 52911 603 41 0 54064 0
vsize: 216420
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 54795 0 0 0 58858 150 0 0 25 0 1 0 541668466 225636352 53894 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55087 53894 603 41 0 55046 0
vsize: 220348
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 55959 0 0 0 59855 153 0 0 25 0 1 0 541668466 230428672 55058 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56257 55058 603 41 0 56216 0
vsize: 225028
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 56746 0 0 0 60853 155 0 0 25 0 1 0 541668466 233701376 55845 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57056 55845 603 41 0 57015 0
vsize: 228224
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 57461 0 0 0 61851 157 0 0 25 0 1 0 541668466 236580864 56560 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57759 56560 603 41 0 57718 0
vsize: 231036
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 58013 0 0 0 62850 158 0 0 25 0 1 0 541668466 238833664 57112 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58309 57112 603 41 0 58268 0
vsize: 233236
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 58779 0 0 0 63848 161 0 0 25 0 1 0 541668466 242003968 57878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59083 57878 603 41 0 59042 0
vsize: 236332
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 59658 0 0 0 64846 163 0 0 25 0 1 0 541668466 245522432 58757 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59942 58757 603 41 0 59901 0
vsize: 239768
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 60402 0 0 0 65844 165 0 0 25 0 1 0 541668466 248557568 59501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60683 59501 603 41 0 60642 0
vsize: 242732
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 61158 0 0 0 66842 167 0 0 25 0 1 0 541668466 251723776 60257 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61456 60257 603 41 0 61415 0
vsize: 245824
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 61867 0 0 0 67840 169 0 0 25 0 1 0 541668466 254611456 60966 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62161 60966 603 41 0 62120 0
vsize: 248644
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 62660 0 0 0 68838 171 0 0 25 0 1 0 541668466 257892352 61759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62962 61759 603 41 0 62921 0
vsize: 251848
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 63484 0 0 0 69837 173 0 0 25 0 1 0 541668466 261169152 62583 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63762 62583 603 41 0 63721 0
vsize: 255048
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 64269 0 0 0 70835 175 0 0 25 0 1 0 541668466 264462336 63368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64566 63368 603 41 0 64525 0
vsize: 258264
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 65286 0 0 0 71833 178 0 0 25 0 1 0 541668466 268521472 64385 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65557 64385 603 41 0 65516 0
vsize: 262228
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 66106 0 0 0 72830 181 0 0 25 0 1 0 541668466 271929344 65205 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66389 65205 603 41 0 66348 0
vsize: 265556
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 66917 0 0 0 73828 182 0 0 25 0 1 0 541668466 275218432 66016 4294967295 134512640 134672761 3221224544 3221223728 134615544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67192 66016 603 41 0 67151 0
vsize: 268768
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 67681 0 0 0 74827 184 0 0 25 0 1 0 541668466 278347776 66780 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67956 66780 603 41 0 67915 0
vsize: 271824
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 68697 0 0 0 75823 188 0 0 25 0 1 0 541668466 282591232 67796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68992 67796 603 41 0 68951 0
vsize: 275968
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 69894 0 0 0 76821 190 0 0 25 0 1 0 541668466 287465472 68993 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70182 68993 603 41 0 70141 0
vsize: 280728
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 70954 0 0 0 77819 193 0 0 25 0 1 0 541668466 291721216 70053 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71221 70053 603 41 0 71180 0
vsize: 284884
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 72058 0 0 0 78817 196 0 0 25 0 1 0 541668466 296263680 71157 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72330 71157 603 41 0 72289 0
vsize: 289320
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 73101 0 0 0 79814 198 0 0 25 0 1 0 541668466 300552192 72200 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73377 72200 603 41 0 73336 0
vsize: 293508
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 74178 0 0 0 80812 201 0 0 25 0 1 0 541668466 305041408 73277 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74473 73277 603 41 0 74432 0
vsize: 297892
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 75416 0 0 0 81810 203 0 0 25 0 1 0 541668466 310001664 74515 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75684 74515 603 41 0 75643 0
vsize: 302736
[startup+830.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76688 0 0 0 82807 207 0 0 25 0 1 0 541668466 315408384 75755 4294967295 134512640 134672761 3221224544 3221222592 134645412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75755 603 41 0 76963 0
vsize: 308016
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 83806 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 84807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 85807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 86807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 87807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 88807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+900.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 89807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 90807 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 91808 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 92808 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+940.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 93808 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+950.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 94808 207 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+960.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 95808 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+970.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 96809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+980.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 97809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 98809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 99809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 100809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 101809 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 102810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 103810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 104810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 105810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223744 134610654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 106810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 107810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 108810 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 109811 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 110811 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 111812 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 112812 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 113812 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 114812 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 115812 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 116813 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 117813 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 118813 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20462
Raw data (stat): 20460 (minisat+) R 20459 23176 23175 0 -1 0 76845 0 0 0 119813 208 0 0 25 0 1 0 541668466 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20462
Raw data (stat): 20460 (minisat+) Z 20459 23176 23175 0 -1 12 76845 0 0 0 119813 222 0 0 25 0 1 0 541668466 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.2
CPU time (s): 1200.36
CPU user time (s): 1198.14
CPU system time (s): 2.22466
CPU usage (%): 100.013
Max. virtual memory (Kb): 308016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####