PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	c00b2eef1eabd5880b83093b756a5dd4
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	429056
Optimality of the best value was proved	NO
Number of terms in the objective function	210
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	7516192761
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	7516192761
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	1201.34
Number of variables	270
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	90
Trace number 21785

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        725100 kB
Buffers:         21904 kB
Cached:         266784 kB
SwapCached:        516 kB
Active:          35664 kB
Inactive:       255032 kB
HighTotal:      131008 kB
HighFree:        30660 kB
LowTotal:       903652 kB
LowFree:        694440 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13208 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:17:27 (client local time) WITH STATUS 10 IN 1200.61 SECONDS
stats: 12660 7 1200.61 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 3452927   bits: 23/22
c ---[  10]---> Adder-cost: 380   maxlim: 3689471   bits: 23/22
c ---[   8]---> Adder-cost: 350   maxlim: 3561471   bits: 23/22
c ---[   6]---> Adder-cost: 340   maxlim: 3823615   bits: 23/22
c ---[   4]---> Adder-cost: 390   maxlim: 3614719   bits: 23/22
c ---[   2]---> Adder-cost: 358   maxlim: 3749887   bits: 23/22
c ---[   0]---> Adder-cost: 374   maxlim: 3556351   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17626    64179 |    5287       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2592          
c   -- var.elim.:  2000/2592          
c   -- var.elim.:  2592/2592          
c   -- var.elim.:  281/281          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  118/118          
c |         0 |   16771    59554 |      --       0       --      -- |     --   | -418/-1339
c |         0 |   16771    59554 |    6708       0        0     nan |  0.000 % |
c |       100 |   16771    59554 |    7379     100      698     7.0 | 13.955 % |
c ==============================================================================
c (current CPU-time: 0.554915 s)
c ==============================================================================
c [1mFound solution: 6554624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       186 |   19439    65782 |    5831     186     2417    13.0 | 13.955 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1014          
c   -- var.elim.:  1014/1014          
c   -- var.elim.:  545/545          
c   -- subsuming                       
c   -- var.elim.:  52/52          
c   -- var.elim.:  13/13          
c |       186 |   19081    66654 |      --     186       --      -- |     --   | -358/873
c |       186 |   19081    66654 |    7632     186     2417    13.0 | 13.955 % |
c ==============================================================================
c (current CPU-time: 0.781881 s)
c ==============================================================================
c [1mFound solution: 6069248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       265 |   19201    66990 |    5760     265     4579    17.3 | 13.955 % |
c   -- subsuming                       
c   -- var.elim.:  214/214          
c   -- var.elim.:  135/135          
c |       265 |   19132    66979 |      --     265       --      -- |     --   | -69/-10
c |       265 |   19132    66979 |    7652     265     4579    17.3 | 13.955 % |
c ==============================================================================
c (current CPU-time: 0.859869 s)
c ==============================================================================
c [1mFound solution: 5647360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       282 |   19178    67125 |    5753     282     5150    18.3 | 13.955 % |
c   -- subsuming                       
c   -- var.elim.:  98/98          
c   -- var.elim.:  73/73          
c |       282 |   19154    67162 |      --     282       --      -- |     --   | -24/38
c |       282 |   19154    67162 |    7661     282     5150    18.3 | 13.955 % |
c |       382 |   19154    67162 |    8427     382    18211    47.7 | 11.935 % |
c ==============================================================================
c (current CPU-time: 1.08983 s)
c ==============================================================================
c [1mFound solution: 5253120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       440 |   19190    67274 |    5756     440    18576    42.2 | 11.935 % |
c   -- subsuming                       
c   -- var.elim.:  75/75          
c   -- var.elim.:  56/56          
c |       440 |   19171    67288 |      --     440       --      -- |     --   | -19/15
c |       440 |   19171    67288 |    7668     440    18576    42.2 | 11.935 % |
c |       542 |   19171    67288 |    8435     542    38121    70.3 | 11.958 % |
c |       692 |   19171    67288 |    9278     692    61476    88.8 | 11.958 % |
c ==============================================================================
c (current CPU-time: 1.59676 s)
c ==============================================================================
c [1mFound solution: 5082112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       699 |   19231    67467 |    5769     699    61624    88.2 | 11.958 % |
c   -- subsuming                       
c   -- var.elim.:  118/118          
c   -- var.elim.:  83/83          
c |       699 |   19204    67696 |      --     699       --      -- |     --   | -27/230
c |       699 |   19204    67696 |    7681     699    61624    88.2 | 11.958 % |
c ==============================================================================
c (current CPU-time: 1.67974 s)
c ==============================================================================
c [1mFound solution: 3433472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       736 |   19259    67870 |    5777     736    62556    85.0 | 11.958 % |
c   -- subsuming                       
c   -- var.elim.:  117/117          
c   -- var.elim.:  84/84          
c |       736 |   19231    67974 |      --     736       --      -- |     --   | -28/105
c |       736 |   19231    67974 |    7692     736    62556    85.0 | 11.958 % |
c ==============================================================================
c (current CPU-time: 1.76373 s)
c ==============================================================================
c [1mFound solution: 3035136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       747 |   19279    68131 |    5783     747    62949    84.3 | 11.958 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  81/81          
c |       747 |   19252    68210 |      --     747       --      -- |     --   | -27/80
c |       747 |   19252    68210 |    7700     747    62949    84.3 | 11.958 % |
c ==============================================================================
c (current CPU-time: 1.83472 s)
c ==============================================================================
c [1mFound solution: 1900544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       759 |   19294    68351 |    5788     759    62985    83.0 | 11.958 % |
c   -- subsuming                       
c   -- var.elim.:  97/97          
c   -- var.elim.:  71/71          
c |       759 |   19273    68387 |      --     759       --      -- |     --   | -21/37
c |       759 |   19273    68387 |    7709     759    62985    83.0 | 11.958 % |
c ==============================================================================
c (current CPU-time: 2.10368 s)
c ==============================================================================
c [1mFound solution: 1768448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       840 |   19310    68514 |    5792     840    80070    95.3 | 11.958 % |
c   -- subsuming                       
c   -- var.elim.:  87/87          
c   -- var.elim.:  68/68          
c   -- var.elim.:  2/2          
c |       840 |   19290    68533 |      --     840       --      -- |     --   | -20/20
c |       840 |   19290    68533 |    7716     840    80070    95.3 | 11.958 % |
c |       941 |   19290    68533 |    8487     941    80645    85.7 | 12.016 % |
c |      1091 |   19290    68533 |    9336    1091    83505    76.5 | 12.016 % |
c |      1316 |   19290    68533 |   10269    1316    90458    68.7 | 12.016 % |
c ==============================================================================
c (current CPU-time: 2.6196 s)
c ==============================================================================
c [1mFound solution: 1587200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1536 |   19323    68650 |    5796    1536   105654    68.8 | 12.016 % |
c   -- subsuming                       
c   -- var.elim.:  82/82          
c   -- var.elim.:  64/64          
c |      1536 |   19305    68659 |      --    1536       --      -- |     --   | -18/10
c |      1536 |   19305    68659 |    7722    1536   105654    68.8 | 12.016 % |
c |      1636 |   19305    68659 |    8494    1636   108492    66.3 | 12.035 % |
c |      1786 |   19305    68659 |    9343    1786   110047    61.6 | 12.035 % |
c |      2011 |   19305    68659 |   10277    2011   112733    56.1 | 12.035 % |
c |      2348 |   19305    68659 |   11305    2348   128911    54.9 | 12.035 % |
c |      2855 |   19305    68659 |   12436    2855   155905    54.6 | 12.035 % |
c |      3614 |   19305    68659 |   13679    3614   186722    51.7 | 12.035 % |
c |      4753 |   19305    68659 |   15047    4753   238405    50.2 | 12.035 % |
c |      6461 |   19305    68659 |   16552    6461   308109    47.7 | 12.035 % |
c |      9024 |   19305    68659 |   18208    9024   418401    46.4 | 12.035 % |
c |     12868 |   19305    68659 |   20028   12868   572118    44.5 | 12.035 % |
c |     18635 |   19305    68659 |   22031   18635   873538    46.9 | 12.035 % |
c |     27287 |   19305    68659 |   24234   17237  1054061    61.2 | 12.035 % |
c |     40261 |   19305    68659 |   26658   18164  1513913    83.3 | 12.035 % |
c |     59724 |   19305    68659 |   29324   22970  1550840    67.5 | 12.035 % |
c |     88918 |   19305    68659 |   32256   19035  1213766    63.8 | 12.035 % |
c |    132707 |   19305    68659 |   35482   23162   927650    40.1 | 12.035 % |
c ==============================================================================
c (current CPU-time: 235.509 s)
c ==============================================================================
c [1mFound solution: 1383424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    152273 |   19329    68741 |    5798   18614  1133373    60.9 | 12.035 % |
c   -- subsuming                       
c   -- var.elim.:  55/55          
c   -- var.elim.:  42/42          
c |    152273 |   19315    68764 |      --   18614       --      -- |     --   | -14/24
c |    152273 |   19315    68764 |    7726   18614  1133373    60.9 | 12.035 % |
c |    152374 |   19310    68697 |    8496    5616   287606    51.2 | 12.083 % |
c |    152525 |   19310    68697 |    9346    5767   289863    50.3 | 12.082 % |
c |    152750 |   19310    68697 |   10280    5992   296713    49.5 | 12.082 % |
c |    153088 |   19310    68697 |   11308    6330   305984    48.3 | 12.082 % |
c |    153594 |   19310    68697 |   12439    6836   327014    47.8 | 12.082 % |
c |    154353 |   19310    68697 |   13683    7595   359652    47.4 | 12.082 % |
c |    155492 |   19310    68697 |   15051    8734   413433    47.3 | 12.082 % |
c |    157200 |   19303    68623 |   16551   10441   472213    45.2 | 12.112 % |
c |    159763 |   19276    68431 |   18180   13002   554777    42.7 | 12.170 % |
c |    163608 |   19276    68431 |   19998   16847   740239    43.9 | 12.170 % |
c |    169374 |   19276    68431 |   21998   14540   648867    44.6 | 12.170 % |
c |    178025 |   19276    68431 |   24198   13232   770364    58.2 | 12.170 % |
c |    19099#### 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.52 0.85 0.88 2/54 1031
Raw data (stat): 1031 (runsolver) R 1030 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491353539 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.001 s]
Raw data (loadavg): 0.59 0.86 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 2893 0 0 0 990 7 0 0 25 0 1 0 491353539 9383936 1787 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2291 1787 603 41 0 2250 0
vsize: 9164
[startup+20.014 s]
Raw data (loadavg): 0.66 0.86 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 3571 0 0 0 1989 10 0 0 25 0 1 0 491353539 12140544 2465 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2964 2465 603 41 0 2923 0
vsize: 11856
[startup+30.0141 s]
Raw data (loadavg): 0.71 0.86 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 3737 0 0 0 2989 10 0 0 25 0 1 0 491353539 12808192 2631 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3127 2631 603 41 0 3086 0
vsize: 12508
[startup+40.0223 s]
Raw data (loadavg): 0.75 0.87 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4119 0 0 0 3990 11 0 0 25 0 1 0 491353539 14389248 3013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 3013 603 41 0 3472 0
vsize: 14052
[startup+50.1347 s]
Raw data (loadavg): 0.79 0.87 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4467 0 0 0 5000 12 0 0 25 0 1 0 491353539 15765504 3360 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3849 3360 603 41 0 3808 0
vsize: 15396
[startup+60.1349 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4467 0 0 0 6001 12 0 0 25 0 1 0 491353539 15765504 3360 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3849 3360 603 41 0 3808 0
vsize: 15396
[startup+70.1347 s]
Raw data (loadavg): 0.85 0.88 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4867 0 0 0 7000 13 0 0 25 0 1 0 491353539 17375232 3759 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3759 603 41 0 4201 0
vsize: 16968
[startup+80.1348 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4867 0 0 0 8000 13 0 0 25 0 1 0 491353539 17375232 3759 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3759 603 41 0 4201 0
vsize: 16968
[startup+90.1353 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4867 0 0 0 9001 13 0 0 25 0 1 0 491353539 17375232 3759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3759 603 41 0 4201 0
vsize: 16968
[startup+100.135 s]
Raw data (loadavg): 0.91 0.89 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4869 0 0 0 10001 13 0 0 25 0 1 0 491353539 17375232 3761 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3761 603 41 0 4201 0
vsize: 16968
[startup+110.143 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4965 0 0 0 11002 13 0 0 25 0 1 0 491353539 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3857 603 41 0 4293 0
vsize: 17336
[startup+120.144 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4965 0 0 0 12002 13 0 0 25 0 1 0 491353539 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3857 603 41 0 4293 0
vsize: 17336
[startup+130.144 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 4965 0 0 0 13002 13 0 0 25 0 1 0 491353539 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3857 603 41 0 4293 0
vsize: 17336
[startup+140.144 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5123 0 0 0 14002 14 0 0 25 0 1 0 491353539 18460672 4015 4294967295 134512640 134672761 3221224544 3221223640 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4015 603 41 0 4466 0
vsize: 18028
[startup+150.148 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 1031
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5123 0 0 0 15003 14 0 0 25 0 1 0 491353539 18460672 4015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4015 603 41 0 4466 0
vsize: 18028
[startup+160.149 s]
Raw data (loadavg): 0.96 0.91 0.89 2/55 1032
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5158 0 0 0 16004 14 0 0 25 0 1 0 491353539 18722816 4050 4294967295 134512640 134672761 3221224544 3221223376 1075349975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4050 603 41 0 4530 0
vsize: 18284
[startup+170.182 s]
Raw data (loadavg): 1.20 0.96 0.91 3/57 1068
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5196 0 0 0 17007 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+180.183 s]
Raw data (loadavg): 1.33 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5196 0 0 0 18007 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+190.185 s]
Raw data (loadavg): 1.27 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5196 0 0 0 19008 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+200.185 s]
Raw data (loadavg): 1.23 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5229 0 0 0 20008 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+210.192 s]
Raw data (loadavg): 1.20 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5229 0 0 0 21009 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+220.2 s]
Raw data (loadavg): 1.16 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5229 0 0 0 22010 14 0 0 25 0 1 0 491353539 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4055 603 41 0 4530 0
vsize: 18284
[startup+230.201 s]
Raw data (loadavg): 1.14 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5271 0 0 0 23011 14 0 0 25 0 1 0 491353539 18722816 4061 4294967295 134512640 134672761 3221224544 3221223728 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4061 603 41 0 4530 0
vsize: 18284
[startup+240.201 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 1084
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 24010 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+250.202 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 25011 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+260.203 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 26011 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+270.204 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 27011 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+280.204 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 28012 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+290.209 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 29013 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+300.21 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 30013 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+310.21 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5390 0 0 0 31013 15 0 0 25 0 1 0 491353539 18853888 4100 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+320.21 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5431 0 0 0 32013 15 0 0 25 0 1 0 491353539 19124224 4141 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4669 4141 603 41 0 4628 0
vsize: 18676
[startup+330.212 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 5892 0 0 0 33012 17 0 0 25 0 1 0 491353539 20975616 4602 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5121 4602 603 41 0 5080 0
vsize: 20484
[startup+340.212 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6206 0 0 0 34012 17 0 0 25 0 1 0 491353539 22208512 4915 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+350.212 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6206 0 0 0 35012 17 0 0 25 0 1 0 491353539 22208512 4915 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+360.213 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6206 0 0 0 36013 17 0 0 25 0 1 0 491353539 22208512 4915 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+370.213 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 37012 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223536 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+380.213 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 38012 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+390.214 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 39012 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+400.214 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 40013 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+410.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 41014 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+420.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 42014 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223584 134612764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+430.221 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6416 0 0 0 43014 18 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223744 134610642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+440.221 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6449 0 0 0 44015 19 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+450.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6449 0 0 0 45015 19 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223584 134603495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+460.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6449 0 0 0 46016 19 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+470.224 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6449 0 0 0 47016 19 0 0 25 0 1 0 491353539 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+480.224 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6482 0 0 0 48016 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+490.224 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6482 0 0 0 49017 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+500.224 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6482 0 0 0 50017 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+510.223 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6518 0 0 0 51017 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+520.223 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6518 0 0 0 52017 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+530.223 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6518 0 0 0 53018 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+540.223 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1086
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6554 0 0 0 54018 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+550.223 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6554 0 0 0 55018 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+560.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6554 0 0 0 56018 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+570.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6554 0 0 0 57019 19 0 0 25 0 1 0 491353539 23027712 5119 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+580.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6590 0 0 0 58019 19 0 0 25 0 1 0 491353539 23023616 5118 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+590.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6590 0 0 0 59019 19 0 0 25 0 1 0 491353539 23023616 5118 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+600.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6590 0 0 0 60020 19 0 0 25 0 1 0 491353539 23023616 5118 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+610.222 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6590 0 0 0 61020 19 0 0 25 0 1 0 491353539 23023616 5118 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+620.221 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6941 0 0 0 62019 20 0 0 25 0 1 0 491353539 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+630.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6941 0 0 0 63019 20 0 0 25 0 1 0 491353539 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+640.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6941 0 0 0 64020 20 0 0 25 0 1 0 491353539 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+650.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 6941 0 0 0 65020 20 0 0 25 0 1 0 491353539 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+660.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7316 0 0 0 66018 22 0 0 25 0 1 0 491353539 25870336 5804 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6316 5804 603 41 0 6275 0
vsize: 25264
[startup+670.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 67017 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+680.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 68018 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+690.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 69018 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+700.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 70018 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+710.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 71019 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+720.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7687 0 0 0 72019 23 0 0 25 0 1 0 491353539 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+730.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7727 0 0 0 73019 24 0 0 25 0 1 0 491353539 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+740.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7727 0 0 0 74019 24 0 0 25 0 1 0 491353539 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+750.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7727 0 0 0 75020 24 0 0 25 0 1 0 491353539 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+760.219 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7727 0 0 0 76020 24 0 0 25 0 1 0 491353539 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+770.218 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7727 0 0 0 77020 24 0 0 25 0 1 0 491353539 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+780.218 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7982 0 0 0 78020 24 0 0 25 0 1 0 491353539 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+790.218 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7982 0 0 0 79020 24 0 0 25 0 1 0 491353539 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+800.217 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7982 0 0 0 80021 24 0 0 25 0 1 0 491353539 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+810.217 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7982 0 0 0 81021 24 0 0 25 0 1 0 491353539 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+820.217 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7982 0 0 0 82021 24 0 0 25 0 1 0 491353539 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+830.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 7983 0 0 0 83021 24 0 0 25 0 1 0 491353539 28057600 6350 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6850 6350 603 41 0 6809 0
vsize: 27400
[startup+840.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8055 0 0 0 84022 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+850.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8055 0 0 0 85022 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+860.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8055 0 0 0 86022 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+870.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8055 0 0 0 87023 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+880.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8055 0 0 0 88023 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+890.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 89023 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+900.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 90024 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+910.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 91024 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+920.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 92024 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+930.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 93025 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+940.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 94025 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+950.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8098 0 0 0 95025 24 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+960.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 96025 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+970.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 97026 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+980.216 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 98026 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+990.217 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 99026 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+1000.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 100027 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+1010.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 101027 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+1020.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8141 0 0 0 102027 25 0 0 25 0 1 0 491353539 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+1030.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 103028 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1040.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 104028 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1050.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 105028 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1060.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 106029 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1070.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 107029 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1080.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8208 0 0 0 108029 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1090.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 109030 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1100.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 110030 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1110.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 111030 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1120.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 112031 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1130.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 113031 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1140.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 114031 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1150.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8251 0 0 0 115032 25 0 0 25 0 1 0 491353539 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1160.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8296 0 0 0 116032 25 0 0 25 0 1 0 491353539 28528640 6448 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6965 6448 603 41 0 6924 0
vsize: 27860
[startup+1170.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8608 0 0 0 117032 26 0 0 25 0 1 0 491353539 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1180.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8608 0 0 0 118032 26 0 0 25 0 1 0 491353539 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1190.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8608 0 0 0 119032 26 0 0 25 0 1 0 491353539 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1200.22 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1088
Raw data (stat): 1031 (minisat+) R 1030 29653 29652 0 -1 0 8608 0 0 0 120033 26 0 0 25 0 1 0 491353539 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 1088
Raw data (stat): 1031 (minisat+) Z 1030 29653 29652 0 -1 12 8609 0 0 0 120033 27 0 0 25 0 1 0 491353539 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.24
CPU time (s): 1200.61
CPU user time (s): 1200.33
CPU system time (s): 0.274958
CPU usage (%): 100.031
Max. virtual memory (Kb): 29064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####