PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	111dddb6adf389a5275ab413feff6076
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.36
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 16388

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 07:07:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13531 boxname=wulflinc1 idbench=1041 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  111dddb6adf389a5275ab413feff6076  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 13531
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        505608 kB
Buffers:          8032 kB
Cached:         493504 kB
SwapCached:        168 kB
Active:         305240 kB
Inactive:       199636 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        505356 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            18452 kB
Committed_AS:    92804 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:27:07 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 13531 7 1200.2 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.546916 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.761884 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.836872 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.06284 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.56676 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.65175 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.73174 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.80373 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.06569 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.57261 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: 232.856 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 |    1909#### 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.47 0.81 0.86 2/56 23711
Raw data (stat): 23711 (runsolver) R 23710 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 428076227 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.0004 s]
Raw data (loadavg): 0.55 0.82 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 2897 0 0 0 990 9 0 0 25 0 1 0 428076227 9383936 1791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2291 1791 603 41 0 2250 0
vsize: 9164
[startup+20.0012 s]
Raw data (loadavg): 0.62 0.82 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 3586 0 0 0 1988 11 0 0 25 0 1 0 428076227 12140544 2480 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2964 2480 603 41 0 2923 0
vsize: 11856
[startup+30.001 s]
Raw data (loadavg): 0.68 0.83 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 3737 0 0 0 2987 12 0 0 25 0 1 0 428076227 12808192 2631 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3127 2631 603 41 0 3086 0
vsize: 12508
[startup+40.0007 s]
Raw data (loadavg): 0.73 0.83 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4155 0 0 0 3986 13 0 0 25 0 1 0 428076227 14520320 3049 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3545 3049 603 41 0 3504 0
vsize: 14180
[startup+50.0014 s]
Raw data (loadavg): 0.77 0.84 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4467 0 0 0 4985 14 0 0 25 0 1 0 428076227 15765504 3360 4294967295 134512640 134672761 3221224544 3221223552 134522369 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.0016 s]
Raw data (loadavg): 0.80 0.84 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4467 0 0 0 5985 14 0 0 25 0 1 0 428076227 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+70.002 s]
Raw data (loadavg): 0.83 0.85 0.86 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4867 0 0 0 6984 16 0 0 25 0 1 0 428076227 17375232 3759 4294967295 134512640 134672761 3221224544 3221223680 134614677 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.0018 s]
Raw data (loadavg): 0.86 0.85 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4867 0 0 0 7984 16 0 0 25 0 1 0 428076227 17375232 3759 4294967295 134512640 134672761 3221224544 3221223728 134615564 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.0015 s]
Raw data (loadavg): 0.88 0.86 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4867 0 0 0 8984 16 0 0 25 0 1 0 428076227 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.001 s]
Raw data (loadavg): 0.90 0.86 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4873 0 0 0 9984 16 0 0 25 0 1 0 428076227 17375232 3765 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4242 3765 603 41 0 4201 0
vsize: 16968
[startup+110.002 s]
Raw data (loadavg): 0.91 0.86 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4965 0 0 0 10984 16 0 0 25 0 1 0 428076227 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.002 s]
Raw data (loadavg): 0.93 0.87 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4965 0 0 0 11985 16 0 0 25 0 1 0 428076227 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615741 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.002 s]
Raw data (loadavg): 0.94 0.87 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 4965 0 0 0 12985 16 0 0 25 0 1 0 428076227 17752064 3857 4294967295 134512640 134672761 3221224544 3221223728 134615585 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.002 s]
Raw data (loadavg): 0.95 0.88 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5123 0 0 0 13985 16 0 0 25 0 1 0 428076227 18460672 4015 4294967295 134512640 134672761 3221224544 3221223728 134615755 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.002 s]
Raw data (loadavg): 0.95 0.88 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5123 0 0 0 14985 16 0 0 25 0 1 0 428076227 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.003 s]
Raw data (loadavg): 0.96 0.88 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5196 0 0 0 15985 16 0 0 25 0 1 0 428076227 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+170.003 s]
Raw data (loadavg): 0.97 0.89 0.87 2/56 23711
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5196 0 0 0 16985 16 0 0 25 0 1 0 428076227 18722816 4055 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.003 s]
Raw data (loadavg): 0.97 0.89 0.87 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5196 0 0 0 17985 16 0 0 25 0 1 0 428076227 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615755 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.003 s]
Raw data (loadavg): 0.98 0.89 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5196 0 0 0 18985 16 0 0 25 0 1 0 428076227 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.003 s]
Raw data (loadavg): 0.98 0.90 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5229 0 0 0 19985 16 0 0 25 0 1 0 428076227 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615681 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.003 s]
Raw data (loadavg): 0.98 0.90 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5229 0 0 0 20986 16 0 0 25 0 1 0 428076227 18722816 4055 4294967295 134512640 134672761 3221224544 3221223728 134615724 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.004 s]
Raw data (loadavg): 0.98 0.90 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5230 0 0 0 21986 16 0 0 25 0 1 0 428076227 18722816 4056 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4571 4056 603 41 0 4530 0
vsize: 18284
[startup+230.004 s]
Raw data (loadavg): 0.99 0.90 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5271 0 0 0 22986 16 0 0 25 0 1 0 428076227 18722816 4061 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.004 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 23986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+250.004 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 24986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223620 1075347023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+260.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 25986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223680 134614715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+270.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 26986 17 0 0 25 0 1 0 428076227 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+280.005 s]
Raw data (loadavg): 0.99 0.92 0.88 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 27986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615689 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.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 28986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615665 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.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 29986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5390 0 0 0 30986 17 0 0 25 0 1 0 428076227 18853888 4100 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4100 603 41 0 4562 0
vsize: 18412
[startup+320.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 5643 0 0 0 31985 19 0 0 25 0 1 0 428076227 19922944 4353 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4864 4353 603 41 0 4823 0
vsize: 19456
[startup+330.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6085 0 0 0 32983 20 0 0 25 0 1 0 428076227 21770240 4795 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5315 4795 603 41 0 5274 0
vsize: 21260
[startup+340.006 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6206 0 0 0 33983 21 0 0 25 0 1 0 428076227 22208512 4915 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+350.006 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6206 0 0 0 34983 21 0 0 25 0 1 0 428076227 22208512 4915 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+360.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6206 0 0 0 35983 21 0 0 25 0 1 0 428076227 22208512 4915 4294967295 134512640 134672761 3221224544 3221223728 134615557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5422 4915 603 41 0 5381 0
vsize: 21688
[startup+370.008 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 36983 21 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+380.007 s]
Raw data (loadavg): 0.99 0.94 0.89 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 37983 21 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+390.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 38983 21 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+400.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 39983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+410.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 40983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+420.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6416 0 0 0 41983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+430.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6449 0 0 0 42983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+440.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6449 0 0 0 43983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+450.01 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6449 0 0 0 44983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+460.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6449 0 0 0 45983 22 0 0 25 0 1 0 428076227 23052288 5124 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5628 5124 603 41 0 5587 0
vsize: 22512
[startup+470.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 23713
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6482 0 0 0 46983 22 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+480.011 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6482 0 0 0 47983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+490.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6482 0 0 0 48983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+500.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6518 0 0 0 49983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+510.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6518 0 0 0 50983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615749 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.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6518 0 0 0 51983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6518 0 0 0 52983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6554 0 0 0 53983 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6554 0 0 0 54984 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+560.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6554 0 0 0 55984 23 0 0 25 0 1 0 428076227 23027712 5119 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5622 5119 603 41 0 5581 0
vsize: 22488
[startup+570.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6590 0 0 0 56984 23 0 0 25 0 1 0 428076227 23023616 5118 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+580.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6590 0 0 0 57984 24 0 0 25 0 1 0 428076227 23023616 5118 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+590.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6590 0 0 0 58984 24 0 0 25 0 1 0 428076227 23023616 5118 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+600.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6590 0 0 0 59984 24 0 0 25 0 1 0 428076227 23023616 5118 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5621 5118 603 41 0 5580 0
vsize: 22484
[startup+610.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6941 0 0 0 60983 25 0 0 25 0 1 0 428076227 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+620.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6941 0 0 0 61983 25 0 0 25 0 1 0 428076227 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+630.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6941 0 0 0 62983 25 0 0 25 0 1 0 428076227 24285184 5429 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5929 5429 603 41 0 5888 0
vsize: 23716
[startup+640.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 6969 0 0 0 63983 25 0 0 25 0 1 0 428076227 24416256 5457 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5961 5457 603 41 0 5920 0
vsize: 23844
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7422 0 0 0 64982 27 0 0 25 0 1 0 428076227 26263552 5910 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6412 5910 603 41 0 6371 0
vsize: 25648
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7687 0 0 0 65981 27 0 0 25 0 1 0 428076227 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7687 0 0 0 66981 27 0 0 25 0 1 0 428076227 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7687 0 0 0 67981 28 0 0 25 0 1 0 428076227 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7687 0 0 0 68981 28 0 0 25 0 1 0 428076227 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7687 0 0 0 69982 28 0 0 25 0 1 0 428076227 27181056 6135 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6135 603 41 0 6595 0
vsize: 26544
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7727 0 0 0 70982 28 0 0 25 0 1 0 428076227 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7727 0 0 0 71982 28 0 0 25 0 1 0 428076227 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7727 0 0 0 72982 28 0 0 25 0 1 0 428076227 27176960 6134 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7727 0 0 0 73982 28 0 0 25 0 1 0 428076227 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7727 0 0 0 74982 29 0 0 25 0 1 0 428076227 27176960 6134 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 6134 603 41 0 6594 0
vsize: 26540
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7805 0 0 0 75982 29 0 0 25 0 1 0 428076227 27570176 6212 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6731 6212 603 41 0 6690 0
vsize: 26924
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23715
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7982 0 0 0 76982 29 0 0 25 0 1 0 428076227 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7982 0 0 0 77982 29 0 0 25 0 1 0 428076227 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7982 0 0 0 78982 29 0 0 25 0 1 0 428076227 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7982 0 0 0 79982 29 0 0 25 0 1 0 428076227 28057600 6349 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 7982 0 0 0 80982 29 0 0 25 0 1 0 428076227 28057600 6349 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6850 6349 603 41 0 6809 0
vsize: 27400
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 81982 29 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 82982 29 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 83982 29 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 84982 29 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 85983 29 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8055 0 0 0 86983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 87983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 88983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 89983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 90983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 91983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8098 0 0 0 92983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 93983 30 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 94983 31 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 95983 31 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 96983 31 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 97983 31 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8141 0 0 0 98983 31 0 0 25 0 1 0 428076227 28168192 6379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6877 6379 603 41 0 6836 0
vsize: 27508
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 99983 31 0 0 25 0 1 0 428076227 28528640 6446 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6965 6446 603 41 0 6924 0
vsize: 27860
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 100983 31 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 101983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 102983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 103983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8208 0 0 0 104983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 105983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23717
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 106983 32 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 107982 33 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 108982 33 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 109982 33 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 110982 34 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8251 0 0 0 111983 34 0 0 25 0 1 0 428076227 28266496 6403 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6403 603 41 0 6860 0
vsize: 27604
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8252 0 0 0 112982 34 0 0 25 0 1 0 428076227 28266496 6404 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6404 603 41 0 6860 0
vsize: 27604
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8418 0 0 0 113982 34 0 0 25 0 1 0 428076227 29057024 6570 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7094 6570 603 41 0 7053 0
vsize: 28376
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 114982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 115982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 116982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 117982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 118982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 23719
Raw data (stat): 23711 (minisat+) R 23710 12452 12451 0 -1 0 8608 0 0 0 119982 35 0 0 25 0 1 0 428076227 29761536 6743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7266 6743 603 41 0 7225 0
vsize: 29064
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 23719
Raw data (stat): 23711 (minisat+) Z 23710 12452 12451 0 -1 12 8609 0 0 0 119982 36 0 0 25 0 1 0 428076227 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.05
CPU time (s): 1200.2
CPU user time (s): 1199.83
CPU system time (s): 0.366944
CPU usage (%): 100.012
Max. virtual memory (Kb): 29064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####