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/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb
MD5SUM	452acf9ed3adc2d2cfe293dad01c0934
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167110
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.02
Number of variables	280
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	130
Trace number 13657

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        793448 kB
Buffers:         34208 kB
Cached:         173348 kB
SwapCached:        660 kB
Active:          77352 kB
Inactive:       132356 kB
HighTotal:      131008 kB
HighFree:          420 kB
LowTotal:       903652 kB
LowFree:        793028 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            25772 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 21:35:17 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 14479 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 662   maxlim: 3510008   bits: 23/22
c ---[   8]---> Adder-cost: 660   maxlim: 3759828   bits: 23/22
c ---[   6]---> Adder-cost: 770   maxlim: 3884662   bits: 23/22
c ---[   4]---> Adder-cost: 500   maxlim: 3402645   bits: 23/22
c ---[   2]---> Adder-cost: 574   maxlim: 3468109   bits: 23/22
c ---[   0]---> Adder-cost: 558   maxlim: 3462997   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25873    92160 |    8624       0        0     nan |  0.000 % |
c |       101 |   25865    92134 |    9486     100      785     7.8 |  8.749 % |
c ==============================================================================
c [1mFound solution: 7118272[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 210   maxlim: 5464634   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       223 |   27281    97292 |    9093     222     1715     7.7 |  8.749 % |
c |       326 |   27281    97292 |   10002     325     2295     7.1 |  8.585 % |
c ==============================================================================
c [1mFound solution: 3128718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9454188   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       333 |   27272    97247 |    9090     332     2324     7.0 |  8.585 % |
c ==============================================================================
c [1mFound solution: 2755982[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9826924   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       339 |   27302    97470 |    9100     338     3980    11.8 |  8.585 % |
c |       439 |   27302    97470 |   10010     438     6525    14.9 |  9.063 % |
c |       590 |   27278    97392 |   11011     586     7434    12.7 |  9.129 % |
c |       815 |   27270    97366 |   12112     810    11011    13.6 |  9.151 % |
c |      1152 |   27254    97314 |   13323    1145    14430    12.6 |  9.195 % |
c |      1659 |   27254    97314 |   14655    1652    20576    12.5 |  9.195 % |
c |      2418 |   27254    97314 |   16121    2411    34257    14.2 |  9.195 % |
c ==============================================================================
c [1mFound solution: 1586320[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10996586   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3095 |   27227    97154 |    9075    3065   154216    50.3 |  9.195 % |
c |      3196 |   27227    97154 |    9982    3166   157303    49.7 |  9.618 % |
c |      3348 |   27227    97154 |   10980    3318   159619    48.1 |  9.618 % |
c |      3573 |   27227    97154 |   12078    3543   164570    46.4 |  9.618 % |
c |      3911 |   27219    97128 |   13286    3880   170135    43.8 |  9.640 % |
c |      4417 |   27203    97076 |   14615    4384   210853    48.1 |  9.684 % |
c |      5176 |   27203    97076 |   16076    5143   224736    43.7 |  9.684 % |
c |      6315 |   27179    96998 |   17684    6279   252812    40.3 |  9.750 % |
c |      8023 |   27171    96972 |   19453    7986   301478    37.8 |  9.772 % |
c |     10585 |   27171    96972 |   21398   10548   432458    41.0 |  9.772 % |
c ==============================================================================
c [1mFound solution: 1296986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11285920   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11435 |   27192    97126 |    9064   11398   458581    40.2 |  9.772 % |
c |     11535 |   27192    97126 |    9970    5799   196298    33.9 |  9.950 % |
c |     11686 |   27192    97126 |   10967    5950   201228    33.8 |  9.950 % |
c |     11911 |   27192    97126 |   12064    6175   205854    33.3 |  9.950 % |
c |     12249 |   27192    97126 |   13270    6513   212821    32.7 |  9.950 % |
c |     12756 |   27192    97126 |   14597    7020   220459    31.4 |  9.950 % |
c |     13515 |   27192    97126 |   16057    7779   235636    30.3 |  9.950 % |
c |     14655 |   27184    97100 |   17663    8918   304135    34.1 |  9.972 % |
c |     16363 |   27184    97100 |   19429   10626   362807    34.1 |  9.972 % |
c |     18925 |   27176    97074 |   21372   13187   480781    36.5 |  9.993 % |
c |     22770 |   27168    97048 |   23509   17031   656737    38.6 | 10.015 % |
c |     28537 |   27168    97048 |   25860   22798   924116    40.5 | 10.015 % |
c ==============================================================================
c [1mFound solution: 1093846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11489060   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35506 |   27183    97186 |    9061   15194  1058956    69.7 | 10.015 % |
c |     35609 |   27183    97186 |    9967    7700   595510    77.3 | 10.201 % |
c |     35759 |   27183    97186 |   10963    7850   597388    76.1 | 10.201 % |
c |     35985 |   27183    97186 |   12060    8076   602098    74.6 | 10.201 % |
c |     36323 |   27175    97160 |   13266    8413   605788    72.0 | 10.223 % |
c |     36829 |   27175    97160 |   14592    8919   617754    69.3 | 10.223 % |
c |     37589 |   27175    97160 |   16052    9679   634034    65.5 | 10.223 % |
c |     38729 |   27175    97160 |   17657   10819   672820    62.2 | 10.223 % |
c |     40437 |   27175    97160 |   19423   12527   745990    59.6 | 10.223 % |
c |     42999 |   27175    97160 |   21365   15089   830783    55.1 | 10.223 % |
c |     46843 |   27175    97160 |   23501   18933   979023    51.7 | 10.223 % |
c |     52613 |   27175    97160 |   25852   24703  1242027    50.3 | 10.223 % |
c ==============================================================================
c [1mFound solution: 670364[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4   maxlim: 5621086   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52696 |   27129    97127 |    9043   24346  1228062    50.4 | 10.223 % |
c |     52797 |   27054    96583 |    9947    6162   209364    34.0 | 10.891 % |
c |     52948 |   27054    96583 |   10942    6313   210535    33.3 | 10.891 % |
c |     53173 |   27054    96583 |   12036    6538   214788    32.9 | 10.891 % |
c |     53511 |   27054    96583 |   13239    6876   231818    33.7 | 10.891 % |
c |     54017 |   27054    96583 |   14563    7382   244823    33.2 | 10.891 % |
c |     54777 |   27054    96583 |   16020    8142   270787    33.3 | 10.891 % |
c |     55917 |   27054    96583 |   17622    9282   354544    38.2 | 10.891 % |
c |     57626 |   27054    96583 |   19384   10991   433096    39.4 | 10.891 % |
c |     60190 |   27054    96583 |   21322   13555   507166    37.4 | 10.891 % |
c |     64034 |   27054    96583 |   23455   17399   668356    38.4 | 10.891 % |
c |     69804 |   27054    96583 |   25800   23169   989249    42.7 | 10.891 % |
c |     78454 |   27054    96583 |   28380   18389   766228    41.7 | 10.891 % |
c |     91429 |   27054    96583 |   31218   15735   558802    35.5 | 10.891 % |
c |    110890 |   27054    96583 |   34340   17037   764605    44.9 | 10.891 % |
c |    140082 |   27054    96583 |   37774   24779  1040796    42.0 | 10.891 % |
c |    183872 |   27054    96583 |   41552   21946   890900    40.6 | 10.891 % |
c |    249557 |   27046    96561 |   45707   32247  1504677    46.7 | 10.935 % |
c |    348084 |   27046    96561 |   50278   34065  1891680    55.5 | 10.935 % |
c |    495873 |   27046    96561 |   55306   38166  2121339    55.6 | 10.935 % |
c |    717556 |   27046    96561 |   60836   53899  5251345    97.4 | 10.935 % |
#### 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.93 0.98 0.91 2/55 14146
Raw data (stat): 14146 (runsolver) R 14145 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539596071 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 1401 0 0 0 994 3 0 0 25 0 1 0 539596071 7491584 1378 4294967295 134512640 134672761 3221224528 3221223712 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1829 1378 603 41 0 1788 0
vsize: 7316
[startup+20 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2069 0 0 0 1993 5 0 0 25 0 1 0 539596071 10268672 2046 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2507 2046 603 41 0 2466 0
vsize: 10028
[startup+29.9998 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2616 0 0 0 2991 7 0 0 25 0 1 0 539596071 12406784 2593 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3029 2593 603 41 0 2988 0
vsize: 12116
[startup+39.9998 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2705 0 0 0 3989 8 0 0 25 0 1 0 539596071 12808192 2682 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3127 2682 603 41 0 3086 0
vsize: 12508
[startup+50.0064 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2706 0 0 0 4989 8 0 0 25 0 1 0 539596071 12808192 2683 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3127 2683 603 41 0 3086 0
vsize: 12508
[startup+60.0144 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2706 0 0 0 5990 8 0 0 25 0 1 0 539596071 12808192 2683 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3127 2683 603 41 0 3086 0
vsize: 12508
[startup+70.0161 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2706 0 0 0 6990 8 0 0 25 0 1 0 539596071 12808192 2683 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3127 2683 603 41 0 3086 0
vsize: 12508
[startup+80.0158 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2707 0 0 0 7989 8 0 0 25 0 1 0 539596071 12808192 2684 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3127 2684 603 41 0 3086 0
vsize: 12508
[startup+90.0155 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2708 0 0 0 8989 8 0 0 25 0 1 0 539596071 12808192 2685 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3127 2685 603 41 0 3086 0
vsize: 12508
[startup+100.104 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2780 0 0 0 9998 9 0 0 25 0 1 0 539596071 13074432 2757 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3192 2757 603 41 0 3151 0
vsize: 12768
[startup+110.106 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2780 0 0 0 10998 9 0 0 25 0 1 0 539596071 13074432 2757 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3192 2757 603 41 0 3151 0
vsize: 12768
[startup+120.109 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 2968 0 0 0 11999 9 0 0 25 0 1 0 539596071 14012416 2945 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2945 603 41 0 3380 0
vsize: 13684
[startup+130.108 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3052 0 0 0 12998 9 0 0 25 0 1 0 539596071 14274560 3029 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3485 3029 603 41 0 3444 0
vsize: 13940
[startup+140.108 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3058 0 0 0 13998 9 0 0 25 0 1 0 539596071 14438400 3035 4294967295 134512640 134672761 3221224528 3221223688 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3035 603 41 0 3484 0
vsize: 14100
[startup+150.108 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3058 0 0 0 14999 9 0 0 25 0 1 0 539596071 14438400 3035 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3525 3035 603 41 0 3484 0
vsize: 14100
[startup+160.108 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3294 0 0 0 15998 10 0 0 25 0 1 0 539596071 15376384 3271 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3754 3271 603 41 0 3713 0
vsize: 15016
[startup+170.108 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3310 0 0 0 16998 10 0 0 25 0 1 0 539596071 15536128 3287 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3793 3287 603 41 0 3752 0
vsize: 15172
[startup+180.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3325 0 0 0 17999 10 0 0 25 0 1 0 539596071 15536128 3302 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3793 3302 603 41 0 3752 0
vsize: 15172
[startup+190.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3334 0 0 0 19000 10 0 0 25 0 1 0 539596071 15536128 3311 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3793 3311 603 41 0 3752 0
vsize: 15172
[startup+200.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3437 0 0 0 20000 11 0 0 25 0 1 0 539596071 15937536 3414 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3891 3414 603 41 0 3850 0
vsize: 15564
[startup+210.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3508 0 0 0 21000 11 0 0 25 0 1 0 539596071 16207872 3485 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3957 3485 603 41 0 3916 0
vsize: 15828
[startup+220.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3531 0 0 0 22000 11 0 0 25 0 1 0 539596071 16351232 3508 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3992 3508 603 41 0 3951 0
vsize: 15968
[startup+230.122 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3562 0 0 0 23000 11 0 0 25 0 1 0 539596071 16515072 3539 4294967295 134512640 134672761 3221224528 3221223624 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4032 3539 603 41 0 3991 0
vsize: 16128
[startup+240.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3661 0 0 0 24000 11 0 0 25 0 1 0 539596071 16920576 3638 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4131 3638 603 41 0 4090 0
vsize: 16524
[startup+250.125 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3686 0 0 0 25000 11 0 0 25 0 1 0 539596071 17100800 3663 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4175 3663 603 41 0 4134 0
vsize: 16700
[startup+260.133 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3686 0 0 0 26000 11 0 0 25 0 1 0 539596071 17100800 3663 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3663 603 41 0 4134 0
vsize: 16700
[startup+270.133 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3695 0 0 0 27001 11 0 0 25 0 1 0 539596071 17100800 3672 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4175 3672 603 41 0 4134 0
vsize: 16700
[startup+280.133 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14146
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3754 0 0 0 28001 11 0 0 25 0 1 0 539596071 17371136 3731 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3731 603 41 0 4200 0
vsize: 16964
[startup+290.133 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3754 0 0 0 29001 11 0 0 25 0 1 0 539596071 17371136 3731 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3731 603 41 0 4200 0
vsize: 16964
[startup+300.134 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3754 0 0 0 30001 11 0 0 25 0 1 0 539596071 17371136 3731 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3731 603 41 0 4200 0
vsize: 16964
[startup+310.142 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 3764 0 0 0 31002 11 0 0 25 0 1 0 539596071 17371136 3741 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3741 603 41 0 4200 0
vsize: 16964
[startup+320.143 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 4314 0 0 0 32000 13 0 0 25 0 1 0 539596071 19652608 4291 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4798 4291 603 41 0 4757 0
vsize: 19192
[startup+330.142 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 4314 0 0 0 33000 13 0 0 25 0 1 0 539596071 19652608 4291 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4798 4291 603 41 0 4757 0
vsize: 19192
[startup+340.142 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 4410 0 0 0 34000 14 0 0 25 0 1 0 539596071 20058112 4387 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4897 4387 603 41 0 4856 0
vsize: 19588
[startup+350.142 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 34999 15 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221222236 134566355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+360.149 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 36000 15 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+370.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 37000 16 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+380.151 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 38000 16 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+390.151 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 39000 16 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+400.151 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 40000 16 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+410.151 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5125 0 0 0 41000 16 0 0 25 0 1 0 539596071 23007232 5102 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5102 603 41 0 5576 0
vsize: 22468
[startup+420.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5141 0 0 0 42000 16 0 0 25 0 1 0 539596071 23007232 5118 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5617 5118 603 41 0 5576 0
vsize: 22468
[startup+430.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5499 0 0 0 43000 17 0 0 25 0 1 0 539596071 24473600 5476 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5476 603 41 0 5934 0
vsize: 23900
[startup+440.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5499 0 0 0 44000 17 0 0 25 0 1 0 539596071 24473600 5476 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5476 603 41 0 5934 0
vsize: 23900
[startup+450.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5499 0 0 0 45000 17 0 0 25 0 1 0 539596071 24473600 5476 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5476 603 41 0 5934 0
vsize: 23900
[startup+460.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5499 0 0 0 46000 17 0 0 25 0 1 0 539596071 24473600 5476 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5476 603 41 0 5934 0
vsize: 23900
[startup+470.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5500 0 0 0 47000 17 0 0 25 0 1 0 539596071 24473600 5477 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5477 603 41 0 5934 0
vsize: 23900
[startup+480.153 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5500 0 0 0 48000 17 0 0 25 0 1 0 539596071 24473600 5477 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5975 5477 603 41 0 5934 0
vsize: 23900
[startup+490.153 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5500 0 0 0 48999 17 0 0 25 0 1 0 539596071 24473600 5477 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5477 603 41 0 5934 0
vsize: 23900
[startup+500.153 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5500 0 0 0 49999 18 0 0 25 0 1 0 539596071 24473600 5477 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5477 603 41 0 5934 0
vsize: 23900
[startup+510.152 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5500 0 0 0 51000 18 0 0 25 0 1 0 539596071 24473600 5477 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5975 5477 603 41 0 5934 0
vsize: 23900
[startup+520.157 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5910 0 0 0 51999 19 0 0 25 0 1 0 539596071 26226688 5887 4294967295 134512640 134672761 3221224528 3221222848 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5887 603 41 0 6362 0
vsize: 25612
[startup+530.156 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5910 0 0 0 52999 19 0 0 25 0 1 0 539596071 26226688 5887 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5887 603 41 0 6362 0
vsize: 25612
[startup+540.157 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5917 0 0 0 53999 19 0 0 25 0 1 0 539596071 26226688 5894 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5894 603 41 0 6362 0
vsize: 25612
[startup+550.157 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5917 0 0 0 55000 19 0 0 25 0 1 0 539596071 26226688 5894 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5894 603 41 0 6362 0
vsize: 25612
[startup+560.158 s]
Raw data (loadavg): 1.07 1.00 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 5920 0 0 0 56000 19 0 0 25 0 1 0 539596071 26226688 5897 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5897 603 41 0 6362 0
vsize: 25612
[startup+570.158 s]
Raw data (loadavg): 1.06 1.00 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6172 0 0 0 56999 19 0 0 25 0 1 0 539596071 27303936 6149 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6666 6149 603 41 0 6625 0
vsize: 26664
[startup+580.158 s]
Raw data (loadavg): 1.05 1.00 0.91 2/55 14148
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6748 0 0 0 57998 21 0 0 25 0 1 0 539596071 29593600 6725 4294967295 134512640 134672761 3221224528 3221223712 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6725 603 41 0 7184 0
vsize: 28900
[startup+590.159 s]
Raw data (loadavg): 1.04 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6748 0 0 0 58998 21 0 0 25 0 1 0 539596071 29593600 6725 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6725 603 41 0 7184 0
vsize: 28900
[startup+600.159 s]
Raw data (loadavg): 1.04 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6748 0 0 0 59998 21 0 0 25 0 1 0 539596071 29593600 6725 4294967295 134512640 134672761 3221224528 3221223712 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7225 6725 603 41 0 7184 0
vsize: 28900
[startup+610.16 s]
Raw data (loadavg): 1.03 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6748 0 0 0 60998 21 0 0 25 0 1 0 539596071 29593600 6725 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6725 603 41 0 7184 0
vsize: 28900
[startup+620.159 s]
Raw data (loadavg): 1.03 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6751 0 0 0 61998 21 0 0 25 0 1 0 539596071 29593600 6728 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6728 603 41 0 7184 0
vsize: 28900
[startup+630.159 s]
Raw data (loadavg): 1.02 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 62998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223632 134555379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+640.16 s]
Raw data (loadavg): 1.02 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 63998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+650.16 s]
Raw data (loadavg): 1.01 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 64998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+660.16 s]
Raw data (loadavg): 1.01 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 65998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+670.159 s]
Raw data (loadavg): 1.01 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 66998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+680.159 s]
Raw data (loadavg): 1.01 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 67998 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+690.159 s]
Raw data (loadavg): 1.01 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 68999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+700.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 69999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+710.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 70999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+720.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 71999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+730.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 72999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+740.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 73999 21 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+750.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 74999 22 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+760.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6753 0 0 0 76000 22 0 0 25 0 1 0 539596071 29593600 6730 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6730 603 41 0 7184 0
vsize: 28900
[startup+770.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 6846 0 0 0 76999 22 0 0 25 0 1 0 539596071 29995008 6823 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6823 603 41 0 7282 0
vsize: 29292
[startup+780.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 7186 0 0 0 77998 23 0 0 25 0 1 0 539596071 31330304 7163 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7649 7163 603 41 0 7608 0
vsize: 30596
[startup+790.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 7552 0 0 0 78997 24 0 0 25 0 1 0 539596071 32931840 7529 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8040 7529 603 41 0 7999 0
vsize: 32160
[startup+800.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 7917 0 0 0 79997 25 0 0 25 0 1 0 539596071 34402304 7894 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8399 7894 603 41 0 8358 0
vsize: 33596
[startup+810.159 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 8261 0 0 0 80995 27 0 0 25 0 1 0 539596071 35872768 8238 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 8238 603 41 0 8717 0
vsize: 35032
[startup+820.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 8655 0 0 0 81995 27 0 0 25 0 1 0 539596071 37367808 8632 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9123 8632 603 41 0 9082 0
vsize: 36492
[startup+830.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 8973 0 0 0 82995 28 0 0 25 0 1 0 539596071 38715392 8950 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9452 8950 603 41 0 9411 0
vsize: 37808
[startup+840.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9293 0 0 0 83995 28 0 0 25 0 1 0 539596071 40050688 9270 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9778 9270 603 41 0 9737 0
vsize: 39112
[startup+850.161 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9612 0 0 0 84993 29 0 0 25 0 1 0 539596071 41381888 9589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10103 9589 603 41 0 10062 0
vsize: 40412
[startup+860.161 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 85992 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223024 134565834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+870.161 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 86992 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+880.161 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14150
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 87993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+890.162 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 88993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+900.162 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 89993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+910.162 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 90993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+920.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 91993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+930.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 92993 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+940.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 93994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+950.162 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 94994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+960.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 95994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+970.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 96994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+980.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 97994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+990.163 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 98994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1000.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 99994 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 100995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1020.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 101995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1030.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 102995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1040.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 103995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1050.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 104995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1060.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9923 0 0 0 105995 31 0 0 25 0 1 0 539596071 42590208 9900 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9900 603 41 0 10357 0
vsize: 41592
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 106995 31 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223632 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 107995 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1090.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 108996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1100.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 109996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1110.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 110996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1120.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 111996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1130.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 112996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1140.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9924 0 0 0 113996 32 0 0 25 0 1 0 539596071 42590208 9901 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9901 603 41 0 10357 0
vsize: 41592
[startup+1150.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9926 0 0 0 114996 32 0 0 25 0 1 0 539596071 42590208 9903 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9903 603 41 0 10357 0
vsize: 41592
[startup+1160.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9929 0 0 0 115996 32 0 0 25 0 1 0 539596071 42590208 9906 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9906 603 41 0 10357 0
vsize: 41592
[startup+1170.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9929 0 0 0 116997 32 0 0 25 0 1 0 539596071 42590208 9906 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9906 603 41 0 10357 0
vsize: 41592
[startup+1180.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14152
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9929 0 0 0 117997 32 0 0 25 0 1 0 539596071 42590208 9906 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9906 603 41 0 10357 0
vsize: 41592
[startup+1190.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14154
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9929 0 0 0 118997 32 0 0 25 0 1 0 539596071 42590208 9906 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9906 603 41 0 10357 0
vsize: 41592
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 14154
Raw data (stat): 14146 (minisat+) R 14145 22929 22928 0 -1 0 9929 0 0 0 119997 32 0 0 25 0 1 0 539596071 42590208 9906 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9906 603 41 0 10357 0
vsize: 41592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.91 1/55 14154
Raw data (stat): 14146 (minisat+) Z 14145 22929 22928 0 -1 12 9932 0 0 0 119997 34 0 0 25 0 1 0 539596071 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: 10
Real time (s): 1200.19
CPU time (s): 1200.32
CPU user time (s): 1199.98
CPU system time (s): 0.341948
CPU usage (%): 100.011
Max. virtual memory (Kb): 41592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####