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/miplib/normalized-mps-v2-20-10-p0291.opb
MD5SUM	1d9168a9335e29df835d07b0bdf2adea
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10447498
Optimality of the best value was proved	NO
Number of terms in the objective function	289
Biggest coefficient in the objective function	80000000
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	686518451
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	80000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	686518451
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.335948
Number of variables	291
Total number of constraints	543
Number of constraints which are clauses	189
Number of constraints which are cardinality constraints (but not clauses)	295
Number of constraints which are nor clauses,nor cardinality constraints	59
Minimum length of a constraint	1
Maximum length of a constraint	53
Trace number 16949

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        380568 kB
Buffers:         15612 kB
Cached:         615564 kB
SwapCached:          0 kB
Active:          32680 kB
Inactive:       601288 kB
HighTotal:      131008 kB
HighFree:        30156 kB
LowTotal:       903652 kB
LowFree:        350412 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14428 kB
Committed_AS:    71664 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:28:44 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 12154 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[  14]---> BDD-cost: 1177
c ---[  13]---> BDD-cost:  845
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> BDD-cost:   52
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   28
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:  203
c ---[   1]---> BDD-cost:  144
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6438    18748 |    2146       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 205610566[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:118485     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |  345759   810983 |  115253       3       14     4.7 |  0.000 % |
c |       105 |  345605   810638 |  126778      90     3745    41.6 |  0.053 % |
c |       257 |  345605   810638 |  139456     242     4405    18.2 |  0.053 % |
c |       482 |  345521   810449 |  153401     466     5963    12.8 |  0.072 % |
c |       819 |  345470   810334 |  168741     801    10036    12.5 |  0.084 % |
c |      1326 |  345077   809448 |  185616    1300    26997    20.8 |  0.173 % |
c ==============================================================================
c [1mFound solution: 188210471[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1853 |  345424   811112 |  115141    1827    47761    26.1 |  0.173 % |
c |      1954 |  345424   811112 |  126655    1928    48929    25.4 |  0.174 % |
c |      2104 |  345344   810932 |  139320    2077    50614    24.4 |  0.192 % |
c |      2329 |  345082   810339 |  153252    2293    63404    27.7 |  0.256 % |
c |      2667 |  345082   810339 |  168577    2631    68864    26.2 |  0.256 % |
c |      3173 |  344865   809850 |  185435    3133    72787    23.2 |  0.308 % |
c |      3932 |  344812   809729 |  203979    3890    95012    24.4 |  0.322 % |
c ==============================================================================
c [1mFound solution: 146185330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4265 |  345263   810880 |  115087    4222   107076    25.4 |  0.322 % |
c ==============================================================================
c [1mFound solution: 146185307[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4335 |  345177   810772 |  115059    4290   108180    25.2 |  0.322 % |
c |      4435 |  345177   810772 |  126564    4390   114217    26.0 |  0.353 % |
c ==============================================================================
c [1mFound solution: 108859876[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4562 |  345206   810848 |  115068    4517   125721    27.8 |  0.353 % |
c |      4662 |  345206   810848 |  126574    4617   126443    27.4 |  0.354 % |
c |      4813 |  345206   810848 |  139232    4768   127286    26.7 |  0.354 % |
c |      5040 |  345206   810848 |  153155    4995   134670    27.0 |  0.354 % |
c |      5377 |  345206   810848 |  168471    5332   166177    31.2 |  0.354 % |
c |      5885 |  345206   810848 |  185318    5840   181749    31.1 |  0.354 % |
c |      6644 |  345145   810712 |  203849    6591   199356    30.2 |  0.368 % |
c |      7785 |  345068   810540 |  224234    7724   250500    32.4 |  0.386 % |
c |      9494 |  345068   810540 |  246658    9433   321015    34.0 |  0.386 % |
c ==============================================================================
c [1mFound solution: 106925952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11853 |  345060   810552 |  115020   11778   432735    36.7 |  0.386 % |
c |     11954 |  345060   810552 |  126522   11879   433846    36.5 |  0.432 % |
c |     12104 |  345060   810552 |  139174   12029   435141    36.2 |  0.432 % |
c |     12330 |  345060   810552 |  153091   12255   437802    35.7 |  0.432 % |
c |     12667 |  345060   810552 |  168400   12592   452162    35.9 |  0.432 % |
c ==============================================================================
c [1mFound solution: 85083591[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13170 |  345079   810603 |  115026   13095   519296    39.7 |  0.432 % |
c |     13271 |  344622   809567 |  126528   13174   521970    39.6 |  0.538 % |
c |     13421 |  344622   809567 |  139181   13324   525178    39.4 |  0.538 % |
c |     13648 |  344480   809245 |  153099   13547   526252    38.8 |  0.574 % |
c |     13985 |  344480   809245 |  168409   13884   541214    39.0 |  0.574 % |
c |     14491 |  344480   809245 |  185250   14390   595620    41.4 |  0.574 % |
c |     15250 |  343815   807729 |  203775   15121   613759    40.6 |  0.737 % |
c |     16391 |  343769   807626 |  224153   16260   657301    40.4 |  0.747 % |
c |     18100 |  343710   807492 |  246568   17968   705751    39.3 |  0.761 % |
c |     20662 |  343710   807492 |  271225   20530   741623    36.1 |  0.761 % |
c ==============================================================================
c [1mFound solution: 85076950[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21255 |  343946   808129 |  114648   21116   746090    35.3 |  0.761 % |
c |     21355 |  343946   808129 |  126112   21216   752257    35.5 |  0.834 % |
c |     21505 |  343946   808129 |  138724   21366   753045    35.2 |  0.834 % |
c |     21730 |  343946   808129 |  152596   21591   754515    34.9 |  0.834 % |
c |     22067 |  343885   807990 |  167856   21925   779075    35.5 |  0.849 % |
c |     22573 |  343885   807990 |  184641   22431   815874    36.4 |  0.849 % |
c ==============================================================================
c [1mFound solution: 51875083[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:52778     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22993 |  483996  1135483 |  161332   22540   824610    36.6 |  0.849 % |
c |     23094 |  483917  1135305 |  177465   22640   827755    36.6 |  1.801 % |
c |     23244 |  483917  1135305 |  195211   22790   830876    36.5 |  1.801 % |
c |     23471 |  483917  1135305 |  214732   23017   840506    36.5 |  1.801 % |
c |     23808 |  483917  1135305 |  236206   23354   842629    36.1 |  1.801 % |
c |     24315 |  483102  1133437 |  259826   23750   856772    36.1 |  1.953 % |
c |     25074 |  483102  1133437 |  285809   24509   887149    36.2 |  1.953 % |
c ==============================================================================
c [1mFound solution: 51875003[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:84180     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25293 |  719985  1686385 |  239995   24726   892155    36.1 |  1.953 % |
c |     25393 |  719985  1686385 |  263994   24826   896024    36.1 |  1.465 % |
c |     25543 |  719837  1686051 |  290393   24974   915584    36.7 |  1.482 % |
c |     25768 |  719307  1684869 |  319433   25193   918458    36.5 |  1.542 % |
c |     26105 |  717743  1681299 |  351376   25412   930760    36.6 |  1.731 % |
c ==============================================================================
c [1mFound solution: 51553993[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26208 |  717978  1682432 |  239326   25475   934456    36.7 |  1.731 % |
c |     26309 |  717693  1681785 |  263258   25571   935996    36.6 |  1.778 % |
c |     26459 |  717546  1681452 |  289584   25717   936744    36.4 |  1.795 % |
c |     26684 |  717530  1681416 |  318542   25936   940005    36.2 |  1.796 % |
c |     27021 |  716549  1679189 |  350397   26242   941692    35.9 |  1.910 % |
c |     27527 |  716408  1678871 |  385436   26743   962521    36.0 |  1.927 % |
c |     28287 |  716408  1678871 |  423980   27503   982546    35.7 |  1.927 % |
c ==============================================================================
c [1mFound solution: 51472157[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29242 |  716311  1678811 |  238770   28429  1045650    36.8 |  1.927 % |
c |     29342 |  716281  1678743 |  262647   28525  1046711    36.7 |  2.005 % |
c ==============================================================================
c [1mFound solution: 50734660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29366 |  716374  1679102 |  238791   28549  1047371    36.7 |  2.005 % |
c ==============================================================================
c [1mFound solution: 50724062[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29397 |  716388  1679156 |  238796   28580  1048585    36.7 |  2.005 % |
c |     29497 |  716388  1679156 |  262675   28680  1049225    36.6 |  2.006 % |
c |     29647 |  712828  1671026 |  288943   28771  1049935    36.5 |  2.422 % |
c |     29872 |  712397  1670037 |  317837   28991  1055758    36.4 |  2.475 % |
c |     30209 |  711346  1667626 |  349621   29155  1076015    36.9 |  2.606 % |
c |     30715 |  711346  1667626 |  384583   29661  1111727    37.5 |  2.606 % |
c ==============================================================================
c [1mFound solution: 50550635[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30835 |  711358  1667667 |  237119   29781  1118170    37.5 |  2.606 % |
c |     30935 |  711358  1667667 |  260830   29881  1124601    37.6 |  2.606 % |
c |     31086 |  709417  1663202 |  286913   29878  1126051    37.7 |  2.848 % |
c |     31312 |  709417  1663202 |  315605   30104  1133909    37.7 |  2.848 % |
c ==============================================================================
c [1mFound solution: 50550442[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31498 |  709430  1663240 |  236476   30290  1156462    38.2 |  2.848 % |
c |     31600 |  709430  1663240 |  260123   30391  1160746    38.2 |  2.852 % |
c ==============================================================================
c [1mFound solution: 45379256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23266     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31675 |  765272  1793710 |  255090   30323  1154339    38.1 |  2.852 % |
c |     31775 |  765272  1793710 |  280599   30423  1155803    38.0 |  3.477 % |
c |     31925 |  765272  1793710 |  308658   30573  1160513    38.0 |  3.477 % |
c |     32152 |  763211  1789011 |  339524   30745  1162558    37.8 |  3.705 % |
c |     32489 |  763211  1789011 |  373477   31082  1206559    38.8 |  3.705 % |
c |     32997 |  763211  1789011 |  410824   31590  1234463    39.1 |  3.705 % |
c ==============================================================================
c [1mFound solution: 44222971[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:78899     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33531 |  980489  2296150 |  326829   31882  1224198    38.4 |  3.705 % |
c |     33631 |  978465  2291563 |  359511   31885  1221354    38.3 |  3.628 % |
c |     33781 |  800145  1880269 |  395463   26247   869217    33.1 | 19.914 % |
c ==============================================================================
c [1mFound solution: 28913802[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85693     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33918 | 1013010  2377890 |  337670   25098   795849    31.7 | 19.914 % |
c |     34018 | 1012919  2377678 |  371437   25197   796428    31.6 | 18.299 % |
c |     34169 | 1012919  2377678 |  408580   25348   813578    32.1 | 18.299 % |
c |     34394 | 1012173  2375961 |  449438   25566   820041    32.1 | 18.355 % |
c ==============================================================================
c [1mFound solution: 25746408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:54578     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34521 | 1164173  2731215 |  388057   25693   827573    32.2 | 18.355 % |
c |     34621 | 1164173  2731215 |  426862   25793   828997    32.1 | 16.377 % |
c |     34771 | 1164060  2730960 |  469548   25939   833010    32.1 | 16.383 % |
c |     34996 | 1164060  2730960 |  516503   26164   860805    32.9 | 16.383 % |
c |     35334 | 1164060  2730960 |  568154   26502   891785    33.6 | 16.383 % |
c |     35840 | 1164060  2730960 |  624969   27008   901110    33.4 | 16.383 % |
c |     36599 | 1162439  2727228 |  687466   27652   909409    32.9 | 16.485 % |
c ==============================================================================
c [1mFound solution: 25678207[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37494 | 1163000  2729107 |  387666   28544   939199    32.9 | 16.485 % |
c |     37595 | 1163000  2729107 |  426432   28645   940262    32.8 | 16.478 % |
c |     37745 | 1162926  2728941 |  469075   28794   941027    32.7 | 16.482 % |
c ==============================================================================
c [1mFound solution: 25107592[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37809 | 1162582  2728324 |  387527   28854   944060    32.7 | 16.482 % |
#### 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.85 0.97 0.94 2/54 5028
Raw data (stat): 5028 (runsolver) R 5027 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485656577 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.0003 s]
Raw data (loadavg): 0.87 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 910 483 603 41 0 869 0
vsize: 3640
[startup+20.001 s]
Raw data (loadavg): 0.89 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 1997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 910 483 603 41 0 869 0
vsize: 3640
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 2997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222496 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 910 483 603 41 0 869 0
vsize: 3640
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 3996 2 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 910 483 603 41 0 869 0
vsize: 3640
[startup+50.002 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 9944 0 0 0 4972 26 0 0 25 0 1 0 485656577 42864640 9607 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10465 9607 603 41 0 10424 0
vsize: 41860
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 5971 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221221232 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 6972 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221221952 134597193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 7971 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222672 134597262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+90.0038 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 8971 28 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 9971 28 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10161 0 0 0 10970 29 0 0 25 0 1 0 485656577 43905024 9823 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9823 603 41 0 10678 0
vsize: 42876
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 11970 29 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9890 603 41 0 10758 0
vsize: 43196
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 12970 29 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221376 134597165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9890 603 41 0 10758 0
vsize: 43196
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 13969 30 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9890 603 41 0 10758 0
vsize: 43196
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 14969 30 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9890 603 41 0 10758 0
vsize: 43196
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 15969 31 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9890 603 41 0 10758 0
vsize: 43196
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 16969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221222208 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 17968 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221221656 134597415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 18969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221222384 134597215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 19969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10265 0 0 0 20969 31 0 0 25 0 1 0 485656577 44232704 9924 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9924 603 41 0 10758 0
vsize: 43196
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 21969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 22969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 23969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222240 134597203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 24970 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10290 0 0 0 25970 31 0 0 25 0 1 0 485656577 44343296 9949 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10826 9949 603 41 0 10785 0
vsize: 43304
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10338 0 0 0 26970 31 0 0 25 0 1 0 485656577 44605440 9997 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10890 9997 603 41 0 10849 0
vsize: 43560
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10376 0 0 0 27970 31 0 0 25 0 1 0 485656577 44740608 10035 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10923 10035 603 41 0 10882 0
vsize: 43692
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10469 0 0 0 28970 32 0 0 25 0 1 0 485656577 45146112 10128 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11022 10128 603 41 0 10981 0
vsize: 44088
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10572 0 0 0 29969 33 0 0 25 0 1 0 485656577 45551616 10231 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11121 10231 603 41 0 11080 0
vsize: 44484
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 30969 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 31969 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222528 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 32970 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222240 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 33970 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221221808 134597012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10647 0 0 0 34970 33 0 0 25 0 1 0 485656577 45891584 10303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11204 10303 603 41 0 11163 0
vsize: 44816
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 35970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 36970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 37970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 38970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10741 0 0 0 39970 33 0 0 25 0 1 0 485656577 46157824 10396 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10396 603 41 0 11228 0
vsize: 45076
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10788 0 0 0 40970 33 0 0 25 0 1 0 485656577 46428160 10443 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 10443 603 41 0 11294 0
vsize: 45340
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10888 0 0 0 41970 34 0 0 25 0 1 0 485656577 46899200 10543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11450 10543 603 41 0 11409 0
vsize: 45800
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 42970 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 43971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221221632 134522373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 44971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221221952 134597008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 45971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221223104 134597195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 46971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11058 0 0 0 47971 34 0 0 25 0 1 0 485656577 47562752 10709 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11612 10709 603 41 0 11571 0
vsize: 46448
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 48971 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 49971 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 50972 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222148 1074971756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 51972 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15507 0 0 0 52962 44 0 0 25 0 1 0 485656577 70733824 14828 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 14828 603 41 0 17228 0
vsize: 69076
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15524 0 0 0 53962 44 0 0 25 0 1 0 485656577 70733824 14845 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 14845 603 41 0 17228 0
vsize: 69076
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 54962 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221520 134597225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 55962 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221520 134597185 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 56963 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 57963 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21724 0 0 0 58950 57 0 0 25 0 1 0 485656577 91209728 21045 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 21045 603 41 0 22227 0
vsize: 89072
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21782 0 0 0 59950 57 0 0 25 0 1 0 485656577 91344896 21103 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22301 21103 603 41 0 22260 0
vsize: 89204
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 60950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221221952 134597256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 61950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 62950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 63951 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21980 0 0 0 64951 58 0 0 25 0 1 0 485656577 91488256 21298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22336 21298 603 41 0 22295 0
vsize: 89344
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22037 0 0 0 65951 58 0 0 25 0 1 0 485656577 91750400 21355 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22400 21355 603 41 0 22359 0
vsize: 89600
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22060 0 0 0 66951 58 0 0 25 0 1 0 485656577 91885568 21378 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22433 21378 603 41 0 22392 0
vsize: 89732
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 67951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 68951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 69951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 70952 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 71952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 72952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221548 1075346551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 73952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221952 134597161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 74953 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221222384 134597018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 75953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 76953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 77953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221808 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 78953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221952 134597195 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22162 0 0 0 79953 58 0 0 25 0 1 0 485656577 92192768 21474 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22508 21474 603 41 0 22467 0
vsize: 90032
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22162 0 0 0 80954 58 0 0 25 0 1 0 485656577 92192768 21474 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22508 21474 603 41 0 22467 0
vsize: 90032
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22184 0 0 0 81954 58 0 0 25 0 1 0 485656577 92327936 21496 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22541 21496 603 41 0 22500 0
vsize: 90164
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 82954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 83954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 84954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221221808 134597203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 85954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22239 0 0 0 86954 58 0 0 25 0 1 0 485656577 92499968 21550 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22583 21550 603 41 0 22542 0
vsize: 90332
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 87955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 88955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 89955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 90955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22280 0 0 0 91955 58 0 0 25 0 1 0 485656577 92655616 21588 4294967295 134512640 134672761 3221224544 3221223808 134562470 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22621 21588 603 41 0 22580 0
vsize: 90484
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 92955 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 93956 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222096 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+950.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 94956 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+960.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 95957 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222496 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+970.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23850 0 0 0 96953 63 0 0 25 0 1 0 485656577 117944320 23158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28795 23158 603 41 0 28754 0
vsize: 115180
[startup+980.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23866 0 0 0 97953 63 0 0 25 0 1 0 485656577 117944320 23174 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28795 23174 603 41 0 28754 0
vsize: 115180
[startup+990.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23902 0 0 0 98953 63 0 0 25 0 1 0 485656577 118075392 23210 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28827 23210 603 41 0 28786 0
vsize: 115308
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23945 0 0 0 99953 63 0 0 25 0 1 0 485656577 118214656 23253 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 23253 603 41 0 28820 0
vsize: 115444
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 100953 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 101954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222816 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 102954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222352 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 103954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222784 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 30994 0 0 0 104940 78 0 0 25 0 1 0 485656577 138240000 29643 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33750 29643 603 41 0 33709 0
vsize: 135000
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 31071 0 0 0 105940 78 0 0 25 0 1 0 485656577 139563008 29720 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34073 29720 603 41 0 34032 0
vsize: 136292
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 31071 0 0 0 106940 78 0 0 25 0 1 0 485656577 139563008 29720 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34073 29720 603 41 0 34032 0
vsize: 136292
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 35907 0 0 0 107929 89 0 0 25 0 1 0 485656577 152698880 34556 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37280 34556 603 41 0 37239 0
vsize: 149120
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 35981 0 0 0 108929 89 0 0 25 0 1 0 485656577 152698880 34630 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37280 34630 603 41 0 37239 0
vsize: 149120
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 36067 0 0 0 109929 90 0 0 25 0 1 0 485656577 152698880 34716 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37280 34716 603 41 0 37239 0
vsize: 149120
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39755 0 0 0 110922 97 0 0 25 0 1 0 485656577 167436288 38404 4294967295 134512640 134672761 3221224544 3221219584 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40878 38405 603 41 0 40837 0
vsize: 163512
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39799 0 0 0 111922 97 0 0 25 0 1 0 485656577 167706624 38448 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 38448 603 41 0 40903 0
vsize: 163776
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39843 0 0 0 112922 97 0 0 25 0 1 0 485656577 167841792 38492 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40977 38492 603 41 0 40936 0
vsize: 163908
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39895 0 0 0 113922 97 0 0 25 0 1 0 485656577 167976960 38544 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41010 38544 603 41 0 40969 0
vsize: 164040
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39997 0 0 0 114922 97 0 0 25 0 1 0 485656577 168124416 38646 4294967295 134512640 134672761 3221224544 3221221868 1075349761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41046 38646 603 41 0 41005 0
vsize: 164184
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39997 0 0 0 115922 97 0 0 25 0 1 0 485656577 168124416 38646 4294967295 134512640 134672761 3221224544 3221222240 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41046 38646 603 41 0 41005 0
vsize: 164184
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40026 0 0 0 116922 98 0 0 25 0 1 0 485656577 168124416 38675 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41046 38675 603 41 0 41005 0
vsize: 164184
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40026 0 0 0 117922 98 0 0 25 0 1 0 485656577 168124416 38675 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41046 38675 603 41 0 41005 0
vsize: 164184
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40041 0 0 0 118923 98 0 0 25 0 1 0 485656577 168198144 38690 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41064 38690 603 41 0 41023 0
vsize: 164256
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 5028
Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40041 0 0 0 119923 98 0 0 25 0 1 0 485656577 168198144 38690 4294967295 134512640 134672761 3221224544 3221222228 134597471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41064 38690 603 41 0 41023 0
vsize: 164256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 5028
Raw data (stat): 5028 (minisat+) Z 5027 5897 5896 0 -1 12 40044 0 0 0 119923 105 0 0 25 0 1 0 485656577 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.13
CPU time (s): 1200.29
CPU user time (s): 1199.23
CPU system time (s): 1.05584
CPU usage (%): 100.013
Max. virtual memory (Kb): 164256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####