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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
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.28
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 22295

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-22 02:39:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11907 boxname=wulflinc24 idbench=916 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-l152lav.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-l152lav.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-l152lav.opb
IDLAUNCH: 11907
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        468720 kB
Buffers:         34968 kB
Cached:         506468 kB
SwapCached:        524 kB
Active:         217672 kB
Inactive:       325768 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        468468 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16668 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:59:02 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 11907 7 1200.25 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]---> BDD-cost:75537
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]---> BDD-cost:56893
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  412764  1190247 |  137588       0        0     nan |  0.000 % |
c |       100 |  412764  1190247 |  151346     100     3757    37.6 |  0.066 % |
c |       250 |  412764  1190247 |  166481     250     7598    30.4 |  0.066 % |
c |       475 |  412764  1190247 |  183129     475    54404   114.5 |  0.066 % |
c |       812 |  412764  1190247 |  201442     812   195316   240.5 |  0.066 % |
c |      1319 |  412764  1190247 |  221586    1319   263810   200.0 |  0.066 % |
c |      2082 |  412764  1190247 |  243745    2082   346507   166.4 |  0.066 % |
c |      3223 |  412764  1190247 |  268120    3223   918568   285.0 |  0.066 % |
c |      4931 |  412764  1190247 |  294932    4931  1706139   346.0 |  0.066 % |
c |      7496 |  412764  1190247 |  324425    7496  3061447   408.4 |  0.066 % |
c |     11343 |  412764  1190247 |  356867   11343  5012779   441.9 |  0.066 % |
c |     17115 |  412764  1190247 |  392554   17115  7966858   465.5 |  0.066 % |
c |     25765 |  412764  1190247 |  431810   25765 14434558   560.2 |  0.066 % |
#### 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.94 0.90 2/54 22914
Raw data (stat): 22914 (runsolver) R 22913 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550181752 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 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 13771 0 0 0 964 34 0 0 25 0 1 0 550181752 63496192 12872 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15502 12872 603 41 0 15461 0
vsize: 62008
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 13988 0 0 0 1962 35 0 0 25 0 1 0 550181752 64434176 13089 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15731 13089 603 41 0 15690 0
vsize: 62924
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14174 0 0 0 2961 36 0 0 25 0 1 0 550181752 65101824 13275 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15894 13275 603 41 0 15853 0
vsize: 63576
[startup+40.0001 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14260 0 0 0 3961 36 0 0 25 0 1 0 550181752 65503232 13361 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15992 13361 603 41 0 15951 0
vsize: 63968
[startup+50 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14333 0 0 0 4961 36 0 0 25 0 1 0 550181752 65773568 13434 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 13434 603 41 0 16017 0
vsize: 64232
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14420 0 0 0 5961 37 0 0 25 0 1 0 550181752 66187264 13521 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16159 13521 603 41 0 16118 0
vsize: 64636
[startup+70.0001 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14528 0 0 0 6961 37 0 0 25 0 1 0 550181752 66596864 13629 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16259 13629 603 41 0 16218 0
vsize: 65036
[startup+80.0012 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14611 0 0 0 7961 37 0 0 25 0 1 0 550181752 66859008 13712 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16323 13712 603 41 0 16282 0
vsize: 65292
[startup+90.0006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14686 0 0 0 8960 38 0 0 25 0 1 0 550181752 67244032 13787 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16417 13787 603 41 0 16376 0
vsize: 65668
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14729 0 0 0 9960 38 0 0 25 0 1 0 550181752 67383296 13830 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16451 13830 603 41 0 16410 0
vsize: 65804
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14797 0 0 0 10960 38 0 0 25 0 1 0 550181752 67641344 13898 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16514 13898 603 41 0 16473 0
vsize: 66056
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 14870 0 0 0 11960 39 0 0 25 0 1 0 550181752 68046848 13971 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16613 13971 603 41 0 16572 0
vsize: 66452
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15019 0 0 0 12960 39 0 0 25 0 1 0 550181752 68571136 14120 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16741 14120 603 41 0 16700 0
vsize: 66964
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15173 0 0 0 13960 40 0 0 25 0 1 0 550181752 69251072 14274 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16907 14274 603 41 0 16866 0
vsize: 67628
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15310 0 0 0 14959 40 0 0 25 0 1 0 550181752 69763072 14411 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17032 14411 603 41 0 16991 0
vsize: 68128
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15470 0 0 0 15959 41 0 0 25 0 1 0 550181752 70418432 14571 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17192 14571 603 41 0 17151 0
vsize: 68768
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15543 0 0 0 16959 41 0 0 25 0 1 0 550181752 70680576 14644 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17256 14644 603 41 0 17215 0
vsize: 69024
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15672 0 0 0 17959 41 0 0 25 0 1 0 550181752 71225344 14773 4294967295 134512640 134672761 3221224528 3221223708 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17389 14773 603 41 0 17348 0
vsize: 69556
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15820 0 0 0 18959 41 0 0 25 0 1 0 550181752 71897088 14921 4294967295 134512640 134672761 3221224528 3221223632 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17553 14921 603 41 0 17512 0
vsize: 70212
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15881 0 0 0 19959 41 0 0 25 0 1 0 550181752 72155136 14982 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17616 14982 603 41 0 17575 0
vsize: 70464
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15895 0 0 0 20959 41 0 0 25 0 1 0 550181752 72155136 14996 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17616 14996 603 41 0 17575 0
vsize: 70464
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 15931 0 0 0 21959 41 0 0 25 0 1 0 550181752 72282112 15032 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17647 15032 603 41 0 17606 0
vsize: 70588
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16150 0 0 0 22959 42 0 0 25 0 1 0 550181752 73220096 15251 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17876 15251 603 41 0 17835 0
vsize: 71504
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16309 0 0 0 23959 43 0 0 25 0 1 0 550181752 73895936 15410 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18041 15410 603 41 0 18000 0
vsize: 72164
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16383 0 0 0 24959 43 0 0 25 0 1 0 550181752 74153984 15484 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18104 15484 603 41 0 18063 0
vsize: 72416
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16398 0 0 0 25959 43 0 0 25 0 1 0 550181752 74272768 15499 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 15499 603 41 0 18092 0
vsize: 72532
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16414 0 0 0 26959 43 0 0 25 0 1 0 550181752 74272768 15515 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 15515 603 41 0 18092 0
vsize: 72532
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16435 0 0 0 27959 43 0 0 25 0 1 0 550181752 74399744 15536 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18164 15536 603 41 0 18123 0
vsize: 72656
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16501 0 0 0 28959 43 0 0 25 0 1 0 550181752 74641408 15602 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18223 15602 603 41 0 18182 0
vsize: 72892
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16559 0 0 0 29959 43 0 0 25 0 1 0 550181752 74907648 15660 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18288 15660 603 41 0 18247 0
vsize: 73152
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16680 0 0 0 30959 44 0 0 25 0 1 0 550181752 75444224 15781 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18419 15781 603 41 0 18378 0
vsize: 73676
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16790 0 0 0 31959 44 0 0 25 0 1 0 550181752 75976704 15891 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 15891 603 41 0 18508 0
vsize: 74196
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 16958 0 0 0 32958 44 0 0 25 0 1 0 550181752 76709888 16059 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18728 16059 603 41 0 18687 0
vsize: 74912
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 17178 0 0 0 33958 45 0 0 25 0 1 0 550181752 77639680 16279 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18955 16279 603 41 0 18914 0
vsize: 75820
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 17410 0 0 0 34957 46 0 0 25 0 1 0 550181752 78585856 16511 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19186 16511 603 41 0 19145 0
vsize: 76744
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 17631 0 0 0 35957 47 0 0 25 0 1 0 550181752 79376384 16732 4294967295 134512640 134672761 3221224528 3221223632 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19379 16732 603 41 0 19338 0
vsize: 77516
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 17889 0 0 0 36956 47 0 0 25 0 1 0 550181752 80457728 16990 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19643 16990 603 41 0 19602 0
vsize: 78572
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 18164 0 0 0 37956 48 0 0 25 0 1 0 550181752 81653760 17265 4294967295 134512640 134672761 3221224528 3221223632 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19935 17265 603 41 0 19894 0
vsize: 79740
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 18552 0 0 0 38955 49 0 0 25 0 1 0 550181752 83267584 17653 4294967295 134512640 134672761 3221224528 3221223632 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20329 17653 603 41 0 20288 0
vsize: 81316
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 18900 0 0 0 39955 50 0 0 25 0 1 0 550181752 84615168 18001 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20658 18001 603 41 0 20617 0
vsize: 82632
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19120 0 0 0 40954 51 0 0 25 0 1 0 550181752 85561344 18221 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20889 18221 603 41 0 20848 0
vsize: 83556
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19323 0 0 0 41954 51 0 0 25 0 1 0 550181752 86372352 18424 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21087 18424 603 41 0 21046 0
vsize: 84348
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19576 0 0 0 42953 52 0 0 25 0 1 0 550181752 87445504 18677 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21349 18677 603 41 0 21308 0
vsize: 85396
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19803 0 0 0 43953 52 0 0 25 0 1 0 550181752 88375296 18904 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21576 18904 603 41 0 21535 0
vsize: 86304
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19942 0 0 0 44952 53 0 0 25 0 1 0 550181752 88915968 19043 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21708 19043 603 41 0 21667 0
vsize: 86832
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 19996 0 0 0 45952 53 0 0 25 0 1 0 550181752 89051136 19097 4294967295 134512640 134672761 3221224528 3221223632 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21741 19097 603 41 0 21700 0
vsize: 86964
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20104 0 0 0 46953 53 0 0 25 0 1 0 550181752 89583616 19205 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21871 19205 603 41 0 21830 0
vsize: 87484
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20180 0 0 0 47953 53 0 0 25 0 1 0 550181752 89849856 19281 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21936 19281 603 41 0 21895 0
vsize: 87744
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20269 0 0 0 48953 53 0 0 25 0 1 0 550181752 90259456 19370 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22036 19370 603 41 0 21995 0
vsize: 88144
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20333 0 0 0 49953 54 0 0 25 0 1 0 550181752 90529792 19434 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22102 19434 603 41 0 22061 0
vsize: 88408
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20391 0 0 0 50952 54 0 0 25 0 1 0 550181752 90664960 19492 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22135 19492 603 41 0 22094 0
vsize: 88540
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20405 0 0 0 51952 54 0 0 25 0 1 0 550181752 90804224 19506 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19506 603 41 0 22128 0
vsize: 88676
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20420 0 0 0 52953 54 0 0 25 0 1 0 550181752 90804224 19521 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19521 603 41 0 22128 0
vsize: 88676
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20442 0 0 0 53953 54 0 0 25 0 1 0 550181752 90939392 19543 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22202 19543 603 41 0 22161 0
vsize: 88808
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20463 0 0 0 54953 54 0 0 25 0 1 0 550181752 91074560 19564 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22235 19564 603 41 0 22194 0
vsize: 88940
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20485 0 0 0 55953 55 0 0 25 0 1 0 550181752 91074560 19586 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22235 19586 603 41 0 22194 0
vsize: 88940
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20514 0 0 0 56953 55 0 0 25 0 1 0 550181752 91209728 19615 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22268 19615 603 41 0 22227 0
vsize: 89072
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20534 0 0 0 57953 55 0 0 25 0 1 0 550181752 91344896 19635 4294967295 134512640 134672761 3221224528 3221223632 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22301 19635 603 41 0 22260 0
vsize: 89204
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20571 0 0 0 58953 55 0 0 25 0 1 0 550181752 91480064 19672 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 19672 603 41 0 22293 0
vsize: 89336
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20600 0 0 0 59953 55 0 0 25 0 1 0 550181752 91619328 19701 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19701 603 41 0 22327 0
vsize: 89472
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20615 0 0 0 60954 55 0 0 25 0 1 0 550181752 91619328 19716 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19716 603 41 0 22327 0
vsize: 89472
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20626 0 0 0 61954 55 0 0 25 0 1 0 550181752 91619328 19727 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19727 603 41 0 22327 0
vsize: 89472
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20636 0 0 0 62954 55 0 0 25 0 1 0 550181752 91754496 19737 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22401 19737 603 41 0 22360 0
vsize: 89604
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20692 0 0 0 63954 55 0 0 25 0 1 0 550181752 91889664 19793 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22434 19793 603 41 0 22393 0
vsize: 89736
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20810 0 0 0 64953 56 0 0 25 0 1 0 550181752 92426240 19911 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22565 19911 603 41 0 22524 0
vsize: 90260
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 20996 0 0 0 65953 56 0 0 25 0 1 0 550181752 93241344 20097 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22764 20097 603 41 0 22723 0
vsize: 91056
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 21224 0 0 0 66953 57 0 0 25 0 1 0 550181752 94171136 20325 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22991 20325 603 41 0 22950 0
vsize: 91964
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 21456 0 0 0 67952 58 0 0 25 0 1 0 550181752 95182848 20557 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23238 20557 603 41 0 23197 0
vsize: 92952
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 21722 0 0 0 68952 58 0 0 25 0 1 0 550181752 96247808 20823 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23498 20823 603 41 0 23457 0
vsize: 93992
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 21930 0 0 0 69951 59 0 0 25 0 1 0 550181752 97034240 21031 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23690 21031 603 41 0 23649 0
vsize: 94760
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22061 0 0 0 70951 59 0 0 25 0 1 0 550181752 97554432 21162 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23817 21162 603 41 0 23776 0
vsize: 95268
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22165 0 0 0 71951 59 0 0 25 0 1 0 550181752 98041856 21266 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23936 21266 603 41 0 23895 0
vsize: 95744
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22286 0 0 0 72951 60 0 0 25 0 1 0 550181752 98557952 21387 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24062 21387 603 41 0 24021 0
vsize: 96248
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22457 0 0 0 73951 60 0 0 25 0 1 0 550181752 99192832 21558 4294967295 134512640 134672761 3221224528 3221223632 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24217 21558 603 41 0 24176 0
vsize: 96868
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22692 0 0 0 74950 61 0 0 25 0 1 0 550181752 100245504 21793 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24474 21793 603 41 0 24433 0
vsize: 97896
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 22936 0 0 0 75949 62 0 0 25 0 1 0 550181752 101179392 22037 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24702 22037 603 41 0 24661 0
vsize: 98808
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 23229 0 0 0 76948 63 0 0 25 0 1 0 550181752 102367232 22330 4294967295 134512640 134672761 3221224528 3221223632 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24992 22330 603 41 0 24951 0
vsize: 99968
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 23462 0 0 0 77948 64 0 0 25 0 1 0 550181752 103288832 22563 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25217 22563 603 41 0 25176 0
vsize: 100868
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 23740 0 0 0 78946 65 0 0 25 0 1 0 550181752 104468480 22841 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25505 22841 603 41 0 25464 0
vsize: 102020
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 24013 0 0 0 79945 66 0 0 25 0 1 0 550181752 105664512 23114 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25797 23114 603 41 0 25756 0
vsize: 103188
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 24280 0 0 0 80944 67 0 0 25 0 1 0 550181752 106692608 23381 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26048 23381 603 41 0 26007 0
vsize: 104192
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 24566 0 0 0 81944 68 0 0 25 0 1 0 550181752 107884544 23667 4294967295 134512640 134672761 3221224528 3221223632 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26339 23667 603 41 0 26298 0
vsize: 105356
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 24824 0 0 0 82943 69 0 0 25 0 1 0 550181752 108953600 23925 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26600 23925 603 41 0 26559 0
vsize: 106400
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 25091 0 0 0 83942 70 0 0 25 0 1 0 550181752 110018560 24192 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26860 24192 603 41 0 26819 0
vsize: 107440
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 25354 0 0 0 84941 71 0 0 25 0 1 0 550181752 111050752 24455 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27112 24455 603 41 0 27071 0
vsize: 108448
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 25560 0 0 0 85941 72 0 0 25 0 1 0 550181752 111984640 24661 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27340 24661 603 41 0 27299 0
vsize: 109360
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 25828 0 0 0 86941 72 0 0 25 0 1 0 550181752 113020928 24929 4294967295 134512640 134672761 3221224528 3221223632 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27593 24929 603 41 0 27552 0
vsize: 110372
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 26102 0 0 0 87941 73 0 0 25 0 1 0 550181752 114081792 25203 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27852 25203 603 41 0 27811 0
vsize: 111408
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 26387 0 0 0 88940 73 0 0 25 0 1 0 550181752 115265536 25488 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28141 25488 603 41 0 28100 0
vsize: 112564
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 26659 0 0 0 89940 74 0 0 25 0 1 0 550181752 116428800 25760 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28425 25760 603 41 0 28384 0
vsize: 113700
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 26917 0 0 0 90939 74 0 0 25 0 1 0 550181752 117489664 26018 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28684 26018 603 41 0 28643 0
vsize: 114736
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 27164 0 0 0 91939 75 0 0 25 0 1 0 550181752 118542336 26265 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28941 26265 603 41 0 28900 0
vsize: 115764
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 27403 0 0 0 92938 76 0 0 25 0 1 0 550181752 119455744 26504 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29164 26504 603 41 0 29123 0
vsize: 116656
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 27731 0 0 0 93937 77 0 0 25 0 1 0 550181752 120811520 26832 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29495 26832 603 41 0 29454 0
vsize: 117980
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 27950 0 0 0 94937 78 0 0 25 0 1 0 550181752 121749504 27051 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27051 603 41 0 29683 0
vsize: 118896
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28233 0 0 0 95935 79 0 0 25 0 1 0 550181752 122810368 27334 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29983 27334 603 41 0 29942 0
vsize: 119932
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28311 0 0 0 96934 80 0 0 25 0 1 0 550181752 123219968 27412 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30083 27412 603 41 0 30042 0
vsize: 120332
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28361 0 0 0 97934 80 0 0 25 0 1 0 550181752 123355136 27462 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30116 27462 603 41 0 30075 0
vsize: 120464
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28397 0 0 0 98934 81 0 0 25 0 1 0 550181752 123490304 27498 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30149 27498 603 41 0 30108 0
vsize: 120596
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28423 0 0 0 99934 81 0 0 25 0 1 0 550181752 123625472 27524 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30182 27524 603 41 0 30141 0
vsize: 120728
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28445 0 0 0 100934 81 0 0 25 0 1 0 550181752 123760640 27546 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30215 27546 603 41 0 30174 0
vsize: 120860
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28475 0 0 0 101934 81 0 0 25 0 1 0 550181752 123887616 27576 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30246 27576 603 41 0 30205 0
vsize: 120984
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28506 0 0 0 102934 81 0 0 25 0 1 0 550181752 124022784 27607 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30279 27607 603 41 0 30238 0
vsize: 121116
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28539 0 0 0 103934 81 0 0 25 0 1 0 550181752 124149760 27640 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30310 27640 603 41 0 30269 0
vsize: 121240
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28565 0 0 0 104934 82 0 0 25 0 1 0 550181752 124280832 27666 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30342 27666 603 41 0 30301 0
vsize: 121368
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28590 0 0 0 105934 82 0 0 25 0 1 0 550181752 124280832 27691 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30342 27691 603 41 0 30301 0
vsize: 121368
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28606 0 0 0 106934 82 0 0 25 0 1 0 550181752 124399616 27707 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30371 27707 603 41 0 30330 0
vsize: 121484
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28625 0 0 0 107934 82 0 0 25 0 1 0 550181752 124542976 27726 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30406 27726 603 41 0 30365 0
vsize: 121624
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28649 0 0 0 108934 82 0 0 25 0 1 0 550181752 124526592 27750 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30402 27750 603 41 0 30361 0
vsize: 121608
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28664 0 0 0 109934 82 0 0 25 0 1 0 550181752 124661760 27765 4294967295 134512640 134672761 3221224528 3221223632 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 27765 603 41 0 30394 0
vsize: 121740
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28681 0 0 0 110935 82 0 0 25 0 1 0 550181752 124661760 27782 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 27782 603 41 0 30394 0
vsize: 121740
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28708 0 0 0 111934 83 0 0 25 0 1 0 550181752 124780544 27809 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30464 27809 603 41 0 30423 0
vsize: 121856
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28727 0 0 0 112934 83 0 0 25 0 1 0 550181752 124919808 27828 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30498 27828 603 41 0 30457 0
vsize: 121992
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28745 0 0 0 113935 83 0 0 25 0 1 0 550181752 124919808 27846 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30498 27846 603 41 0 30457 0
vsize: 121992
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28761 0 0 0 114935 83 0 0 25 0 1 0 550181752 125054976 27862 4294967295 134512640 134672761 3221224528 3221223632 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30531 27862 603 41 0 30490 0
vsize: 122124
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28780 0 0 0 115935 83 0 0 25 0 1 0 550181752 125054976 27881 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30531 27881 603 41 0 30490 0
vsize: 122124
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28808 0 0 0 116935 83 0 0 25 0 1 0 550181752 125186048 27909 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30563 27909 603 41 0 30522 0
vsize: 122252
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28833 0 0 0 117935 83 0 0 25 0 1 0 550181752 125325312 27934 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30597 27934 603 41 0 30556 0
vsize: 122388
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28852 0 0 0 118935 83 0 0 25 0 1 0 550181752 125444096 27953 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30626 27953 603 41 0 30585 0
vsize: 122504
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22914
Raw data (stat): 22914 (minisat+) R 22913 28546 28545 0 -1 0 28891 0 0 0 119935 83 0 0 25 0 1 0 550181752 125579264 27992 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30659 27992 603 41 0 30618 0
vsize: 122636
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22914
Raw data (stat): 22914 (minisat+) Z 22913 28546 28545 0 -1 12 28893 0 0 0 119935 89 0 0 25 0 1 0 550181752 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.25
CPU user time (s): 1199.36
CPU system time (s): 0.891864
CPU usage (%): 100.014
Max. virtual memory (Kb): 122636
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####