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/miplib3/normalized-mps-v2-20-10-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	4742
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.33
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 21400

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        377552 kB
Buffers:         29760 kB
Cached:         604612 kB
SwapCached:          0 kB
Active:         244336 kB
Inactive:       392808 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        377300 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14152 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:04:02 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 13494 7 1200.18 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  123819   394251 |   41273       0        0     nan |  0.000 % |
c |       100 |  123689   393805 |   45400      82     1033    12.6 |  0.582 % |
c |       250 |  123611   393519 |   49940     223    12255    55.0 |  0.635 % |
c |       476 |  123592   393454 |   54934     446    25868    58.0 |  0.651 % |
c |       813 |  123592   393454 |   60427     783    31769    40.6 |  0.651 % |
c |      1319 |  122327   388987 |   66470    1056    36336    34.4 |  1.522 % |
c |      2078 |  122067   388081 |   73117    1773    50521    28.5 |  1.722 % |
c |      3217 |  122033   387971 |   80429    2908   115105    39.6 |  1.750 % |
c |      4925 |  121872   387428 |   88472    4589   198107    43.2 |  1.864 % |
c |      7487 |  121369   385669 |   97319    7065   281333    39.8 |  2.222 % |
c |     11331 |  121046   384558 |  107051   10860   383375    35.3 |  2.446 % |
c |     17097 |  120433   382447 |  117756   16530   595557    36.0 |  2.816 % |
c |     25746 |  120172   381574 |  129532   25104  1198644    47.7 |  2.979 % |
c |     38722 |  120096   381316 |  142485   38063  3051886    80.2 |  3.020 % |
c |     58183 |  119808   380306 |  156734   57411  5055291    88.1 |  3.158 % |
c |     87381 |  119754   380120 |  172407   86599 15798491   182.4 |  3.183 % |
c |    131170 |  119668   379828 |  189648  130372 30883892   236.9 |  3.228 % |
#### 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.81 0.93 0.90 2/54 29989
Raw data (stat): 29989 (runsolver) R 29988 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490913612 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0053 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 4362 0 0 0 977 11 0 0 24 0 1 0 490913612 19894272 3998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4857 3998 603 41 0 4816 0
vsize: 19428
[startup+20.0143 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 4566 0 0 0 1977 12 0 0 25 0 1 0 490913612 20840448 4202 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5088 4202 603 41 0 5047 0
vsize: 20352
[startup+30.0144 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 4676 0 0 0 2976 13 0 0 25 0 1 0 490913612 21295104 4312 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5199 4312 603 41 0 5158 0
vsize: 20796
[startup+40.0147 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 4834 0 0 0 3976 13 0 0 25 0 1 0 490913612 21835776 4470 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5331 4470 603 41 0 5290 0
vsize: 21324
[startup+50.015 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 5001 0 0 0 4975 14 0 0 25 0 1 0 490913612 22630400 4637 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5525 4637 603 41 0 5484 0
vsize: 22100
[startup+60.0147 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 5272 0 0 0 5974 16 0 0 25 0 1 0 490913612 23732224 4908 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5794 4908 603 41 0 5753 0
vsize: 23176
[startup+70.0163 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 5609 0 0 0 6973 17 0 0 25 0 1 0 490913612 25079808 5245 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6123 5245 603 41 0 6082 0
vsize: 24492
[startup+80.0173 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 6081 0 0 0 7972 18 0 0 25 0 1 0 490913612 26972160 5717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6585 5717 603 41 0 6544 0
vsize: 26340
[startup+90.017 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 6678 0 0 0 8970 20 0 0 25 0 1 0 490913612 29392896 6314 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7176 6314 603 41 0 7135 0
vsize: 28704
[startup+100.017 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 7165 0 0 0 9969 22 0 0 25 0 1 0 490913612 31539200 6801 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7700 6801 603 41 0 7659 0
vsize: 30800
[startup+110.018 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 7480 0 0 0 10968 23 0 0 25 0 1 0 490913612 32874496 7116 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8026 7116 603 41 0 7985 0
vsize: 32104
[startup+120.018 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 7845 0 0 0 11966 24 0 0 25 0 1 0 490913612 34336768 7481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8383 7481 603 41 0 8342 0
vsize: 33532
[startup+130.019 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 8220 0 0 0 12965 26 0 0 25 0 1 0 490913612 35807232 7856 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8742 7856 603 41 0 8701 0
vsize: 34968
[startup+140.019 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 8646 0 0 0 13964 27 0 0 25 0 1 0 490913612 37552128 8282 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9168 8282 603 41 0 9127 0
vsize: 36672
[startup+150.02 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 8942 0 0 0 14963 28 0 0 25 0 1 0 490913612 38764544 8578 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9464 8578 603 41 0 9423 0
vsize: 37856
[startup+160.02 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 9105 0 0 0 15962 29 0 0 25 0 1 0 490913612 39436288 8741 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9628 8741 603 41 0 9587 0
vsize: 38512
[startup+170.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 9333 0 0 0 16961 30 0 0 25 0 1 0 490913612 40357888 8969 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9853 8969 603 41 0 9812 0
vsize: 39412
[startup+180.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 9692 0 0 0 17959 32 0 0 25 0 1 0 490913612 41844736 9328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10216 9328 603 41 0 10175 0
vsize: 40864
[startup+190.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 9943 0 0 0 18959 33 0 0 25 0 1 0 490913612 42782720 9579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10445 9579 603 41 0 10404 0
vsize: 41780
[startup+200.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 10473 0 0 0 19957 35 0 0 25 0 1 0 490913612 44941312 10109 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10972 10109 603 41 0 10931 0
vsize: 43888
[startup+210.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 10996 0 0 0 20955 37 0 0 25 0 1 0 490913612 47091712 10632 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11497 10632 603 41 0 11456 0
vsize: 45988
[startup+220.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 11483 0 0 0 21953 39 0 0 25 0 1 0 490913612 49102848 11119 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11988 11119 603 41 0 11947 0
vsize: 47952
[startup+230.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 11955 0 0 0 22952 40 0 0 25 0 1 0 490913612 51257344 11591 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12514 11591 603 41 0 12473 0
vsize: 50056
[startup+240.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 12316 0 0 0 23951 42 0 0 25 0 1 0 490913612 52736000 11952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12875 11952 603 41 0 12834 0
vsize: 51500
[startup+250.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 12587 0 0 0 24950 43 0 0 25 0 1 0 490913612 53932032 12223 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13167 12223 603 41 0 13126 0
vsize: 52668
[startup+260.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 12872 0 0 0 25949 44 0 0 25 0 1 0 490913612 54992896 12508 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13426 12508 603 41 0 13385 0
vsize: 53704
[startup+270.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 13295 0 0 0 26948 45 0 0 25 0 1 0 490913612 56729600 12931 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13850 12931 603 41 0 13809 0
vsize: 55400
[startup+280.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 14070 0 0 0 27946 47 0 0 25 0 1 0 490913612 59981824 13706 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14644 13706 603 41 0 14603 0
vsize: 58576
[startup+290.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 14815 0 0 0 28945 49 0 0 25 0 1 0 490913612 62955520 14451 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15370 14451 603 41 0 15329 0
vsize: 61480
[startup+300.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 15479 0 0 0 29943 51 0 0 25 0 1 0 490913612 65658880 15115 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16030 15115 603 41 0 15989 0
vsize: 64120
[startup+310.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 15970 0 0 0 30941 53 0 0 25 0 1 0 490913612 67690496 15606 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16526 15606 603 41 0 16485 0
vsize: 66104
[startup+320.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 16446 0 0 0 31940 54 0 0 25 0 1 0 490913612 69705728 16082 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17018 16082 603 41 0 16977 0
vsize: 68072
[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 16981 0 0 0 32939 56 0 0 25 0 1 0 490913612 71880704 16617 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17549 16617 603 41 0 17508 0
vsize: 70196
[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 17556 0 0 0 33937 57 0 0 25 0 1 0 490913612 74186752 17192 4294967295 134512640 134672761 3221224544 3221223728 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18112 17192 603 41 0 18071 0
vsize: 72448
[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 18078 0 0 0 34935 59 0 0 25 0 1 0 490913612 76337152 17714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18637 17714 603 41 0 18596 0
vsize: 74548
[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 18584 0 0 0 35934 60 0 0 25 0 1 0 490913612 78364672 18220 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19132 18220 603 41 0 19091 0
vsize: 76528
[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 19111 0 0 0 36932 62 0 0 25 0 1 0 490913612 80519168 18747 4294967295 134512640 134672761 3221224544 3221223656 1075347105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19658 18747 603 41 0 19617 0
vsize: 78632
[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 19618 0 0 0 37931 64 0 0 25 0 1 0 490913612 82702336 19254 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20191 19254 603 41 0 20150 0
vsize: 80764
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 20108 0 0 0 38930 66 0 0 25 0 1 0 490913612 84729856 19744 4294967295 134512640 134672761 3221224544 3221223728 134559244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20686 19744 603 41 0 20645 0
vsize: 82744
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 20653 0 0 0 39928 67 0 0 25 0 1 0 490913612 86884352 20289 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21212 20289 603 41 0 21171 0
vsize: 84848
[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 21163 0 0 0 40927 69 0 0 25 0 1 0 490913612 89038848 20799 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21738 20799 603 41 0 21697 0
vsize: 86952
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 21801 0 0 0 41925 70 0 0 25 0 1 0 490913612 91586560 21437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22360 21437 603 41 0 22319 0
vsize: 89440
[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 22406 0 0 0 42924 72 0 0 25 0 1 0 490913612 94134272 22042 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22982 22042 603 41 0 22941 0
vsize: 91928
[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 22996 0 0 0 43923 73 0 0 25 0 1 0 490913612 96534528 22632 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23568 22632 603 41 0 23527 0
vsize: 94272
[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 23607 0 0 0 44921 75 0 0 25 0 1 0 490913612 98951168 23243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24158 23243 603 41 0 24117 0
vsize: 96632
[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 24193 0 0 0 45921 76 0 0 25 0 1 0 490913612 101347328 23829 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24743 23829 603 41 0 24702 0
vsize: 98972
[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 24715 0 0 0 46919 78 0 0 25 0 1 0 490913612 103522304 24351 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25274 24351 603 41 0 25233 0
vsize: 101096
[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 25232 0 0 0 47917 79 0 0 25 0 1 0 490913612 105660416 24868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25796 24868 603 41 0 25755 0
vsize: 103184
[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 25724 0 0 0 48916 81 0 0 25 0 1 0 490913612 107679744 25360 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26289 25360 603 41 0 26248 0
vsize: 105156
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 26307 0 0 0 49914 82 0 0 25 0 1 0 490913612 110108672 25943 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26882 25943 603 41 0 26841 0
vsize: 107528
[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 26789 0 0 0 50913 84 0 0 25 0 1 0 490913612 112005120 26425 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27345 26425 603 41 0 27304 0
vsize: 109380
[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 27336 0 0 0 51911 86 0 0 25 0 1 0 490913612 114307072 26972 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27907 26972 603 41 0 27866 0
vsize: 111628
[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 27812 0 0 0 52910 87 0 0 25 0 1 0 490913612 116191232 27448 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28367 27448 603 41 0 28326 0
vsize: 113468
[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 28288 0 0 0 53909 89 0 0 25 0 1 0 490913612 118214656 27924 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 27924 603 41 0 28820 0
vsize: 115444
[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 28759 0 0 0 54907 91 0 0 25 0 1 0 490913612 120119296 28395 4294967295 134512640 134672761 3221224544 3221223680 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29326 28395 603 41 0 29285 0
vsize: 117304
[startup+560.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 29242 0 0 0 55906 92 0 0 25 0 1 0 490913612 122159104 28878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29824 28878 603 41 0 29783 0
vsize: 119296
[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 29724 0 0 0 56905 93 0 0 25 0 1 0 490913612 124047360 29360 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30285 29360 603 41 0 30244 0
vsize: 121140
[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 30199 0 0 0 57904 94 0 0 25 0 1 0 490913612 126111744 29835 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30789 29835 603 41 0 30748 0
vsize: 123156
[startup+590.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 30736 0 0 0 58901 97 0 0 25 0 1 0 490913612 128294912 30372 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31322 30372 603 41 0 31281 0
vsize: 125288
[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 31317 0 0 0 59900 98 0 0 25 0 1 0 490913612 130736128 30953 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31918 30953 603 41 0 31877 0
vsize: 127672
[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 31884 0 0 0 60898 100 0 0 25 0 1 0 490913612 133017600 31520 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32475 31520 603 41 0 32434 0
vsize: 129900
[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 32243 0 0 0 61897 101 0 0 25 0 1 0 490913612 134496256 31879 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32836 31879 603 41 0 32795 0
vsize: 131344
[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 32690 0 0 0 62897 102 0 0 25 0 1 0 490913612 136372224 32326 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33294 32326 603 41 0 33253 0
vsize: 133176
[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 33035 0 0 0 63896 103 0 0 25 0 1 0 490913612 137711616 32671 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33621 32671 603 41 0 33580 0
vsize: 134484
[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 33476 0 0 0 64895 104 0 0 25 0 1 0 490913612 139456512 33112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34047 33112 603 41 0 34006 0
vsize: 136188
[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 33858 0 0 0 65894 105 0 0 25 0 1 0 490913612 141066240 33494 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34440 33494 603 41 0 34399 0
vsize: 137760
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 34264 0 0 0 66893 107 0 0 25 0 1 0 490913612 142680064 33900 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34834 33900 603 41 0 34793 0
vsize: 139336
[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 34685 0 0 0 67891 108 0 0 25 0 1 0 490913612 144420864 34321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35259 34321 603 41 0 35218 0
vsize: 141036
[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 35140 0 0 0 68890 110 0 0 25 0 1 0 490913612 146305024 34776 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35719 34776 603 41 0 35678 0
vsize: 142876
[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 35567 0 0 0 69888 111 0 0 25 0 1 0 490913612 148049920 35203 4294967295 134512640 134672761 3221224544 3221223648 134560039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36145 35203 603 41 0 36104 0
vsize: 144580
[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 35881 0 0 0 70888 112 0 0 25 0 1 0 490913612 149258240 35517 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36440 35517 603 41 0 36399 0
vsize: 145760
[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 36171 0 0 0 71887 113 0 0 25 0 1 0 490913612 150474752 35807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36737 35807 603 41 0 36696 0
vsize: 146948
[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 36442 0 0 0 72886 115 0 0 25 0 1 0 490913612 151539712 36078 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36997 36078 603 41 0 36956 0
vsize: 147988
[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 36673 0 0 0 73885 116 0 0 25 0 1 0 490913612 153001984 36309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37354 36309 603 41 0 37313 0
vsize: 149416
[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 37034 0 0 0 74884 116 0 0 25 0 1 0 490913612 154484736 36670 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37716 36670 603 41 0 37675 0
vsize: 150864
[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 37539 0 0 0 75883 117 0 0 25 0 1 0 490913612 156622848 37175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38238 37175 603 41 0 38197 0
vsize: 152952
[startup+770.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 38124 0 0 0 76882 119 0 0 25 0 1 0 490913612 159047680 37760 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38830 37760 603 41 0 38789 0
vsize: 155320
[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 38833 0 0 0 77880 121 0 0 25 0 1 0 490913612 161878016 38469 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39521 38469 603 41 0 39480 0
vsize: 158084
[startup+790.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 39513 0 0 0 78878 123 0 0 25 0 1 0 490913612 164712448 39149 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40213 39149 603 41 0 40172 0
vsize: 160852
[startup+800.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 40152 0 0 0 79876 125 0 0 25 0 1 0 490913612 167280640 39788 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40840 39788 603 41 0 40799 0
vsize: 163360
[startup+810.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 40785 0 0 0 80875 126 0 0 25 0 1 0 490913612 169844736 40421 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41466 40421 603 41 0 41425 0
vsize: 165864
[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 41445 0 0 0 81873 128 0 0 25 0 1 0 490913612 172564480 41081 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42130 41081 603 41 0 42089 0
vsize: 168520
[startup+830.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 42075 0 0 0 82871 130 0 0 25 0 1 0 490913612 175140864 41711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42759 41711 603 41 0 42718 0
vsize: 171036
[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 42669 0 0 0 83869 132 0 0 25 0 1 0 490913612 177586176 42305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43356 42305 603 41 0 43315 0
vsize: 173424
[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 43293 0 0 0 84868 134 0 0 25 0 1 0 490913612 180178944 42929 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43989 42929 603 41 0 43948 0
vsize: 175956
[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 43792 0 0 0 85866 136 0 0 25 0 1 0 490913612 182210560 43428 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44485 43428 603 41 0 44444 0
vsize: 177940
[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 44213 0 0 0 86864 138 0 0 25 0 1 0 490913612 183947264 43849 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44909 43849 603 41 0 44868 0
vsize: 179636
[startup+880.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 44763 0 0 0 87863 139 0 0 25 0 1 0 490913612 186105856 44399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45436 44399 603 41 0 45395 0
vsize: 181744
[startup+890.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 45172 0 0 0 88862 140 0 0 25 0 1 0 490913612 187858944 44808 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45864 44808 603 41 0 45823 0
vsize: 183456
[startup+900.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 45653 0 0 0 89860 142 0 0 25 0 1 0 490913612 189734912 45289 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46322 45289 603 41 0 46281 0
vsize: 185288
[startup+910.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 46094 0 0 0 90859 143 0 0 25 0 1 0 490913612 191619072 45730 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46782 45730 603 41 0 46741 0
vsize: 187128
[startup+920.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 46677 0 0 0 91857 146 0 0 25 0 1 0 490913612 193900544 46313 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47339 46313 603 41 0 47298 0
vsize: 189356
[startup+930.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 47188 0 0 0 92855 148 0 0 25 0 1 0 490913612 196034560 46824 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47860 46824 603 41 0 47819 0
vsize: 191440
[startup+940.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 47620 0 0 0 93853 150 0 0 25 0 1 0 490913612 197779456 47256 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48286 47256 603 41 0 48245 0
vsize: 193144
[startup+950.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 48023 0 0 0 94851 151 0 0 25 0 1 0 490913612 199389184 47659 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48679 47659 603 41 0 48638 0
vsize: 194716
[startup+960.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29989
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 48454 0 0 0 95849 154 0 0 25 0 1 0 490913612 201256960 48090 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49135 48090 603 41 0 49094 0
vsize: 196540
[startup+970.063 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 48963 0 0 0 96839 163 0 0 25 0 1 0 490913612 203268096 48599 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49626 48599 603 41 0 49585 0
vsize: 198504
[startup+980.063 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 49312 0 0 0 97838 164 0 0 25 0 1 0 490913612 204763136 48948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49991 48948 603 41 0 49950 0
vsize: 199964
[startup+990.064 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 49461 0 0 0 98838 164 0 0 25 0 1 0 490913612 205303808 49097 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50123 49097 603 41 0 50082 0
vsize: 200492
[startup+1000.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 49685 0 0 0 99838 165 0 0 25 0 1 0 490913612 206237696 49321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50351 49321 603 41 0 50310 0
vsize: 201404
[startup+1010.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 49838 0 0 0 100838 165 0 0 25 0 1 0 490913612 206786560 49474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50485 49474 603 41 0 50444 0
vsize: 201940
[startup+1020.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 50411 0 0 0 101837 166 0 0 25 0 1 0 490913612 209215488 50047 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51078 50047 603 41 0 51037 0
vsize: 204312
[startup+1030.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30042
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 50711 0 0 0 102836 167 0 0 25 0 1 0 490913612 210411520 50347 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51370 50347 603 41 0 51329 0
vsize: 205480
[startup+1040.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 51094 0 0 0 103836 168 0 0 25 0 1 0 490913612 212013056 50730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51761 50730 603 41 0 51720 0
vsize: 207044
[startup+1050.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 51698 0 0 0 104834 170 0 0 25 0 1 0 490913612 214429696 51334 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52351 51334 603 41 0 52310 0
vsize: 209404
[startup+1060.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 51902 0 0 0 105834 171 0 0 25 0 1 0 490913612 215236608 51538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52548 51538 603 41 0 52507 0
vsize: 210192
[startup+1070.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 52203 0 0 0 106833 171 0 0 25 0 1 0 490913612 216449024 51839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52844 51839 603 41 0 52803 0
vsize: 211376
[startup+1080.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 52584 0 0 0 107832 173 0 0 25 0 1 0 490913612 218066944 52220 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53239 52220 603 41 0 53198 0
vsize: 212956
[startup+1090.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 53082 0 0 0 108831 174 0 0 25 0 1 0 490913612 220045312 52718 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53722 52718 603 41 0 53681 0
vsize: 214888
[startup+1100.07 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 53276 0 0 0 109830 175 0 0 25 0 1 0 490913612 220856320 52912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53920 52912 603 41 0 53879 0
vsize: 215680
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 53330 0 0 0 110830 175 0 0 25 0 1 0 490913612 221126656 52966 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53986 52966 603 41 0 53945 0
vsize: 215944
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 53392 0 0 0 111830 175 0 0 25 0 1 0 490913612 221392896 53028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54051 53028 603 41 0 54010 0
vsize: 216204
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 53833 0 0 0 112829 177 0 0 25 0 1 0 490913612 223129600 53469 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54475 53469 603 41 0 54434 0
vsize: 217900
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 54281 0 0 0 113828 177 0 0 25 0 1 0 490913612 224989184 53917 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54929 53917 603 41 0 54888 0
vsize: 219716
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 54666 0 0 0 114827 178 0 0 25 0 1 0 490913612 226615296 54302 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55326 54302 603 41 0 55285 0
vsize: 221304
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 54976 0 0 0 115827 179 0 0 25 0 1 0 490913612 227807232 54612 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55617 54612 603 41 0 55576 0
vsize: 222468
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 55316 0 0 0 116826 180 0 0 25 0 1 0 490913612 229269504 54952 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55974 54952 603 41 0 55933 0
vsize: 223896
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 55682 0 0 0 117826 181 0 0 25 0 1 0 490913612 230707200 55318 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56325 55318 603 41 0 56284 0
vsize: 225300
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 56022 0 0 0 118825 182 0 0 25 0 1 0 490913612 232140800 55658 4294967295 134512640 134672761 3221224544 3221223648 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56675 55658 603 41 0 56634 0
vsize: 226700
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30044
Raw data (stat): 29989 (minisat+) R 29988 30854 30853 0 -1 0 56355 0 0 0 119823 183 0 0 25 0 1 0 490913612 233439232 55991 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56992 55991 603 41 0 56951 0
vsize: 227968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 30044
Raw data (stat): 29989 (minisat+) Z 29988 30854 30853 0 -1 12 56357 0 0 0 119823 194 0 0 25 0 1 0 490913612 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.18
CPU time (s): 1200.18
CPU user time (s): 1198.24
CPU system time (s): 1.9427
CPU usage (%): 100
Max. virtual memory (Kb): 227968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####