PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.333948
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 19021

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 17:29:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17146 boxname=wulflinc10 idbench=1319 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1d9168a9335e29df835d07b0bdf2adea  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-p0291.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-p0291.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-p0291.opb
IDLAUNCH: 17146
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        532652 kB
Buffers:         20392 kB
Cached:         460164 kB
SwapCached:          0 kB
Active:         277328 kB
Inactive:       205752 kB
HighTotal:      131008 kB
HighFree:         8008 kB
LowTotal:       903652 kB
LowFree:        524644 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13388 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:49:51 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 17146 7 1200.26 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.93 0.97 0.91 2/54 3133
Raw data (stat): 3133 (runsolver) R 3132 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488676233 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99983 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 505 0 0 0 998 1 0 0 25 0 1 0 488676233 3727360 483 4294967295 134512640 134672761 3221224544 3221221952 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+19.9993 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 505 0 0 0 1998 1 0 0 25 0 1 0 488676233 3727360 483 4294967295 134512640 134672761 3221224544 3221222096 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.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 505 0 0 0 2998 1 0 0 25 0 1 0 488676233 3727360 483 4294967295 134512640 134672761 3221224544 3221222384 134597193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 910 483 603 41 0 869 0
vsize: 3640
[startup+39.9995 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 505 0 0 0 3998 1 0 0 25 0 1 0 488676233 3727360 483 4294967295 134512640 134672761 3221224544 3221221952 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.0001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 9946 0 0 0 4974 25 0 0 25 0 1 0 488676233 42864640 9609 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10465 9609 603 41 0 10424 0
vsize: 41860
[startup+60.0001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10126 0 0 0 5973 25 0 0 25 0 1 0 488676233 43663360 9789 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10660 9789 603 41 0 10619 0
vsize: 42640
[startup+70.0002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10126 0 0 0 6972 26 0 0 25 0 1 0 488676233 43663360 9789 4294967295 134512640 134672761 3221224544 3221222384 134597191 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.0008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10126 0 0 0 7973 26 0 0 25 0 1 0 488676233 43663360 9789 4294967295 134512640 134672761 3221224544 3221222240 134597383 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.0006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10126 0 0 0 8973 26 0 0 25 0 1 0 488676233 43663360 9789 4294967295 134512640 134672761 3221224544 3221222672 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.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10126 0 0 0 9973 26 0 0 25 0 1 0 488676233 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10162 0 0 0 10972 26 0 0 25 0 1 0 488676233 43905024 9824 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10719 9824 603 41 0 10678 0
vsize: 42876
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10228 0 0 0 11972 26 0 0 25 0 1 0 488676233 44232704 9890 4294967295 134512640 134672761 3221224544 3221221664 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10228 0 0 0 12972 26 0 0 25 0 1 0 488676233 44232704 9890 4294967295 134512640 134672761 3221224544 3221221376 134597164 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10228 0 0 0 13972 26 0 0 25 0 1 0 488676233 44232704 9890 4294967295 134512640 134672761 3221224544 3221222672 134597176 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10228 0 0 0 14973 26 0 0 25 0 1 0 488676233 44232704 9890 4294967295 134512640 134672761 3221224544 3221222240 134597191 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10228 0 0 0 15973 26 0 0 25 0 1 0 488676233 44232704 9890 4294967295 134512640 134672761 3221224544 3221222672 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10252 0 0 0 16973 26 0 0 25 0 1 0 488676233 44232704 9914 4294967295 134512640 134672761 3221224544 3221221784 134597441 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10252 0 0 0 17973 26 0 0 25 0 1 0 488676233 44232704 9914 4294967295 134512640 134672761 3221224544 3221222240 134597188 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10252 0 0 0 18973 26 0 0 25 0 1 0 488676233 44232704 9914 4294967295 134512640 134672761 3221224544 3221222216 134523265 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10252 0 0 0 19973 26 0 0 25 0 1 0 488676233 44232704 9914 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9914 603 41 0 10758 0
vsize: 43196
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10265 0 0 0 20973 27 0 0 25 0 1 0 488676233 44232704 9924 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10266 0 0 0 21973 27 0 0 25 0 1 0 488676233 44232704 9925 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10266 0 0 0 22973 27 0 0 25 0 1 0 488676233 44232704 9925 4294967295 134512640 134672761 3221224544 3221222528 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10266 0 0 0 23973 27 0 0 25 0 1 0 488676233 44232704 9925 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10266 0 0 0 24973 27 0 0 25 0 1 0 488676233 44232704 9925 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10799 9925 603 41 0 10758 0
vsize: 43196
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10290 0 0 0 25973 27 0 0 25 0 1 0 488676233 44343296 9949 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 9949 603 41 0 10785 0
vsize: 43304
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10338 0 0 0 26973 27 0 0 25 0 1 0 488676233 44605440 9997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10890 9997 603 41 0 10849 0
vsize: 43560
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10378 0 0 0 27974 27 0 0 25 0 1 0 488676233 44740608 10037 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10923 10037 603 41 0 10882 0
vsize: 43692
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10473 0 0 0 28973 28 0 0 25 0 1 0 488676233 45146112 10132 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 10132 603 41 0 10981 0
vsize: 44088
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10572 0 0 0 29973 28 0 0 25 0 1 0 488676233 45551616 10231 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11121 10231 603 41 0 11080 0
vsize: 44484
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10614 0 0 0 30973 28 0 0 25 0 1 0 488676233 45686784 10273 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10614 0 0 0 31973 28 0 0 25 0 1 0 488676233 45686784 10273 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10614 0 0 0 32974 28 0 0 25 0 1 0 488676233 45686784 10273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10614 0 0 0 33974 28 0 0 25 0 1 0 488676233 45686784 10273 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10273 603 41 0 11113 0
vsize: 44616
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10642 0 0 0 34974 28 0 0 25 0 1 0 488676233 45760512 10298 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11172 10298 603 41 0 11131 0
vsize: 44688
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10714 0 0 0 35974 29 0 0 25 0 1 0 488676233 46157824 10370 4294967295 134512640 134672761 3221224544 3221221664 134597184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10714 0 0 0 36974 29 0 0 25 0 1 0 488676233 46157824 10370 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10714 0 0 0 37974 29 0 0 25 0 1 0 488676233 46157824 10370 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10714 0 0 0 38974 29 0 0 25 0 1 0 488676233 46157824 10370 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10370 603 41 0 11228 0
vsize: 45076
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10741 0 0 0 39974 29 0 0 25 0 1 0 488676233 46157824 10396 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11269 10396 603 41 0 11228 0
vsize: 45076
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10773 0 0 0 40975 29 0 0 25 0 1 0 488676233 46292992 10428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11302 10428 603 41 0 11261 0
vsize: 45208
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10877 0 0 0 41975 29 0 0 25 0 1 0 488676233 46899200 10532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11450 10532 603 41 0 11409 0
vsize: 45800
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10987 0 0 0 42975 29 0 0 25 0 1 0 488676233 47296512 10642 4294967295 134512640 134672761 3221224544 3221221232 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10987 0 0 0 43975 29 0 0 25 0 1 0 488676233 47296512 10642 4294967295 134512640 134672761 3221224544 3221221952 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10987 0 0 0 44975 29 0 0 25 0 1 0 488676233 47296512 10642 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10987 0 0 0 45975 29 0 0 25 0 1 0 488676233 47296512 10642 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 10987 0 0 0 46975 29 0 0 25 0 1 0 488676233 47296512 10642 4294967295 134512640 134672761 3221224544 3221222528 134597203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 10642 603 41 0 11506 0
vsize: 46188
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11052 0 0 0 47976 29 0 0 25 0 1 0 488676233 47431680 10703 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11580 10703 603 41 0 11539 0
vsize: 46320
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11103 0 0 0 48976 29 0 0 25 0 1 0 488676233 47693824 10754 4294967295 134512640 134672761 3221224544 3221221664 134597256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11103 0 0 0 49976 29 0 0 25 0 1 0 488676233 47693824 10754 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11103 0 0 0 50976 29 0 0 25 0 1 0 488676233 47693824 10754 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11103 0 0 0 51976 29 0 0 25 0 1 0 488676233 47693824 10754 4294967295 134512640 134672761 3221224544 3221222528 134597184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 11103 0 0 0 52976 29 0 0 25 0 1 0 488676233 47693824 10754 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10754 603 41 0 11603 0
vsize: 46576
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15520 0 0 0 53966 40 0 0 25 0 1 0 488676233 70733824 14841 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17269 14841 603 41 0 17228 0
vsize: 69076
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15589 0 0 0 54966 41 0 0 25 0 1 0 488676233 70864896 14910 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17301 14910 603 41 0 17260 0
vsize: 69204
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15679 0 0 0 55965 41 0 0 25 0 1 0 488676233 71659520 15000 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15679 0 0 0 56966 41 0 0 25 0 1 0 488676233 71659520 15000 4294967295 134512640 134672761 3221224544 3221222200 134523310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15679 0 0 0 57966 41 0 0 25 0 1 0 488676233 71659520 15000 4294967295 134512640 134672761 3221224544 3221222240 134597197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 15679 0 0 0 58966 41 0 0 25 0 1 0 488676233 71659520 15000 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17495 15000 603 41 0 17454 0
vsize: 69980
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21782 0 0 0 59951 56 0 0 25 0 1 0 488676233 91344896 21103 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22301 21103 603 41 0 22260 0
vsize: 89204
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21952 0 0 0 60951 56 0 0 25 0 1 0 488676233 91480064 21273 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21952 0 0 0 61951 56 0 0 25 0 1 0 488676233 91480064 21273 4294967295 134512640 134672761 3221224544 3221221808 134597249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21952 0 0 0 62952 56 0 0 25 0 1 0 488676233 91480064 21273 4294967295 134512640 134672761 3221224544 3221221776 134522352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21952 0 0 0 63952 56 0 0 25 0 1 0 488676233 91480064 21273 4294967295 134512640 134672761 3221224544 3221221664 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22334 21273 603 41 0 22293 0
vsize: 89336
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21980 0 0 0 64952 56 0 0 25 0 1 0 488676233 91488256 21298 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22336 21298 603 41 0 22295 0
vsize: 89344
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 21984 0 0 0 65952 56 0 0 25 0 1 0 488676233 91488256 21302 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22336 21303 603 41 0 22295 0
vsize: 89344
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22038 0 0 0 66952 56 0 0 25 0 1 0 488676233 91750400 21356 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22400 21356 603 41 0 22359 0
vsize: 89600
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22106 0 0 0 67952 57 0 0 25 0 1 0 488676233 92155904 21424 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22106 0 0 0 68952 57 0 0 25 0 1 0 488676233 92155904 21424 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22106 0 0 0 69952 57 0 0 25 0 1 0 488676233 92155904 21424 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22106 0 0 0 70953 57 0 0 25 0 1 0 488676233 92155904 21424 4294967295 134512640 134672761 3221224544 3221221724 1075350135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22499 21424 603 41 0 22458 0
vsize: 89996
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22139 0 0 0 71953 57 0 0 25 0 1 0 488676233 92139520 21457 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22495 21457 603 41 0 22454 0
vsize: 89980
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22141 0 0 0 72953 57 0 0 25 0 1 0 488676233 92139520 21459 4294967295 134512640 134672761 3221224544 3221222208 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22141 0 0 0 73953 57 0 0 25 0 1 0 488676233 92139520 21459 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22141 0 0 0 74953 57 0 0 25 0 1 0 488676233 92139520 21459 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22141 0 0 0 75953 57 0 0 25 0 1 0 488676233 92139520 21459 4294967295 134512640 134672761 3221224544 3221222672 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22495 21459 603 41 0 22454 0
vsize: 89980
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22153 0 0 0 76953 57 0 0 25 0 1 0 488676233 92168192 21468 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22153 0 0 0 77953 57 0 0 25 0 1 0 488676233 92168192 21468 4294967295 134512640 134672761 3221224544 3221222208 134522373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22153 0 0 0 78954 57 0 0 25 0 1 0 488676233 92168192 21468 4294967295 134512640 134672761 3221224544 3221222512 134597661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+800.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22153 0 0 0 79954 57 0 0 25 0 1 0 488676233 92168192 21468 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22502 21468 603 41 0 22461 0
vsize: 90008
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22162 0 0 0 80954 57 0 0 25 0 1 0 488676233 92192768 21474 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22508 21474 603 41 0 22467 0
vsize: 90032
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22173 0 0 0 81954 57 0 0 25 0 1 0 488676233 92327936 21485 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22541 21485 603 41 0 22500 0
vsize: 90164
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22204 0 0 0 82954 57 0 0 25 0 1 0 488676233 92450816 21516 4294967295 134512640 134672761 3221224544 3221223808 134562359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22571 21516 603 41 0 22530 0
vsize: 90284
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22212 0 0 0 83954 57 0 0 25 0 1 0 488676233 92450816 21524 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22212 0 0 0 84954 57 0 0 25 0 1 0 488676233 92450816 21524 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22212 0 0 0 85955 57 0 0 25 0 1 0 488676233 92450816 21524 4294967295 134512640 134672761 3221224544 3221221520 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22571 21524 603 41 0 22530 0
vsize: 90284
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22239 0 0 0 86955 57 0 0 25 0 1 0 488676233 92499968 21550 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22583 21550 603 41 0 22542 0
vsize: 90332
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22239 0 0 0 87955 57 0 0 25 0 1 0 488676233 92499968 21550 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22583 21550 603 41 0 22542 0
vsize: 90332
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22253 0 0 0 88955 57 0 0 25 0 1 0 488676233 92635136 21564 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22253 0 0 0 89955 57 0 0 25 0 1 0 488676233 92635136 21564 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22253 0 0 0 90955 57 0 0 25 0 1 0 488676233 92635136 21564 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22253 0 0 0 91956 57 0 0 25 0 1 0 488676233 92635136 21564 4294967295 134512640 134672761 3221224544 3221221808 134597181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22616 21564 603 41 0 22575 0
vsize: 90464
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22281 0 0 0 92956 57 0 0 25 0 1 0 488676233 92655616 21589 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22281 0 0 0 93956 57 0 0 25 0 1 0 488676233 92655616 21589 4294967295 134512640 134672761 3221224544 3221221664 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+950.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22281 0 0 0 94956 57 0 0 25 0 1 0 488676233 92655616 21589 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 22281 0 0 0 95956 57 0 0 25 0 1 0 488676233 92655616 21589 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 21589 603 41 0 22580 0
vsize: 90484
[startup+970.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23850 0 0 0 96953 61 0 0 25 0 1 0 488676233 117944320 23158 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28795 23158 603 41 0 28754 0
vsize: 115180
[startup+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23866 0 0 0 97953 61 0 0 25 0 1 0 488676233 117944320 23174 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28795 23174 603 41 0 28754 0
vsize: 115180
[startup+990.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23866 0 0 0 98953 61 0 0 25 0 1 0 488676233 117944320 23174 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28795 23174 603 41 0 28754 0
vsize: 115180
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23933 0 0 0 99953 61 0 0 25 0 1 0 488676233 118214656 23241 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28861 23241 603 41 0 28820 0
vsize: 115444
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23947 0 0 0 100953 61 0 0 25 0 1 0 488676233 118214656 23255 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28861 23255 603 41 0 28820 0
vsize: 115444
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23971 0 0 0 101953 62 0 0 25 0 1 0 488676233 118214656 23279 4294967295 134512640 134672761 3221224544 3221221376 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23971 0 0 0 102953 62 0 0 25 0 1 0 488676233 118214656 23279 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 23971 0 0 0 103953 62 0 0 25 0 1 0 488676233 118214656 23279 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28861 23279 603 41 0 28820 0
vsize: 115444
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 30925 0 0 0 104938 77 0 0 25 0 1 0 488676233 138240000 29574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33750 29574 603 41 0 33709 0
vsize: 135000
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 31071 0 0 0 105938 78 0 0 25 0 1 0 488676233 139563008 29720 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34073 29720 603 41 0 34032 0
vsize: 136292
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 31071 0 0 0 106938 78 0 0 25 0 1 0 488676233 139563008 29720 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34073 29720 603 41 0 34032 0
vsize: 136292
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 35907 0 0 0 107927 89 0 0 25 0 1 0 488676233 152698880 34556 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37280 34556 603 41 0 37239 0
vsize: 149120
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 35907 0 0 0 108927 89 0 0 25 0 1 0 488676233 152698880 34556 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37280 34556 603 41 0 37239 0
vsize: 149120
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 36067 0 0 0 109927 89 0 0 25 0 1 0 488676233 152698880 34716 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37280 34716 603 41 0 37239 0
vsize: 149120
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 36067 0 0 0 110927 89 0 0 25 0 1 0 488676233 152698880 34716 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37280 34716 603 41 0 37239 0
vsize: 149120
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 39767 0 0 0 111920 97 0 0 25 0 1 0 488676233 167571456 38416 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40911 38416 603 41 0 40870 0
vsize: 163644
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 39800 0 0 0 112920 97 0 0 25 0 1 0 488676233 167706624 38449 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40944 38449 603 41 0 40903 0
vsize: 163776
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 39844 0 0 0 113920 97 0 0 25 0 1 0 488676233 167841792 38493 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40977 38493 603 41 0 40936 0
vsize: 163908
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 39933 0 0 0 114919 97 0 0 25 0 1 0 488676233 167976960 38582 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41010 38582 603 41 0 40969 0
vsize: 164040
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 39997 0 0 0 115920 97 0 0 25 0 1 0 488676233 168124416 38646 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41046 38646 603 41 0 41005 0
vsize: 164184
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 40026 0 0 0 116920 98 0 0 25 0 1 0 488676233 168124416 38675 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41046 38675 603 41 0 41005 0
vsize: 164184
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 40026 0 0 0 117920 98 0 0 25 0 1 0 488676233 168124416 38675 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41046 38675 603 41 0 41005 0
vsize: 164184
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 40026 0 0 0 118920 98 0 0 25 0 1 0 488676233 168124416 38675 4294967295 134512640 134672761 3221224544 3221222240 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41046 38675 603 41 0 41005 0
vsize: 164184
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3133
Raw data (stat): 3133 (minisat+) R 3132 25347 25346 0 -1 0 40041 0 0 0 119920 98 0 0 25 0 1 0 488676233 168198144 38690 4294967295 134512640 134672761 3221224544 3221222096 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41064 38690 603 41 0 41023 0
vsize: 164256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3133
Raw data (stat): 3133 (minisat+) Z 3132 25347 25346 0 -1 12 40044 0 0 0 119920 105 0 0 25 0 1 0 488676233 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.26
CPU user time (s): 1199.2
CPU system time (s): 1.05784
CPU usage (%): 100.015
Max. virtual memory (Kb): 164256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####