PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-3.opb
MD5SUM	3acd642471b3f4559739eef7eb2e9b58
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41095
Number of constraints which are clauses	41095
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6370

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        826348 kB
Buffers:         33464 kB
Cached:         131456 kB
SwapCached:        524 kB
Active:          52688 kB
Inactive:       115640 kB
HighTotal:      131008 kB
HighFree:         5740 kB
LowTotal:       903652 kB
LowFree:        820608 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34468 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:02:19 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4838 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41095 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41095    82190 |   13698       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  114089   253065 |   38029       0        0     nan |  0.000 % |
c |       100 |  114058   252996 |   41831      99     1268    12.8 |  0.036 % |
c |       250 |  113239   251136 |   46015     225     2052     9.1 |  1.042 % |
c |       477 |  110189   244112 |   50616     363     2893     8.0 |  4.770 % |
c |       815 |  106648   236009 |   55678     604     4642     7.7 |  9.141 % |
c |      1321 |  101873   225037 |   61246     982     8202     8.4 | 14.993 % |
c |      2080 |   97534   215073 |   67370    1621    14496     8.9 | 20.487 % |
c |      3219 |   86418   189311 |   74107    2324    24130    10.4 | 34.872 % |
c |      4927 |   73896   160013 |   81518    3297    34395    10.4 | 51.552 % |
c |      7489 |   61252   130371 |   89670    4638    52162    11.2 | 69.084 % |
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 |      9284 |   56569   119375 |   18856    5469    64919    11.9 | 69.084 % |
c |      9384 |   56549   119329 |   20741    5564    66008    11.9 | 75.430 % |
c |      9534 |   56353   118860 |   22815    5667    66883    11.8 | 75.731 % |
c |      9759 |   55229   116205 |   25097    5615    66860    11.9 | 77.374 % |
c |     10097 |   55039   115757 |   27607    5897    78694    13.3 | 77.655 % |
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 |     10397 |   54616   114774 |   18205    6036    84843    14.1 | 77.655 % |
c |     10499 |   54545   114605 |   20025    6112    86876    14.2 | 78.444 % |
c |     10649 |   54075   113499 |   22028    6111    86043    14.1 | 79.112 % |
c |     10874 |   53522   112198 |   24230    6189    87509    14.1 | 79.912 % |
c |     11211 |   52732   110347 |   26653    6257    90279    14.4 | 81.017 % |
c |     11717 |   52263   109235 |   29319    6612   103097    15.6 | 81.696 % |
c |     12476 |   51981   108574 |   32251    7243   118840    16.4 | 82.090 % |
c |     13615 |   51879   108330 |   35476    8288   145591    17.6 | 82.247 % |
c |     15323 |   51446   107310 |   39024    9509   196920    20.7 | 82.870 % |
c |     17885 |   51080   106446 |   42926   11708   324152    27.7 | 83.417 % |
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 |     18418 |   51038   106335 |   17012   12229   365681    29.9 | 83.417 % |
c |     18518 |   51038   106335 |   18713   12329   370621    30.1 | 83.447 % |
c |     18669 |   50796   105773 |   20584   12384   378205    30.5 | 83.772 % |
c |     18894 |   50402   104841 |   22642   12192   375974    30.8 | 84.375 % |
c |     19231 |   50342   104700 |   24907   12459   394750    31.7 | 84.464 % |
c |     19737 |   50298   104597 |   27397   12948   431294    33.3 | 84.524 % |
c |     20496 |   50241   104464 |   30137   13603   484283    35.6 | 84.604 % |
c |     21635 |   50235   104450 |   33151   14734   567927    38.5 | 84.612 % |
c |     23344 |   49993   103879 |   36466   16152   692776    42.9 | 84.954 % |
c |     25906 |   49801   103434 |   40113   18487   866112    46.8 | 85.211 % |
c |     29750 |   49801   103434 |   44124   22331  1157443    51.8 | 85.211 % |
c |     35516 |   49745   103302 |   48537   27980  1643071    58.7 | 85.296 % |
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 |     43963 |   49798   103433 |   16599   36427  2644681    72.6 | 85.296 % |
c |     44063 |   49798   103433 |   18258   36527  2653258    72.6 | 85.288 % |
c |     44213 |   49515   102764 |   20084   36302  2651010    73.0 | 85.716 % |
c |     44438 |   49515   102764 |   22093   36527  2663112    72.9 | 85.716 % |
c |     44775 |   49515   102764 |   24302   36864  2668943    72.4 | 85.716 % |
c |     45281 |   49491   102707 |   26732   37362  2701554    72.3 | 85.752 % |
c |     46041 |   49491   102707 |   29406   38122  2754430    72.3 | 85.752 % |
c |     47180 |   49491   102707 |   32346   39261  2833310    72.2 | 85.752 % |
c |     48889 |   49485   102693 |   35581   40965  3015346    73.6 | 85.760 % |
c |     51452 |   49485   102693 |   39139   43528  3281839    75.4 | 85.760 % |
c |     55296 |   49471   102661 |   43053   47325  3562510    75.3 | 85.776 % |
c |     61063 |   49465   102647 |   47358   53084  4039687    76.1 | 85.784 % |
c |     69712 |   49465   102647 |   52094   61733  4828308    78.2 | 85.784 % |
c |     82686 |   49465   102647 |   57304   74707  6030509    80.7 | 85.784 % |
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 |     88916 |   49436   102567 |   16478   19152  1250037    65.3 | 85.784 % |
c |     89016 |   49436   102567 |   18125   19252  1258192    65.4 | 85.821 % |
c |     89166 |   49436   102567 |   19938   19402  1268302    65.4 | 85.821 % |
c |     89391 |   49436   102567 |   21932   19627  1284843    65.5 | 85.821 % |
c |     89728 |   49436   102567 |   24125   19964  1309202    65.6 | 85.821 % |
c |     90234 |   49436   102567 |   26537   20470  1349485    65.9 | 85.821 % |
c |     90993 |   49436   102567 |   29191   21229  1429207    67.3 | 85.821 % |
c |     92132 |   49436   102567 |   32110   22368  1517154    67.8 | 85.821 % |
c |     93840 |   49436   102567 |   35322   24076  1628509    67.6 | 85.821 % |
c |     96402 |   49436   102567 |   38854   26638  1845723    69.3 | 85.821 % |
c |    100246 |   49436   102567 |   42739   30482  2159857    70.9 | 85.821 % |
c |    106012 |   49436   102567 |   47013   36248  2554122    70.5 | 85.821 % |
c |    114662 |   49426   102544 |   51715   44896  3326202    74.1 | 85.833 % |
c |    127636 |   49420   102530 |   56886   57869  4665631    80.6 | 85.841 % |
c |    147099 |   49406   102497 |   62575   77326  6588850    85.2 | 85.861 % |
c |    176291 |   49274   102190 |   68832   40347  2524983    62.6 | 86.041 % |
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 |    211449 |   49313   102285 |   16437   75505  5177685    68.6 | 86.041 % |
c |    211550 |   49313   102285 |   18080   18889  1097615    58.1 | 86.005 % |
c |    211700 |   49313   102285 |   19888   19039  1104647    58.0 | 86.005 % |
c |    211925 |   49313   102285 |   21877   19264  1118912    58.1 | 86.005 % |
c |    212263 |   49313   102285 |   24065   19602  1141285    58.2 | 86.005 % |
c |    212769 |   49313   102285 |   26471   20108  1168387    58.1 | 86.005 % |
c |    213528 |   49279   102205 |   29119   20860  1216512    58.3 | 86.053 % |
c |    214667 |   49279   102205 |   32031   21999  1299961    59.1 | 86.053 % |
c |    216375 |   49273   102191 |   35234   23705  1423034    60.0 | 86.061 % |
c |    218937 |   49273   102191 |   38757   26267  1601429    61.0 | 86.061 % |
c |    222781 |   49212   102047 |   42633   30104  2053908    68.2 | 86.153 % |
c |    228548 |   49212   102047 |   46896   35871  2543186    70.9 | 86.153 % |
c |    237198 |   49212   102047 |   51586   44521  3325523    74.7 | 86.153 % |
c |    250172 |   49208   102038 |   56744   57492  4301988    74.8 | 86.157 % |
c |    269634 |   49139   101876 |   62419   76900  5541238    72.1 | 86.257 % |
c |    298826 |   48945   101421 |   68661   39643  2819288    71.1 | 86.533 % |
c |    342615 |   48939   101407 |   75527   83431  5821205    69.8 | 86.541 % |
c |    408299 |   48927   101379 |   83080   71397  3386748    47.4 | 86.557 % |
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 |    416650 |   48891   101275 |   16297   79748  3768230    47.3 | 86.557 % |
c |    416751 |   48891   101275 |   17926   19822   711364    35.9 | 86.602 % |
c |    416901 |   48891   101275 |   19719   19972   718266    36.0 | 86.602 % |
c |    417126 |   48891   101275 |   21691   20197   726776    36.0 | 86.602 % |
c |    417463 |   48881   101252 |   23860   20531   745800    36.3 | 86.614 % |
c |    417969 |   48881   101252 |   26246   21037   769025    36.6 | 86.614 % |
c |    418728 |   48881   101252 |   28871   21796   808372    37.1 | 86.614 % |
c |    419867 |   48881   101252 |   31758   22935   874430    38.1 | 86.614 % |
c |    421576 |   48881   101252 |   34934   24644   980958    39.8 | 86.614 % |
c |    424139 |   48881   101252 |   38427   27207  1148379    42.2 | 86.614 % |
c |    427983 |   48881   101252 |   42270   31051  1332139    42.9 | 86.614 % |
c |    433749 |   48875   101238 |   46497   36812  1687565    45.8 | 86.622 % |
c |    442398 |   48837   101148 |   51146   45452  2281308    50.2 | 86.678 % |
c |    455372 |   48837   101148 |   56261   58426  2759252    47.2 | 86.678 % |
c |    474833 |   48837   101148 |   61887   77887  3505079    45.0 | 86.678 % |
c |    504025 |   48837   101148 |   68076   43658  1984588    45.5 | 86.678 % |
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.92 0.96 0.91 2/54 32221
Raw data (stat): 32221 (runsolver) R 32220 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481793713 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99972 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 3038 0 0 0 990 9 0 0 25 0 1 0 481793713 14630912 3016 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3016 603 41 0 3531 0
vsize: 14288
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 3038 0 0 0 1990 9 0 0 25 0 1 0 481793713 14630912 3016 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3016 603 41 0 3531 0
vsize: 14288
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 3044 0 0 0 2990 9 0 0 25 0 1 0 481793713 14630912 3022 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3022 603 41 0 3531 0
vsize: 14288
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 3299 0 0 0 3988 11 0 0 25 0 1 0 481793713 15917056 3277 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3886 3277 603 41 0 3845 0
vsize: 15544
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 3947 0 0 0 4986 13 0 0 25 0 1 0 481793713 18624512 3925 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4547 3925 603 41 0 4506 0
vsize: 18188
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 4572 0 0 0 5984 15 0 0 25 0 1 0 481793713 21172224 4550 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5169 4550 603 41 0 5128 0
vsize: 20676
[startup+70.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 5223 0 0 0 6983 17 0 0 25 0 1 0 481793713 23834624 5201 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5819 5201 603 41 0 5778 0
vsize: 23276
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 5764 0 0 0 7981 18 0 0 25 0 1 0 481793713 26091520 5742 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6370 5742 603 41 0 6329 0
vsize: 25480
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 6159 0 0 0 8980 20 0 0 25 0 1 0 481793713 27721728 6137 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6768 6137 603 41 0 6727 0
vsize: 27072
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 6672 0 0 0 9978 22 0 0 25 0 1 0 481793713 29741056 6650 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6650 603 41 0 7220 0
vsize: 29044
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 7048 0 0 0 10977 23 0 0 25 0 1 0 481793713 31330304 7026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7649 7026 603 41 0 7608 0
vsize: 30596
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 7420 0 0 0 11975 25 0 0 25 0 1 0 481793713 32800768 7398 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8008 7398 603 41 0 7967 0
vsize: 32032
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 7817 0 0 0 12974 27 0 0 25 0 1 0 481793713 34390016 7795 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8396 7795 603 41 0 8355 0
vsize: 33584
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 8196 0 0 0 13972 28 0 0 25 0 1 0 481793713 35991552 8174 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8787 8174 603 41 0 8746 0
vsize: 35148
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 8547 0 0 0 14971 30 0 0 25 0 1 0 481793713 37330944 8525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9114 8525 603 41 0 9073 0
vsize: 36456
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 8925 0 0 0 15970 31 0 0 25 0 1 0 481793713 39194624 8903 4294967295 134512640 134672761 3221224560 3221223664 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9569 8903 603 41 0 9528 0
vsize: 38276
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 9284 0 0 0 16969 31 0 0 25 0 1 0 481793713 40652800 9262 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9925 9262 603 41 0 9884 0
vsize: 39700
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 9608 0 0 0 17968 32 0 0 25 0 1 0 481793713 41988096 9586 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10251 9586 603 41 0 10210 0
vsize: 41004
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 9920 0 0 0 18968 33 0 0 25 0 1 0 481793713 43188224 9898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10544 9898 603 41 0 10503 0
vsize: 42176
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 19967 34 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 20966 35 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 21966 35 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 22965 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 23965 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 24966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 25965 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 26966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 27966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 28966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 29966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 30966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10244 0 0 0 31966 36 0 0 25 0 1 0 481793713 44515328 10222 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10222 603 41 0 10827 0
vsize: 43472
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10324 0 0 0 32966 37 0 0 25 0 1 0 481793713 44908544 10302 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10964 10302 603 41 0 10923 0
vsize: 43856
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10580 0 0 0 33965 37 0 0 25 0 1 0 481793713 45969408 10558 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11223 10558 603 41 0 11182 0
vsize: 44892
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 10812 0 0 0 34965 38 0 0 25 0 1 0 481793713 46911488 10790 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11453 10790 603 41 0 11412 0
vsize: 45812
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 35964 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 36964 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 37964 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 38964 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 39965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 40965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 41965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 42965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 43965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 44965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223744 134558332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 45965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 46965 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223744 134559665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 47966 39 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 48966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 49966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 50966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 51965 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 52966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 53965 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 54966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 55966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 56966 40 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 57966 41 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11020 0 0 0 58966 41 0 0 25 0 1 0 481793713 47710208 10998 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10998 603 41 0 11607 0
vsize: 46592
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 59966 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 60966 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 61967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 62967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 63967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 64967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 65967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 66967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 67967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 68967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 69967 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 70968 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 71968 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 72968 41 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 73968 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 74968 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 75968 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 76968 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 77969 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11021 0 0 0 78969 42 0 0 25 0 1 0 481793713 47710208 10999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 10999 603 41 0 11607 0
vsize: 46592
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11023 0 0 0 79969 42 0 0 25 0 1 0 481793713 47710208 11001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11001 603 41 0 11607 0
vsize: 46592
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11026 0 0 0 80969 42 0 0 25 0 1 0 481793713 47710208 11004 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11004 603 41 0 11607 0
vsize: 46592
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11029 0 0 0 81969 42 0 0 25 0 1 0 481793713 47710208 11007 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11007 603 41 0 11607 0
vsize: 46592
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11032 0 0 0 82969 42 0 0 25 0 1 0 481793713 47710208 11010 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11010 603 41 0 11607 0
vsize: 46592
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 83969 42 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 84969 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 85969 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 86970 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 87970 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 88970 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 89970 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 90971 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 91971 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 92971 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 93971 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 94971 43 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 95971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 96971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 97971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 98971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 99971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 100971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 101971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 102971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 103971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 104971 44 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32221
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 105971 45 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 32256
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 106971 45 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1080.03 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 107970 45 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1090.03 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 108970 45 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1100.03 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 109970 45 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1110.03 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 110970 46 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1120.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 111970 46 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1130.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 112970 46 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1140.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32274
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11034 0 0 0 113970 46 0 0 25 0 1 0 481793713 47710208 11012 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11012 603 41 0 11607 0
vsize: 46592
[startup+1150.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 114970 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
[startup+1160.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 115970 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
[startup+1170.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 116971 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
[startup+1180.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 117971 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
[startup+1190.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 118971 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
[startup+1200.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32276
Raw data (stat): 32221 (minisat+) R 32220 26298 26297 0 -1 0 11040 0 0 0 119971 46 0 0 25 0 1 0 481793713 47710208 11018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11648 11018 603 41 0 11607 0
vsize: 46592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.02 1.00 0.92 1/54 32276
Raw data (stat): 32221 (minisat+) Z 32220 26298 26297 0 -1 12 11043 0 0 0 119971 48 0 0 25 0 1 0 481793713 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.72
CPU system time (s): 0.489925
CPU usage (%): 100.013
Max. virtual memory (Kb): 46592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####