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-1.opb
MD5SUM	94f501465233508e2f652cf118ddaf2d
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	41314
Number of constraints which are clauses	41314
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 6368

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        881312 kB
Buffers:         36000 kB
Cached:          80140 kB
SwapCached:          4 kB
Active:          56960 kB
Inactive:        62956 kB
HighTotal:      131008 kB
HighFree:        46368 kB
LowTotal:       903652 kB
LowFree:        834944 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27888 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:01:15 (client local time) WITH STATUS 10 IN 1200.83 SECONDS
stats: 4836 7 1200.83 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41314 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 |   41314    82628 |   13771       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -30[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 |  113974   252729 |   37991       0        0     nan |  0.000 % |
c |       101 |  113890   252541 |   41790      99      428     4.3 |  0.113 % |
c |       251 |  112573   249556 |   45969     220     1122     5.1 |  1.625 % |
c |       477 |  109818   243245 |   50566     380     1800     4.7 |  5.089 % |
c |       814 |  106979   236726 |   55622     623     4138     6.6 |  8.505 % |
c |      1321 |  102830   227144 |   61184    1021     7235     7.1 | 13.792 % |
c |      2080 |   95572   210447 |   67303    1527    11150     7.3 | 22.944 % |
c |      3219 |   86506   189402 |   74033    2308    17908     7.8 | 34.815 % |
c |      4928 |   73760   159556 |   81437    3303    29141     8.8 | 51.862 % |
c |      7490 |   61278   130369 |   89580    4698    44562     9.5 | 69.105 % |
c ==============================================================================
c [1mFound solution: -31[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 |      9137 |   56411   118929 |   18803    5477    58507    10.7 | 69.105 % |
c |      9237 |   55960   117878 |   20683    5509    59189    10.7 | 76.780 % |
c |      9389 |   55334   116408 |   22751    5526    60068    10.9 | 77.658 % |
c |      9614 |   55328   116394 |   25026    5747    67633    11.8 | 77.666 % |
c |      9951 |   54542   114549 |   27529    5951    70072    11.8 | 78.776 % |
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 |     10122 |   54509   114464 |   18169    6118    75202    12.3 | 78.776 % |
c |     10222 |   54509   114464 |   19985    6217    76075    12.2 | 78.810 % |
c |     10372 |   54505   114455 |   21984    6367    82475    13.0 | 78.810 % |
c |     10597 |   54505   114455 |   24182    6592    99314    15.1 | 78.810 % |
c |     10934 |   54413   114243 |   26601    6913   107688    15.6 | 78.927 % |
c |     11440 |   53399   111845 |   29261    7118   116329    16.3 | 80.375 % |
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 |     11774 |   53461   112006 |   17820    7452   137895    18.5 | 80.375 % |
c |     11874 |   53461   112006 |   19602    7552   142384    18.9 | 80.337 % |
c |     12024 |   53052   111047 |   21562    7535   146157    19.4 | 80.899 % |
c |     12251 |   52992   110905 |   23718    7735   151667    19.6 | 80.988 % |
c |     12588 |   52853   110580 |   26090    7972   161624    20.3 | 81.181 % |
c |     13094 |   52445   109629 |   28699    8349   178283    21.4 | 81.727 % |
c |     13853 |   52239   109144 |   31569    8987   209867    23.4 | 82.017 % |
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 |     14189 |   52035   108639 |   17345    9196   216723    23.6 | 82.017 % |
c |     14290 |   51785   108039 |   19079    9207   216772    23.5 | 82.661 % |
c |     14440 |   51649   107717 |   20987    9179   220822    24.1 | 82.854 % |
c |     14665 |   51649   107717 |   23086    9404   238119    25.3 | 82.854 % |
c |     15004 |   51621   107651 |   25394    9735   246397    25.3 | 82.894 % |
c |     15510 |   51611   107628 |   27934   10240   271689    26.5 | 82.906 % |
c |     16269 |   51543   107463 |   30727   10966   301270    27.5 | 83.019 % |
c |     17408 |   51543   107463 |   33800   12105   384667    31.8 | 83.019 % |
c |     19116 |   51543   107463 |   37180   13813   532593    38.6 | 83.019 % |
c |     21678 |   51095   106410 |   40898   15951   684360    42.9 | 83.666 % |
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 |     22456 |   51056   106329 |   17018   16686   728762    43.7 | 83.666 % |
c |     22556 |   51056   106329 |   18719   16786   734480    43.8 | 83.812 % |
c |     22707 |   51056   106329 |   20591   16937   742679    43.8 | 83.812 % |
c |     22932 |   51056   106329 |   22650   17162   753647    43.9 | 83.812 % |
c |     23269 |   50980   106148 |   24916   17366   768640    44.3 | 83.928 % |
c |     23775 |   50980   106148 |   27407   17872   805220    45.1 | 83.928 % |
c |     24534 |   50835   105807 |   30148   18568   855886    46.1 | 84.144 % |
c |     25673 |   50336   104627 |   33163   19162   892081    46.6 | 84.861 % |
c |     27381 |   50336   104627 |   36479   20870  1044010    50.0 | 84.861 % |
c |     29943 |   50336   104627 |   40127   23432  1255838    53.6 | 84.861 % |
c |     33787 |   50137   104160 |   44140   26954  1534330    56.9 | 85.141 % |
c |     39553 |   50137   104160 |   48554   32720  2107741    64.4 | 85.141 % |
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 |     41597 |   50099   104063 |   16699   34699  2235249    64.4 | 85.141 % |
c |     41697 |   50099   104063 |   18368   34799  2240736    64.4 | 85.190 % |
c |     41847 |   50099   104063 |   20205   34949  2246232    64.3 | 85.190 % |
c |     42072 |   50099   104063 |   22226   35174  2263478    64.4 | 85.190 % |
c |     42409 |   50099   104063 |   24449   35511  2280731    64.2 | 85.190 % |
c |     42915 |   50093   104049 |   26893   36016  2323391    64.5 | 85.198 % |
c |     43675 |   50016   103868 |   29583   36649  2372488    64.7 | 85.310 % |
c |     44814 |   49992   103811 |   32541   37758  2455924    65.0 | 85.346 % |
c |     46523 |   49992   103811 |   35795   39467  2595848    65.8 | 85.346 % |
c |     49085 |   49914   103626 |   39375   41841  2825405    67.5 | 85.462 % |
c |     52929 |   49665   103044 |   43312   44929  3090249    68.8 | 85.818 % |
c |     58695 |   49665   103044 |   47644   50695  3532905    69.7 | 85.818 % |
c |     67344 |   49665   103044 |   52408   59344  4244623    71.5 | 85.818 % |
c |     80319 |   49613   102920 |   57649   72272  5193582    71.9 | 85.898 % |
c |     99780 |   49554   102785 |   63414   31298  2009301    64.2 | 85.970 % |
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 |    128355 |   49593   102880 |   16531   59873  3921975    65.5 | 85.970 % |
c |    128455 |   49593   102880 |   18184   18030   807013    44.8 | 85.934 % |
c |    128606 |   49593   102880 |   20002   18181   816390    44.9 | 85.934 % |
c |    128831 |   49593   102880 |   22002   18406   829015    45.0 | 85.934 % |
c |    129169 |   49593   102880 |   24203   18744   846155    45.1 | 85.934 % |
c |    129675 |   49593   102880 |   26623   19250   873850    45.4 | 85.934 % |
c |    130435 |   49593   102880 |   29285   20010   914487    45.7 | 85.934 % |
c |    131574 |   49476   102606 |   32214   21123   977624    46.3 | 86.098 % |
c |    133282 |   49476   102606 |   35435   22831  1089121    47.7 | 86.098 % |
c |    135844 |   49434   102508 |   38979   25380  1256164    49.5 | 86.154 % |
c |    139688 |   49394   102413 |   42877   29209  1497336    51.3 | 86.214 % |
c |    145454 |   49370   102357 |   47164   34968  1865423    53.3 | 86.246 % |
c |    154104 |   49370   102357 |   51881   43618  2615365    60.0 | 86.246 % |
c |    167078 |   49366   102348 |   57069   56591  3320337    58.7 | 86.250 % |
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 |    183651 |   49312   102197 |   16437   73150  4144177    56.7 | 86.250 % |
c |    183751 |   49312   102197 |   18080   19049   664882    34.9 | 86.315 % |
c |    183901 |   49312   102197 |   19888   19199   669827    34.9 | 86.315 % |
c |    184126 |   49312   102197 |   21877   19424   676927    34.9 | 86.315 % |
c |    184465 |   49312   102197 |   24065   19763   691480    35.0 | 86.315 % |
c |    184971 |   49312   102197 |   26471   20269   710315    35.0 | 86.315 % |
c |    185734 |   49312   102197 |   29119   21032   735900    35.0 | 86.315 % |
c |    186873 |   49312   102197 |   32031   22171   775479    35.0 | 86.315 % |
c |    188581 |   49308   102188 |   35234   23878   872155    36.5 | 86.319 % |
c |    191144 |   49308   102188 |   38757   26441  1018971    38.5 | 86.319 % |
c |    194988 |   49239   102025 |   42633   30269  1155762    38.2 | 86.423 % |
c |    200754 |   49239   102025 |   46896   36035  1353829    37.6 | 86.423 % |
c |    209403 |   49197   101927 |   51586   44666  1615678    36.2 | 86.483 % |
c |    222377 |   49197   101927 |   56744   57640  1987329    34.5 | 86.483 % |
c |    241838 |   49187   101904 |   62419   77100  2679511    34.8 | 86.495 % |
c |    271030 |   49187   101904 |   68661   41996  1656429    39.4 | 86.495 % |
c |    314821 |   49115   101737 |   75527   85770  3854819    44.9 | 86.591 % |
c |    380506 |   49097   101695 |   83080   73871  2222719    30.1 | 86.615 % |
c |    479033 |   49067   101624 |   91388   87682  2971176    33.9 | 86.659 % |
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.91 0.95 0.90 2/54 21585
Raw data (stat): 21585 (runsolver) R 21584 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481793472 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 3029 0 0 0 989 8 0 0 25 0 1 0 481793472 14614528 3007 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3568 3007 603 41 0 3527 0
vsize: 14272
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 3029 0 0 0 1989 8 0 0 25 0 1 0 481793472 14614528 3007 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3568 3007 603 41 0 3527 0
vsize: 14272
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 3029 0 0 0 2989 8 0 0 25 0 1 0 481793472 14614528 3007 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3568 3007 603 41 0 3527 0
vsize: 14272
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 3273 0 0 0 3987 9 0 0 25 0 1 0 481793472 15753216 3251 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3846 3251 603 41 0 3805 0
vsize: 15384
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 3859 0 0 0 4986 11 0 0 25 0 1 0 481793472 18214912 3837 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4447 3837 603 41 0 4406 0
vsize: 17788
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 4428 0 0 0 5984 12 0 0 25 0 1 0 481793472 20484096 4406 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5001 4406 603 41 0 4960 0
vsize: 20004
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 4983 0 0 0 6982 14 0 0 25 0 1 0 481793472 22757376 4961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5556 4961 603 41 0 5515 0
vsize: 22224
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 5511 0 0 0 7980 16 0 0 25 0 1 0 481793472 25116672 5489 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6132 5489 603 41 0 6091 0
vsize: 24528
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 5934 0 0 0 8980 17 0 0 25 0 1 0 481793472 26718208 5912 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6523 5912 603 41 0 6482 0
vsize: 26092
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 6367 0 0 0 9979 18 0 0 25 0 1 0 481793472 28590080 6345 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6980 6345 603 41 0 6939 0
vsize: 27920
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 6720 0 0 0 10978 19 0 0 25 0 1 0 481793472 29933568 6698 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7308 6698 603 41 0 7267 0
vsize: 29232
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 7104 0 0 0 11976 21 0 0 25 0 1 0 481793472 31526912 7082 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7697 7082 603 41 0 7656 0
vsize: 30788
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 7491 0 0 0 12975 23 0 0 25 0 1 0 481793472 33124352 7469 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8087 7469 603 41 0 8046 0
vsize: 32348
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 7734 0 0 0 13974 24 0 0 25 0 1 0 481793472 34058240 7712 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8315 7712 603 41 0 8274 0
vsize: 33260
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 8080 0 0 0 14972 25 0 0 25 0 1 0 481793472 35397632 8058 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8642 8058 603 41 0 8601 0
vsize: 34568
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 8400 0 0 0 15972 26 0 0 25 0 1 0 481793472 36990976 8378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9031 8378 603 41 0 8990 0
vsize: 36124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 8694 0 0 0 16971 27 0 0 25 0 1 0 481793472 38187008 8672 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9323 8672 603 41 0 9282 0
vsize: 37292
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 8979 0 0 0 17970 29 0 0 25 0 1 0 481793472 39387136 8957 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9616 8957 603 41 0 9575 0
vsize: 38464
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9293 0 0 0 18969 30 0 0 25 0 1 0 481793472 40587264 9271 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9909 9271 603 41 0 9868 0
vsize: 39636
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 19969 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 20969 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 21969 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 22969 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 23969 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 24970 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 25970 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9469 0 0 0 26970 30 0 0 25 0 1 0 481793472 41390080 9447 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9447 603 41 0 10064 0
vsize: 40420
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 27970 30 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221222912 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 28970 30 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 29970 30 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 30970 30 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 31971 30 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 32971 31 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 33971 31 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9479 0 0 0 34971 31 0 0 25 0 1 0 481793472 41390080 9457 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9457 603 41 0 10064 0
vsize: 40420
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 35971 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 36971 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 37972 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 38972 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 39972 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223696 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 40972 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 41972 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 42973 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 43973 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223560 1075350830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 44973 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 45973 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 46973 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 47974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+490.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 48974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+500.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 49974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+510.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 50974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+520.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 51974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+530.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9480 0 0 0 52974 31 0 0 25 0 1 0 481793472 41390080 9458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9458 603 41 0 10064 0
vsize: 40420
[startup+540.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9482 0 0 0 53975 31 0 0 25 0 1 0 481793472 41390080 9460 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9460 603 41 0 10064 0
vsize: 40420
[startup+550.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 54975 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+560.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 55975 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+570.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 56975 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+580.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 57975 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+590.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 58975 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+600.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 59976 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+610.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 60976 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+620.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 61976 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+630.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 62976 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+640.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 63976 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+650.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 64977 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+660.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 65977 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+670.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 66977 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+680.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 67977 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+690.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9484 0 0 0 68977 31 0 0 25 0 1 0 481793472 41390080 9462 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9462 603 41 0 10064 0
vsize: 40420
[startup+700.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9486 0 0 0 69977 31 0 0 25 0 1 0 481793472 41390080 9464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9464 603 41 0 10064 0
vsize: 40420
[startup+710.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9489 0 0 0 70977 31 0 0 25 0 1 0 481793472 41390080 9467 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9467 603 41 0 10064 0
vsize: 40420
[startup+720.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9492 0 0 0 71978 31 0 0 25 0 1 0 481793472 41390080 9470 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9470 603 41 0 10064 0
vsize: 40420
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9495 0 0 0 72978 31 0 0 25 0 1 0 481793472 41390080 9473 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9473 603 41 0 10064 0
vsize: 40420
[startup+740.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 73978 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223696 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 74978 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223516 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+760.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 75978 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+770.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 76978 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+780.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 77979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+790.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 78979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+800.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 79979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+810.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 80979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 81979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 82979 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 83980 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+850.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 84980 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+860.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9497 0 0 0 85980 31 0 0 25 0 1 0 481793472 41390080 9475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9475 603 41 0 10064 0
vsize: 40420
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9515 0 0 0 86980 31 0 0 25 0 1 0 481793472 41525248 9493 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10138 9493 603 41 0 10097 0
vsize: 40552
[startup+880.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9525 0 0 0 87980 31 0 0 25 0 1 0 481793472 41525248 9503 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9503 603 41 0 10097 0
vsize: 40552
[startup+890.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9528 0 0 0 88980 31 0 0 25 0 1 0 481793472 41525248 9506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9506 603 41 0 10097 0
vsize: 40552
[startup+900.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9530 0 0 0 89980 31 0 0 25 0 1 0 481793472 41525248 9508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9508 603 41 0 10097 0
vsize: 40552
[startup+910.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9530 0 0 0 90980 31 0 0 25 0 1 0 481793472 41525248 9508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9508 603 41 0 10097 0
vsize: 40552
[startup+920.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9531 0 0 0 91980 31 0 0 25 0 1 0 481793472 41525248 9509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9509 603 41 0 10097 0
vsize: 40552
[startup+930.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9531 0 0 0 92980 31 0 0 25 0 1 0 481793472 41525248 9509 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9509 603 41 0 10097 0
vsize: 40552
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9531 0 0 0 93981 31 0 0 25 0 1 0 481793472 41525248 9509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9509 603 41 0 10097 0
vsize: 40552
[startup+950.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9534 0 0 0 94981 31 0 0 25 0 1 0 481793472 41525248 9512 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9512 603 41 0 10097 0
vsize: 40552
[startup+960.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9537 0 0 0 95981 31 0 0 25 0 1 0 481793472 41525248 9515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9515 603 41 0 10097 0
vsize: 40552
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 96981 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+980.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 97981 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 98982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 99982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 100982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 101982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 102982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 103982 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 104983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 105983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 106983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 107983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 108983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 109983 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 110984 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 111984 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21585
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9539 0 0 0 112995 31 0 0 25 0 1 0 481793472 41525248 9517 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10138 9517 603 41 0 10097 0
vsize: 40552
[startup+1140.4 s]
Raw data (loadavg): 1.08 1.00 0.92 4/58 21630
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9549 0 0 0 114022 31 0 0 25 0 1 0 481793472 41721856 9527 4294967295 134512640 134672761 3221224560 3221223744 134559280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9527 603 41 0 10145 0
vsize: 40744
[startup+1150.4 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9566 0 0 0 115022 31 0 0 25 0 1 0 481793472 41721856 9544 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9544 603 41 0 10145 0
vsize: 40744
[startup+1160.65 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9567 0 0 0 116048 31 0 0 25 0 1 0 481793472 41721856 9545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9545 603 41 0 10145 0
vsize: 40744
[startup+1170.65 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9567 0 0 0 117048 31 0 0 25 0 1 0 481793472 41721856 9545 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9545 603 41 0 10145 0
vsize: 40744
[startup+1180.65 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9567 0 0 0 118048 31 0 0 25 0 1 0 481793472 41721856 9545 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9545 603 41 0 10145 0
vsize: 40744
[startup+1190.65 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9567 0 0 0 119048 31 0 0 25 0 1 0 481793472 41721856 9545 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9545 603 41 0 10145 0
vsize: 40744
[startup+1200.65 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 21638
Raw data (stat): 21585 (minisat+) R 21584 10614 10613 0 -1 0 9567 0 0 0 120048 31 0 0 25 0 1 0 481793472 41721856 9545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10186 9545 603 41 0 10145 0
vsize: 40744
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.68 s]
Raw data (loadavg): 1.06 1.01 0.93 1/54 21638
Raw data (stat): 21585 (minisat+) Z 21584 10614 10613 0 -1 12 9570 0 0 0 120049 33 0 0 25 0 1 0 481793472 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.68
CPU time (s): 1200.83
CPU user time (s): 1200.49
CPU system time (s): 0.335948
CPU usage (%): 100.013
Max. virtual memory (Kb): 40744
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####