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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-3.opb
MD5SUM	3acd642471b3f4559739eef7eb2e9b58
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
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	760
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	760
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	1175.06
Number of variables	760
Total number of constraints	41095
Number of constraints which are clauses	41095
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5032

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 21:32:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2930 boxname=wulflinc20 idbench=326 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3acd642471b3f4559739eef7eb2e9b58  /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-3.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-3.opb
IDLAUNCH: 2930
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893264 kB
Buffers:         33668 kB
Cached:          72156 kB
SwapCached:       2636 kB
Active:          45860 kB
Inactive:        65456 kB
HighTotal:      131008 kB
HighFree:        55132 kB
LowTotal:       903652 kB
LowFree:        838132 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24624 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:52:35 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 2930 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41095 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 |   41095    82190 |   13698       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77395   167462 |   25798       0        0     nan |  0.000 % |
c |       101 |   77238   167143 |   28377      90      929    10.3 |  0.331 % |
c |       251 |   76847   166316 |   31215     211     2466    11.7 |  1.208 % |
c |       476 |   75972   164442 |   34337     395     4215    10.7 |  3.304 % |
c |       813 |   74494   161218 |   37770     658     7446    11.3 |  6.726 % |
c |      1319 |   71556   154677 |   41547    1013    11473    11.3 | 13.931 % |
c |      2078 |   68045   146771 |   45702    1564    17859    11.4 | 22.774 % |
c |      3217 |   62670   134504 |   50273    2321    28070    12.1 | 36.635 % |
c |      4925 |   56128   119095 |   55300    3417    45635    13.4 | 53.971 % |
c |      7487 |   51841   108909 |   60830    5071    80265    15.8 | 65.575 % |
c ==============================================================================
c [1mFound solution: -32[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 |      8864 |   50474   105612 |   16824    6059   132156    21.8 | 65.575 % |
c |      8964 |   50044   104589 |   18506    6068   132299    21.8 | 70.483 % |
c |      9114 |   49720   103800 |   20357    6093   133270    21.9 | 71.397 % |
c |      9339 |   49622   103571 |   22392    6281   138021    22.0 | 71.655 % |
c |      9677 |   49534   103357 |   24632    6586   144121    21.9 | 71.908 % |
c |     10183 |   49289   102776 |   27095    7005   153375    21.9 | 72.576 % |
c |     10942 |   48817   101638 |   29804    7437   174082    23.4 | 73.908 % |
c |     12081 |   48123    99987 |   32785    8315   226746    27.3 | 75.808 % |
c |     13789 |   47814    99243 |   36063    9822   297504    30.3 | 76.774 % |
c ==============================================================================
c [1mFound solution: -33[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 |     15122 |   47804    99246 |   15934   11128   367947    33.1 | 76.774 % |
c |     15222 |   47639    98853 |   17527   11109   366482    33.0 | 77.190 % |
c |     15372 |   47595    98751 |   19280   11227   369541    32.9 | 77.307 % |
c |     15597 |   47595    98751 |   21208   11452   386987    33.8 | 77.307 % |
c |     15936 |   47595    98751 |   23328   11791   400789    34.0 | 77.307 % |
c |     16442 |   47499    98515 |   25661   12216   419172    34.3 | 77.584 % |
c |     17201 |   47006    97343 |   28228   12699   460842    36.3 | 78.935 % |
c |     18340 |   46999    97326 |   31050   13820   534818    38.7 | 78.955 % |
c |     20048 |   46939    97192 |   34155   15464   658464    42.6 | 79.104 % |
c ==============================================================================
c [1mFound solution: -34[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 |     20986 |   46927    97141 |   15642   16249   721785    44.4 | 79.104 % |
c |     21086 |   46732    96676 |   17206   16212   722537    44.6 | 79.688 % |
c |     21236 |   46721    96649 |   18926   16356   727214    44.5 | 79.720 % |
c |     21463 |   46721    96649 |   20819   16583   740187    44.6 | 79.720 % |
c |     21800 |   46721    96649 |   22901   16920   757005    44.7 | 79.720 % |
c |     22306 |   46721    96649 |   25191   17426   776599    44.6 | 79.720 % |
c |     23065 |   46718    96642 |   27710   18177   823057    45.3 | 79.728 % |
c |     24204 |   46648    96470 |   30481   19252   920173    47.8 | 79.929 % |
c |     25912 |   46551    96239 |   33530   20864  1063720    51.0 | 80.183 % |
c |     28474 |   46411    95903 |   36883   23262  1288226    55.4 | 80.568 % |
c |     32318 |   46361    95779 |   40571   27052  1576672    58.3 | 80.713 % |
c |     38085 |   46232    95472 |   44628   32638  2119521    64.9 | 81.067 % |
c |     46736 |   46197    95387 |   49091   41194  3124221    75.8 | 81.163 % |
c |     59710 |   45887    94639 |   54000   53780  4274679    79.5 | 82.040 % |
c ==============================================================================
c [1mFound solution: -35[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 |     68731 |   45876    94626 |   15292   62730  5053895    80.6 | 82.040 % |
c |     68831 |   45876    94626 |   16821   18447  1108901    60.1 | 82.148 % |
c |     68981 |   45852    94564 |   18503   18590  1112238    59.8 | 82.220 % |
c |     69207 |   45846    94550 |   20353   18795  1124590    59.8 | 82.236 % |
c |     69544 |   45846    94550 |   22389   19132  1156718    60.5 | 82.236 % |
c |     70050 |   45846    94550 |   24627   19638  1198376    61.0 | 82.236 % |
c |     70809 |   45846    94550 |   27090   20397  1276601    62.6 | 82.236 % |
c |     71948 |   45846    94550 |   29799   21536  1352008    62.8 | 82.236 % |
c |     73656 |   45846    94550 |   32779   23244  1501208    64.6 | 82.236 % |
c |     76218 |   45772    94364 |   36057   25794  1717538    66.6 | 82.460 % |
c ==============================================================================
c [1mFound solution: -36[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 |     79852 |   45763    94329 |   15254   29426  2135545    72.6 | 82.460 % |
c |     79952 |   45763    94329 |   16779   29526  2141968    72.5 | 82.494 % |
c |     80102 |   45763    94329 |   18457   29676  2155080    72.6 | 82.494 % |
c |     80327 |   45763    94329 |   20303   29901  2168898    72.5 | 82.494 % |
c |     80665 |   45763    94329 |   22333   30239  2188372    72.4 | 82.494 % |
c |     81171 |   45763    94329 |   24566   30745  2229210    72.5 | 82.494 % |
c |     81930 |   45763    94329 |   27023   31504  2289974    72.7 | 82.494 % |
c |     83069 |   45763    94329 |   29725   32643  2381067    72.9 | 82.494 % |
c |     84777 |   45763    94329 |   32698   34351  2511357    73.1 | 82.494 % |
c |     87340 |   45753    94303 |   35968   36906  2770585    75.1 | 82.526 % |
c |     91184 |   45690    94150 |   39564   40741  3063992    75.2 | 82.706 % |
c |     96950 |   45658    94074 |   43521   46425  3529731    76.0 | 82.794 % |
c |    105600 |   45646    94046 |   47873   55068  4237732    77.0 | 82.826 % |
c |    118574 |   45646    94046 |   52660   68042  5330410    78.3 | 82.826 % |
c |    138036 |   45576    93882 |   57927   34000  2343565    68.9 | 83.014 % |
c ==============================================================================
c [1mFound solution: -37[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 |    149466 |   45599    93945 |   15199   45430  3332463    73.4 | 83.014 % |
c |    149566 |   45599    93945 |   16718   17803  1045062    58.7 | 82.973 % |
c |    149718 |   45599    93945 |   18390   17955  1053066    58.7 | 82.973 % |
c |    149943 |   45599    93945 |   20229   18180  1067373    58.7 | 82.973 % |
c |    150281 |   45596    93938 |   22252   18516  1082787    58.5 | 82.981 % |
c |    150787 |   45593    93931 |   24478   19013  1111621    58.5 | 82.989 % |
c |    151546 |   45593    93931 |   26925   19772  1179618    59.7 | 82.989 % |
c |    152686 |   45593    93931 |   29618   20912  1287628    61.6 | 82.989 % |
c |    154394 |   45593    93931 |   32580   22620  1436347    63.5 | 82.989 % |
c |    156956 |   45580    93900 |   35838   25160  1626071    64.6 | 83.025 % |
c |    160800 |   45469    93635 |   39422   28964  1960525    67.7 | 83.337 % |
c |    166566 |   45422    93516 |   43364   34720  2450264    70.6 | 83.481 % |
c |    175216 |   45422    93516 |   47700   43370  3106157    71.6 | 83.481 % |
c |    188190 |   45409    93485 |   52471   56340  4190159    74.4 | 83.517 % |
c |    207651 |   45378    93412 |   57718   20752   843783    40.7 | 83.597 % |
c |    236844 |   45348    93342 |   63489   49941  3556546    71.2 | 83.677 % |
c |    280635 |   45332    93300 |   69838   29311  1271672    43.4 | 83.729 % |
c ==============================================================================
c [1mFound solution: -38[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 |    344995 |   45289    93179 |   15096   22206   620998    28.0 | 83.729 % |
c |    345095 |   45289    93179 |   16605   22306   624408    28.0 | 83.859 % |
c |    345245 |   45289    93179 |   18266   22456   629871    28.0 | 83.859 % |
c |    345471 |   45289    93179 |   20092   22682   637923    28.1 | 83.859 % |
c |    345808 |   45289    93179 |   22102   23019   650581    28.3 | 83.859 % |
c |    346315 |   45289    93179 |   24312   23526   669167    28.4 | 83.859 % |
c |    347074 |   45221    93013 |   26743   24280   705523    29.1 | 84.055 % |
c |    348213 |   45212    92988 |   29417   25414   778295    30.6 | 84.087 % |
c |    349921 |   45141    92818 |   32359   27103   880732    32.5 | 84.283 % |
c |    352483 |   45141    92818 |   35595   29665  1032114    34.8 | 84.283 % |
c |    356327 |   45141    92818 |   39155   33509  1294905    38.6 | 84.283 % |
c |    362093 |   45141    92818 |   43070   39275  1678091    42.7 | 84.283 % |
c |    370742 |   45141    92818 |   47377   47924  2281068    47.6 | 84.283 % |
c |    383716 |   45141    92818 |   52115   60898  2875601    47.2 | 84.283 % |
c |    403178 |   45131    92794 |   57327   26764   757803    28.3 | 84.311 % |
c |    432371 |   45125    92780 |   63059   55955  2218138    39.6 | 84.327 % |
c |    476160 |   45116    92759 |   69365   36944  1091586    29.5 | 84.351 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 C723 -C722 -C721 -C720 -C719 -C718 -C717 C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 -C420 -C419 -C418 -C417 -C416 -C415 C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75#### 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.84 0.94 0.90 2/54 30876
Raw data (stat): 30876 (runsolver) R 30875 27565 27564 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 479216025 1052672 97 4294967295 134512640 135381576 3221224528 3221219968 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 2850 0 0 0 990 8 0 0 25 0 1 0 479216025 14110720 2828 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3445 2828 603 41 0 3404 0
vsize: 13780
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 2869 0 0 0 1989 8 0 0 25 0 1 0 479216025 14110720 2847 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3445 2847 603 41 0 3404 0
vsize: 13780
[startup+30.0025 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 2925 0 0 0 2989 9 0 0 25 0 1 0 479216025 14381056 2903 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 2903 603 41 0 3470 0
vsize: 14044
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 3298 0 0 0 3988 9 0 0 25 0 1 0 479216025 16134144 3276 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3939 3276 603 41 0 3898 0
vsize: 15756
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 3800 0 0 0 4987 11 0 0 25 0 1 0 479216025 18231296 3778 4294967295 134512640 134672761 3221224624 3221223760 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4451 3778 603 41 0 4410 0
vsize: 17804
[startup+60.0026 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 4390 0 0 0 5985 13 0 0 25 0 1 0 479216025 20643840 4368 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5040 4368 603 41 0 4999 0
vsize: 20160
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 4899 0 0 0 6984 14 0 0 25 0 1 0 479216025 22794240 4877 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5565 4877 603 41 0 5524 0
vsize: 22260
[startup+80.0035 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 5469 0 0 0 7982 16 0 0 25 0 1 0 479216025 25206784 5447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6154 5447 603 41 0 6113 0
vsize: 24616
[startup+90.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 6005 0 0 0 8980 18 0 0 25 0 1 0 479216025 27340800 5983 4294967295 134512640 134672761 3221224624 3221223640 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6675 5983 603 41 0 6634 0
vsize: 26700
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 6481 0 0 0 9979 20 0 0 25 0 1 0 479216025 29347840 6459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7165 6459 603 41 0 7124 0
vsize: 28660
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 6939 0 0 0 10977 22 0 0 25 0 1 0 479216025 31207424 6917 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7619 6917 603 41 0 7578 0
vsize: 30476
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 7243 0 0 0 11976 23 0 0 25 0 1 0 479216025 32415744 7221 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7221 603 41 0 7873 0
vsize: 31656
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 7612 0 0 0 12975 24 0 0 25 0 1 0 479216025 33882112 7590 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8272 7590 603 41 0 8231 0
vsize: 33088
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 7983 0 0 0 13974 26 0 0 25 0 1 0 479216025 35348480 7961 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8630 7961 603 41 0 8589 0
vsize: 34520
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8305 0 0 0 14973 27 0 0 25 0 1 0 479216025 36687872 8283 4294967295 134512640 134672761 3221224624 3221223824 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8957 8283 603 41 0 8916 0
vsize: 35828
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 15972 27 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 16972 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 17972 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 18973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 19973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 20973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 21973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 22973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8459 0 0 0 23973 28 0 0 25 0 1 0 479216025 37265408 8437 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9098 8437 603 41 0 9057 0
vsize: 36392
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8486 0 0 0 24973 28 0 0 25 0 1 0 479216025 37396480 8464 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9130 8464 603 41 0 9089 0
vsize: 36520
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 8822 0 0 0 25973 29 0 0 25 0 1 0 479216025 38985728 8800 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9518 8800 603 41 0 9477 0
vsize: 38072
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9145 0 0 0 26972 30 0 0 25 0 1 0 479216025 40325120 9123 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9123 603 41 0 9804 0
vsize: 39380
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9377 0 0 0 27971 31 0 0 25 0 1 0 479216025 41259008 9355 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10073 9355 603 41 0 10032 0
vsize: 40292
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9377 0 0 0 28971 31 0 0 25 0 1 0 479216025 41259008 9355 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10073 9355 603 41 0 10032 0
vsize: 40292
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9377 0 0 0 29971 31 0 0 25 0 1 0 479216025 41259008 9355 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10073 9355 603 41 0 10032 0
vsize: 40292
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9377 0 0 0 30971 31 0 0 25 0 1 0 479216025 41259008 9355 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10073 9355 603 41 0 10032 0
vsize: 40292
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9377 0 0 0 31972 31 0 0 25 0 1 0 479216025 41259008 9355 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10073 9355 603 41 0 10032 0
vsize: 40292
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 32972 31 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 33972 31 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 34972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 35972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 36972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223728 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 37972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 38972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 39972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 40972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 41972 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 42973 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 43973 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9388 0 0 0 44973 32 0 0 25 0 1 0 479216025 41357312 9366 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9366 603 41 0 10056 0
vsize: 40388
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 45973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 46973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 47973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 48973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 49973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 50973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 51973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 52973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 53973 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 54974 33 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 55974 34 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 56974 34 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 57974 34 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9390 0 0 0 58974 34 0 0 25 0 1 0 479216025 41357312 9368 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9368 603 41 0 10056 0
vsize: 40388
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9393 0 0 0 59974 34 0 0 25 0 1 0 479216025 41357312 9371 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9371 603 41 0 10056 0
vsize: 40388
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9395 0 0 0 60974 34 0 0 25 0 1 0 479216025 41357312 9373 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10097 9373 603 41 0 10056 0
vsize: 40388
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9484 0 0 0 61974 34 0 0 25 0 1 0 479216025 41627648 9462 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10163 9462 603 41 0 10122 0
vsize: 40652
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 62974 34 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 63974 34 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 64974 34 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 65974 34 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 66974 35 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 67974 35 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9638 0 0 0 68974 35 0 0 25 0 1 0 479216025 42291200 9616 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9616 603 41 0 10284 0
vsize: 41300
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 69974 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 70974 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 71975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 72975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 73975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 74975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 75975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9643 0 0 0 76975 35 0 0 25 0 1 0 479216025 42426368 9621 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9621 603 41 0 10317 0
vsize: 41432
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9644 0 0 0 77975 35 0 0 25 0 1 0 479216025 42426368 9622 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9622 603 41 0 10317 0
vsize: 41432
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9652 0 0 0 78975 35 0 0 25 0 1 0 479216025 42426368 9630 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9630 603 41 0 10317 0
vsize: 41432
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9661 0 0 0 79975 35 0 0 25 0 1 0 479216025 42426368 9639 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9639 603 41 0 10317 0
vsize: 41432
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 80975 35 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 81975 35 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 82975 36 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 83975 36 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223792 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 84976 36 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9671 0 0 0 85976 36 0 0 25 0 1 0 479216025 42426368 9649 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9649 603 41 0 10317 0
vsize: 41432
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 86976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 87976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 88976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 89976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 90976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 91976 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 92977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 93977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 94977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 95977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 96977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 97977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 98977 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9672 0 0 0 99978 36 0 0 25 0 1 0 479216025 42426368 9650 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9650 603 41 0 10317 0
vsize: 41432
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9675 0 0 0 100978 36 0 0 25 0 1 0 479216025 42426368 9653 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9653 603 41 0 10317 0
vsize: 41432
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9675 0 0 0 101978 37 0 0 25 0 1 0 479216025 42426368 9653 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10358 9653 603 41 0 10317 0
vsize: 41432
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9680 0 0 0 102978 37 0 0 25 0 1 0 479216025 42590208 9658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9658 603 41 0 10357 0
vsize: 41592
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9681 0 0 0 103978 37 0 0 25 0 1 0 479216025 42590208 9659 4294967295 134512640 134672761 3221224624 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9659 603 41 0 10357 0
vsize: 41592
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9681 0 0 0 104978 37 0 0 25 0 1 0 479216025 42590208 9659 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9659 603 41 0 10357 0
vsize: 41592
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9687 0 0 0 105978 37 0 0 25 0 1 0 479216025 42590208 9665 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9665 603 41 0 10357 0
vsize: 41592
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9690 0 0 0 106978 37 0 0 25 0 1 0 479216025 42590208 9668 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9668 603 41 0 10357 0
vsize: 41592
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9690 0 0 0 107979 37 0 0 25 0 1 0 479216025 42590208 9668 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9668 603 41 0 10357 0
vsize: 41592
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9690 0 0 0 108979 37 0 0 25 0 1 0 479216025 42590208 9668 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9668 603 41 0 10357 0
vsize: 41592
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9690 0 0 0 109979 37 0 0 25 0 1 0 479216025 42590208 9668 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9668 603 41 0 10357 0
vsize: 41592
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9690 0 0 0 110979 37 0 0 25 0 1 0 479216025 42590208 9668 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9668 603 41 0 10357 0
vsize: 41592
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9702 0 0 0 111979 37 0 0 25 0 1 0 479216025 42590208 9680 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9680 603 41 0 10357 0
vsize: 41592
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9702 0 0 0 112979 37 0 0 25 0 1 0 479216025 42590208 9680 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9680 603 41 0 10357 0
vsize: 41592
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9703 0 0 0 113979 37 0 0 25 0 1 0 479216025 42590208 9681 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9681 603 41 0 10357 0
vsize: 41592
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9703 0 0 0 114980 37 0 0 25 0 1 0 479216025 42590208 9681 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9681 603 41 0 10357 0
vsize: 41592
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9703 0 0 0 115979 37 0 0 25 0 1 0 479216025 42590208 9681 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9681 603 41 0 10357 0
vsize: 41592
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9703 0 0 0 116980 38 0 0 25 0 1 0 479216025 42590208 9681 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9681 603 41 0 10357 0
vsize: 41592
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9704 0 0 0 117980 38 0 0 25 0 1 0 479216025 42590208 9682 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9682 603 41 0 10357 0
vsize: 41592
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9704 0 0 0 118980 38 0 0 25 0 1 0 479216025 42590208 9682 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9682 603 41 0 10357 0
vsize: 41592
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 27565 27564 0 -1 0 9704 0 0 0 119980 38 0 0 25 0 1 0 479216025 42590208 9682 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10398 9682 603 41 0 10357 0
vsize: 41592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30876
Raw data (stat): 30876 (minisat+) Z 30875 27565 27564 0 -1 12 9707 0 0 0 119980 40 0 0 25 0 1 0 479216025 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.21
CPU user time (s): 1199.81
CPU system time (s): 0.401938
CPU usage (%): 100.014
Max. virtual memory (Kb): 41592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####