PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        889260 kB
Buffers:         33796 kB
Cached:          77600 kB
SwapCached:         56 kB
Active:          48008 kB
Inactive:        66420 kB
HighTotal:      131008 kB
HighFree:        49336 kB
LowTotal:       903652 kB
LowFree:        839924 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25400 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:12:49 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3709 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41263 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41263    82526 |   13754       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1492   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51462   119000 |   17154       0        0     nan |  0.000 % |
c |       100 |   51444   118938 |   18869      93     1062    11.4 |  0.272 % |
c |       250 |   51420   118856 |   20756     239     2977    12.5 |  0.403 % |
c |       475 |   51411   118825 |   22831     459     4898    10.7 |  0.451 % |
c |       812 |   51393   118763 |   25115     792     8424    10.6 |  0.539 % |
c |      1319 |   51375   118701 |   27626    1295    18334    14.2 |  0.627 % |
c |      2078 |   51228   118196 |   30389    2007    28362    14.1 |  1.388 % |
c |      3217 |   51072   117662 |   33428    3106    50265    16.2 |  2.332 % |
c |      4925 |   50658   116240 |   36771    4699    85389    18.2 |  4.655 % |
c |      7487 |   49938   113766 |   40448    7063   162345    23.0 |  9.714 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8800 |   49829   113391 |   16609    8331   210542    25.3 |  9.714 % |
c |      8900 |   49810   113324 |   18269    8425   212568    25.2 | 10.648 % |
c |      9050 |   49769   113183 |   20096    8561   218905    25.6 | 10.915 % |
c |      9276 |   49760   113152 |   22106    8783   223979    25.5 | 10.957 % |
c |      9614 |   49691   112911 |   24317    9096   235218    25.9 | 11.404 % |
c |     10120 |   49508   112284 |   26748    9549   251735    26.4 | 12.839 % |
c |     10879 |   49416   111968 |   29423   10238   282956    27.6 | 13.462 % |
c |     12018 |   49289   111531 |   32366   11354   382731    33.7 | 14.535 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12311 |   49275   111475 |   16425   11598   392603    33.9 | 14.535 % |
c |     12411 |   49275   111475 |   18067   11698   396124    33.9 | 14.624 % |
c |     12561 |   49161   111079 |   19874   11815   399173    33.8 | 15.478 % |
c |     12787 |   49103   110879 |   21861   12025   407137    33.9 | 15.877 % |
c |     13124 |   49065   110747 |   24047   12354   430009    34.8 | 16.193 % |
c |     13630 |   49001   110529 |   26452   12849   450979    35.1 | 16.730 % |
c |     14391 |   48936   110304 |   29097   13541   491971    36.3 | 17.174 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15287 |   48996   110499 |   16332   14413   535204    37.1 | 17.174 % |
c |     15388 |   48814   109861 |   17965   14441   537298    37.2 | 19.505 % |
c |     15538 |   48814   109861 |   19761   14591   541118    37.1 | 19.505 % |
c |     15763 |   48803   109822 |   21737   14812   554821    37.5 | 19.593 % |
c |     16100 |   48757   109664 |   23911   15132   566224    37.4 | 19.947 % |
c |     16606 |   48715   109518 |   26302   15627   600281    38.4 | 20.301 % |
c |     17366 |   48663   109340 |   28933   16372   636277    38.9 | 20.699 % |
c |     18505 |   48663   109340 |   31826   17511   733910    41.9 | 20.699 % |
c |     20213 |   48617   109180 |   35009   19170   810956    42.3 | 21.012 % |
c |     22777 |   48341   108222 |   38510   21478   971297    45.2 | 23.087 % |
c |     26621 |   48252   107917 |   42361   25120  1250723    49.8 | 23.618 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29487 |   48236   107865 |   16078   27953  1455778    52.1 | 23.618 % |
c |     29589 |   48236   107865 |   17685   14079   720500    51.2 | 23.789 % |
c |     29739 |   48114   107441 |   19454   14181   723219    51.0 | 24.713 % |
c |     29964 |   48114   107441 |   21399   14406   737235    51.2 | 24.713 % |
c |     30304 |   48114   107441 |   23539   14746   750694    50.9 | 24.713 % |
c |     30813 |   48096   107379 |   25893   15224   772005    50.7 | 24.801 % |
c |     31572 |   48096   107379 |   28483   15983   841758    52.7 | 24.804 % |
c |     32711 |   48069   107286 |   31331   17062   900385    52.8 | 24.934 % |
c |     34419 |   47906   106729 |   34464   18696   974951    52.1 | 26.174 % |
c |     36981 |   47871   106612 |   37911   21201  1212734    57.2 | 26.440 % |
c |     40826 |   47854   106553 |   41702   25020  1603365    64.1 | 26.570 % |
c |     46592 |   47782   106305 |   45872   30680  2135900    69.6 | 27.104 % |
c |     55241 |   47752   106197 |   50459   39218  2619885    66.8 | 27.321 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61585 |   47744   106174 |   15914   45530  3019657    66.3 | 27.321 % |
c |     61686 |   47744   106174 |   17505   16541   706061    42.7 | 27.400 % |
c |     61838 |   47744   106174 |   19255   16693   712475    42.7 | 27.397 % |
c |     62063 |   47744   106174 |   21181   16918   722438    42.7 | 27.397 % |
c |     62403 |   47744   106174 |   23299   17258   745160    43.2 | 27.397 % |
c |     62909 |   47744   106174 |   25629   17764   768871    43.3 | 27.397 % |
c |     63669 |   47708   106050 |   28192   18401   819231    44.5 | 27.666 % |
c |     64808 |   47708   106050 |   31011   19540   869996    44.5 | 27.662 % |
c |     66516 |   47688   105980 |   34113   21233   956872    45.1 | 27.795 % |
c |     69078 |   47688   105980 |   37524   23795  1185109    49.8 | 27.798 % |
c |     72923 |   47662   105890 |   41276   27602  1425868    51.7 | 27.972 % |
c |     78689 |   47628   105772 |   45404   33324  1816593    54.5 | 28.237 % |
c |     87339 |   47628   105772 |   49944   41974  2850892    67.9 | 28.240 % |
c |    100313 |   47628   105772 |   54939   19797  1533511    77.5 | 28.237 % |
c |    119774 |   47628   105772 |   60433   39258  3462744    88.2 | 28.237 % |
c |    148967 |   47628   105772 |   66476   22622  2305939   101.9 | 28.237 % |
c |    192756 |   47628   105772 |   73124   66411 10256948   154.4 | 28.241 % |
c |    258440 |   47591   105645 |   80436   74005 10680067   144.3 | 28.546 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    264901 |   47592   105651 |   15864   80466 11406747   141.8 | 28.546 % |
c |    265001 |   47584   105623 |   17450    8459   687255    81.2 | 28.666 % |
c |    265151 |   47578   105603 |   19195    8605   690137    80.2 | 28.710 % |
c |    265376 |   47578   105603 |   21114    8830   699542    79.2 | 28.710 % |
c |    265714 |   47567   105564 |   23226    9167   713018    77.8 | 28.799 % |
c |    266221 |   47567   105564 |   25549    9674   739498    76.4 | 28.799 % |
c |    266982 |   47556   105525 |   28104   10431   779559    74.7 | 28.887 % |
c |    268123 |   47556   105525 |   30914   11572   847333    73.2 | 28.887 % |
c |    269831 |   47516   105395 |   34005   13264   922473    69.5 | 29.240 % |
c |    272396 |   47508   105367 |   37406   15825  1068182    67.5 | 29.329 % |
c |    276240 |   47508   105367 |   41147   19669  1413834    71.9 | 29.332 % |
c |    282006 |   47491   105308 |   45261   25427  1749870    68.8 | 29.461 % |
c |    290655 |   47491   105308 |   49788   34076  2382875    69.9 | 29.465 % |
c |    303629 |   47491   105308 |   54766   47050  3753523    79.8 | 29.461 % |
c |    323092 |   47491   105308 |   60243   26529  2004722    75.6 | 29.463 % |
c |    352286 |   47491   105308 |   66267   55723  5093306    91.4 | 29.461 % |
c |    396075 |   47491   105308 |   72894   48174  3360285    69.8 | 29.463 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    412900 |   47492   105316 |   15830   64999  5330218    82.0 | 29.463 % |
c |    413002 |   47492   105316 |   17413   15524  1593450   102.6 | 29.495 % |
c |    413153 |   47492   105316 |   19154   15675  1595616   101.8 | 29.492 % |
c |    413380 |   47492   105316 |   21069   15902  1609003   101.2 | 29.492 % |
c |    413717 |   47492   105316 |   23176   16239  1622109    99.9 | 29.492 % |
c |    414223 |   47492   105316 |   25494   16745  1650980    98.6 | 29.496 % |
c |    414986 |   47492   105316 |   28043   17508  1683353    96.1 | 29.492 % |
c |    416125 |   47492   105316 |   30848   18647  1736087    93.1 | 29.492 % |
c |    417833 |   47492   105316 |   33933   20355  1826250    89.7 | 29.492 % |
c |    420395 |   47492   105316 |   37326   22917  2027496    88.5 | 29.496 % |
c |    424239 |   47471   105241 |   41058   26756  2309064    86.3 | 29.717 % |
c |    430006 |   47471   105241 |   45164   32523  3057529    94.0 | 29.717 % |
c |    438658 |   47471   105241 |   49681   41175  3846739    93.4 | 29.713 % |
c |    451633 |   47458   105194 |   54649   18950  1073008    56.6 | 29.848 % |
c |    471094 |   47458   105194 |   60114   38411  3937921   102.5 | 29.845 % |
c |    500286 |   47435   105115 |   66125   22867   741391    32.4 | 30.026 % |
c |    544075 |   47435   105115 |   72738   66656  3370743    50.6 | 30.026 % |
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 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/55 26737
Raw data (stat): 26737 (runsolver) R 26736 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479693440 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 2131 0 0 0 993 5 0 0 25 0 1 0 479693440 10371072 2109 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2532 2109 603 41 0 2491 0
vsize: 10128
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 2189 0 0 0 1992 6 0 0 25 0 1 0 479693440 10637312 2167 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2597 2167 603 41 0 2556 0
vsize: 10388
[startup+30.0024 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 2816 0 0 0 2988 9 0 0 25 0 1 0 479693440 13180928 2794 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3218 2794 603 41 0 3177 0
vsize: 12872
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 2963 0 0 0 3988 10 0 0 25 0 1 0 479693440 13717504 2941 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3349 2941 603 41 0 3308 0
vsize: 13396
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 3711 0 0 0 4987 11 0 0 25 0 1 0 479693440 16797696 3689 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4101 3689 603 41 0 4060 0
vsize: 16404
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4110 0 0 0 5985 12 0 0 25 0 1 0 479693440 18526208 4088 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4523 4088 603 41 0 4482 0
vsize: 18092
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4515 0 0 0 6984 14 0 0 25 0 1 0 479693440 20262912 4493 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4947 4493 603 41 0 4906 0
vsize: 19788
[startup+80.006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4588 0 0 0 7983 15 0 0 25 0 1 0 479693440 20533248 4566 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4566 603 41 0 4972 0
vsize: 20052
[startup+90.0064 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4589 0 0 0 8983 15 0 0 25 0 1 0 479693440 20533248 4567 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4567 603 41 0 4972 0
vsize: 20052
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4589 0 0 0 9983 15 0 0 25 0 1 0 479693440 20533248 4567 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4567 603 41 0 4972 0
vsize: 20052
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 4769 0 0 0 10982 16 0 0 25 0 1 0 479693440 21196800 4747 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5175 4747 603 41 0 5134 0
vsize: 20700
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5362 0 0 0 11980 18 0 0 25 0 1 0 479693440 23728128 5340 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5793 5340 603 41 0 5752 0
vsize: 23172
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5447 0 0 0 12980 19 0 0 25 0 1 0 479693440 23998464 5425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5859 5425 603 41 0 5818 0
vsize: 23436
[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5447 0 0 0 13980 19 0 0 25 0 1 0 479693440 23998464 5425 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5859 5425 603 41 0 5818 0
vsize: 23436
[startup+150.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5447 0 0 0 14979 19 0 0 25 0 1 0 479693440 23998464 5425 4294967295 134512640 134672761 3221224560 3221223744 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5859 5425 603 41 0 5818 0
vsize: 23436
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5447 0 0 0 15979 19 0 0 25 0 1 0 479693440 23998464 5425 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5859 5425 603 41 0 5818 0
vsize: 23436
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 5946 0 0 0 16978 21 0 0 25 0 1 0 479693440 26001408 5924 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5924 603 41 0 6307 0
vsize: 25392
[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 6435 0 0 0 17976 23 0 0 25 0 1 0 479693440 28135424 6413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 6413 603 41 0 6828 0
vsize: 27476
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 6915 0 0 0 18974 25 0 0 25 0 1 0 479693440 30003200 6893 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7325 6893 603 41 0 7284 0
vsize: 29300
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26737
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7342 0 0 0 19973 26 0 0 25 0 1 0 479693440 31748096 7320 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7751 7320 603 41 0 7710 0
vsize: 31004
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 20970 29 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 21969 30 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+230.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 22970 30 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+240.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 23970 30 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+250.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 24969 30 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 7915 0 0 0 25969 31 0 0 25 0 1 0 479693440 34152448 7893 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8338 7893 603 41 0 8297 0
vsize: 33352
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 8013 0 0 0 26969 31 0 0 25 0 1 0 479693440 34553856 7991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8436 7991 603 41 0 8395 0
vsize: 33744
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 8550 0 0 0 27967 33 0 0 25 0 1 0 479693440 36700160 8528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8960 8528 603 41 0 8919 0
vsize: 35840
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 9134 0 0 0 28966 35 0 0 25 0 1 0 479693440 39116800 9112 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9550 9112 603 41 0 9509 0
vsize: 38200
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 9692 0 0 0 29964 37 0 0 25 0 1 0 479693440 41406464 9670 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10109 9670 603 41 0 10068 0
vsize: 40436
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 10264 0 0 0 30962 39 0 0 25 0 1 0 479693440 43700224 10242 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10669 10242 603 41 0 10628 0
vsize: 42676
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 10794 0 0 0 31961 40 0 0 25 0 1 0 479693440 45993984 10772 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11229 10772 603 41 0 11188 0
vsize: 44916
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 11320 0 0 0 32960 41 0 0 25 0 1 0 479693440 48152576 11298 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11756 11298 603 41 0 11715 0
vsize: 47024
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 11825 0 0 0 33959 43 0 0 25 0 1 0 479693440 50184192 11803 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11803 603 41 0 12211 0
vsize: 49008
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 12257 0 0 0 34958 44 0 0 25 0 1 0 479693440 52256768 12235 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12758 12235 603 41 0 12717 0
vsize: 51032
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 12697 0 0 0 35955 46 0 0 25 0 1 0 479693440 54140928 12675 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13218 12675 603 41 0 13177 0
vsize: 52872
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13136 0 0 0 36953 48 0 0 25 0 1 0 479693440 55885824 13114 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13644 13114 603 41 0 13603 0
vsize: 54576
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13530 0 0 0 37953 48 0 0 25 0 1 0 479693440 57507840 13508 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13508 603 41 0 13999 0
vsize: 56160
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13530 0 0 0 38953 48 0 0 25 0 1 0 479693440 57507840 13508 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13508 603 41 0 13999 0
vsize: 56160
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13530 0 0 0 39953 48 0 0 25 0 1 0 479693440 57507840 13508 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13508 603 41 0 13999 0
vsize: 56160
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13531 0 0 0 40953 49 0 0 25 0 1 0 479693440 57507840 13509 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13509 603 41 0 13999 0
vsize: 56160
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13531 0 0 0 41953 49 0 0 25 0 1 0 479693440 57507840 13509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13509 603 41 0 13999 0
vsize: 56160
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26739
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 42953 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 26776
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 43954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+450.024 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 44954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+460.024 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 45954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+470.024 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 46954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+480.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 47954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+490.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 48954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+500.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26792
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 49954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+510.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 50954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+520.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 51954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+530.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 52954 49 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+540.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13532 0 0 0 53954 50 0 0 25 0 1 0 479693440 57507840 13510 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14040 13510 603 41 0 13999 0
vsize: 56160
[startup+550.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13535 0 0 0 54954 50 0 0 25 0 1 0 479693440 57507840 13513 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13513 603 41 0 13999 0
vsize: 56160
[startup+560.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 55954 50 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+570.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 56954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+580.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 57954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+590.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 58954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+600.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 59954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+610.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 60954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+620.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 61954 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+630.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 62955 51 0 0 25 0 1 0 479693440 58429440 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14265 13745 603 41 0 14224 0
vsize: 57060
[startup+640.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 63955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+650.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 64955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+660.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 65955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+670.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 66955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+680.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 67955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+690.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 68955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+700.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 69955 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+710.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 70956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+720.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 71956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+730.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 72956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+740.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26796
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 73956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+750.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 74956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+760.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 75956 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+770.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 76957 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+780.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 77957 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 78957 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+800.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26798
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 79957 51 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+810.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 80956 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+820.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 81956 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 82956 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+840.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 83956 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+850.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 84957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 85957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+870.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 86957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 87957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+890.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 88957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+900.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 89957 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+910.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 90958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+920.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 91958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+930.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 92958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+940.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 93958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+950.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 94958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+960.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 95958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+970.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 96958 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+980.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 97959 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+990.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 98959 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 99959 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 100959 52 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 101958 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 102958 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 103958 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 104959 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 105959 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13767 0 0 0 106959 53 0 0 25 0 1 0 479693440 58425344 13745 4294967295 134512640 134672761 3221224560 3221223804 134558191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13745 603 41 0 14223 0
vsize: 57056
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 107959 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 108959 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26800
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 109959 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 110960 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 111960 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 112960 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 113960 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 114960 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13768 0 0 0 115961 53 0 0 25 0 1 0 479693440 58425344 13746 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13746 603 41 0 14223 0
vsize: 57056
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13769 0 0 0 116961 53 0 0 25 0 1 0 479693440 58425344 13747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13747 603 41 0 14223 0
vsize: 57056
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13769 0 0 0 117961 53 0 0 25 0 1 0 479693440 58425344 13747 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13747 603 41 0 14223 0
vsize: 57056
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13769 0 0 0 118961 53 0 0 25 0 1 0 479693440 58425344 13747 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13747 603 41 0 14223 0
vsize: 57056
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26802
Raw data (stat): 26737 (minisat+) R 26736 22929 22928 0 -1 0 13769 0 0 0 119961 53 0 0 25 0 1 0 479693440 58425344 13747 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14264 13747 603 41 0 14223 0
vsize: 57056
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 26802
Raw data (stat): 26737 (minisat+) Z 26736 22929 22928 0 -1 12 13772 0 0 0 119961 56 0 0 25 0 1 0 479693440 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.18
CPU user time (s): 1199.62
CPU system time (s): 0.563914
CPU usage (%): 100.009
Max. virtual memory (Kb): 57060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####