PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air01.opb
MD5SUM	90db1995bd949fc5ac74143a523f3bcf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3398
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	3698
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	1192753
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3698
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	1192753
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02884
Number of variables	771
Total number of constraints	794
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	438
Trace number 32253

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-05-27 08:43:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23634 boxname=wulflinc26 idbench=1278 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 23634
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915308 kB
Buffers:          1576 kB
Cached:          97272 kB
SwapCached:        636 kB
Active:          14760 kB
Inactive:        86204 kB
HighTotal:      131008 kB
HighFree:        30996 kB
LowTotal:       903652 kB
LowFree:        884312 kB
SwapTotal:     2097892 kB
SwapFree:      2096396 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            12656 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:03:53 (client local time) WITH STATUS 152 IN 1230.05 SECONDS
stats: 23634 7 1230.05 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> BDD-cost:   49
c ---[  42]---> BDD-cost:   39
c ---[  40]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   61
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  139
c ---[  26]---> BDD-cost:  197
c ---[  24]---> BDD-cost:  233
c ---[  22]---> BDD-cost:  273
c ---[  20]---> BDD-cost:  353
c ---[  18]---> BDD-cost:  331
c ---[  16]---> BDD-cost:  527
c ---[  14]---> BDD-cost:  589
c ---[  12]---> BDD-cost:  607
c ---[  10]---> BDD-cost:  559
c ---[   8]---> BDD-cost:  755
c ---[   6]---> BDD-cost:  769
c ---[   4]---> BDD-cost:  741
c ---[   2]---> BDD-cost:  781
c ---[   0]---> BDD-cost:  873
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20564    53488 |    6854       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 9600[0m
c ---[   0]---> Sorter-cost:405471     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        26 | 1076333  2519033 |  358777      26     1591    61.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 7246[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        41 | 1081308  2532280 |  360436      41     2258    55.1 |  0.000 % |
c ==============================================================================
c [1mFound solution: 6035[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        49 | 1082093  2535275 |  360697      49     3635    74.2 |  0.000 % |
c |       162 | 1081886  2534808 |  396766     161    34933   217.0 |  0.020 % |
c |       314 | 1081870  2534772 |  436443     312    59302   190.1 |  0.021 % |
c |       539 | 1081556  2534062 |  480087     536   173133   323.0 |  0.042 % |
c |       876 | 1078519  2527142 |  528096     815   192949   236.7 |  0.263 % |
c ==============================================================================
c [1mFound solution: 5928[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       950 | 1080226  2531316 |  360075     889   233545   262.7 |  0.263 % |
c |      1050 | 1079697  2530112 |  396082     987   245138   248.4 |  0.302 % |
c |      1200 | 1079697  2530112 |  435690    1137   260298   228.9 |  0.302 % |
c |      1425 | 1079573  2529830 |  479259    1360   262082   192.7 |  0.311 % |
c |      1765 | 1077094  2524166 |  527185    1659   276840   166.9 |  0.494 % |
c |      2272 | 1073638  2516255 |  579904    2113   391798   185.4 |  0.751 % |
c |      3032 | 1073207  2515277 |  637894    2855  1360522   476.5 |  0.782 % |
c ==============================================================================
c [1mFound solution: 5471[0m
c ---[   0]---> Sorter-cost:305145     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3194 | 1838554  4302735 |  612851    3016  1397590   463.4 |  0.782 % |
c ==============================================================================
c [1mFound solution: 5311[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3218 | 1840124  4308648 |  613374    3040  1418436   466.6 |  0.782 % |
c |      3318 | 1840124  4308648 |  674711    3140  1423590   453.4 |  0.661 % |
c |      3469 | 1839313  4306837 |  742182    3280  1436724   438.0 |  0.697 % |
c |      3696 | 1836198  4299794 |  816400    3466  1459627   421.1 |  0.834 % |
c |      4033 | 1829295  4284035 |  898040    3784  1605079   424.2 |  1.140 % |
c |      4542 | 1829295  4284035 |  987844    4293  1859193   433.1 |  1.140 % |
c |      5304 | 1829295  4284035 | 1086629    5055  2513459   497.2 |  1.140 % |
c ==============================================================================
c [1mFound solution: 4729[0m
c ---[   0]---> Sorter-cost:331342     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6102 | 2652877  6207237 |  884292    5818  3333972   573.0 |  1.140 % |
c |      6202 | 2652020  6205291 |  972721    5915  3359494   568.0 |  1.230 % |
c ==============================================================================
c [1mFound solution: 4607[0m
c ---[   0]---> Sorter-cost:332348     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6340 | 3520429  8233160 | 1173476    6000  3368486   561.4 |  1.230 % |
c |      6441 | 3513168  8216645 | 1290823    6079  3370074   554.4 |  1.421 % |
c |      6597 | 3510881  8211423 | 1419905    6233  3506059   562.5 |  1.473 % |
c |      6822 | 3510532  8210636 | 1561896    6457  3537448   547.8 |  1.481 % |
c |      7159 | 3505536  8199254 | 1718086    6711  3570665   532.1 |  1.598 % |
c |      7665 | 3496472  8178540 | 1889894    7107  3686794   518.8 |  1.811 % |
c |      8424 | 3496205  8177935 | 2078884    7865  3920527   498.5 |  1.818 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 17815 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.98 0.97 0.91 2/54 17811
Raw data (stat): 17811 (runsolver) R 17810 20687 20686 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854819032 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99975 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+39.9998 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0002 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0004 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.001 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.007 s]
Raw data (loadavg): 1.07 1.01 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.007 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.008 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.007 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.009 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.008 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17815
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/56 17816
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 17868
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.89 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 17870
Raw data (stat): 17811 (minisat+_script) S 17810 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854819032 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.89
CPU time (s): 1230.05
CPU user time (s): 1227.25
CPU system time (s): 2.80257
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####