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/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 20769

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 21:47:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14492 boxname=wulflinc24 idbench=1115 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 14492
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        640200 kB
Buffers:         32532 kB
Cached:         337952 kB
SwapCached:        524 kB
Active:         160500 kB
Inactive:       212024 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        639948 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16360 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:07:24 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 14492 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  16]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 708   maxlim: 3756758   bits: 23/22
c ---[  10]---> Adder-cost: 758   maxlim: 4064912   bits: 23/22
c ---[   8]---> Adder-cost: 714   maxlim: 3859164   bits: 23/22
c ---[   6]---> Adder-cost: 676   maxlim: 4153021   bits: 23/22
c ---[   4]---> Adder-cost: 812   maxlim: 3812158   bits: 23/22
c ---[   2]---> Adder-cost: 766   maxlim: 4131466   bits: 23/22
c ---[   0]---> Adder-cost: 692   maxlim: 3780388   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35695   127215 |   11898       0        0     nan |  0.000 % |
c |       100 |   35695   127215 |   13087     100      303     3.0 |  7.565 % |
c |       250 |   35680   127170 |   14396     247     1013     4.1 |  7.617 % |
c |       476 |   35680   127170 |   15836     473     2194     4.6 |  7.617 % |
c |       814 |   35680   127170 |   17419     811     4306     5.3 |  7.617 % |
c |      1320 |   35680   127170 |   19161    1317    10551     8.0 |  7.617 % |
c ==============================================================================
c [1mFound solution: 3901833[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 252   maxlim: 10778224   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1577 |   37383   133343 |   12461    1574    13187     8.4 |  7.617 % |
c |      1679 |   37383   133343 |   13707    1676    14042     8.4 |  7.484 % |
c |      1829 |   37383   133343 |   15077    1826    16000     8.8 |  7.484 % |
c |      2054 |   37375   133317 |   16585    2050    26493    12.9 |  7.500 % |
c |      2391 |   37375   133317 |   18244    2387    32297    13.5 |  7.500 % |
c ==============================================================================
c [1mFound solution: 3732019[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10948038   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2478 |   37409   133571 |   12469    2474    32988    13.3 |  7.500 % |
c |      2578 |   37402   133548 |   13715    2573    34796    13.5 |  7.669 % |
c |      2729 |   37402   133548 |   15087    2724    36472    13.4 |  7.669 % |
c |      2954 |   37394   133522 |   16596    2948    39525    13.4 |  7.686 % |
c |      3293 |   37394   133522 |   18255    3287    56003    17.0 |  7.686 % |
c |      3799 |   37381   133480 |   20081    3791   129210    34.1 |  7.719 % |
c |      4558 |   37373   133454 |   22089    4549   170854    37.6 |  7.735 % |
c |      5697 |   37373   133454 |   24298    5688   219647    38.6 |  7.735 % |
c ==============================================================================
c [1mFound solution: 3582882[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11097175   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6372 |   37387   133582 |   12462    6363   351394    55.2 |  7.735 % |
c |      6473 |   37387   133582 |   13708    6464   359740    55.7 |  7.854 % |
c |      6624 |   37387   133582 |   15079    6615   362370    54.8 |  7.854 % |
c |      6851 |   37387   133582 |   16586    6842   364407    53.3 |  7.854 % |
c |      7189 |   37387   133582 |   18245    7180   401943    56.0 |  7.854 % |
c |      7695 |   37387   133582 |   20070    7686   417436    54.3 |  7.854 % |
c ==============================================================================
c [1mFound solution: 3255627[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11424430   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8018 |   37405   133780 |   12468    8009   432994    54.1 |  7.854 % |
c |      8118 |   37405   133780 |   13714    8109   434566    53.6 |  8.017 % |
c |      8269 |   37405   133780 |   15086    8260   453725    54.9 |  8.017 % |
c |      8494 |   37405   133780 |   16594    8485   463004    54.6 |  8.017 % |
c |      8831 |   37405   133780 |   18254    8822   468093    53.1 |  8.017 % |
c ==============================================================================
c [1mFound solution: 1943815[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12736242   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9027 |   37350   133257 |   12450    9016   470534    52.2 |  8.017 % |
c |      9127 |   37350   133257 |   13695    9116   476737    52.3 |  8.321 % |
c |      9277 |   37350   133257 |   15064    9266   479971    51.8 |  8.321 % |
c |      9502 |   37342   133231 |   16570    9490   486158    51.2 |  8.337 % |
c |      9839 |   37342   133231 |   18228    9827   509294    51.8 |  8.337 % |
c |     10345 |   37342   133231 |   20050   10333   521174    50.4 |  8.337 % |
c |     11104 |   37335   133208 |   22055   11090   601417    54.2 |  8.354 % |
c |     12243 |   37326   133179 |   24261   12228   659416    53.9 |  8.387 % |
c |     13951 |   37318   133153 |   26687   13935   716850    51.4 |  8.403 % |
c |     16513 |   37310   133127 |   29356   16496   798166    48.4 |  8.419 % |
c |     20359 |   37310   133127 |   32292   20342   985563    48.4 |  8.419 % |
c |     26125 |   37310   133127 |   35521   26108  1514056    58.0 |  8.419 % |
c |     34774 |   37302   133101 |   39073   34756  2091689    60.2 |  8.436 % |
c ==============================================================================
c [1mFound solution: 1675280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13004777   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34832 |   37323   133279 |   12441   34814  2096208    60.2 |  8.436 % |
c |     34936 |   37323   133279 |   13685    7695   326352    42.4 |  8.619 % |
c |     35086 |   37323   133279 |   15053    7845   332244    42.4 |  8.619 % |
c |     35311 |   37323   133279 |   16558    8070   337410    41.8 |  8.619 % |
c |     35648 |   37323   133279 |   18214    8407   347047    41.3 |  8.619 % |
c |     36155 |   37323   133279 |   20036    8914   365071    41.0 |  8.619 % |
c |     36916 |   37323   133279 |   22039    9675   386522    40.0 |  8.619 % |
c |     38055 |   37323   133279 |   24243   10814   438796    40.6 |  8.619 % |
c |     39763 |   37315   133253 |   26668   12521   487062    38.9 |  8.635 % |
c |     42325 |   37315   133253 |   29335   15083   569450    37.8 |  8.635 % |
c |     46170 |   37307   133227 |   32268   18927   779761    41.2 |  8.652 % |
c |     51936 |   37307   133227 |   35495   24693  1009667    40.9 |  8.652 % |
c ==============================================================================
c [1mFound solution: 1590016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13090041   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55469 |   37328   133412 |   12442   28226  1289980    45.7 |  8.652 % |
c |     55571 |   37328   133412 |   13686    7159   323324    45.2 |  8.823 % |
c |     55722 |   37328   133412 |   15054    7310   351942    48.1 |  8.823 % |
c |     55947 |   37328   133412 |   16560    7535   362477    48.1 |  8.823 % |
c |     56285 |   37328   133412 |   18216    7873   371761    47.2 |  8.823 % |
c |     56791 |   37328   133412 |   20037    8379   418445    49.9 |  8.823 % |
c |     57551 |   37328   133412 |   22041    9139   443203    48.5 |  8.823 % |
c |     58691 |   37328   133412 |   24245   10279   484142    47.1 |  8.823 % |
c |     60401 |   37328   133412 |   26670   11989   633994    52.9 |  8.823 % |
c |     62964 |   37328   133412 |   29337   14552   735854    50.6 |  8.823 % |
c |     66809 |   37328   133412 |   32271   18397   947232    51.5 |  8.823 % |
c |     72575 |   37320   133386 |   35498   24162  1530071    63.3 |  8.839 % |
c ==============================================================================
c [1mFound solution: 1519899[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13160158   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73010 |   37342   133585 |   12447   24597  1573773    64.0 |  8.839 % |
c |     73111 |   37342   133585 |   13691   12400   827312    66.7 |  9.019 % |
c |     73261 |   37342   133585 |   15060   12550   830434    66.2 |  9.019 % |
c |     73486 |   37342   133585 |   16566   12775   837046    65.5 |  9.019 % |
c |     73823 |   37342   133585 |   18223   13112   847026    64.6 |  9.019 % |
c |     74331 |   37342   133585 |   20046   13620   864150    63.4 |  9.019 % |
c |     75090 |   37342   133585 |   22050   14379   898655    62.5 |  9.019 % |
c |     76229 |   37342   133585 |   24255   15518   927387    59.8 |  9.019 % |
c |     77937 |   37342   133585 |   26681   17226   997875    57.9 |  9.019 % |
c |     80500 |   37342   133585 |   29349   19789  1155155    58.4 |  9.019 % |
c ==============================================================================
c [1mFound solution: 696547[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 6643478   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80703 |   37322   133626 |   12440   19845  1157571    58.3 |  9.019 % |
c |     80803 |   37322   133626 |   13684   10023   343586    34.3 |  9.365 % |
c |     80953 |   37322   133626 |   15052   10173   344703    33.9 |  9.365 % |
c |     81179 |   37322   133626 |   16557   10399   349501    33.6 |  9.365 % |
c |     81517 |   37310   133584 |   18213   10735   356649    33.2 |  9.382 % |
c |     82024 |   37310   133584 |   20034   11242   368052    32.7 |  9.382 % |
c |     82784 |   37239   133341 |   22038   11988   398513    33.2 |  9.608 % |
c |     83923 |   37239   133341 |   24242   13127   431004    32.8 |  9.608 % |
c |     85631 |   37239   133341 |   26666   14835   500461    33.7 |  9.608 % |
c |     88193 |   37239   133341 |   29332   17397   613437    35.3 |  9.608 % |
c |     92039 |   37239   133341 |   32266   21243   821585    38.7 |  9.608 % |
c |     97805 |   37231   133315 |   35492   27007  1055452    39.1 |  9.624 % |
c |    106454 |   37231   133315 |   39042   35656  1550439    43.5 |  9.624 % |
c |    119428 |   37231   133315 |   42946   21665   976172    45.1 |  9.624 % |
c |    138889 |   37231   133315 |   47240   41126  2132438    51.9 |  9.624 % |
c |    168081 |   37231   133315 |   51964   36447  1894778    52.0 |  9.624 % |
c |    211870 |   37223   133289 |   57161   41195  1925511    46.7 |  9.640 % |
c |    277554 |   37215   133263 |   62877   19179  1805425    94.1 |  9.656 % |
c |    376080 |   37215   133263 |   69165   20633  1385603    67.2 |  9.656 % |
c ==============================================================================
c [1mFound solution: 555057[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6784968   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    426313 |   37217   133349 |   12405   70864  4836343    68.2 |  9.656 % |
c |    426413 |   37217   133349 |   13645    7485   406626    54.3 |  9.837 % |
c |    426564 |   37209   133323 |   15010    7635   408315    53.5 |  9.853 % |
c |    426789 |   37209   133323 |   16511    7860   411682    52.4 |  9.853 % |
c |    427126 |   37209   133323 |   18162    8197   415921    50.7 |  9.853 % |
c |    427632 |   37209   133323 |   19978    8703   428199    49.2 |  9.853 % |
c |    428391 |   37209   133323 |   21976    9462   439159    46.4 |  9.853 % |
c |    429532 |   37209   133323 |   24173   10603   473808    44.7 |  9.853 % |
c |    431241 |   37209   133323 |   26591   12312   525960    42.7 |  9.853 % |
c |    433803 |   37209   133323 |   29250   14874   631983    42.5 |  9.853 % |
c |    437647 |   37209   133323 |   32175   18718   775163    41.4 |  9.853 % |
c |    443414 |   37209   133323 |   35392   24485  1032585    42.2 |  9.853 % |
c |    452063 |   37209   133323 |   38932   33134  1593504    48.1 |  9.853 % |
c |    465037 |   37209   133323 |   42825   18239  1802920    98.8 |  9.853 % |
c |    484498 |   37209   133323 |   47107   37700  3538156    93.9 |  9.853 % |
c |    513691 |   37209   133323 |   51818   30907  2135570    69.1 |  9.853 % |
c |    557480 |   37209   133323 |   57000   34331  2800137    81.6 |  9.853 % |
c |    623168 |   37209   133323 |   62700   55995  3501059    62.5 |  9.853 % |
c |    721694 |   37209   133323 |   68970   56047  3841902    68.5 |  9.853 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 18222
Raw data (stat): 18222 (runsolver) R 18221 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548431739 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 1622 0 0 0 995 4 0 0 25 0 1 0 548431739 8458240 1599 4294967295 134512640 134672761 3221224528 3221223588 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2065 1599 603 41 0 2024 0
vsize: 8260
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 2464 0 0 0 1992 7 0 0 25 0 1 0 548431739 11943936 2441 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2441 603 41 0 2875 0
vsize: 11664
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3116 0 0 0 2991 8 0 0 25 0 1 0 548431739 14630912 3093 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3572 3093 603 41 0 3531 0
vsize: 14288
[startup+40.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3457 0 0 0 3989 9 0 0 25 0 1 0 548431739 16101376 3434 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3434 603 41 0 3890 0
vsize: 15724
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3457 0 0 0 4989 10 0 0 25 0 1 0 548431739 16101376 3434 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3434 603 41 0 3890 0
vsize: 15724
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3459 0 0 0 5989 10 0 0 25 0 1 0 548431739 16101376 3436 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3436 603 41 0 3890 0
vsize: 15724
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3459 0 0 0 6989 10 0 0 25 0 1 0 548431739 16101376 3436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3436 603 41 0 3890 0
vsize: 15724
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3463 0 0 0 7988 11 0 0 25 0 1 0 548431739 16101376 3440 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3440 603 41 0 3890 0
vsize: 15724
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3463 0 0 0 8988 11 0 0 25 0 1 0 548431739 16101376 3440 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3440 603 41 0 3890 0
vsize: 15724
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3463 0 0 0 9988 12 0 0 25 0 1 0 548431739 16101376 3440 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3440 603 41 0 3890 0
vsize: 15724
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3470 0 0 0 10987 12 0 0 25 0 1 0 548431739 16101376 3447 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3447 603 41 0 3890 0
vsize: 15724
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3470 0 0 0 11987 12 0 0 25 0 1 0 548431739 16101376 3447 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3447 603 41 0 3890 0
vsize: 15724
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3507 0 0 0 12987 13 0 0 25 0 1 0 548431739 16232448 3484 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3963 3484 603 41 0 3922 0
vsize: 15852
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 3902 0 0 0 13985 14 0 0 25 0 1 0 548431739 17866752 3879 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4362 3879 603 41 0 4321 0
vsize: 17448
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4221 0 0 0 14985 15 0 0 25 0 1 0 548431739 19214336 4198 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4198 603 41 0 4650 0
vsize: 18764
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4253 0 0 0 15984 16 0 0 25 0 1 0 548431739 19349504 4230 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4724 4230 603 41 0 4683 0
vsize: 18896
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4253 0 0 0 16984 16 0 0 25 0 1 0 548431739 19349504 4230 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4724 4230 603 41 0 4683 0
vsize: 18896
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4253 0 0 0 17984 16 0 0 25 0 1 0 548431739 19349504 4230 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4724 4230 603 41 0 4683 0
vsize: 18896
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4253 0 0 0 18984 16 0 0 25 0 1 0 548431739 19349504 4230 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4724 4230 603 41 0 4683 0
vsize: 18896
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4253 0 0 0 19984 17 0 0 25 0 1 0 548431739 19349504 4230 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4724 4230 603 41 0 4683 0
vsize: 18896
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4675 0 0 0 20983 18 0 0 25 0 1 0 548431739 21094400 4652 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4652 603 41 0 5109 0
vsize: 20600
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4685 0 0 0 21983 18 0 0 25 0 1 0 548431739 21094400 4662 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4662 603 41 0 5109 0
vsize: 20600
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4685 0 0 0 22982 19 0 0 25 0 1 0 548431739 21094400 4662 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4662 603 41 0 5109 0
vsize: 20600
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4685 0 0 0 23982 19 0 0 25 0 1 0 548431739 21094400 4662 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4662 603 41 0 5109 0
vsize: 20600
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 4791 0 0 0 24982 20 0 0 25 0 1 0 548431739 21495808 4768 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4768 603 41 0 5207 0
vsize: 20992
[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 5342 0 0 0 25981 22 0 0 25 0 1 0 548431739 23781376 5319 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 5319 603 41 0 5765 0
vsize: 23224
[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 5851 0 0 0 26980 23 0 0 25 0 1 0 548431739 25788416 5828 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6296 5828 603 41 0 6255 0
vsize: 25184
[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6339 0 0 0 27979 25 0 0 25 0 1 0 548431739 27799552 6316 4294967295 134512640 134672761 3221224528 3221223632 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6787 6316 603 41 0 6746 0
vsize: 27148
[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6554 0 0 0 28978 26 0 0 25 0 1 0 548431739 28741632 6531 4294967295 134512640 134672761 3221224528 3221223696 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6531 603 41 0 6976 0
vsize: 28068
[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6554 0 0 0 29978 26 0 0 25 0 1 0 548431739 28741632 6531 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6531 603 41 0 6976 0
vsize: 28068
[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6554 0 0 0 30977 27 0 0 25 0 1 0 548431739 28741632 6531 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6531 603 41 0 6976 0
vsize: 28068
[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6554 0 0 0 31978 27 0 0 25 0 1 0 548431739 28741632 6531 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6531 603 41 0 6976 0
vsize: 28068
[startup+330.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6554 0 0 0 32978 27 0 0 25 0 1 0 548431739 28741632 6531 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6531 603 41 0 6976 0
vsize: 28068
[startup+340.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 6842 0 0 0 33977 29 0 0 25 0 1 0 548431739 29945856 6819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7311 6819 603 41 0 7270 0
vsize: 29244
[startup+350.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 7253 0 0 0 34975 31 0 0 25 0 1 0 548431739 31547392 7230 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7702 7230 603 41 0 7661 0
vsize: 30808
[startup+360.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 7662 0 0 0 35973 33 0 0 25 0 1 0 548431739 33284096 7639 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8126 7639 603 41 0 8085 0
vsize: 32504
[startup+370.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8074 0 0 0 36972 34 0 0 25 0 1 0 548431739 34893824 8051 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8519 8051 603 41 0 8478 0
vsize: 34076
[startup+380.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8498 0 0 0 37970 36 0 0 25 0 1 0 548431739 36646912 8475 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8947 8475 603 41 0 8906 0
vsize: 35788
[startup+390.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8933 0 0 0 38969 38 0 0 25 0 1 0 548431739 38526976 8910 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9406 8910 603 41 0 9365 0
vsize: 37624
[startup+400.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 39968 38 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+410.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 40969 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+420.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 41970 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+430.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 42971 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+440.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 43972 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+450.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 44972 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+460.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 45972 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+470.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 46972 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+480.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 47973 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+490.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 8973 0 0 0 48973 39 0 0 25 0 1 0 548431739 38662144 8950 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9439 8950 603 41 0 9398 0
vsize: 37756
[startup+500.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9105 0 0 0 49972 40 0 0 25 0 1 0 548431739 39198720 9082 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9570 9082 603 41 0 9529 0
vsize: 38280
[startup+510.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 50973 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+520.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 51973 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+530.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 52974 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+540.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 53975 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+550.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 54975 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223712 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+560.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 55975 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+570.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9166 0 0 0 56975 40 0 0 25 0 1 0 548431739 39469056 9143 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9143 603 41 0 9595 0
vsize: 38544
[startup+580.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 57976 40 0 0 25 0 1 0 548431739 39469056 9144 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9636 9144 603 41 0 9595 0
vsize: 38544
[startup+590.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 58974 40 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+600.118 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 59973 40 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+610.119 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 60973 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+620.129 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 61973 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+630.129 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 62974 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223712 134558775 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+640.132 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 63974 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+650.136 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 64975 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+660.136 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9167 0 0 0 65975 41 0 0 25 0 1 0 548431739 39464960 9144 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 9144 603 41 0 9594 0
vsize: 38540
[startup+670.144 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9171 0 0 0 66976 41 0 0 25 0 1 0 548431739 39727104 9148 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9148 603 41 0 9658 0
vsize: 38796
[startup+680.155 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9174 0 0 0 67977 41 0 0 25 0 1 0 548431739 39727104 9151 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9151 603 41 0 9658 0
vsize: 38796
[startup+690.157 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 68977 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+700.157 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 69977 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+710.158 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 70977 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+720.159 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 71978 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+730.177 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 72980 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+740.177 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 73979 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+750.177 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 74979 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+760.177 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 18222
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 75979 41 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+770.178 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 76976 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+780.179 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 77976 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+790.179 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 78976 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+800.179 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 79977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+810.179 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 80977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+820.178 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 81977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+830.178 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18275
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 82977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223712 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+840.178 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 83977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+850.179 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 84977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+860.179 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 85977 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+870.179 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 86978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+880.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 87978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+890.179 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 88978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+900.179 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 89978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+910.179 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 90978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+920.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 91978 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+930.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 92979 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+940.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 93979 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+950.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 94979 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223624 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+960.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 95979 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+970.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 96979 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+980.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 97980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+990.179 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 98980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1000.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 99980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1010.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 100980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1020.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 101980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223712 134559397 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1030.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 102980 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1040.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 103981 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1050.18 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 104981 44 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1060.18 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 105981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1070.18 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 106981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1080.18 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 107981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1090.18 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 108981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1100.18 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 109981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1110.18 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 110982 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223632 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1120.18 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18277
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 111982 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1130.18 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 112981 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1140.18 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9175 0 0 0 113982 45 0 0 25 0 1 0 548431739 39727104 9152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9152 603 41 0 9658 0
vsize: 38796
[startup+1150.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 114982 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
[startup+1160.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 115982 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
[startup+1170.18 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 116982 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
[startup+1180.18 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 117982 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223632 134560501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
[startup+1190.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 118983 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223584 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18279
Raw data (stat): 18222 (minisat+) R 18221 28546 28545 0 -1 0 9176 0 0 0 119983 45 0 0 25 0 1 0 548431739 39727104 9153 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9699 9153 603 41 0 9658 0
vsize: 38796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 18279
Raw data (stat): 18222 (minisat+) Z 18221 28546 28545 0 -1 12 9179 0 0 0 119983 47 0 0 25 0 1 0 548431739 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.2
CPU time (s): 1200.3
CPU user time (s): 1199.83
CPU system time (s): 0.470928
CPU usage (%): 100.009
Max. virtual memory (Kb): 38796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####