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 5994

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        891644 kB
Buffers:         34912 kB
Cached:          65128 kB
SwapCached:        192 kB
Active:          54272 kB
Inactive:        48836 kB
HighTotal:      131008 kB
HighFree:        62104 kB
LowTotal:       903652 kB
LowFree:        829540 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34440 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:11:43 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4462 7 1200.19 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.85 0.97 0.91 2/54 7650
Raw data (stat): 7650 (runsolver) R 7649 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481130727 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 2835 0 0 0 990 8 0 0 25 0 1 0 481130727 14053376 2813 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3431 2813 603 41 0 3390 0
vsize: 13724
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 2854 0 0 0 1990 8 0 0 25 0 1 0 481130727 14053376 2832 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3431 2832 603 41 0 3390 0
vsize: 13724
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 2897 0 0 0 2990 8 0 0 25 0 1 0 481130727 14323712 2875 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3497 2875 603 41 0 3456 0
vsize: 13988
[startup+40.0004 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 3214 0 0 0 3987 10 0 0 25 0 1 0 481130727 15863808 3192 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3192 603 41 0 3832 0
vsize: 15492
[startup+50.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 3716 0 0 0 4985 11 0 0 25 0 1 0 481130727 17977344 3694 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4389 3694 603 41 0 4348 0
vsize: 17556
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 4287 0 0 0 5983 14 0 0 25 0 1 0 481130727 20262912 4265 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4947 4265 603 41 0 4906 0
vsize: 19788
[startup+70.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 4795 0 0 0 6981 16 0 0 25 0 1 0 481130727 22286336 4773 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5441 4773 603 41 0 5400 0
vsize: 21764
[startup+80.0012 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 5354 0 0 0 7980 17 0 0 25 0 1 0 481130727 24682496 5332 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6026 5332 603 41 0 5985 0
vsize: 24104
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 5906 0 0 0 8979 18 0 0 25 0 1 0 481130727 26943488 5884 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6578 5884 603 41 0 6537 0
vsize: 26312
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 6387 0 0 0 9977 20 0 0 25 0 1 0 481130727 28946432 6365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7067 6365 603 41 0 7026 0
vsize: 28268
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 6830 0 0 0 10976 22 0 0 25 0 1 0 481130727 30666752 6808 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7487 6808 603 41 0 7446 0
vsize: 29948
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 7148 0 0 0 11976 22 0 0 25 0 1 0 481130727 31997952 7126 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7812 7126 603 41 0 7771 0
vsize: 31248
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 7516 0 0 0 12975 23 0 0 25 0 1 0 481130727 33472512 7494 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8172 7494 603 41 0 8131 0
vsize: 32688
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 7882 0 0 0 13974 24 0 0 25 0 1 0 481130727 34942976 7860 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8531 7860 603 41 0 8490 0
vsize: 34124
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8204 0 0 0 14973 26 0 0 25 0 1 0 481130727 36270080 8182 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8855 8182 603 41 0 8814 0
vsize: 35420
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 15972 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 16972 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 17972 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 18973 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 19973 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 20973 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 21973 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 22973 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 23974 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8417 0 0 0 24974 27 0 0 25 0 1 0 481130727 37146624 8395 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9069 8395 603 41 0 9028 0
vsize: 36276
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8663 0 0 0 25973 28 0 0 25 0 1 0 481130727 38346752 8641 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9362 8641 603 41 0 9321 0
vsize: 37448
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 8968 0 0 0 26972 29 0 0 25 0 1 0 481130727 39694336 8946 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 8946 603 41 0 9650 0
vsize: 38764
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9281 0 0 0 27972 30 0 0 25 0 1 0 481130727 40898560 9259 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9985 9259 603 41 0 9944 0
vsize: 39940
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 28972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 29972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 30972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223744 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 31972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 32972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 33972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 34972 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 35973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 36973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 37973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 38973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 39973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 40974 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 41973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 42973 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 43974 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9347 0 0 0 44974 30 0 0 25 0 1 0 481130727 41164800 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9325 603 41 0 10009 0
vsize: 40200
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9348 0 0 0 45974 30 0 0 25 0 1 0 481130727 41164800 9326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9326 603 41 0 10009 0
vsize: 40200
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 46974 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 47974 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 48974 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7650
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 49975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 50975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 51975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 52975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 53975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 54975 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 55976 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7703
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 56976 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 57976 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 58976 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9349 0 0 0 59976 30 0 0 25 0 1 0 481130727 41164800 9327 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9327 603 41 0 10009 0
vsize: 40200
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9351 0 0 0 60977 30 0 0 25 0 1 0 481130727 41164800 9329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9329 603 41 0 10009 0
vsize: 40200
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9354 0 0 0 61977 30 0 0 25 0 1 0 481130727 41164800 9332 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10050 9332 603 41 0 10009 0
vsize: 40200
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9436 0 0 0 62977 30 0 0 25 0 1 0 481130727 41558016 9414 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10146 9414 603 41 0 10105 0
vsize: 40584
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 63977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223056 134565819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 64977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 65977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 66977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 67977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 68977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9609 0 0 0 69977 31 0 0 25 0 1 0 481130727 42229760 9587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9587 603 41 0 10269 0
vsize: 41240
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 70978 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 71978 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 72978 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 73978 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 74978 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 75979 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223664 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 76979 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 77979 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9613 0 0 0 78979 31 0 0 25 0 1 0 481130727 42229760 9591 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9591 603 41 0 10269 0
vsize: 41240
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9616 0 0 0 79979 31 0 0 25 0 1 0 481130727 42229760 9594 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9594 603 41 0 10269 0
vsize: 41240
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9625 0 0 0 80979 31 0 0 25 0 1 0 481130727 42229760 9603 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9603 603 41 0 10269 0
vsize: 41240
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7705
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 81979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 82979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 83979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 84979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 85979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 86979 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9631 0 0 0 87980 31 0 0 25 0 1 0 481130727 42377216 9609 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9609 603 41 0 10305 0
vsize: 41384
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9632 0 0 0 88980 31 0 0 25 0 1 0 481130727 42377216 9610 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9610 603 41 0 10305 0
vsize: 41384
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9632 0 0 0 89980 31 0 0 25 0 1 0 481130727 42377216 9610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9610 603 41 0 10305 0
vsize: 41384
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9637 0 0 0 90980 31 0 0 25 0 1 0 481130727 42377216 9615 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9615 603 41 0 10305 0
vsize: 41384
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9638 0 0 0 91980 31 0 0 25 0 1 0 481130727 42377216 9616 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9616 603 41 0 10305 0
vsize: 41384
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 92980 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 93981 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 94981 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 95981 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 96981 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 97981 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 98982 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 99982 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 100982 31 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9639 0 0 0 101981 32 0 0 25 0 1 0 481130727 42377216 9617 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10346 9617 603 41 0 10305 0
vsize: 41384
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9644 0 0 0 102981 32 0 0 25 0 1 0 481130727 42377216 9622 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9622 603 41 0 10305 0
vsize: 41384
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9644 0 0 0 103981 32 0 0 25 0 1 0 481130727 42377216 9622 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9622 603 41 0 10305 0
vsize: 41384
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9650 0 0 0 104981 32 0 0 25 0 1 0 481130727 42377216 9628 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9628 603 41 0 10305 0
vsize: 41384
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9650 0 0 0 105981 32 0 0 25 0 1 0 481130727 42377216 9628 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9628 603 41 0 10305 0
vsize: 41384
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9650 0 0 0 106981 32 0 0 25 0 1 0 481130727 42377216 9628 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9628 603 41 0 10305 0
vsize: 41384
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9657 0 0 0 107982 32 0 0 25 0 1 0 481130727 42377216 9635 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9635 603 41 0 10305 0
vsize: 41384
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9660 0 0 0 108982 32 0 0 25 0 1 0 481130727 42377216 9638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9638 603 41 0 10305 0
vsize: 41384
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9660 0 0 0 109982 32 0 0 25 0 1 0 481130727 42377216 9638 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9638 603 41 0 10305 0
vsize: 41384
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9660 0 0 0 110982 32 0 0 25 0 1 0 481130727 42377216 9638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9638 603 41 0 10305 0
vsize: 41384
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9660 0 0 0 111982 32 0 0 25 0 1 0 481130727 42377216 9638 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10346 9638 603 41 0 10305 0
vsize: 41384
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9667 0 0 0 112983 32 0 0 25 0 1 0 481130727 42541056 9645 4294967295 134512640 134672761 3221224560 3221223712 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9645 603 41 0 10345 0
vsize: 41544
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9673 0 0 0 113983 32 0 0 25 0 1 0 481130727 42541056 9651 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9651 603 41 0 10345 0
vsize: 41544
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9685 0 0 0 114983 32 0 0 25 0 1 0 481130727 42541056 9663 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9663 603 41 0 10345 0
vsize: 41544
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9685 0 0 0 115983 32 0 0 25 0 1 0 481130727 42541056 9663 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9663 603 41 0 10345 0
vsize: 41544
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9687 0 0 0 116983 32 0 0 25 0 1 0 481130727 42541056 9665 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9665 603 41 0 10345 0
vsize: 41544
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9687 0 0 0 117983 32 0 0 25 0 1 0 481130727 42541056 9665 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9665 603 41 0 10345 0
vsize: 41544
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9688 0 0 0 118984 32 0 0 25 0 1 0 481130727 42541056 9666 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9666 603 41 0 10345 0
vsize: 41544
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7707
Raw data (stat): 7650 (minisat+) R 7649 3260 3259 0 -1 0 9688 0 0 0 119984 32 0 0 25 0 1 0 481130727 42541056 9666 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9666 603 41 0 10345 0
vsize: 41544
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7707
Raw data (stat): 7650 (minisat+) Z 7649 3260 3259 0 -1 12 9691 0 0 0 119984 34 0 0 25 0 1 0 481130727 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.19
CPU user time (s): 1199.85
CPU system time (s): 0.340948
CPU usage (%): 100.013
Max. virtual memory (Kb): 41544
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####