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/submitted/manquinho/logic-synthesis/normalized-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 6171

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 03:38:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4578 boxname=wulflinc4 idbench=66 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc4/normalized-e64.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc4/normalized-e64.b.opb /oldhome/oroussel/tmp/wulflinc4/normalized-e64.b.opb
IDLAUNCH: 4578
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891824 kB
Buffers:         36336 kB
Cached:          86676 kB
SwapCached:          0 kB
Active:          55360 kB
Inactive:        70472 kB
HighTotal:      131008 kB
HighFree:        40600 kB
LowTotal:       903652 kB
LowFree:        851224 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11404 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:58:48 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4578 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27428     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   64458   156677 |   21486       1       16    16.0 |  0.000 % |
c |       101 |   64433   156620 |   23634     100      539     5.4 |  0.084 % |
c |       251 |   64433   156620 |   25998     250     1620     6.5 |  0.084 % |
c |       476 |   64411   156571 |   28597     474     2819     5.9 |  0.111 % |
c |       813 |   64138   155954 |   31457     800     4934     6.2 |  0.464 % |
c |      1321 |   64138   155954 |   34603    1308    11530     8.8 |  0.464 % |
c |      2080 |   64049   155753 |   38063    2064    23054    11.2 |  0.580 % |
c |      3220 |   64009   155662 |   41870    3202    36476    11.4 |  0.636 % |
c |      4930 |   63937   155496 |   46057    4879    66820    13.7 |  0.747 % |
c |      7494 |   63717   155000 |   50662    7424   102104    13.8 |  1.026 % |
c |     11338 |   63597   154727 |   55729   11246   144954    12.9 |  1.188 % |
c |     17104 |   63597   154727 |   61302   17012   367418    21.6 |  1.188 % |
c |     25753 |   63367   154208 |   67432   24618   454533    18.5 |  1.471 % |
c ==============================================================================
c [1mFound solution: 81[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27014 |   63415   154329 |   21138   25879   476935    18.4 |  1.471 % |
c |     27116 |   63415   154329 |   23251   13042   114182     8.8 |  1.475 % |
c |     27266 |   63404   154305 |   25576   13191   116951     8.9 |  1.489 % |
c |     27493 |   63371   154231 |   28134   13415   120589     9.0 |  1.531 % |
c |     27833 |   63371   154231 |   30948   13755   126253     9.2 |  1.531 % |
c |     28340 |   63371   154231 |   34042   14262   145563    10.2 |  1.531 % |
c |     29099 |   63371   154231 |   37447   15021   154648    10.3 |  1.531 % |
c |     30238 |   63371   154231 |   41191   16160   199896    12.4 |  1.531 % |
c |     31947 |   63371   154231 |   45311   17869   237592    13.3 |  1.531 % |
c |     34509 |   63371   154231 |   49842   20431   284987    13.9 |  1.531 % |
c |     38353 |   63371   154231 |   54826   24275   357986    14.7 |  1.531 % |
c |     44121 |   63371   154231 |   60309   30043   529309    17.6 |  1.531 % |
c |     52770 |   63371   154231 |   66340   38692   944624    24.4 |  1.531 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56875 |   62146   151435 |   20715   41489  1005481    24.2 |  1.531 % |
c |     56980 |   62146   151435 |   22786   20236   584579    28.9 |  3.182 % |
c |     57131 |   62146   151435 |   25065   20387   585994    28.7 |  3.182 % |
c |     57356 |   62146   151435 |   27571   20612   588141    28.5 |  3.182 % |
c |     57693 |   62146   151435 |   30328   20949   593037    28.3 |  3.182 % |
c |     58199 |   62146   151435 |   33361   21455   598844    27.9 |  3.182 % |
c |     58958 |   62146   151435 |   36697   22214   633634    28.5 |  3.182 % |
c |     60099 |   62146   151435 |   40367   23355   660071    28.3 |  3.182 % |
c ==============================================================================
c [1mFound solution: 79[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60453 |   62188   151542 |   20729   23709   665651    28.1 |  3.182 % |
c |     60556 |   62188   151542 |   22801   11958   140622    11.8 |  3.185 % |
c |     60707 |   62188   151542 |   25082   12109   143040    11.8 |  3.185 % |
c |     60933 |   62188   151542 |   27590   12335   145361    11.8 |  3.185 % |
c |     61270 |   62188   151542 |   30349   12672   151172    11.9 |  3.185 % |
c |     61777 |   62188   151542 |   33384   13179   157611    12.0 |  3.185 % |
c |     62536 |   62188   151542 |   36722   13938   171603    12.3 |  3.185 % |
c |     63675 |   62188   151542 |   40394   15077   213454    14.2 |  3.185 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64125 |   62149   151445 |   20716   15312   204499    13.4 |  3.185 % |
c |     64225 |   62149   151445 |   22787   15412   206309    13.4 |  3.244 % |
c |     64375 |   62149   151445 |   25066   15562   208328    13.4 |  3.244 % |
c |     64600 |   62149   151445 |   27572   15787   210273    13.3 |  3.245 % |
c |     64937 |   62149   151445 |   30330   16124   215655    13.4 |  3.245 % |
c |     65445 |   62149   151445 |   33363   16632   223793    13.5 |  3.244 % |
c |     66204 |   62149   151445 |   36699   17391   241234    13.9 |  3.244 % |
c |     67343 |   62149   151445 |   40369   18530   274445    14.8 |  3.244 % |
c |     69052 |   62149   151445 |   44406   20239   308735    15.3 |  3.244 % |
c |     71620 |   62013   151138 |   48847   22788   357525    15.7 |  3.416 % |
c |     75464 |   61958   151015 |   53731   26631   478230    18.0 |  3.481 % |
c |     81230 |   61884   150848 |   59105   32395   673349    20.8 |  3.578 % |
c |     89880 |   61884   150848 |   65015   41045   993961    24.2 |  3.578 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89988 |   61729   150502 |   20576   40768   976132    23.9 |  3.578 % |
c |     90088 |   61729   150502 |   22633   20484   410929    20.1 |  3.987 % |
c |     90239 |   61729   150502 |   24896   20635   412541    20.0 |  3.987 % |
c |     90464 |   61729   150502 |   27386   20860   415025    19.9 |  3.987 % |
c |     90803 |   61729   150502 |   30125   21199   419184    19.8 |  3.987 % |
c |     91309 |   61729   150502 |   33137   21705   425155    19.6 |  3.987 % |
c |     92068 |   61729   150502 |   36451   22464   446188    19.9 |  3.987 % |
c |     93207 |   61729   150502 |   40096   23603   479376    20.3 |  3.987 % |
c |     94916 |   61729   150502 |   44106   25312   531799    21.0 |  3.987 % |
c |     97478 |   61729   150502 |   48517   27874   711712    25.5 |  3.987 % |
c |    101323 |   61666   150359 |   53368   31718   838806    26.4 |  4.070 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103861 |   58610   143351 |   19536   33544   871732    26.0 |  4.070 % |
c |    103962 |   58610   143351 |   21489   16873   279370    16.6 |  8.454 % |
c |    104115 |   58610   143351 |   23638   17026   283114    16.6 |  8.455 % |
c |    104340 |   58610   143351 |   26002   17251   287140    16.6 |  8.454 % |
c |    104678 |   58557   143231 |   28602   17582   290475    16.5 |  8.524 % |
c |    105184 |   58557   143231 |   31462   18088   308566    17.1 |  8.524 % |
c |    105943 |   58557   143231 |   34609   18847   336221    17.8 |  8.524 % |
c |    107085 |   58557   143231 |   38070   19989   367601    18.4 |  8.524 % |
c |    108793 |   58557   143231 |   41877   21697   407431    18.8 |  8.524 % |
c |    111357 |   58557   143231 |   46064   24261   494337    20.4 |  8.524 % |
c |    115204 |   58557   143231 |   50671   28108   654580    23.3 |  8.524 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115934 |   58593   143323 |   19531   28838   683518    23.7 |  8.524 % |
c |    116034 |   58593   143323 |   21484   14519   223017    15.4 |  8.528 % |
c |    116184 |   58593   143323 |   23632   14669   224246    15.3 |  8.528 % |
c |    116413 |   58593   143323 |   25995   14898   232407    15.6 |  8.528 % |
c |    116750 |   58593   143323 |   28595   15235   236236    15.5 |  8.528 % |
c |    117257 |   58593   143323 |   31454   15742   248317    15.8 |  8.528 % |
c |    118017 |   58593   143323 |   34600   16502   269121    16.3 |  8.528 % |
c |    119156 |   58593   143323 |   38060   17641   302392    17.1 |  8.528 % |
c |    120865 |   58593   143323 |   41866   19350   407748    21.1 |  8.528 % |
c |    123428 |   58593   143323 |   46053   21913   493097    22.5 |  8.528 % |
c |    127272 |   58593   143323 |   50658   25757   602285    23.4 |  8.528 % |
c |    133038 |   58562   143251 |   55724   31522   802642    25.5 |  8.570 % |
c |    141687 |   58562   143251 |   61296   40171  1146713    28.5 |  8.570 % |
c |    154661 |   58562   143251 |   67426   53145  1961664    36.9 |  8.570 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165819 |   58520   143140 |   19506   64301  2433993    37.9 |  8.570 % |
c |    165919 |   58520   143140 |   21456   12098   103737     8.6 |  8.638 % |
c |    166072 |   58520   143140 |   23602   12251   106423     8.7 |  8.638 % |
c |    166297 |   58520   143140 |   25962   12476   119922     9.6 |  8.638 % |
c |    166634 |   58520   143140 |   28558   12813   129992    10.1 |  8.638 % |
c |    167140 |   58473   143032 |   31414   13315   138014    10.4 |  8.707 % |
c |    167899 |   58448   142976 |   34556   14073   167604    11.9 |  8.740 % |
c |    169038 |   58448   142976 |   38011   15212   218676    14.4 |  8.740 % |
c |    170746 |   58448   142976 |   41812   16920   259209    15.3 |  8.740 % |
c |    173309 |   58358   142771 |   45994   19474   310650    16.0 |  8.855 % |
c |    177155 |   58306   142652 |   50593   23316   410787    17.6 |  8.920 % |
c |    182921 |   58306   142652 |   55652   29082   784450    27.0 |  8.920 % |
c |    191570 |   58306   142652 |   61218   37731  1183612    31.4 |  8.920 % |
c |    204545 |   58306   142652 |   67340   50706  1901687    37.5 |  8.920 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206542 |   58345   142751 |   19448   52703  2081755    39.5 |  8.920 % |
c |    206642 |   58314   142680 |   21392   12053   185230    15.4 |  8.969 % |
c |    206792 |   58314   142680 |   23532   12203   188021    15.4 |  8.969 % |
c |    207017 |   58314   142680 |   25885   12428   192287    15.5 |  8.970 % |
c |    207356 |   58314   142680 |   28473   12767   199084    15.6 |  8.969 % |
c |    207862 |   58314   142680 |   31321   13273   209921    15.8 |  8.969 % |
c |    208623 |   58314   142680 |   34453   14034   220299    15.7 |  8.969 % |
c |    209762 |   58277   142597 |   37898   15168   243737    16.1 |  9.015 % |
c |    211471 |   57841   141602 |   41688   16713   284440    17.0 |  9.629 % |
c |    214034 |   57841   141602 |   45857   19276   346288    18.0 |  9.629 % |
c |    217878 |   57841   141602 |   50443   23120   562548    24.3 |  9.629 % |
c |    223644 |   57833   141584 |   55487   28884   917445    31.8 |  9.638 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    224011 |   57503   140806 |   19167   29048   910831    31.4 |  9.638 % |
c |    224111 |   57503   140806 |   21083   14624   219694    15.0 | 10.126 % |
c |    224261 |   57503   140806 |   23192   14774   221871    15.0 | 10.127 % |
c |    224488 |   57503   140806 |   25511   15001   224710    15.0 | 10.126 % |
c |    224825 |   57503   140806 |   28062   15338   229085    14.9 | 10.127 % |
c |    225331 |   57503   140806 |   30868   15844   238971    15.1 | 10.126 % |
c |    226090 |   57469   140728 |   33955   16601   255805    15.4 | 10.168 % |
c |    227230 |   57469   140728 |   37351   17741   280173    15.8 | 10.168 % |
c |    228938 |   57469   140728 |   41086   19449   332081    17.1 | 10.168 % |
c |    231500 |   57469   140728 |   45194   22011   393912    17.9 | 10.168 % |
c |    235344 |   57469   140728 |   49714   25855   568140    22.0 | 10.168 % |
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239249 |   57504   140817 |   19168   29760   820114    27.6 | 10.168 % |
c |    239350 |   57504   140817 |   21084   14981   263217    17.6 | 10.172 % |
c |    239500 |   57348   140465 |   23193   15118   264888    17.5 | 10.384 % |
c |    239726 |   57309   140377 |   25512   15323   267596    17.5 | 10.434 % |
c |    240064 |   57309   140377 |   28063   15661   274570    17.5 | 10.434 % |
c |    240570 |   57196   140122 |   30870   16146   283327    17.5 | 10.582 % |
c |    241330 |   57175   140072 |   33957   16904   313052    18.5 | 10.619 % |
c |    242469 |   56998   139670 |   37353   18026   353589    19.6 | 10.854 % |
c |    244177 |   56998   139670 |   41088   19734   403835    20.5 | 10.854 % |
c |    246739 |   56998   139670 |   45197   22296   641361    28.8 | 10.854 % |
c |    250583 |   56998   139670 |   49716   26140   843408    32.3 | 10.854 % |
c |    256351 |   56998   139670 |   54688   31908  1150908    36.1 | 10.854 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    258781 |   56948   139539 |   18982   34334  1326198    38.6 | 10.854 % |
c |    258881 |   56948   139539 |   20880   17267   392269    22.7 | 10.931 % |
c |    259031 |   56948   139539 |   22968   17417   394379    22.6 | 10.931 % |
c |    259256 |   56948   139539 |   25265   17642   400223    22.7 | 10.932 % |
c |    259594 |   56948   139539 |   27791   17980   404136    22.5 | 10.932 % |
c |    260100 |   56948   139539 |   30570   18486   414025    22.4 | 10.932 % |
c |    260859 |   56926   139489 |   33627   19244   432618    22.5 | 10.959 % |
c |    262000 |   56891   139409 |   36990   20384   467616    22.9 | 11.010 % |
c |    263708 |   56891   139409 |   40689   22092   542280    24.5 | 11.010 % |
c |    266273 |   56870   139361 |   44758   24655   661892    26.8 | 11.037 % |
c |    270121 |   56854   139325 |   49234   28502   891445    31.3 | 11.056 % |
c |    275887 |   56854   139325 |   54157   34268  1203130    35.1 | 11.056 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    282244 |   56502   138527 |   18834   40586  1359900    33.5 | 11.056 % |
c |    282345 |   56502   138527 |   20717   20394   233168    11.4 | 11.592 % |
c |    282495 |   56502   138527 |   22789   20544   234709    11.4 | 11.592 % |
c |    282720 |   54807   134635 |   25068   20416   233808    11.5 | 13.984 % |
c |    283058 |   54807   134635 |   27574   20754   240261    11.6 | 13.984 % |
c |    283565 |   54807   134635 |   30332   21261   259153    12.2 | 13.984 % |
c |    284324 |   54807   134635 |   33365   22020   307837    14.0 | 13.984 % |
c |    285466 |   54807   134635 |   36702   23162   332896    14.4 | 13.984 % |
c |    287175 |   54708   134406 |   40372   24867   374653    15.1 | 14.122 % |
c |    289738 |   54708   134406 |   44409   27430   489974    17.9 | 14.122 % |
c |    293585 |   54708   134406 |   48850   31277   649189    20.8 | 14.122 % |
c |    299351 |   54708   134406 |   53735   37043  1085572    29.3 | 14.122 % |
c |    308000 |   54708   134406 |   59109   45692  1721589    37.7 | 14.122 % |
c |    320974 |   54708   134406 |   65020   58666  2411561    41.1 | 14.122 % |
c |    340437 |   54588   134131 |   71522   31293  1186540    37.9 | 14.292 % |
c |    369630 |   54588   134131 |   78674   60486  2763729    45.7 | 14.293 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    391599 |   53680   132005 |   17893   81739  4063821    49.7 | 14.293 % |
c |    391705 |   53680   132005 |   19682   13614   131456     9.7 | 15.678 % |
c |    391855 |   53680   132005 |   21650   13764   135592     9.9 | 15.678 % |
c |    392083 |   53680   132005 |   23815   13992   143612    10.3 | 15.678 % |
c |    392421 |   53680   132005 |   26197   14330   149463    10.4 | 15.678 % |
c |    392928 |   53680   132005 |   28816   14837   167736    11.3 | 15.678 % |
c |    393687 |   53680   132005 |   31698   15596   188454    12.1 | 15.678 % |
c |    394826 |   53680   132005 |   34868   16735   221205    13.2 | 15.678 % |
c |    396535 |   53680   132005 |   38355   18444   297608    16.1 | 15.678 % |
c |    399097 |   53680   132005 |   42190   21006   372261    17.7 | 15.678 % |
c |    402941 |   53671   131985 |   46409   24849   548671    22.1 | 15.692 % |
c |    408707 |   53665   131971 |   51050   30614  1009014    33.0 | 15.701 % |
c |    417356 |   53641   131917 |   56155   39258  1454998    37.1 | 15.728 % |
c |    430330 |   53641   131917 |   61771   52232  2066000    39.6 | 15.728 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    439020 |   53674   132000 |   17891   60922  2692350    44.2 | 15.728 % |
c |    439120 |   53674   132000 |   19680   13173   105786     8.0 | 15.729 % |
c |    439270 |   53674   132000 |   21648   13323   107609     8.1 | 15.729 % |
c |    439496 |   53656   131959 |   23812   13547   110282     8.1 | 15.753 % |
c |    439833 |   53656   131959 |   26194   13884   113642     8.2 | 15.752 % |
c |    440342 |   53656   131959 |   28813   14393   120935     8.4 | 15.752 % |
c |    441101 |   53656   131959 |   31694   15152   132146     8.7 | 15.752 % |
c |    442240 |   53340   131223 |   34864   16240   155911     9.6 | 16.245 % |
c |    443950 |   53203   130909 |   38350   17593   182389    10.4 | 16.434 % |
c |    446512 |   53181   130858 |   42186   20152   237283    11.8 | 16.466 % |
c |    450356 |   53181   130858 |   46404   23996   468634    19.5 | 16.466 % |
c |    456122 |   53181   130858 |   51045   29762   794329    26.7 | 16.466 % |
c |    464772 |   53181   130858 |   56149   38412  1414486    36.8 | 16.466 % |
c |    477746 |   53086   130641 |   61764   51371  2233889    43.5 | 16.595 % |
c |    497207 |   53086   130641 |   67941   27710   648079    23.4 | 16.595 % |
c |    526400 |   53086   130641 |   74735   56903  3408321    59.9 | 16.595 % |
#### 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.88 0.97 0.92 2/54 13015
Raw data (stat): 13015 (runsolver) R 13014 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423189149 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.90 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2331 0 0 0 993 5 0 0 25 0 1 0 423189149 11407360 2244 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2785 2244 603 41 0 2744 0
vsize: 11140
[startup+20.0011 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2510 0 0 0 1991 6 0 0 25 0 1 0 423189149 12075008 2423 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2948 2423 603 41 0 2907 0
vsize: 11792
[startup+30.0008 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2760 0 0 0 2989 7 0 0 25 0 1 0 423189149 13131776 2673 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3206 2673 603 41 0 3165 0
vsize: 12824
[startup+40.001 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2951 0 0 0 3989 8 0 0 25 0 1 0 423189149 14053376 2864 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3431 2864 603 41 0 3390 0
vsize: 13724
[startup+50.0015 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2951 0 0 0 4989 8 0 0 25 0 1 0 423189149 14053376 2864 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3431 2864 603 41 0 3390 0
vsize: 13724
[startup+60.0014 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 2951 0 0 0 5989 8 0 0 25 0 1 0 423189149 14053376 2864 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3431 2864 603 41 0 3390 0
vsize: 13724
[startup+70.0026 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3071 0 0 0 6988 9 0 0 25 0 1 0 423189149 14594048 2984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3563 2984 603 41 0 3522 0
vsize: 14252
[startup+80.0031 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3283 0 0 0 7988 9 0 0 25 0 1 0 423189149 15523840 3196 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3790 3196 603 41 0 3749 0
vsize: 15160
[startup+90.0029 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3471 0 0 0 8988 9 0 0 25 0 1 0 423189149 16326656 3384 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3986 3384 603 41 0 3945 0
vsize: 15944
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 9986 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 10986 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 11987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 12987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 13987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 14987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 15987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 16987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 17987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 18987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 19987 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 20988 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 21988 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3762 0 0 0 22988 11 0 0 25 0 1 0 423189149 17489920 3675 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3675 603 41 0 4229 0
vsize: 17080
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 3772 0 0 0 23988 11 0 0 25 0 1 0 423189149 17489920 3685 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4270 3685 603 41 0 4229 0
vsize: 17080
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 4083 0 0 0 24987 12 0 0 25 0 1 0 423189149 18825216 3996 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 3996 603 41 0 4555 0
vsize: 18384
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 4348 0 0 0 25986 13 0 0 25 0 1 0 423189149 19898368 4261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4858 4261 603 41 0 4817 0
vsize: 19432
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 4647 0 0 0 26986 14 0 0 25 0 1 0 423189149 21135360 4560 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4560 603 41 0 5119 0
vsize: 20640
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 4867 0 0 0 27985 15 0 0 25 0 1 0 423189149 21942272 4780 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5357 4780 603 41 0 5316 0
vsize: 21428
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5050 0 0 0 28985 15 0 0 25 0 1 0 423189149 22745088 4963 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5553 4963 603 41 0 5512 0
vsize: 22212
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5204 0 0 0 29985 16 0 0 25 0 1 0 423189149 23412736 5117 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5716 5117 603 41 0 5675 0
vsize: 22864
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5347 0 0 0 30984 16 0 0 25 0 1 0 423189149 23945216 5260 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5846 5260 603 41 0 5805 0
vsize: 23384
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5510 0 0 0 31984 16 0 0 25 0 1 0 423189149 24600576 5423 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5423 603 41 0 5965 0
vsize: 24024
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5510 0 0 0 32984 16 0 0 25 0 1 0 423189149 24600576 5423 4294967295 134512640 134672761 3221224576 3221223744 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5423 603 41 0 5965 0
vsize: 24024
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5510 0 0 0 33985 16 0 0 25 0 1 0 423189149 24600576 5423 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5423 603 41 0 5965 0
vsize: 24024
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5510 0 0 0 34985 16 0 0 25 0 1 0 423189149 24600576 5423 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5423 603 41 0 5965 0
vsize: 24024
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5510 0 0 0 35985 16 0 0 25 0 1 0 423189149 24600576 5423 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5423 603 41 0 5965 0
vsize: 24024
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 36985 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 37985 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 38985 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 39986 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 40986 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5511 0 0 0 41986 17 0 0 25 0 1 0 423189149 24600576 5424 4294967295 134512640 134672761 3221224576 3221223760 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5424 603 41 0 5965 0
vsize: 24024
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 42986 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223876 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 43986 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 44986 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223760 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 45986 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 46987 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 47987 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 48987 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 49987 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 50987 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223712 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 51988 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 52988 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 53988 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223760 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 54988 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223776 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 55988 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 56989 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 57989 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 58989 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 59989 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 60989 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5512 0 0 0 61990 17 0 0 25 0 1 0 423189149 24600576 5425 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6006 5425 603 41 0 5965 0
vsize: 24024
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5681 0 0 0 62989 17 0 0 25 0 1 0 423189149 25260032 5594 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6167 5594 603 41 0 6126 0
vsize: 24668
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 5864 0 0 0 63989 18 0 0 25 0 1 0 423189149 26062848 5777 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6363 5777 603 41 0 6322 0
vsize: 25452
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6107 0 0 0 64989 18 0 0 25 0 1 0 423189149 26992640 6020 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6590 6020 603 41 0 6549 0
vsize: 26360
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6359 0 0 0 65987 20 0 0 25 0 1 0 423189149 28327936 6272 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6916 6272 603 41 0 6875 0
vsize: 27664
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6600 0 0 0 66987 21 0 0 25 0 1 0 423189149 29257728 6513 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7143 6513 603 41 0 7102 0
vsize: 28572
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6760 0 0 0 67986 21 0 0 25 0 1 0 423189149 29929472 6673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6673 603 41 0 7266 0
vsize: 29228
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6760 0 0 0 68987 21 0 0 25 0 1 0 423189149 29929472 6673 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6673 603 41 0 7266 0
vsize: 29228
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6760 0 0 0 69987 21 0 0 25 0 1 0 423189149 29929472 6673 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6673 603 41 0 7266 0
vsize: 29228
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6760 0 0 0 70987 21 0 0 25 0 1 0 423189149 29929472 6673 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6673 603 41 0 7266 0
vsize: 29228
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 71987 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 72987 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223712 134560657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 73988 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 74988 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 75988 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 76988 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6761 0 0 0 77988 21 0 0 25 0 1 0 423189149 29929472 6674 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6674 603 41 0 7266 0
vsize: 29228
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 6817 0 0 0 78988 21 0 0 25 0 1 0 423189149 30195712 6730 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7372 6730 603 41 0 7331 0
vsize: 29488
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7057 0 0 0 79988 22 0 0 25 0 1 0 423189149 31141888 6970 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7603 6970 603 41 0 7562 0
vsize: 30412
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7235 0 0 0 80988 22 0 0 25 0 1 0 423189149 31956992 7148 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7802 7148 603 41 0 7761 0
vsize: 31208
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7444 0 0 0 81988 23 0 0 25 0 1 0 423189149 32759808 7357 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7998 7357 603 41 0 7957 0
vsize: 31992
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7709 0 0 0 82987 24 0 0 25 0 1 0 423189149 33824768 7622 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8258 7622 603 41 0 8217 0
vsize: 33032
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 83987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 84987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 85987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 86987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 87987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 88987 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 89988 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 90988 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 91988 24 0 0 25 0 1 0 423189149 34054144 7683 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8314 7683 603 41 0 8273 0
vsize: 33256
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 92988 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 93988 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 94988 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 95989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 96989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 97989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 98989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 99989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 100989 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7770 0 0 0 101990 24 0 0 25 0 1 0 423189149 34050048 7683 4294967295 134512640 134672761 3221224576 3221223776 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7683 603 41 0 8272 0
vsize: 33252
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 102990 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 103990 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 104990 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 105990 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 106990 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 107991 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 108991 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 109991 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 110991 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 111991 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 112992 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 113992 24 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 114992 25 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7771 0 0 0 115992 25 0 0 25 0 1 0 423189149 34050048 7684 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8313 7684 603 41 0 8272 0
vsize: 33252
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 7904 0 0 0 116992 25 0 0 25 0 1 0 423189149 34578432 7817 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8442 7817 603 41 0 8401 0
vsize: 33768
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 8072 0 0 0 117992 25 0 0 25 0 1 0 423189149 35246080 7985 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8605 7985 603 41 0 8564 0
vsize: 34420
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 8271 0 0 0 118992 26 0 0 25 0 1 0 423189149 36052992 8184 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8802 8184 603 41 0 8761 0
vsize: 35208
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 13015
Raw data (stat): 13015 (minisat+) R 13014 5897 5896 0 -1 0 8526 0 0 0 119991 27 0 0 25 0 1 0 423189149 37122048 8439 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9063 8439 603 41 0 9022 0
vsize: 36252
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 13015
Raw data (stat): 13015 (minisat+) Z 13014 5897 5896 0 -1 12 8529 0 0 0 119991 29 0 0 25 0 1 0 423189149 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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