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-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUM	f88781e3d6e9a5487d13eaa213c27b55
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4272
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	205
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	105
Trace number 14739

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 00:59:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19479 boxname=wulflinc12 idbench=1499 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 19479
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        855884 kB
Buffers:         15124 kB
Cached:         142048 kB
SwapCached:        316 kB
Active:          17016 kB
Inactive:       142420 kB
HighTotal:      131008 kB
HighFree:        58968 kB
LowTotal:       903652 kB
LowFree:        796916 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            13600 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:19:24 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 19479 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21500    76369 |    7166       0        0     nan |  0.000 % |
c |       101 |   21500    76369 |    7882     101      468     4.6 |  7.165 % |
c |       251 |   21500    76369 |    8670     251     3196    12.7 |  7.165 % |
c |       480 |   21492    76343 |    9537     479     7965    16.6 |  7.194 % |
c ==============================================================================
c [1mFound solution: 552006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       620 |   25213    85029 |    8404     619     9130    14.7 |  7.194 % |
c |       721 |   25213    85029 |    9244     720    18323    25.4 |  5.272 % |
c |       873 |   25213    85029 |   10168     872    38194    43.8 |  5.272 % |
c |      1099 |   25205    85003 |   11185    1097    44770    40.8 |  5.293 % |
c |      1436 |   25205    85003 |   12304    1434    50426    35.2 |  5.293 % |
c ==============================================================================
c [1mFound solution: 326866[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1527 |   25232    85100 |    8410    1525    51894    34.0 |  5.293 % |
c |      1628 |   25224    85074 |    9251    1625    53036    32.6 |  5.315 % |
c |      1779 |   25216    85048 |   10176    1775    55394    31.2 |  5.335 % |
c |      2004 |   25208    85022 |   11193    1999    58767    29.4 |  5.356 % |
c |      2341 |   25192    84970 |   12313    2334    62861    26.9 |  5.398 % |
c |      2847 |   25184    84944 |   13544    2839    69965    24.6 |  5.418 % |
c |      3608 |   25184    84944 |   14898    3600    95435    26.5 |  5.418 % |
c |      4747 |   25184    84944 |   16388    4739   144758    30.5 |  5.418 % |
c ==============================================================================
c [1mFound solution: 90720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4797 |   25161    84848 |    8387    4722   138574    29.3 |  5.418 % |
c |      4897 |   25161    84848 |    9225    4822   142605    29.6 |  5.550 % |
c |      5047 |   25161    84848 |   10148    4972   144103    29.0 |  5.550 % |
c |      5272 |   25161    84848 |   11163    5197   147996    28.5 |  5.550 % |
c |      5609 |   25161    84848 |   12279    5534   162224    29.3 |  5.550 % |
c |      6115 |   25161    84848 |   13507    6040   167189    27.7 |  5.550 % |
c |      6874 |   25161    84848 |   14858    6799   192943    28.4 |  5.550 % |
c |      8013 |   25161    84848 |   16343    7938   219858    27.7 |  5.550 % |
c |      9722 |   25161    84848 |   17978    9647   293177    30.4 |  5.550 % |
c |     12285 |   25161    84848 |   19776   12210   421505    34.5 |  5.550 % |
c ==============================================================================
c [1mFound solution: 71680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13517 |   25175    84879 |    8391   13442   503492    37.5 |  5.550 % |
c |     13617 |   25175    84879 |    9230    6821   271301    39.8 |  5.566 % |
c |     13767 |   25175    84879 |   10153    6971   274301    39.3 |  5.566 % |
c |     13993 |   25175    84879 |   11168    7197   278686    38.7 |  5.566 % |
c |     14330 |   25175    84879 |   12285    7534   287188    38.1 |  5.566 % |
c |     14837 |   25167    84861 |   13513    8040   298611    37.1 |  5.607 % |
c |     15596 |   25167    84861 |   14865    8799   324504    36.9 |  5.607 % |
c |     16737 |   25167    84861 |   16351    9940   380508    38.3 |  5.607 % |
c |     18445 |   25159    84835 |   17986   11647   441573    37.9 |  5.628 % |
c |     21010 |   25159    84835 |   19785   14212   538347    37.9 |  5.628 % |
c |     24854 |   25159    84835 |   21764   18056   694983    38.5 |  5.628 % |
c |     30620 |   25151    84809 |   23940   12175   440850    36.2 |  5.649 % |
c |     39270 |   25151    84809 |   26334   20825   861201    41.4 |  5.649 % |
c |     52244 |   25143    84787 |   28968   19364  1066264    55.1 |  5.690 % |
c |     71706 |   25143    84787 |   31864   21785   832604    38.2 |  5.690 % |
c |    100898 |   25143    84787 |   35051   30864  1585633    51.4 |  5.690 % |
c |    144688 |   25127    84735 |   38556   30209  1934568    64.0 |  5.731 % |
c ==============================================================================
c [1mFound solution: 57194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156428 |   24849    84050 |    8283   16798   793938    47.3 |  5.731 % |
c |    156528 |   24849    84050 |    9111    8499   353305    41.6 |  7.456 % |
c |    156678 |   24849    84050 |   10022    8649   356887    41.3 |  7.456 % |
c |    156906 |   24849    84050 |   11024    8877   362140    40.8 |  7.456 % |
c |    157244 |   24841    84024 |   12127    9213   367653    39.9 |  7.786 % |
c |    157750 |   24791    83912 |   13339    9716   380059    39.1 |  7.786 % |
c |    158510 |   24791    83912 |   14673   10476   402291    38.4 |  7.786 % |
c |    159650 |   24791    83912 |   16141   11616   445572    38.4 |  7.786 % |
c |    161358 |   24791    83912 |   17755   13324   500491    37.6 |  7.786 % |
c |    163922 |   24633    83548 |   19530   15878   584275    36.8 |  8.963 % |
c |    167767 |   24633    83548 |   21483   19723   717286    36.4 |  8.963 % |
c |    173533 |   24633    83548 |   23632   14127   524723    37.1 |  8.963 % |
c |    182182 |   24615    83508 |   25995   22775   900769    39.6 |  9.067 % |
c |    195157 |   24615    83508 |   28595   22368   947167    42.3 |  9.067 % |
c |    214618 |   24609    83494 |   31454   25616  1241598    48.5 |  9.108 % |
c |    243810 |   24609    83494 |   34600   15970  1161777    72.7 |  9.108 % |
c |    287599 |   24609    83494 |   38060   17320   924662    53.4 |  9.108 % |
c |    353284 |   24609    83494 |   41866   33078  2000413    60.5 |  9.108 % |
c ==============================================================================
c [1mFound solution: 50892[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    357437 |   24626    83535 |    8208   37231  2195337    59.0 |  9.108 % |
c |    357538 |   24626    83535 |    9028    7749   343658    44.3 |  9.110 % |
c |    357688 |   24626    83535 |    9931    7899   346693    43.9 |  9.110 % |
c |    357913 |   24626    83535 |   10924    8124   351062    43.2 |  9.110 % |
c |    358250 |   24626    83535 |   12017    8461   353734    41.8 |  9.110 % |
c |    358756 |   24626    83535 |   13219    8967   373042    41.6 |  9.110 % |
c |    359516 |   24626    83535 |   14540    9727   389280    40.0 |  9.110 % |
c |    360655 |   24626    83535 |   15995   10866   432959    39.8 |  9.110 % |
c |    362365 |   24626    83535 |   17594   12576   498251    39.6 |  9.110 % |
c |    364927 |   24626    83535 |   19354   15138   598074    39.5 |  9.110 % |
c |    368772 |   24626    83535 |   21289   18983   932407    49.1 |  9.110 % |
c |    374538 |   24626    83535 |   23418   13599   607840    44.7 |  9.110 % |
c |    383187 |   24626    83535 |   25760   22248  1058848    47.6 |  9.110 % |
c |    396162 |   24626    83535 |   28336   20986  1245980    59.4 |  9.110 % |
c |    415623 |   24619    83519 |   31169   22739  1211865    53.3 |  9.171 % |
c |    444817 |   24619    83519 |   34286   33541  1608075    47.9 |  9.171 % |
c |    488606 |   24602    83481 |   37715   16382   727364    44.4 |  9.275 % |
c |    554292 |   24602    83481 |   41487   31383  2050371    65.3 |  9.275 % |
c ==============================================================================
c [1mFound solution: 48690[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    558165 |   24611    83506 |    8203   35256  2301853    65.3 |  9.275 % |
c |    558266 |   24611    83506 |    9023    7352   361671    49.2 |  9.286 % |
c |    558416 |   24611    83506 |    9925    7502   363308    48.4 |  9.286 % |
c |    558641 |   24611    83506 |   10918    7727   367204    47.5 |  9.286 % |
c |    558978 |   24611    83506 |   12010    8064   374027    46.4 |  9.286 % |
c |    559485 |   24611    83506 |   13211    8571   390397    45.5 |  9.286 % |
c |    560245 |   24611    83506 |   14532    9331   411224    44.1 |  9.286 % |
c |    561384 |   24611    83506 |   15985   10470   451355    43.1 |  9.286 % |
c |    563093 |   24611    83506 |   17583   12179   555621    45.6 |  9.286 % |
c |    565655 |   24611    83506 |   19342   14741   639049    43.4 |  9.286 % |
c |    569500 |   24611    83506 |   21276   18586   781212    42.0 |  9.286 % |
c |    575266 |   24611    83506 |   23404   13076   496567    38.0 |  9.286 % |
c |    583917 |   24611    83506 |   25744   21727   836747    38.5 |  9.286 % |
c |    596891 |   24611    83506 |   28318   21220   824464    38.9 |  9.286 % |
c |    616352 |   24611    83506 |   31150   24464  1080641    44.2 |  9.286 % |
c |    645545 |   24611    83506 |   34265   15444   790113    51.2 |  9.286 % |
c |    689337 |   24611    83506 |   37692   15693   616696    39.3 |  9.286 % |
c |    755022 |   24611    83506 |   41461   30159  3542491   117.5 |  9.286 % |
c |    853548 |   24611    83506 |   45608   18346   925859    50.5 |  9.286 % |
#### 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.79 0.92 0.89 2/54 18052
Raw data (stat): 18052 (runsolver) R 18051 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482721128 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 18052
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 1517 0 0 0 993 4 0 0 25 0 1 0 482721128 7983104 1495 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1949 1495 603 41 0 1908 0
vsize: 7796
[startup+20.0004 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 18052
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 1977 0 0 0 1991 5 0 0 25 0 1 0 482721128 9850880 1955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2405 1955 603 41 0 2364 0
vsize: 9620
[startup+30.0002 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 18052
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2111 0 0 0 2990 6 0 0 25 0 1 0 482721128 10391552 2089 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2537 2089 603 41 0 2496 0
vsize: 10148
[startup+40.0013 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 18052
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2466 0 0 0 3988 8 0 0 25 0 1 0 482721128 11870208 2444 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2898 2444 603 41 0 2857 0
vsize: 11592
[startup+50.0018 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2588 0 0 0 4987 9 0 0 25 0 1 0 482721128 12271616 2566 4294967295 134512640 134672761 3221224624 3221223760 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2996 2566 603 41 0 2955 0
vsize: 11984
[startup+60.0016 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2762 0 0 0 5987 9 0 0 25 0 1 0 482721128 13103104 2740 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3199 2740 603 41 0 3158 0
vsize: 12796
[startup+70.0028 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2772 0 0 0 6987 9 0 0 25 0 1 0 482721128 13103104 2750 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3199 2750 603 41 0 3158 0
vsize: 12796
[startup+80.0033 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 2805 0 0 0 7987 10 0 0 25 0 1 0 482721128 13365248 2783 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3263 2783 603 41 0 3222 0
vsize: 13052
[startup+90.0031 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 3046 0 0 0 8986 11 0 0 25 0 1 0 482721128 14299136 3024 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3491 3024 603 41 0 3450 0
vsize: 13964
[startup+100.003 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 3378 0 0 0 9985 12 0 0 25 0 1 0 482721128 15638528 3356 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3356 603 41 0 3777 0
vsize: 15272
[startup+110.003 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 18105
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 3378 0 0 0 10985 12 0 0 25 0 1 0 482721128 15638528 3356 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3356 603 41 0 3777 0
vsize: 15272
[startup+120.004 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 3576 0 0 0 11984 13 0 0 25 0 1 0 482721128 16437248 3554 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4013 3554 603 41 0 3972 0
vsize: 16052
[startup+130.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 3979 0 0 0 12982 16 0 0 25 0 1 0 482721128 18182144 3957 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 3957 603 41 0 4398 0
vsize: 17756
[startup+140.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4016 0 0 0 13981 16 0 0 25 0 1 0 482721128 18317312 3994 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4472 3994 603 41 0 4431 0
vsize: 17888
[startup+150.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4016 0 0 0 14981 16 0 0 25 0 1 0 482721128 18317312 3994 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4472 3994 603 41 0 4431 0
vsize: 17888
[startup+160.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4017 0 0 0 15981 16 0 0 25 0 1 0 482721128 18317312 3995 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4472 3995 603 41 0 4431 0
vsize: 17888
[startup+170.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 16981 17 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+180.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 17981 17 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+190.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 18981 17 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+200.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 19981 18 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+210.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 20981 18 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223728 134555084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+220.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 21981 18 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+230.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 22981 18 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+240.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 23981 18 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+250.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 24981 19 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+260.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4057 0 0 0 25981 19 0 0 25 0 1 0 482721128 18452480 4035 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 4035 603 41 0 4464 0
vsize: 18020
[startup+270.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 26980 20 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223748 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+280.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 27980 21 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+290.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 28982 21 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+300.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 29982 21 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+310.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 30982 22 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+320.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 31981 22 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+330.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 32982 22 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+340.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 33982 23 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+350.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 34981 23 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+360.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 35981 23 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+370.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 36981 24 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+380.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18107
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 37981 24 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223808 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+390.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 38980 25 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+400.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 39980 25 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+410.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 40980 26 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+420.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 41979 26 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223824 134557967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+430.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 42979 26 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+440.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 43979 27 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+450.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 44979 27 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+460.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 45979 27 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+470.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 46979 28 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+480.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 47979 28 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+490.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 48979 28 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+500.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 49979 28 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+510.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 50979 29 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223808 134558754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+520.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 51979 29 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+530.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 52978 30 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+540.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 53978 30 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223788 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+550.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 54978 30 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221222752 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+560.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 55978 31 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+570.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 56978 31 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+580.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 57978 31 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+590.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 58978 31 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+600.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4385 0 0 0 59978 31 0 0 25 0 1 0 482721128 19795968 4363 4294967295 134512640 134672761 3221224624 3221223800 134559124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4833 4363 603 41 0 4792 0
vsize: 19332
[startup+610.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 4677 0 0 0 60977 33 0 0 25 0 1 0 482721128 21004288 4655 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5128 4655 603 41 0 5087 0
vsize: 20512
[startup+620.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 61977 33 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223676 1075349669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+630.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 62976 34 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+640.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 63976 34 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223808 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+650.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 64976 34 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+660.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 65976 35 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+670.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 66976 35 0 0 25 0 1 0 482721128 22626304 5037 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5524 5037 603 41 0 5483 0
vsize: 22096
[startup+680.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 67975 36 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+690.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 68976 36 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+700.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 69975 36 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223788 134565156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+710.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 70975 36 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+720.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 71975 37 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+730.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 72975 37 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223808 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+740.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 73975 37 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+750.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 74975 37 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+760.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 75975 38 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+770.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 76975 38 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+780.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 77975 38 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223808 134559561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+790.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 78975 39 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+800.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 79974 39 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+810.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 80975 40 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+820.086 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 81977 40 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+830.095 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 82978 40 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+840.108 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 83979 40 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+850.127 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 84981 40 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+860.126 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5059 0 0 0 85981 41 0 0 25 0 1 0 482721128 22585344 5037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5514 5037 603 41 0 5473 0
vsize: 22056
[startup+870.13 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5473 0 0 0 86979 43 0 0 25 0 1 0 482721128 24338432 5451 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5942 5451 603 41 0 5901 0
vsize: 23768
[startup+880.13 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 5886 0 0 0 87977 45 0 0 25 0 1 0 482721128 25948160 5864 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6335 5864 603 41 0 6294 0
vsize: 25340
[startup+890.149 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6050 0 0 0 88977 46 0 0 25 0 1 0 482721128 26615808 6028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6498 6028 603 41 0 6457 0
vsize: 25992
[startup+900.149 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6050 0 0 0 89977 47 0 0 25 0 1 0 482721128 26615808 6028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6498 6028 603 41 0 6457 0
vsize: 25992
[startup+910.149 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6050 0 0 0 90978 47 0 0 25 0 1 0 482721128 26615808 6028 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6498 6028 603 41 0 6457 0
vsize: 25992
[startup+920.158 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6050 0 0 0 91978 47 0 0 25 0 1 0 482721128 26615808 6028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6498 6028 603 41 0 6457 0
vsize: 25992
[startup+930.158 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6249 0 0 0 92977 48 0 0 25 0 1 0 482721128 27418624 6227 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6694 6227 603 41 0 6653 0
vsize: 26776
[startup+940.161 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6592 0 0 0 93977 49 0 0 25 0 1 0 482721128 28889088 6570 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7053 6570 603 41 0 7012 0
vsize: 28212
[startup+950.161 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 6939 0 0 0 94976 50 0 0 25 0 1 0 482721128 30232576 6917 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7381 6917 603 41 0 7340 0
vsize: 29524
[startup+960.162 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 95976 50 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+970.163 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 96976 51 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+980.163 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 97976 51 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+990.163 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 98976 51 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1000.16 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 99975 52 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1010.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 100975 52 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223692 1075346622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1020.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 101975 52 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223776 134559753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1030.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 102975 52 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1040.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 103975 53 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1050.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 104976 53 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1060.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 105975 53 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1070.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 106975 54 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1080.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 107974 54 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1090.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7002 0 0 0 108974 55 0 0 25 0 1 0 482721128 30498816 6980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6980 603 41 0 7405 0
vsize: 29784
[startup+1100.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 109974 55 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1110.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 110974 55 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1120.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 111974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1130.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 112974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1140.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 113974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1150.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 114974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1160.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 115974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1170.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 116974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1180.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 117974 56 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1190.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 118974 57 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18109
Raw data (stat): 18052 (minisat+) R 18051 25285 25284 0 -1 0 7005 0 0 0 119974 57 0 0 25 0 1 0 482721128 30498816 6983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7446 6983 603 41 0 7405 0
vsize: 29784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 18109
Raw data (stat): 18052 (minisat+) Z 18051 25285 25284 0 -1 12 7008 0 0 0 119974 58 0 0 25 0 1 0 482721128 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.19
CPU time (s): 1200.34
CPU user time (s): 1199.75
CPU system time (s): 0.58591
CPU usage (%): 100.012
Max. virtual memory (Kb): 29784
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####