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-5.opb
MD5SUM	38d41fdbe49543e8928c5210e4323f00
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	760
Total number of constraints	41619
Number of constraints which are clauses	41619
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 5996

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        891712 kB
Buffers:         36268 kB
Cached:          86316 kB
SwapCached:        564 kB
Active:          54876 kB
Inactive:        71112 kB
HighTotal:      131008 kB
HighFree:        40768 kB
LowTotal:       903652 kB
LowFree:        850944 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11436 kB
Committed_AS:    63508 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:11:45 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4464 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41619 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 |   41619    83238 |   13873       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -27[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 |   77738   168085 |   25912       0        0     nan |  0.000 % |
c |       100 |   77393   167370 |   28503      74      614     8.3 |  0.753 % |
c |       250 |   76571   165604 |   31353     182     1860    10.2 |  2.662 % |
c |       475 |   75416   163089 |   34488     361     3656    10.1 |  5.412 % |
c |       812 |   73469   158808 |   37937     588     7576    12.9 | 10.134 % |
c |      1318 |   71470   154363 |   41731     995    12456    12.5 | 15.052 % |
c |      2077 |   68055   146635 |   45904    1571    21571    13.7 | 23.713 % |
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 |      2368 |   66345   142775 |   22115    1722    23486    13.6 | 23.713 % |
c |      2468 |   65954   141886 |   24326    1798    24101    13.4 | 29.188 % |
c |      2618 |   65428   140687 |   26759    1916    26017    13.6 | 30.521 % |
c |      2843 |   64784   139204 |   29435    2104    29300    13.9 | 32.202 % |
c |      3180 |   63783   136936 |   32378    2343    33178    14.2 | 34.720 % |
c |      3686 |   62671   134380 |   35616    2764    38470    13.9 | 37.600 % |
c |      4445 |   60688   129777 |   39178    3385    46444    13.7 | 42.715 % |
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 |      4942 |   59952   128172 |   19984    3811    62121    16.3 | 42.715 % |
c |      5042 |   59679   127517 |   21982    3894    63964    16.4 | 45.623 % |
c |      5192 |   59303   126633 |   24180    4014    65656    16.4 | 46.620 % |
c |      5417 |   58170   123919 |   26598    4092    67984    16.6 | 49.720 % |
c |      5755 |   57394   122041 |   29258    4355    72331    16.6 | 51.880 % |
c |      6261 |   56683   120374 |   32184    4714    77744    16.5 | 53.783 % |
c |      7020 |   54571   115370 |   35402    5132    87529    17.1 | 59.526 % |
c |      8159 |   53100   111874 |   38943    6005   106837    17.8 | 63.555 % |
c |      9867 |   51361   107721 |   42837    7233   142892    19.8 | 68.277 % |
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 |     11787 |   49479   103125 |   16493    8440   181552    21.5 | 68.277 % |
c |     11887 |   49297   102693 |   18142    8475   182904    21.6 | 74.014 % |
c |     12037 |   49131   102301 |   19956    8543   185298    21.7 | 74.456 % |
c |     12262 |   49025   102033 |   21952    8701   189426    21.8 | 74.770 % |
c |     12602 |   48860   101631 |   24147    8952   197477    22.1 | 75.240 % |
c |     13108 |   48811   101518 |   26562    9438   225449    23.9 | 75.369 % |
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 |     13835 |   48637   101137 |   16212   10042   261315    26.0 | 75.369 % |
c |     13935 |   48570   100975 |   17833   10127   264156    26.1 | 76.055 % |
c |     14085 |   48570   100975 |   19616   10277   269303    26.2 | 76.055 % |
c |     14312 |   48535   100890 |   21578   10475   276829    26.4 | 76.156 % |
c |     14649 |   48224   100143 |   23735   10596   283579    26.8 | 77.024 % |
c |     15155 |   47936    99449 |   26109   10862   295418    27.2 | 77.815 % |
c |     15915 |   47936    99449 |   28720   11622   352382    30.3 | 77.815 % |
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 |     16092 |   47809    99110 |   15936   11694   348286    29.8 | 77.815 % |
c |     16193 |   47809    99110 |   17529   11795   351047    29.8 | 78.162 % |
c |     16343 |   47809    99110 |   19282   11945   358187    30.0 | 78.162 % |
c |     16568 |   47699    98850 |   21210   12069   366809    30.4 | 78.463 % |
c |     16907 |   47699    98850 |   23331   12408   381170    30.7 | 78.463 % |
c |     17413 |   47691    98830 |   25665   12893   410134    31.8 | 78.487 % |
c |     18172 |   47570    98547 |   28231   13507   456879    33.8 | 78.813 % |
c |     19312 |   47514    98418 |   31054   14523   514679    35.4 | 78.957 % |
c |     21020 |   47429    98213 |   34160   16152   617687    38.2 | 79.194 % |
c |     23582 |   47246    97781 |   37576   18577   833388    44.9 | 79.692 % |
c |     27427 |   47199    97655 |   41333   22352  1265776    56.6 | 79.845 % |
c |     33193 |   47092    97395 |   45467   28078  1866446    66.5 | 80.150 % |
c |     41842 |   46935    97003 |   50013   36506  2578978    70.6 | 80.608 % |
c |     54816 |   46775    96601 |   55015   49208  3834743    77.9 | 81.078 % |
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 |     66599 |   46701    96441 |   15567   60446  4917752    81.4 | 81.078 % |
c |     66699 |   46701    96441 |   17123   18649  1166349    62.5 | 81.358 % |
c |     66849 |   46701    96441 |   18836   18799  1175990    62.6 | 81.358 % |
c |     67075 |   46701    96441 |   20719   19025  1183368    62.2 | 81.358 % |
c |     67412 |   46698    96434 |   22791   19361  1203497    62.2 | 81.366 % |
c |     67920 |   46667    96361 |   25070   19848  1238599    62.4 | 81.450 % |
c |     68680 |   46645    96307 |   27577   20600  1270078    61.7 | 81.514 % |
c |     69819 |   46584    96158 |   30335   21676  1347252    62.2 | 81.690 % |
c |     71527 |   46518    95998 |   33369   23343  1512076    64.8 | 81.874 % |
c |     74089 |   46518    95998 |   36706   25905  1789120    69.1 | 81.874 % |
c |     77933 |   46488    95928 |   40376   29711  2161793    72.8 | 81.954 % |
c |     83701 |   46272    95398 |   44414   35390  2699227    76.3 | 82.566 % |
c |     92350 |   46247    95337 |   48855   43978  3619619    82.3 | 82.639 % |
c |    105326 |   46247    95337 |   53741   56954  5420125    95.2 | 82.638 % |
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 |    109573 |   46236    95289 |   15412   61020  6058538    99.3 | 82.638 % |
c |    109673 |   46236    95289 |   16953   17964  1912579   106.5 | 82.676 % |
c |    109824 |   46236    95289 |   18648   18115  1920817   106.0 | 82.676 % |
c |    110050 |   46236    95289 |   20513   18341  1933595   105.4 | 82.676 % |
c |    110387 |   46221    95254 |   22564   18674  1951460   104.5 | 82.716 % |
c |    110894 |   46221    95254 |   24821   19181  1987235   103.6 | 82.716 % |
c |    111653 |   46221    95254 |   27303   19940  2051460   102.9 | 82.716 % |
c |    112792 |   46174    95141 |   30033   21056  2143668   101.8 | 82.844 % |
c |    114503 |   46174    95141 |   33036   22767  2317315   101.8 | 82.844 % |
c |    117066 |   46174    95141 |   36340   25330  2565419   101.3 | 82.844 % |
c |    120910 |   46140    95059 |   39974   29170  2926517   100.3 | 82.940 % |
c |    126676 |   46140    95059 |   43972   34936  3469893    99.3 | 82.940 % |
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 |    128815 |   46161    95117 |   15387   37075  3702991    99.9 | 82.940 % |
c |    128916 |   46161    95117 |   16925   17069  1143112    67.0 | 82.903 % |
c |    129066 |   46161    95117 |   18618   17219  1153278    67.0 | 82.903 % |
c |    129293 |   46161    95117 |   20480   17446  1162668    66.6 | 82.903 % |
c |    129630 |   46126    95028 |   22528   17771  1187614    66.8 | 83.011 % |
c |    130137 |   46126    95028 |   24780   18278  1223931    67.0 | 83.011 % |
c |    130896 |   46051    94848 |   27259   19008  1237330    65.1 | 83.219 % |
c |    132035 |   46015    94758 |   29984   20133  1322301    65.7 | 83.315 % |
c |    133744 |   46015    94758 |   32983   21842  1465933    67.1 | 83.315 % |
c |    136307 |   46015    94758 |   36281   24405  1721914    70.6 | 83.315 % |
c |    140151 |   46015    94758 |   39909   28249  2009666    71.1 | 83.315 % |
c |    145918 |   46013    94754 |   43900   34014  2543986    74.8 | 83.319 % |
c |    154568 |   45959    94626 |   48290   42576  3184772    74.8 | 83.467 % |
c |    167543 |   45913    94520 |   53120   55540  4225297    76.1 | 83.587 % |
c |    187005 |   45913    94520 |   58432   75002  6244640    83.3 | 83.587 % |
c |    216198 |   45876    94429 |   64275   44973  3102677    69.0 | 83.694 % |
c |    259987 |   45876    94429 |   70702   22219  1193746    53.7 | 83.694 % |
c |    325671 |   45838    94339 |   77773   87896  5215189    59.3 | 83.798 % |
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 |    362744 |   45824    94273 |   15274   45452  1802921    39.7 | 83.798 % |
c |    362845 |   45824    94273 |   16801   20765   632823    30.5 | 83.844 % |
c |    362996 |   45824    94273 |   18481   20916   640662    30.6 | 83.844 % |
c |    363222 |   45824    94273 |   20329   21142   649300    30.7 | 83.844 % |
c |    363560 |   45824    94273 |   22362   21480   662066    30.8 | 83.844 % |
c |    364066 |   45824    94273 |   24598   21986   685062    31.2 | 83.844 % |
c |    364826 |   45824    94273 |   27058   22746   727210    32.0 | 83.844 % |
c |    365965 |   45824    94273 |   29764   23885   810735    33.9 | 83.844 % |
c |    367674 |   45824    94273 |   32741   25594   906072    35.4 | 83.844 % |
c |    370236 |   45824    94273 |   36015   28156  1054352    37.4 | 83.844 % |
c |    374082 |   45737    94058 |   39616   31979  1334937    41.7 | 84.083 % |
c |    379848 |   45698    93956 |   43578   37273  1691710    45.4 | 84.203 % |
c |    388498 |   45694    93948 |   47936   45919  2503857    54.5 | 84.211 % |
c |    401472 |   45694    93948 |   52729   58893  3447993    58.5 | 84.211 % |
c |    420934 |   45643    93821 |   58002   23036   699613    30.4 | 84.363 % |
c |    450126 |   45640    93814 |   63803   52227  1837279    35.2 | 84.371 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 C572 -C571 C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 C476 -C475 -C474 -C473 C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 C271 -C270 -C269 -C268 -C267 -C266 C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 3287
Raw data (stat): 3287 (runsolver) R 3286 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422910801 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 2835 0 0 0 992 6 0 0 25 0 1 0 422910801 14049280 2813 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2813 603 41 0 3389 0
vsize: 13720
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 2914 0 0 0 1992 6 0 0 25 0 1 0 422910801 14487552 2892 4294967295 134512640 134672761 3221224560 3221223732 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3537 2892 603 41 0 3496 0
vsize: 14148
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 2951 0 0 0 2991 7 0 0 25 0 1 0 422910801 14622720 2929 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3570 2929 603 41 0 3529 0
vsize: 14280
[startup+40.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 3156 0 0 0 3990 8 0 0 25 0 1 0 422910801 15646720 3134 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3134 603 41 0 3779 0
vsize: 15280
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 3723 0 0 0 4988 10 0 0 25 0 1 0 422910801 17977344 3701 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3701 603 41 0 4348 0
vsize: 17556
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 4462 0 0 0 5986 12 0 0 25 0 1 0 422910801 20930560 4440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5110 4440 603 41 0 5069 0
vsize: 20440
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 4984 0 0 0 6985 14 0 0 25 0 1 0 422910801 23056384 4962 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5629 4962 603 41 0 5588 0
vsize: 22516
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 5524 0 0 0 7983 15 0 0 25 0 1 0 422910801 25321472 5502 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6215 5503 603 41 0 6174 0
vsize: 24728
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 6052 0 0 0 8982 17 0 0 25 0 1 0 422910801 27594752 6030 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6737 6030 603 41 0 6696 0
vsize: 26948
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 6476 0 0 0 9980 18 0 0 25 0 1 0 422910801 29192192 6454 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7127 6454 603 41 0 7086 0
vsize: 28508
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 6960 0 0 0 10979 19 0 0 25 0 1 0 422910801 31199232 6938 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7617 6938 603 41 0 7576 0
vsize: 30468
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 7345 0 0 0 11978 21 0 0 25 0 1 0 422910801 32808960 7323 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8010 7323 603 41 0 7969 0
vsize: 32040
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 7731 0 0 0 12976 22 0 0 25 0 1 0 422910801 34402304 7709 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8399 7709 603 41 0 8358 0
vsize: 33596
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8023 0 0 0 13975 24 0 0 25 0 1 0 422910801 35459072 8001 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8657 8001 603 41 0 8616 0
vsize: 34628
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 14975 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 15975 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 16975 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 17975 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 18976 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 19976 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 20976 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8292 0 0 0 21976 24 0 0 25 0 1 0 422910801 36626432 8270 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8942 8270 603 41 0 8901 0
vsize: 35768
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8532 0 0 0 22975 25 0 0 25 0 1 0 422910801 37564416 8510 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9171 8510 603 41 0 9130 0
vsize: 36684
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 8997 0 0 0 23974 27 0 0 25 0 1 0 422910801 39555072 8975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9657 8975 603 41 0 9616 0
vsize: 38628
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9494 0 0 0 24972 29 0 0 25 0 1 0 422910801 41553920 9472 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10145 9472 603 41 0 10104 0
vsize: 40580
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 25972 29 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 26972 29 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 27972 29 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 28972 29 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 29972 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 30972 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 31973 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 32973 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 33973 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 34973 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 35973 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 36974 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9601 0 0 0 37974 30 0 0 25 0 1 0 422910801 41955328 9579 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9579 603 41 0 10202 0
vsize: 40972
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9602 0 0 0 38974 30 0 0 25 0 1 0 422910801 41955328 9580 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9580 603 41 0 10202 0
vsize: 40972
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9605 0 0 0 39974 30 0 0 25 0 1 0 422910801 41955328 9583 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10243 9583 603 41 0 10202 0
vsize: 40972
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9608 0 0 0 40974 30 0 0 25 0 1 0 422910801 42217472 9586 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10307 9586 603 41 0 10266 0
vsize: 41228
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9610 0 0 0 41974 30 0 0 25 0 1 0 422910801 42217472 9588 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10307 9588 603 41 0 10266 0
vsize: 41228
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 9833 0 0 0 42974 31 0 0 25 0 1 0 422910801 43147264 9811 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10534 9811 603 41 0 10493 0
vsize: 42136
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10121 0 0 0 43973 32 0 0 25 0 1 0 422910801 44351488 10099 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10828 10099 603 41 0 10787 0
vsize: 43312
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10343 0 0 0 44972 32 0 0 25 0 1 0 422910801 45285376 10321 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10321 603 41 0 11015 0
vsize: 44224
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 45972 32 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 46973 32 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 47973 32 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223744 134559463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 48973 32 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3287
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 49973 32 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+510.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 50971 34 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+520.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 51971 34 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+530.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 52971 34 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+540.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 53971 34 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+550.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 54970 35 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+560.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 55970 35 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+570.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3340
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 56969 36 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+580.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 57969 37 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+590.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 58969 37 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134559644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+600.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 59969 37 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+610.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10358 0 0 0 60969 37 0 0 25 0 1 0 422910801 45285376 10336 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10336 603 41 0 11015 0
vsize: 44224
[startup+620.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10359 0 0 0 61969 37 0 0 25 0 1 0 422910801 45285376 10337 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10337 603 41 0 11015 0
vsize: 44224
[startup+630.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10367 0 0 0 62969 38 0 0 25 0 1 0 422910801 45285376 10345 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10345 603 41 0 11015 0
vsize: 44224
[startup+640.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10371 0 0 0 63969 38 0 0 25 0 1 0 422910801 45285376 10349 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10349 603 41 0 11015 0
vsize: 44224
[startup+650.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 64969 38 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+660.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 65968 39 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+670.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 66968 39 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+680.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 67968 39 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+690.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 68968 40 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+700.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 69968 40 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+710.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 70968 40 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+720.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 71967 41 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+730.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 72967 41 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 73968 41 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 74967 41 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 75967 42 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+770.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 76967 42 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+780.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 77967 42 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 78966 43 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+800.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 79966 43 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+810.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 80966 44 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+820.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3342
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10373 0 0 0 81966 44 0 0 25 0 1 0 422910801 45285376 10351 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11056 10351 603 41 0 11015 0
vsize: 44224
[startup+830.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10382 0 0 0 82965 45 0 0 25 0 1 0 422910801 45449216 10360 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10360 603 41 0 11055 0
vsize: 44384
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10393 0 0 0 83965 46 0 0 25 0 1 0 422910801 45449216 10371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10371 603 41 0 11055 0
vsize: 44384
[startup+850.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10395 0 0 0 84964 46 0 0 25 0 1 0 422910801 45449216 10373 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10373 603 41 0 11055 0
vsize: 44384
[startup+860.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10399 0 0 0 85964 46 0 0 25 0 1 0 422910801 45449216 10377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10377 603 41 0 11055 0
vsize: 44384
[startup+870.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10402 0 0 0 86964 47 0 0 25 0 1 0 422910801 45449216 10380 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10380 603 41 0 11055 0
vsize: 44384
[startup+880.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10404 0 0 0 87964 47 0 0 25 0 1 0 422910801 45449216 10382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10382 603 41 0 11055 0
vsize: 44384
[startup+890.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 88964 47 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 89964 48 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+910.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 90964 48 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+920.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 91963 48 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+930.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 92963 49 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+940.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 93963 49 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+950.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 94963 49 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+960.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 95963 50 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+970.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 96962 50 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 97962 51 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+990.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 98962 51 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 99962 51 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 100962 51 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 101962 51 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 102962 52 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 103962 52 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 104962 52 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 105962 52 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 106962 53 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 107961 53 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 108961 54 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 109961 54 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 110961 54 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 111961 55 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 112960 55 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 113960 56 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 114960 56 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 115960 56 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 116959 57 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 117959 57 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 118959 58 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3344
Raw data (stat): 3287 (minisat+) R 3286 30854 30853 0 -1 0 10405 0 0 0 119959 58 0 0 25 0 1 0 422910801 45449216 10383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10383 603 41 0 11055 0
vsize: 44384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3344
Raw data (stat): 3287 (minisat+) Z 3286 30854 30853 0 -1 12 10408 0 0 0 119959 60 0 0 25 0 1 0 422910801 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.05
CPU time (s): 1200.2
CPU user time (s): 1199.59
CPU system time (s): 0.603908
CPU usage (%): 100.013
Max. virtual memory (Kb): 44384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####