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-2.opb
MD5SUM	270e069f649d19b0da4e4d23c0e1ebfc
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
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	41263
Number of constraints which are clauses	41263
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 6369

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 04:41:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4837 boxname=wulflinc21 idbench=325 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  270e069f649d19b0da4e4d23c0e1ebfc  /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-2.opb /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-2.opb
IDLAUNCH: 4837
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        870964 kB
Buffers:         28856 kB
Cached:         114760 kB
SwapCached:          0 kB
Active:          48508 kB
Inactive:        97968 kB
HighTotal:      131008 kB
HighFree:        13048 kB
LowTotal:       903652 kB
LowFree:        857916 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11728 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:01:52 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 4837 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41263 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 |   41263    82526 |   13754       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[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 |  113992   252769 |   37997       0        0     nan |  0.000 % |
c |       100 |  113973   252727 |   41796      99      414     4.2 |  0.024 % |
c |       250 |  112513   249397 |   45976     207     1060     5.1 |  1.779 % |
c |       475 |  110203   244153 |   50574     372     2298     6.2 |  4.438 % |
c |       812 |  107910   238889 |   55631     652     5508     8.4 |  7.268 % |
c |      1318 |  103052   227718 |   61194    1036     9023     8.7 | 13.344 % |
c ==============================================================================
c [1mFound solution: -30[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 |      1519 |  100537   221927 |   33512    1170    10630     9.1 | 13.344 % |
c |      1619 |  100135   221007 |   36863    1264    11899     9.4 | 16.988 % |
c |      1769 |   98999   218382 |   40549    1387    12843     9.3 | 18.448 % |
c |      1994 |   96806   213310 |   44604    1536    15881    10.3 | 21.301 % |
c |      2332 |   94028   206887 |   49064    1765    17768    10.1 | 24.914 % |
c |      2838 |   90214   198084 |   53971    2157    22899    10.6 | 29.785 % |
c |      3597 |   85081   186171 |   59368    2755    31563    11.5 | 36.470 % |
c |      4736 |   77461   168327 |   65305    3502    41058    11.7 | 46.728 % |
c |      6444 |   70039   150890 |   71835    4629    56504    12.2 | 56.861 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7554 |   66905   143647 |   22301    5405    64389    11.9 | 56.861 % |
c |      7654 |   66901   143638 |   24531    5503    65510    11.9 | 61.446 % |
c |      7804 |   66457   142585 |   26984    5595    66148    11.8 | 62.086 % |
c |      8029 |   64628   138308 |   29682    5585    67160    12.0 | 64.604 % |
c |      8366 |   63130   134789 |   32650    5589    70474    12.6 | 66.700 % |
c |      8873 |   61298   130479 |   35915    5877    75081    12.8 | 69.235 % |
c |      9632 |   59718   126743 |   39507    6317    85218    13.5 | 71.403 % |
c |     10773 |   57036   120447 |   43458    6787    94371    13.9 | 75.181 % |
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 |     12477 |   54596   114708 |   18198    7610   120252    15.8 | 75.181 % |
c |     12578 |   54554   114611 |   20017    7698   120787    15.7 | 78.659 % |
c |     12728 |   53576   112313 |   22019    7471   117914    15.8 | 80.023 % |
c |     12953 |   53397   111900 |   24221    7617   120488    15.8 | 80.244 % |
c |     13291 |   52988   110930 |   26643    7842   125200    16.0 | 80.960 % |
c |     13798 |   52624   110081 |   29308    8241   136135    16.5 | 81.342 % |
c |     14558 |   52528   109857 |   32238    8961   168466    18.8 | 81.471 % |
c |     15698 |   52455   109685 |   35462   10074   222604    22.1 | 81.575 % |
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 |     15817 |   52513   109834 |   17504   10193   227371    22.3 | 81.575 % |
c |     15917 |   52513   109834 |   19254   10293   234995    22.8 | 81.536 % |
c |     16068 |   52368   109489 |   21179   10368   236843    22.8 | 81.761 % |
c |     16293 |   51669   107838 |   23297   10034   236311    23.6 | 82.757 % |
c |     16630 |   51555   107566 |   25627   10322   242782    23.5 | 82.926 % |
c |     17136 |   51555   107566 |   28190   10828   271589    25.1 | 82.926 % |
c |     17895 |   51242   106830 |   31009   11317   290037    25.6 | 83.368 % |
c |     19034 |   51236   106816 |   34110   12446   362333    29.1 | 83.376 % |
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 |     20668 |   51014   106265 |   17004   13809   435819    31.6 | 83.376 % |
c |     20768 |   51014   106265 |   18704   13909   438099    31.5 | 83.679 % |
c |     20918 |   51004   106242 |   20574   14034   444935    31.7 | 83.691 % |
c |     21143 |   50924   106054 |   22632   14167   453310    32.0 | 83.807 % |
c |     21480 |   50918   106040 |   24895   14503   469763    32.4 | 83.816 % |
c |     21986 |   50842   105861 |   27385   14935   509396    34.1 | 83.924 % |
c |     22745 |   50770   105689 |   30123   15554   555482    35.7 | 84.032 % |
c |     23885 |   50742   105623 |   33135   16663   641666    38.5 | 84.073 % |
c |     25594 |   50742   105623 |   36449   18372   820050    44.6 | 84.073 % |
c |     28157 |   50531   105132 |   40094   20665   950187    46.0 | 84.358 % |
c |     32001 |   50531   105132 |   44103   24509  1316877    53.7 | 84.358 % |
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 |     34030 |   50596   105294 |   16865   26538  1503481    56.7 | 84.358 % |
c |     34130 |   50596   105294 |   18551   26638  1508176    56.6 | 84.341 % |
c |     34280 |   50596   105294 |   20406   26788  1515475    56.6 | 84.341 % |
c |     34505 |   50596   105294 |   22447   27013  1529362    56.6 | 84.341 % |
c |     34843 |   50596   105294 |   24692   27351  1546851    56.6 | 84.341 % |
c |     35349 |   50500   105069 |   27161   27672  1571343    56.8 | 84.477 % |
c |     36108 |   50500   105069 |   29877   28431  1622114    57.1 | 84.477 % |
c |     37247 |   50500   105069 |   32865   29570  1759811    59.5 | 84.478 % |
c |     38955 |   50500   105069 |   36151   31278  1924124    61.5 | 84.477 % |
c |     41517 |   50500   105069 |   39766   33840  2155827    63.7 | 84.477 % |
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 |     44938 |   50418   104867 |   16806   37033  2384032    64.4 | 84.477 % |
c |     45038 |   50418   104867 |   18486   37133  2392559    64.4 | 84.587 % |
c |     45188 |   50418   104867 |   20335   37283  2400440    64.4 | 84.587 % |
c |     45414 |   50418   104867 |   22368   37509  2416811    64.4 | 84.587 % |
c |     45751 |   50418   104867 |   24605   37846  2451748    64.8 | 84.587 % |
c |     46257 |   50418   104867 |   27066   38352  2495762    65.1 | 84.587 % |
c |     47017 |   50418   104867 |   29772   39112  2561113    65.5 | 84.587 % |
c |     48156 |   50418   104867 |   32750   40251  2692175    66.9 | 84.587 % |
c |     49867 |   50418   104867 |   36025   41962  2835819    67.6 | 84.587 % |
c |     52429 |   50418   104867 |   39627   44524  3033695    68.1 | 84.587 % |
c |     56273 |   50418   104867 |   43590   48368  3339698    69.0 | 84.587 % |
c |     62039 |   50414   104858 |   47949   54133  3854706    71.2 | 84.591 % |
c |     70688 |   50371   104754 |   52744   62777  4620112    73.6 | 84.667 % |
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 |     76263 |   50413   104858 |   16804   68352  5104419    74.7 | 84.667 % |
c |     76363 |   50227   104417 |   18484   19229  1122336    58.4 | 84.916 % |
c |     76513 |   49959   103782 |   20332   19304  1123841    58.2 | 85.300 % |
c |     76738 |   49959   103782 |   22366   19529  1138149    58.3 | 85.300 % |
c |     77076 |   49959   103782 |   24602   19867  1157765    58.3 | 85.300 % |
c |     77583 |   49953   103768 |   27063   20369  1183162    58.1 | 85.308 % |
c |     78343 |   49953   103768 |   29769   21129  1240817    58.7 | 85.308 % |
c |     79482 |   49953   103768 |   32746   22268  1311531    58.9 | 85.308 % |
c |     81190 |   49929   103711 |   36020   23972  1463276    61.0 | 85.344 % |
c |     83752 |   49929   103711 |   39622   26534  1632690    61.5 | 85.344 % |
c |     87597 |   49742   103267 |   43585   29887  1910897    63.9 | 85.623 % |
c |     93364 |   49742   103267 |   47943   35654  2319712    65.1 | 85.624 % |
c |    102013 |   49742   103267 |   52738   44303  2935150    66.3 | 85.623 % |
c |    114988 |   49742   103267 |   58011   57278  3695604    64.5 | 85.624 % |
c |    134449 |   49742   103267 |   63813   76739  4735408    61.7 | 85.624 % |
c |    163641 |   49716   103205 |   70194   37708  1548551    41.1 | 85.664 % |
c |    207431 |   49716   103205 |   77213   81498  3664399    45.0 | 85.664 % |
c |    273116 |   49706   103182 |   84935   67599  2896662    42.9 | 85.675 % |
c |    371643 |   49676   103113 |   93428   77527  4062109    52.4 | 85.711 % |
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 |    403135 |   49611   102937 |   16537  108995  5356846    49.1 | 85.711 % |
c |    403237 |   49611   102937 |   18190   20900   605177    29.0 | 85.793 % |
c |    403387 |   49611   102937 |   20009   21050   608270    28.9 | 85.793 % |
c |    403612 |   49611   102937 |   22010   21275   617803    29.0 | 85.793 % |
c |    403949 |   49577   102856 |   24211   21602   631470    29.2 | 85.845 % |
c |    404455 |   49563   102823 |   26633   22106   661720    29.9 | 85.865 % |
c |    405214 |   49555   102804 |   29296   22862   706837    30.9 | 85.876 % |
c |    406353 |   49450   102557 |   32225   23983   778193    32.4 | 86.024 % |
c |    408061 |   49450   102557 |   35448   25691   930565    36.2 | 86.024 % |
c |    410623 |   49450   102557 |   38993   28253  1039698    36.8 | 86.024 % |
c |    414468 |   49450   102557 |   42892   32098  1165117    36.3 | 86.024 % |
c |    420234 |   49450   102557 |   47181   37864  1407364    37.2 | 86.024 % |
c |    428883 |   49450   102557 |   51900   46513  1736018    37.3 | 86.024 % |
c |    441857 |   49444   102543 |   57090   59484  2228786    37.5 | 86.032 % |
c |    461320 |   49444   102543 |   62799   78947  2920488    37.0 | 86.032 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 C743 -C742 C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 C571 C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 C325 -C324 -C323 -C322 -C321 -C320 -C319 C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.92 2/55 5430
Raw data (stat): 5430 (runsolver) R 5429 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 359056124 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 3031 0 0 0 990 9 0 0 25 0 1 0 359056124 14622720 3009 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3570 3009 603 41 0 3529 0
vsize: 14280
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 3108 0 0 0 1990 9 0 0 25 0 1 0 359056124 15032320 3086 4294967295 134512640 134672761 3221224560 3221223712 134554625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3086 603 41 0 3629 0
vsize: 14680
[startup+30.0007 s]
Raw data (loadavg): 0.90 0.94 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 3109 0 0 0 2990 9 0 0 25 0 1 0 359056124 15032320 3087 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3087 603 41 0 3629 0
vsize: 14680
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 3229 0 0 0 3989 10 0 0 25 0 1 0 359056124 15638528 3207 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3207 603 41 0 3777 0
vsize: 15272
[startup+49.9999 s]
Raw data (loadavg): 0.93 0.94 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 3740 0 0 0 4987 12 0 0 25 0 1 0 359056124 17805312 3718 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4347 3718 603 41 0 4306 0
vsize: 17388
[startup+59.9995 s]
Raw data (loadavg): 0.94 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 4402 0 0 0 5985 14 0 0 25 0 1 0 359056124 20467712 4380 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4997 4380 603 41 0 4956 0
vsize: 19988
[startup+69.9998 s]
Raw data (loadavg): 0.95 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 4989 0 0 0 6983 16 0 0 25 0 1 0 359056124 22777856 4967 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5561 4967 603 41 0 5520 0
vsize: 22244
[startup+80.0001 s]
Raw data (loadavg): 0.96 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 5511 0 0 0 7982 17 0 0 25 0 1 0 359056124 25038848 5489 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6113 5489 603 41 0 6072 0
vsize: 24452
[startup+89.9998 s]
Raw data (loadavg): 0.96 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 5949 0 0 0 8981 18 0 0 25 0 1 0 359056124 26808320 5927 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6545 5927 603 41 0 6504 0
vsize: 26180
[startup+99.9994 s]
Raw data (loadavg): 0.97 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 6358 0 0 0 9979 20 0 0 25 0 1 0 359056124 28553216 6336 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6971 6336 603 41 0 6930 0
vsize: 27884
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 6751 0 0 0 10978 21 0 0 25 0 1 0 359056124 30154752 6729 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7362 6729 603 41 0 7321 0
vsize: 29448
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 7140 0 0 0 11977 22 0 0 25 0 1 0 359056124 31629312 7118 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7722 7118 603 41 0 7681 0
vsize: 30888
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 7537 0 0 0 12976 24 0 0 25 0 1 0 359056124 33247232 7515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7515 603 41 0 8076 0
vsize: 32468
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 7890 0 0 0 13975 25 0 0 25 0 1 0 359056124 34721792 7868 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7868 603 41 0 8436 0
vsize: 33908
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8214 0 0 0 14975 26 0 0 25 0 1 0 359056124 36048896 8192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8801 8192 603 41 0 8760 0
vsize: 35204
[startup+159.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8524 0 0 0 15974 26 0 0 25 0 1 0 359056124 37502976 8502 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9156 8502 603 41 0 9115 0
vsize: 36624
[startup+169.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 16974 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+179.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 17974 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 18975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223760 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+199.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 19975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+209.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 20975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+219.999 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 21975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+229.998 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 22975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+239.998 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 23975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+249.998 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 24975 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 25976 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8686 0 0 0 26976 26 0 0 25 0 1 0 359056124 38158336 8664 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8664 603 41 0 9275 0
vsize: 37264
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8687 0 0 0 27976 26 0 0 25 0 1 0 359056124 38158336 8665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8665 603 41 0 9275 0
vsize: 37264
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8690 0 0 0 28976 26 0 0 25 0 1 0 359056124 38158336 8668 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8668 603 41 0 9275 0
vsize: 37264
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8694 0 0 0 29976 26 0 0 25 0 1 0 359056124 38158336 8672 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8672 603 41 0 9275 0
vsize: 37264
[startup+309.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8697 0 0 0 30976 26 0 0 25 0 1 0 359056124 38158336 8675 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8675 603 41 0 9275 0
vsize: 37264
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8779 0 0 0 31976 27 0 0 25 0 1 0 359056124 38572032 8757 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9417 8757 603 41 0 9376 0
vsize: 37668
[startup+329.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 8943 0 0 0 32976 27 0 0 25 0 1 0 359056124 39235584 8921 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9579 8921 603 41 0 9538 0
vsize: 38316
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9011 0 0 0 33975 28 0 0 25 0 1 0 359056124 39497728 8989 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8989 603 41 0 9602 0
vsize: 38572
[startup+349.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9011 0 0 0 34975 28 0 0 25 0 1 0 359056124 39497728 8989 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8989 603 41 0 9602 0
vsize: 38572
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9011 0 0 0 35976 28 0 0 25 0 1 0 359056124 39497728 8989 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8989 603 41 0 9602 0
vsize: 38572
[startup+369.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 36976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+379.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 37976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 38976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 39976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 40976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+419.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 41976 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+429.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 42977 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 43977 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 44977 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 45977 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+469.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 46977 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+479.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9012 0 0 0 47978 28 0 0 25 0 1 0 359056124 39497728 8990 4294967295 134512640 134672761 3221224560 3221223664 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8990 603 41 0 9602 0
vsize: 38572
[startup+489.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9018 0 0 0 48978 28 0 0 25 0 1 0 359056124 39497728 8996 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 8996 603 41 0 9602 0
vsize: 38572
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9024 0 0 0 49978 28 0 0 25 0 1 0 359056124 39497728 9002 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9002 603 41 0 9602 0
vsize: 38572
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9032 0 0 0 50978 28 0 0 25 0 1 0 359056124 39497728 9010 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9643 9010 603 41 0 9602 0
vsize: 38572
[startup+519.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9041 0 0 0 51978 28 0 0 25 0 1 0 359056124 39661568 9019 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9019 603 41 0 9642 0
vsize: 38732
[startup+529.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9045 0 0 0 52978 28 0 0 25 0 1 0 359056124 39661568 9023 4294967295 134512640 134672761 3221224560 3221223744 134559482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9023 603 41 0 9642 0
vsize: 38732
[startup+539.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9048 0 0 0 53978 28 0 0 25 0 1 0 359056124 39661568 9026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9026 603 41 0 9642 0
vsize: 38732
[startup+549.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 54979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 55979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+569.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 56979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 57979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+589.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 58979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+599.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 59979 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+609.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 60980 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+619.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 61980 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+629.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 62980 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+639.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 63980 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+649.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9049 0 0 0 64980 28 0 0 25 0 1 0 359056124 39661568 9027 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9027 603 41 0 9642 0
vsize: 38732
[startup+659.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9057 0 0 0 65980 28 0 0 25 0 1 0 359056124 39661568 9035 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9035 603 41 0 9642 0
vsize: 38732
[startup+669.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9073 0 0 0 66980 29 0 0 25 0 1 0 359056124 39661568 9051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9051 603 41 0 9642 0
vsize: 38732
[startup+679.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9076 0 0 0 67980 29 0 0 25 0 1 0 359056124 39661568 9054 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9054 603 41 0 9642 0
vsize: 38732
[startup+689.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9080 0 0 0 68980 29 0 0 25 0 1 0 359056124 39858176 9058 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9731 9058 603 41 0 9690 0
vsize: 38924
[startup+699.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9083 0 0 0 69980 29 0 0 25 0 1 0 359056124 39858176 9061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9731 9061 603 41 0 9690 0
vsize: 38924
[startup+709.994 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9083 0 0 0 70980 29 0 0 25 0 1 0 359056124 39858176 9061 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9731 9061 603 41 0 9690 0
vsize: 38924
[startup+719.994 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9083 0 0 0 71980 29 0 0 25 0 1 0 359056124 39858176 9061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9731 9061 603 41 0 9690 0
vsize: 38924
[startup+729.994 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9235 0 0 0 72980 30 0 0 25 0 1 0 359056124 40390656 9213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9861 9213 603 41 0 9820 0
vsize: 39444
[startup+739.994 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9484 0 0 0 73979 31 0 0 25 0 1 0 359056124 41447424 9462 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10119 9462 603 41 0 10078 0
vsize: 40476
[startup+749.994 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9685 0 0 0 74978 32 0 0 25 0 1 0 359056124 42237952 9663 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10312 9663 603 41 0 10271 0
vsize: 41248
[startup+759.995 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9897 0 0 0 75977 33 0 0 25 0 1 0 359056124 43163648 9875 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10538 9875 603 41 0 10497 0
vsize: 42152
[startup+769.995 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9993 0 0 0 76977 33 0 0 25 0 1 0 359056124 43425792 9971 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 9971 603 41 0 10561 0
vsize: 42408
[startup+779.995 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9993 0 0 0 77978 33 0 0 25 0 1 0 359056124 43425792 9971 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 9971 603 41 0 10561 0
vsize: 42408
[startup+789.995 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9993 0 0 0 78977 33 0 0 25 0 1 0 359056124 43425792 9971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 9971 603 41 0 10561 0
vsize: 42408
[startup+799.994 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9993 0 0 0 79977 33 0 0 25 0 1 0 359056124 43425792 9971 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 9971 603 41 0 10561 0
vsize: 42408
[startup+809.995 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9993 0 0 0 80978 33 0 0 25 0 1 0 359056124 43425792 9971 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 9971 603 41 0 10561 0
vsize: 42408
[startup+819.995 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 9998 0 0 0 81978 33 0 0 25 0 1 0 359056124 43581440 9976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10640 9976 603 41 0 10599 0
vsize: 42560
[startup+829.994 s]
Raw data (loadavg): 1.08 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10008 0 0 0 82978 33 0 0 25 0 1 0 359056124 43581440 9986 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10640 9986 603 41 0 10599 0
vsize: 42560
[startup+839.995 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10008 0 0 0 83978 33 0 0 25 0 1 0 359056124 43581440 9986 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10640 9986 603 41 0 10599 0
vsize: 42560
[startup+849.995 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10016 0 0 0 84978 33 0 0 25 0 1 0 359056124 43581440 9994 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10640 9994 603 41 0 10599 0
vsize: 42560
[startup+859.995 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10029 0 0 0 85978 33 0 0 25 0 1 0 359056124 43745280 10007 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10680 10007 603 41 0 10639 0
vsize: 42720
[startup+869.995 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10036 0 0 0 86978 33 0 0 25 0 1 0 359056124 43745280 10014 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10680 10014 603 41 0 10639 0
vsize: 42720
[startup+879.995 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10036 0 0 0 87978 33 0 0 25 0 1 0 359056124 43745280 10014 4294967295 134512640 134672761 3221224560 3221223664 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10680 10014 603 41 0 10639 0
vsize: 42720
[startup+889.994 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10036 0 0 0 88979 33 0 0 25 0 1 0 359056124 43745280 10014 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10680 10014 603 41 0 10639 0
vsize: 42720
[startup+899.994 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10051 0 0 0 89979 33 0 0 25 0 1 0 359056124 43745280 10029 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10680 10029 603 41 0 10639 0
vsize: 42720
[startup+909.995 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10079 0 0 0 90979 34 0 0 25 0 1 0 359056124 43909120 10057 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10720 10057 603 41 0 10679 0
vsize: 42880
[startup+919.995 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10087 0 0 0 91979 34 0 0 25 0 1 0 359056124 43909120 10065 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10720 10065 603 41 0 10679 0
vsize: 42880
[startup+929.994 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10113 0 0 0 92979 34 0 0 25 0 1 0 359056124 44072960 10091 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10760 10091 603 41 0 10719 0
vsize: 43040
[startup+939.995 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10114 0 0 0 93979 34 0 0 25 0 1 0 359056124 44072960 10092 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10092 603 41 0 10719 0
vsize: 43040
[startup+949.994 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10115 0 0 0 94979 34 0 0 25 0 1 0 359056124 44072960 10093 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10093 603 41 0 10719 0
vsize: 43040
[startup+959.995 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10116 0 0 0 95979 34 0 0 25 0 1 0 359056124 44072960 10094 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10094 603 41 0 10719 0
vsize: 43040
[startup+969.995 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10119 0 0 0 96979 34 0 0 25 0 1 0 359056124 44072960 10097 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10097 603 41 0 10719 0
vsize: 43040
[startup+979.994 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10119 0 0 0 97979 34 0 0 25 0 1 0 359056124 44072960 10097 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10097 603 41 0 10719 0
vsize: 43040
[startup+989.994 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10119 0 0 0 98979 34 0 0 25 0 1 0 359056124 44072960 10097 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10097 603 41 0 10719 0
vsize: 43040
[startup+999.994 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10120 0 0 0 99980 34 0 0 25 0 1 0 359056124 44072960 10098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10098 603 41 0 10719 0
vsize: 43040
[startup+1009.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10120 0 0 0 100980 34 0 0 25 0 1 0 359056124 44072960 10098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10098 603 41 0 10719 0
vsize: 43040
[startup+1019.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10121 0 0 0 101980 34 0 0 25 0 1 0 359056124 44072960 10099 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10760 10099 603 41 0 10719 0
vsize: 43040
[startup+1029.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10131 0 0 0 102980 34 0 0 25 0 1 0 359056124 44171264 10109 4294967295 134512640 134672761 3221224560 3221223664 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10109 603 41 0 10743 0
vsize: 43136
[startup+1039.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10132 0 0 0 103980 34 0 0 25 0 1 0 359056124 44171264 10110 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10110 603 41 0 10743 0
vsize: 43136
[startup+1049.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10132 0 0 0 104980 34 0 0 25 0 1 0 359056124 44171264 10110 4294967295 134512640 134672761 3221224560 3221223696 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10110 603 41 0 10743 0
vsize: 43136
[startup+1059.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10132 0 0 0 105980 34 0 0 25 0 1 0 359056124 44171264 10110 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10110 603 41 0 10743 0
vsize: 43136
[startup+1069.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10132 0 0 0 106981 34 0 0 25 0 1 0 359056124 44171264 10110 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10110 603 41 0 10743 0
vsize: 43136
[startup+1079.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10132 0 0 0 107980 34 0 0 25 0 1 0 359056124 44171264 10110 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10110 603 41 0 10743 0
vsize: 43136
[startup+1089.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5430
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10135 0 0 0 108980 35 0 0 25 0 1 0 359056124 44171264 10113 4294967295 134512640 134672761 3221224560 3221223712 134565212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10113 603 41 0 10743 0
vsize: 43136
[startup+1099.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5483
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 109978 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5483
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 110973 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1119.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5483
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 111974 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1129.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5483
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 112974 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1139.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5483
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 113974 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1149.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5485
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 114974 37 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1159.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5485
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 115973 38 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1169.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5487
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 116973 38 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1179.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5487
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 117973 38 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223648 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1189.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5487
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 118973 38 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
[startup+1199.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 5487
Raw data (stat): 5430 (minisat+) R 5429 30927 30926 0 -1 0 10136 0 0 0 119973 38 0 0 25 0 1 0 359056124 44171264 10114 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10784 10114 603 41 0 10743 0
vsize: 43136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 5487
Raw data (stat): 5430 (minisat+) Z 5429 30927 30926 0 -1 12 10139 0 0 0 119973 40 0 0 25 0 1 0 359056124 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.14
CPU user time (s): 1199.74
CPU system time (s): 0.406938
CPU usage (%): 100.01
Max. virtual memory (Kb): 43136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####