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/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUM	a3dd3cd7dd293e24bffaff8bb73da54c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 18661

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 15:58:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17685 boxname=wulflinc29 idbench=1361 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17685
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        915856 kB
Buffers:         11932 kB
Cached:          80936 kB
SwapCached:       4304 kB
Active:          16460 kB
Inactive:        82172 kB
HighTotal:      131008 kB
HighFree:        52584 kB
LowTotal:       903652 kB
LowFree:        863272 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14440 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:18:37 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 17685 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       100 |   25752    84253 |    9453      98     6192    63.2 |  2.792 % |
c ==============================================================================
c [1mFound solution: 1583488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       220 |   25767    84288 |    8589     218    12443    57.1 |  2.792 % |
c ==============================================================================
c [1mFound solution: 1580928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |   25776    84312 |    8592     266    20437    76.8 |  2.792 % |
c |       368 |   25776    84312 |    9451     366    22162    60.6 |  2.817 % |
c |       518 |   25776    84312 |   10396     516    29655    57.5 |  2.817 % |
c |       744 |   25776    84312 |   11435     742    42680    57.5 |  2.817 % |
c ==============================================================================
c [1mFound solution: 1508608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       870 |   25789    84343 |    8596     868    48024    55.3 |  2.817 % |
c |       970 |   25789    84343 |    9455     968    60363    62.4 |  2.829 % |
c |      1120 |   25778    84319 |   10401    1117    68505    61.3 |  2.872 % |
c |      1347 |   25778    84319 |   11441    1344    77932    58.0 |  2.872 % |
c |      1684 |   25778    84319 |   12585    1681   103593    61.6 |  2.872 % |
c |      2190 |   25778    84319 |   13843    2187   126927    58.0 |  2.872 % |
c |      2950 |   25767    84295 |   15228    2946   212260    72.1 |  2.916 % |
c |      4090 |   25767    84295 |   16751    4086   295763    72.4 |  2.916 % |
c |      5798 |   25731    84167 |   18426    5787   492222    85.1 |  2.945 % |
c ==============================================================================
c [1mFound solution: 1477248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7454 |   25683    83993 |    8561    7434   643106    86.5 |  2.945 % |
c |      7556 |   25683    83993 |    9417    7536   659060    87.5 |  3.056 % |
c |      7706 |   25683    83993 |   10358    7686   665481    86.6 |  3.056 % |
c |      7931 |   25683    83993 |   11394    7911   690952    87.3 |  3.056 % |
c |      8270 |   25672    83969 |   12534    8249   707791    85.8 |  3.099 % |
c |      8776 |   25672    83969 |   13787    8755   792296    90.5 |  3.099 % |
c |      9537 |   25618    83822 |   15166    9509   863713    90.8 |  3.243 % |
c |     10678 |   25536    83532 |   16682   10641   946280    88.9 |  3.358 % |
c |     12386 |   25503    83415 |   18351   12346  1087746    88.1 |  3.387 % |
c |     14949 |   25449    83245 |   20186   14900  1399535    93.9 |  3.488 % |
c |     18793 |   25395    83098 |   22205   18736  1754727    93.7 |  3.632 % |
c ==============================================================================
c [1mFound solution: 1475328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20218 |   25398    83107 |    8466   20160  1881199    93.3 |  3.632 % |
c |     20322 |   25398    83107 |    9312    5144   289617    56.3 |  3.686 % |
c |     20472 |   25398    83107 |   10243    5294   299464    56.6 |  3.686 % |
c |     20697 |   25398    83107 |   11268    5519   320431    58.1 |  3.686 % |
c |     21034 |   25387    83083 |   12395    5854   334549    57.1 |  3.729 % |
c |     21540 |   25387    83083 |   13634    6360   407264    64.0 |  3.729 % |
c |     22300 |   25354    82966 |   14998    7118   497542    69.9 |  3.758 % |
c |     23439 |   25343    82942 |   16497    8256   599062    72.6 |  3.801 % |
c |     25148 |   25316    82847 |   18147    9957   832837    83.6 |  3.830 % |
c |     27712 |   25316    82847 |   19962   12521  1060640    84.7 |  3.830 % |
c |     31557 |   25316    82847 |   21958   16366  1691483   103.4 |  3.830 % |
c ==============================================================================
c [1mFound solution: 1460608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34542 |   25294    82772 |    8431   19345  1961844   101.4 |  3.830 % |
c |     34643 |   25294    82772 |    9274    4938   275109    55.7 |  3.899 % |
c |     34793 |   25294    82772 |   10201    5088   277980    54.6 |  3.899 % |
c |     35019 |   25294    82772 |   11221    5314   292878    55.1 |  3.899 % |
c |     35357 |   25294    82772 |   12343    5652   319785    56.6 |  3.899 % |
c |     35863 |   25294    82772 |   13578    6158   364356    59.2 |  3.899 % |
c |     36623 |   25294    82772 |   14936    6918   441267    63.8 |  3.899 % |
c |     37763 |   25294    82772 |   16429    8058   574366    71.3 |  3.899 % |
c ==============================================================================
c [1mFound solution: 1458688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38579 |   25307    82802 |    8435    8874   681730    76.8 |  3.899 % |
c |     38679 |   25307    82802 |    9278    4537   324758    71.6 |  3.910 % |
c |     38830 |   25296    82778 |   10206    4686   329928    70.4 |  3.953 % |
c |     39055 |   25280    82743 |   11226    4907   340655    69.4 |  4.025 % |
c |     39392 |   25204    82492 |   12349    5238   355692    67.9 |  4.168 % |
c ==============================================================================
c [1mFound solution: 1438848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39556 |   25216    82524 |    8405    5402   383073    70.9 |  4.168 % |
c |     39656 |   25173    82401 |    9245    5496   384861    70.0 |  4.279 % |
c |     39806 |   25173    82401 |   10170    5646   400312    70.9 |  4.279 % |
c |     40032 |   25151    82353 |   11187    5868   408033    69.5 |  4.365 % |
c |     40369 |   25106    82252 |   12305    6197   430376    69.4 |  4.566 % |
c |     40875 |   25106    82252 |   13536    6703   493435    73.6 |  4.566 % |
c |     41634 |   25106    82252 |   14889    7462   569328    76.3 |  4.566 % |
c |     42773 |   25106    82252 |   16378    8601   707090    82.2 |  4.566 % |
c |     44481 |   25032    82007 |   18016   10298   853239    82.9 |  4.709 % |
c |     47043 |   25021    81983 |   19818   12858  1115212    86.7 |  4.752 % |
c |     50892 |   24980    81840 |   21800   16699  1507898    90.3 |  4.824 % |
c ==============================================================================
c [1mFound solution: 1431808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53691 |   24988    81862 |    8329   19495  1771927    90.9 |  4.824 % |
c |     53791 |   24988    81862 |    9161    4974   265913    53.5 |  4.847 % |
c |     53941 |   24988    81862 |   10078    5124   269820    52.7 |  4.847 % |
c |     54167 |   24988    81862 |   11085    5350   286961    53.6 |  4.847 % |
c |     54504 |   24958    81794 |   12194    5679   304170    53.6 |  4.962 % |
c |     55010 |   24958    81794 |   13413    6185   351539    56.8 |  4.962 % |
c |     55769 |   24958    81794 |   14755    6944   416677    60.0 |  4.962 % |
c |     56909 |   24958    81794 |   16230    8084   562839    69.6 |  4.962 % |
c |     58619 |   24947    81770 |   17853    9793   735565    75.1 |  5.005 % |
c |     61182 |   24920    81700 |   19639   12351   959102    77.7 |  5.091 % |
c |     65026 |   24907    81671 |   21603   16193  1315910    81.3 |  5.148 % |
c |     70795 |   24907    81671 |   23763   21962  1922551    87.5 |  5.148 % |
c |     79447 |   24865    81540 |   26139   18016  1482239    82.3 |  5.234 % |
c |     92423 |   24801    81385 |   28753   16615  1259492    75.8 |  5.464 % |
c ==============================================================================
c [1mFound solution: 1427968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107128 |   24723    81184 |    8241   16283  1157306    71.1 |  5.464 % |
c |    107230 |   24723    81184 |    9065    8244   476372    57.8 |  5.758 % |
c |    107382 |   24723    81184 |    9971    8396   489220    58.3 |  5.759 % |
c |    107608 |   24723    81184 |   10968    8622   522291    60.6 |  5.759 % |
c |    107945 |   24723    81184 |   12065    8959   555312    62.0 |  5.758 % |
c |    108452 |   24723    81184 |   13272    9466   618197    65.3 |  5.759 % |
c |    109212 |   24678    81023 |   14599   10221   672039    65.8 |  5.787 % |
c |    110351 |   24678    81023 |   16059   11360   765864    67.4 |  5.787 % |
c |    112060 |   24678    81023 |   17665   13069  1024443    78.4 |  5.787 % |
c |    114622 |   24620    80894 |   19431   15623  1365937    87.4 |  6.031 % |
c |    118467 |   24590    80816 |   21375   19460  1763317    90.6 |  6.131 % |
c |    124235 |   24590    80816 |   23512   14161  1019179    72.0 |  6.131 % |
c |    132891 |   24551    80683 |   25863   22813  1779717    78.0 |  6.203 % |
c |    145865 |   24551    80683 |   28450   22536  2054772    91.2 |  6.203 % |
c ==============================================================================
c [1mFound solution: 1423488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146568 |   24563    80714 |    8187   23239  2124527    91.4 |  6.203 % |
c |    146668 |   24563    80714 |    9005    5910   256320    43.4 |  6.210 % |
c |    146819 |   24563    80714 |    9906    6061   262458    43.3 |  6.210 % |
c |    147044 |   24463    80383 |   10896    6275   285602    45.5 |  6.410 % |
c |    147381 |   24423    80256 |   11986    6604   292865    44.3 |  6.496 % |
c |    147887 |   24423    80256 |   13185    7110   338836    47.7 |  6.496 % |
c |    148646 |   24423    80256 |   14503    7869   435930    55.4 |  6.496 % |
c |    149788 |   24423    80256 |   15954    9011   542343    60.2 |  6.496 % |
c |    151497 |   24406    80218 |   17549   10719   752216    70.2 |  6.567 % |
c |    154060 |   24386    80171 |   19304   13280   990365    74.6 |  6.639 % |
c |    157906 |   24386    80171 |   21234   17126  1287121    75.2 |  6.639 % |
c |    163672 |   24340    80044 |   23358   11559   700256    60.6 |  6.796 % |
c |    172321 |   24340    80044 |   25694   20208  1333788    66.0 |  6.796 % |
c |    185296 |   24314    79967 |   28263   19623  1161767    59.2 |  6.854 % |
c |    204758 |   24314    79967 |   31090   23903  1595766    66.8 |  6.854 % |
c |    233951 |   24224    79722 |   34199   21100  1491804    70.7 |  7.154 % |
c ==============================================================================
c [1mFound solution: 1420288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    269048 |   24088    79244 |    8029   16815  1491486    88.7 |  7.154 % |
c |    269148 |   24088    79244 |    8831    8508   640879    75.3 |  7.459 % |
c |    269298 |   24088    79244 |    9715    8658   661275    76.4 |  7.459 % |
c |    269523 |   24088    79244 |   10686    8883   678039    76.3 |  7.459 % |
c |    269860 |   24088    79244 |   11755    9220   719171    78.0 |  7.460 % |
c |    270367 |   24088    79244 |   12930    9727   729922    75.0 |  7.459 % |
c |    271127 |   24088    79244 |   14223   10487   840546    80.2 |  7.459 % |
c |    272266 |   24073    79211 |   15646   11624   968142    83.3 |  7.516 % |
c |    273975 |   24073    79211 |   17210   13333  1152071    86.4 |  7.516 % |
c |    276537 |   24045    79149 |   18931   15889  1433911    90.2 |  7.631 % |
c |    280383 |   23865    78603 |   20825   19704  1796107    91.2 |  8.117 % |
c |    286151 |   23865    78603 |   22907   14391  1054594    73.3 |  8.117 % |
c |    294801 |   23865    78603 |   25198   23041  1954414    84.8 |  8.117 % |
c |    307776 |   23854    78579 |   27718   22285  2001861    89.8 |  8.159 % |
c |    327237 |   23847    78564 |   30490   27154  2268727    83.6 |  8.188 % |
c |    356429 |   23803    78464 |   33539   24241  1688878    69.7 |  8.402 % |
c ==============================================================================
c [1mFound solution: 1416448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    384550 |   23765    78382 |    7921   32917  2863259    87.0 |  8.402 % |
c |    384650 |   23754    78358 |    8713    7690   702581    91.4 |  8.665 % |
c |    384801 |   23754    78358 |    9584    7841   714078    91.1 |  8.665 % |
c |    385027 |   23754    78358 |   10542    8067   743664    92.2 |  8.665 % |
c |    385364 |   23754    78358 |   11597    8404   790915    94.1 |  8.665 % |
c |    385870 |   23678    78088 |   12756    8901   805477    90.5 |  8.822 % |
c |    386631 |   23678    78088 |   14032    9662   860772    89.1 |  8.822 % |
c |    387773 |   23678    78088 |   15435   10804  1046707    96.9 |  8.822 % |
c |    389481 |   23678    78088 |   16979   12512  1164690    93.1 |  8.822 % |
c |    392043 |   23678    78088 |   18677   15074  1561117   103.6 |  8.822 % |
c |    395887 |   23678    78088 |   20545   18918  1996674   105.5 |  8.822 % |
c |    401654 |   23678    78088 |   22599   13746  1222434    88.9 |  8.822 % |
c |    410306 |   23665    78059 |   24859   22395  2137343    95.4 |  8.879 % |
c |    423280 |   23647    77997 |   27345   21922  2153316    98.2 |  8.908 % |
#### 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.92 2/54 1156
Raw data (stat): 1156 (runsolver) R 1155 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546339079 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 1926 0 0 0 994 5 0 0 25 0 1 0 546339079 9252864 1856 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2259 1856 603 41 0 2218 0
vsize: 9036
[startup+20.0016 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 2440 0 0 0 1992 6 0 0 25 0 1 0 546339079 11407360 2370 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2785 2370 603 41 0 2744 0
vsize: 11140
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 2969 0 0 0 2990 9 0 0 25 0 1 0 546339079 13561856 2899 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3311 2899 603 41 0 3270 0
vsize: 13244
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 3988 10 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3699 3273 603 41 0 3658 0
vsize: 14796
[startup+50.002 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 4988 11 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3699 3273 603 41 0 3658 0
vsize: 14796
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3343 0 0 0 5988 11 0 0 25 0 1 0 546339079 15151104 3273 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3699 3273 603 41 0 3658 0
vsize: 14796
[startup+70.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 6987 12 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1156
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 7987 12 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 1168
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 8984 14 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 9982 16 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 10981 17 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223728 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 11981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 12981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3482 0 0 0 13981 18 0 0 25 0 1 0 546339079 15683584 3412 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3412 603 41 0 3788 0
vsize: 15316
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3694 0 0 0 14980 19 0 0 25 0 1 0 546339079 16613376 3624 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3624 603 41 0 4015 0
vsize: 16224
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1209
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3902 0 0 0 15979 20 0 0 25 0 1 0 546339079 17412096 3832 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4251 3832 603 41 0 4210 0
vsize: 17004
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3902 0 0 0 16979 21 0 0 25 0 1 0 546339079 17412096 3832 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4251 3832 603 41 0 4210 0
vsize: 17004
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3910 0 0 0 17978 22 0 0 25 0 1 0 546339079 17412096 3840 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4251 3840 603 41 0 4210 0
vsize: 17004
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 3924 0 0 0 18978 22 0 0 25 0 1 0 546339079 17555456 3854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4286 3854 603 41 0 4245 0
vsize: 17144
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4277 0 0 0 19976 24 0 0 25 0 1 0 546339079 18894848 4207 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4613 4207 603 41 0 4572 0
vsize: 18452
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4389 0 0 0 20976 24 0 0 25 0 1 0 546339079 19423232 4319 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4319 603 41 0 4701 0
vsize: 18968
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4389 0 0 0 21976 25 0 0 25 0 1 0 546339079 19423232 4319 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4319 603 41 0 4701 0
vsize: 18968
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4408 0 0 0 22975 25 0 0 25 0 1 0 546339079 19423232 4338 4294967295 134512640 134672761 3221224624 3221223760 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4338 603 41 0 4701 0
vsize: 18968
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4449 0 0 0 23975 26 0 0 25 0 1 0 546339079 19718144 4379 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 4379 603 41 0 4773 0
vsize: 19256
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4513 0 0 0 24975 26 0 0 25 0 1 0 546339079 20029440 4443 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4443 603 41 0 4849 0
vsize: 19560
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 25975 26 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 26974 27 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223760 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 27974 27 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 28974 28 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 29973 28 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4524 0 0 0 30973 29 0 0 25 0 1 0 546339079 20029440 4454 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4454 603 41 0 4849 0
vsize: 19560
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 31973 29 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 32973 30 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 33972 30 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 34972 31 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 35971 31 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 36971 32 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 37971 32 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 38970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 39970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4526 0 0 0 40970 33 0 0 25 0 1 0 546339079 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4527 0 0 0 41970 34 0 0 25 0 1 0 546339079 20029440 4457 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4457 603 41 0 4849 0
vsize: 19560
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1211
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4528 0 0 0 42969 34 0 0 25 0 1 0 546339079 20029440 4458 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4458 603 41 0 4849 0
vsize: 19560
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4566 0 0 0 43968 35 0 0 25 0 1 0 546339079 20193280 4496 4294967295 134512640 134672761 3221224624 3221223808 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4930 4496 603 41 0 4889 0
vsize: 19720
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4610 0 0 0 44968 36 0 0 25 0 1 0 546339079 20357120 4540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4970 4540 603 41 0 4929 0
vsize: 19880
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4641 0 0 0 45968 36 0 0 25 0 1 0 546339079 20553728 4571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5018 4571 603 41 0 4977 0
vsize: 20072
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4685 0 0 0 46967 37 0 0 25 0 1 0 546339079 20881408 4615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5098 4615 603 41 0 5057 0
vsize: 20392
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4685 0 0 0 47967 37 0 0 25 0 1 0 546339079 20881408 4615 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5098 4615 603 41 0 5057 0
vsize: 20392
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4711 0 0 0 48967 37 0 0 25 0 1 0 546339079 21045248 4641 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5138 4641 603 41 0 5097 0
vsize: 20552
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4713 0 0 0 49967 38 0 0 25 0 1 0 546339079 21045248 4643 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5138 4643 603 41 0 5097 0
vsize: 20552
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4742 0 0 0 50967 38 0 0 25 0 1 0 546339079 21209088 4672 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5178 4672 603 41 0 5137 0
vsize: 20712
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4784 0 0 0 51967 38 0 0 25 0 1 0 546339079 21405696 4714 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5226 4714 603 41 0 5185 0
vsize: 20904
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4834 0 0 0 52966 39 0 0 25 0 1 0 546339079 21798912 4764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4764 603 41 0 5281 0
vsize: 21288
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 53966 39 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4765 603 41 0 5281 0
vsize: 21288
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 54965 40 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4765 603 41 0 5281 0
vsize: 21288
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4835 0 0 0 55965 41 0 0 25 0 1 0 546339079 21798912 4765 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4765 603 41 0 5281 0
vsize: 21288
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4837 0 0 0 56965 41 0 0 25 0 1 0 546339079 21798912 4767 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4767 603 41 0 5281 0
vsize: 21288
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4838 0 0 0 57964 42 0 0 25 0 1 0 546339079 21798912 4768 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4768 603 41 0 5281 0
vsize: 21288
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 4838 0 0 0 58964 42 0 0 25 0 1 0 546339079 21798912 4768 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4768 603 41 0 5281 0
vsize: 21288
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5037 0 0 0 59963 43 0 0 25 0 1 0 546339079 22601728 4967 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5518 4967 603 41 0 5477 0
vsize: 22072
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5249 0 0 0 60962 44 0 0 25 0 1 0 546339079 23408640 5179 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5715 5179 603 41 0 5674 0
vsize: 22860
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 61962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5715 5187 603 41 0 5674 0
vsize: 22860
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 62962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5715 5187 603 41 0 5674 0
vsize: 22860
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5257 0 0 0 63962 45 0 0 25 0 1 0 546339079 23408640 5187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5715 5187 603 41 0 5674 0
vsize: 22860
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5453 0 0 0 64961 46 0 0 25 0 1 0 546339079 24203264 5383 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5909 5383 603 41 0 5868 0
vsize: 23636
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5898 0 0 0 65960 48 0 0 25 0 1 0 546339079 26206208 5828 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6398 5828 603 41 0 6357 0
vsize: 25592
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 66960 48 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6430 5858 603 41 0 6389 0
vsize: 25720
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 67960 48 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6430 5858 603 41 0 6389 0
vsize: 25720
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 68960 49 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6430 5858 603 41 0 6389 0
vsize: 25720
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 5928 0 0 0 69959 49 0 0 25 0 1 0 546339079 26337280 5858 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6430 5858 603 41 0 6389 0
vsize: 25720
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6299 0 0 0 70958 51 0 0 25 0 1 0 546339079 27815936 6229 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6791 6229 603 41 0 6750 0
vsize: 27164
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 71957 51 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 72957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 73957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 74957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 75957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 76957 52 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 77957 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 78957 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 79958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 80958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 81958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223760 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 82958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 83958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6406 0 0 0 84958 53 0 0 25 0 1 0 546339079 28213248 6336 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6336 603 41 0 6847 0
vsize: 27552
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 85959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 86959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 87959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 88959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 89959 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 90960 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223808 134558638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6407 0 0 0 91960 53 0 0 25 0 1 0 546339079 28213248 6337 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6337 603 41 0 6847 0
vsize: 27552
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 92960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 93960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 94960 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 95961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 96961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 97961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6408 0 0 0 98961 53 0 0 25 0 1 0 546339079 28213248 6338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6338 603 41 0 6847 0
vsize: 27552
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 99961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 100961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 101960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 102960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 103960 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 104961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 105961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 106961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 107961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 108961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 109961 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 110962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 111962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223824 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 112962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 113962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 114962 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 115963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 116963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 117963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 118963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
[startup+1200.03 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 1213
Raw data (stat): 1156 (minisat+) R 1155 27222 27221 0 -1 0 6410 0 0 0 119963 53 0 0 25 0 1 0 546339079 28213248 6340 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6888 6340 603 41 0 6847 0
vsize: 27552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.07 0.99 0.93 1/54 1213
Raw data (stat): 1156 (minisat+) Z 1155 27222 27221 0 -1 12 6413 0 0 0 119963 54 0 0 25 0 1 0 546339079 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.64
CPU system time (s): 0.546916
CPU usage (%): 100.012
Max. virtual memory (Kb): 27552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####