PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5095

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 21:55:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3290 boxname=wulflinc22 idbench=366 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc22/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 3290
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        866968 kB
Buffers:         31144 kB
Cached:          93316 kB
SwapCached:        524 kB
Active:          43704 kB
Inactive:        84116 kB
HighTotal:      131008 kB
HighFree:        33936 kB
LowTotal:       903652 kB
LowFree:        833032 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34180 kB
Committed_AS:    63500 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:15:16 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3290 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4084    11649 |    1361       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 355[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20800     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39610    94771 |   13203       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        52 |   40635    97290 |   13545      47      509    10.8 |  0.000 % |
c |       153 |   40635    97290 |   14899     148     2006    13.6 |  0.807 % |
c |       303 |   40635    97290 |   16389     298     3680    12.3 |  0.807 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       335 |   40816    97778 |   13605     330     3969    12.0 |  0.807 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       381 |   40957    98168 |   13652     376     4254    11.3 |  0.807 % |
c |       482 |   40957    98168 |   15017     477     6680    14.0 |  0.809 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |   41021    98358 |   13673     538     7309    13.6 |  0.809 % |
c |       643 |   41007    98330 |   15040     637     8156    12.8 |  0.847 % |
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       741 |   41137    98688 |   13712     735    12723    17.3 |  0.847 % |
c |       841 |   41137    98688 |   15083     835    14812    17.7 |  0.858 % |
c |       991 |   41137    98688 |   16591     985    15900    16.1 |  0.858 % |
c |      1216 |   41137    98688 |   18250    1210    24830    20.5 |  0.858 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1549 |   40826    98032 |   13608    1526    31796    20.8 |  0.858 % |
c |      1649 |   40807    97993 |   14968    1625    32748    20.2 |  1.610 % |
c |      1799 |   40807    97993 |   16465    1775    35020    19.7 |  1.610 % |
c |      2024 |   40807    97993 |   18112    2000    57066    28.5 |  1.610 % |
c |      2361 |   40157    96519 |   19923    2253    61245    27.2 |  2.962 % |
c |      2870 |   40157    96519 |   21915    2762    71091    25.7 |  2.962 % |
c |      3629 |   40157    96519 |   24107    3521    86728    24.6 |  2.962 % |
c |      4768 |   40069    96331 |   26518    4641   109000    23.5 |  3.209 % |
c |      6476 |   39881    95923 |   29169    6320   241528    38.2 |  3.710 % |
c |      9040 |   39881    95923 |   32086    8884   558335    62.8 |  3.710 % |
c |     12886 |   39881    95923 |   35295   12730   837536    65.8 |  3.710 % |
c |     18654 |   39881    95923 |   38825   18498  1338946    72.4 |  3.710 % |
c |     27303 |   39881    95923 |   42707   27147  2479319    91.3 |  3.710 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30230 |   39885    95933 |   13295   30074  2833854    94.2 |  3.710 % |
c |     30330 |   39885    95933 |   14624   13138  1476713   112.4 |  3.714 % |
c |     30481 |   39885    95933 |   16086   13289  1480028   111.4 |  3.714 % |
c |     30709 |   39885    95933 |   17695   13517  1485023   109.9 |  3.714 % |
c |     31046 |   39885    95933 |   19465   13854  1491450   107.7 |  3.714 % |
c |     31552 |   39885    95933 |   21411   14360  1526895   106.3 |  3.714 % |
c |     32311 |   39885    95933 |   23552   15119  1570893   103.9 |  3.714 % |
c |     33452 |   39885    95933 |   25908   16260  1620404    99.7 |  3.714 % |
c |     35160 |   39871    95901 |   28499   17966  1667556    92.8 |  3.734 % |
c |     37722 |   39871    95901 |   31348   20528  1922784    93.7 |  3.734 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37876 |   39892    95963 |   13297   20682  1934151    93.5 |  3.734 % |
c |     37977 |   39838    95840 |   14626   10433   624856    59.9 |  3.810 % |
c |     38128 |   39838    95840 |   16089   10584   628193    59.4 |  3.810 % |
c |     38354 |   39838    95840 |   17698   10810   630346    58.3 |  3.810 % |
c |     38692 |   39838    95840 |   19468   11148   638017    57.2 |  3.810 % |
c |     39198 |   39838    95840 |   21414   11654   656390    56.3 |  3.810 % |
c |     39957 |   39820    95799 |   23556   12406   664944    53.6 |  3.835 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40470 |   39846    95875 |   13282   12919   696562    53.9 |  3.835 % |
c |     40570 |   39846    95875 |   14610   13019   698367    53.6 |  3.837 % |
c |     40720 |   39846    95875 |   16071   13169   700531    53.2 |  3.837 % |
c |     40945 |   39846    95875 |   17678   13394   705284    52.7 |  3.837 % |
c |     41282 |   39739    95631 |   19446   13723   724893    52.8 |  4.074 % |
c |     41789 |   39739    95631 |   21390   14230   774776    54.4 |  4.074 % |
c |     42549 |   39721    95589 |   23529   14989   793085    52.9 |  4.129 % |
c |     43688 |   39721    95589 |   25882   16128   862249    53.5 |  4.129 % |
c |     45397 |   39721    95589 |   28471   17837   943295    52.9 |  4.129 % |
c |     47959 |   39721    95589 |   31318   20399  1340906    65.7 |  4.129 % |
c |     51803 |   39721    95589 |   34450   24243  1730566    71.4 |  4.129 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53697 |   39759    95694 |   13253   26132  1833701    70.2 |  4.129 % |
c |     53798 |   39759    95694 |   14578   13167   983300    74.7 |  4.137 % |
c |     53948 |   39721    95606 |   16036   13310   984452    74.0 |  4.197 % |
c |     54173 |   39721    95606 |   17639   13535   995185    73.5 |  4.197 % |
c |     54510 |   39721    95606 |   19403   13872  1004647    72.4 |  4.197 % |
c ==============================================================================
c [1mFound solution: 9[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54616 |   39766    95725 |   13255   13978  1006538    72.0 |  4.197 % |
c |     54716 |   39748    95684 |   14580   14071  1007232    71.6 |  4.220 % |
c |     54866 |   39748    95684 |   16038   14221  1012093    71.2 |  4.220 % |
c |     55091 |   39742    95670 |   17642   14443  1014604    70.2 |  4.230 % |
c |     55428 |   39738    95661 |   19406   14779  1023087    69.2 |  4.235 % |
c |     55934 |   39738    95661 |   21347   15285  1037095    67.9 |  4.235 % |
c |     56693 |   39738    95661 |   23482   16044  1092277    68.1 |  4.235 % |
c |     57832 |   39738    95661 |   25830   17183  1134775    66.0 |  4.235 % |
c |     59541 |   39738    95661 |   28413   18892  1247008    66.0 |  4.235 % |
c |     62103 |   39738    95661 |   31254   21454  1403165    65.4 |  4.235 % |
c |     65947 |   39738    95661 |   34380   25298  2020808    79.9 |  4.235 % |
c |     71714 |   39738    95661 |   37818   31065  2590932    83.4 |  4.235 % |
c |     80363 |   39738    95661 |   41599   39714  3547339    89.3 |  4.235 % |
c |     93337 |   39738    95661 |   45759   19456  2317262   119.1 |  4.235 % |
c |    112798 |   39738    95661 |   50335   38917  5379251   138.2 |  4.235 % |
c |    141992 |   39716    95612 |   55369   26150  3557617   136.0 |  4.270 % |
c |    185781 |   39640    95444 |   60906   27874  1990715    71.4 |  4.457 % |
c |    251466 |   39640    95444 |   66997   44447  9458461   212.8 |  4.457 % |
#### 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.85 0.94 0.90 2/54 29112
Raw data (stat): 29112 (runsolver) R 29111 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479351076 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 2224 0 0 0 992 6 0 0 25 0 1 0 479351076 11313152 2149 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2762 2149 603 41 0 2721 0
vsize: 11048
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 2703 0 0 0 1989 8 0 0 25 0 1 0 479351076 13336576 2628 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3256 2628 603 41 0 3215 0
vsize: 13024
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 3124 0 0 0 2986 11 0 0 25 0 1 0 479351076 15073280 3049 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3680 3049 603 41 0 3639 0
vsize: 14720
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 3538 0 0 0 3985 12 0 0 25 0 1 0 479351076 16818176 3463 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4106 3463 603 41 0 4065 0
vsize: 16424
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 3931 0 0 0 4984 13 0 0 25 0 1 0 479351076 18423808 3856 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4498 3856 603 41 0 4457 0
vsize: 17992
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 4329 0 0 0 5983 15 0 0 25 0 1 0 479351076 20029440 4254 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4890 4254 603 41 0 4849 0
vsize: 19560
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 4712 0 0 0 6982 16 0 0 25 0 1 0 479351076 21508096 4637 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5251 4637 603 41 0 5210 0
vsize: 21004
[startup+80.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 7981 17 0 0 25 0 1 0 479351076 23068672 5008 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5632 5008 603 41 0 5591 0
vsize: 22528
[startup+90.0014 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 8981 17 0 0 25 0 1 0 479351076 23068672 5008 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5632 5008 603 41 0 5591 0
vsize: 22528
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 9981 17 0 0 25 0 1 0 479351076 23068672 5008 4294967295 134512640 134672761 3221224624 3221223808 134559254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5632 5008 603 41 0 5591 0
vsize: 22528
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 10981 17 0 0 25 0 1 0 479351076 23068672 5008 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5632 5008 603 41 0 5591 0
vsize: 22528
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 11981 17 0 0 25 0 1 0 479351076 23068672 5008 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5632 5008 603 41 0 5591 0
vsize: 22528
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 12981 17 0 0 25 0 1 0 479351076 23064576 5008 4294967295 134512640 134672761 3221224624 3221223880 134562563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5631 5008 603 41 0 5590 0
vsize: 22524
[startup+140.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 13981 17 0 0 25 0 1 0 479351076 23064576 5008 4294967295 134512640 134672761 3221224624 3221223728 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5631 5008 603 41 0 5590 0
vsize: 22524
[startup+150.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 14982 17 0 0 25 0 1 0 479351076 23064576 5008 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5631 5008 603 41 0 5590 0
vsize: 22524
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5083 0 0 0 15982 17 0 0 25 0 1 0 479351076 23064576 5008 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5631 5008 603 41 0 5590 0
vsize: 22524
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5085 0 0 0 16982 17 0 0 25 0 1 0 479351076 23064576 5010 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5631 5010 603 41 0 5590 0
vsize: 22524
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5415 0 0 0 17981 18 0 0 25 0 1 0 479351076 24518656 5340 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5986 5340 603 41 0 5945 0
vsize: 23944
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 5825 0 0 0 18980 19 0 0 25 0 1 0 479351076 26128384 5750 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6379 5750 603 41 0 6338 0
vsize: 25516
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 6163 0 0 0 19980 20 0 0 25 0 1 0 479351076 27598848 6088 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6738 6088 603 41 0 6697 0
vsize: 26952
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 6566 0 0 0 20979 21 0 0 25 0 1 0 479351076 29200384 6491 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7129 6491 603 41 0 7088 0
vsize: 28516
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 6999 0 0 0 21977 23 0 0 25 0 1 0 479351076 30920704 6924 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7549 6924 603 41 0 7508 0
vsize: 30196
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 22976 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 23977 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 24977 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 25977 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 26977 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29112
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 27977 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29113
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 28978 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+300.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7402 0 0 0 29978 24 0 0 25 0 1 0 479351076 32657408 7327 4294967295 134512640 134672761 3221224624 3221223728 134560267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7327 603 41 0 7932 0
vsize: 31892
[startup+310.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 7726 0 0 0 30977 25 0 0 25 0 1 0 479351076 34004992 7651 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8302 7651 603 41 0 8261 0
vsize: 33208
[startup+320.005 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 8130 0 0 0 31976 26 0 0 25 0 1 0 479351076 35606528 8055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 8055 603 41 0 8652 0
vsize: 34772
[startup+330.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 8476 0 0 0 32974 28 0 0 25 0 1 0 479351076 36945920 8401 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9020 8401 603 41 0 8979 0
vsize: 36080
[startup+340.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 8861 0 0 0 33973 29 0 0 25 0 1 0 479351076 38543360 8786 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9410 8786 603 41 0 9369 0
vsize: 37640
[startup+350.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 9264 0 0 0 34972 31 0 0 25 0 1 0 479351076 40275968 9189 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9833 9189 603 41 0 9792 0
vsize: 39332
[startup+360.006 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29165
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 9648 0 0 0 35971 32 0 0 25 0 1 0 479351076 41754624 9573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10194 9573 603 41 0 10153 0
vsize: 40776
[startup+370.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 10079 0 0 0 36969 34 0 0 25 0 1 0 479351076 43499520 10004 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10620 10004 603 41 0 10579 0
vsize: 42480
[startup+380.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 10534 0 0 0 37969 34 0 0 25 0 1 0 479351076 45359104 10459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11074 10459 603 41 0 11033 0
vsize: 44296
[startup+390.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 10981 0 0 0 38969 35 0 0 25 0 1 0 479351076 47235072 10906 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11532 10906 603 41 0 11491 0
vsize: 46128
[startup+400.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 39969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+410.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 40968 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+420.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 41968 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+430.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 42969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+440.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 43969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+450.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 44969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+460.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 45969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+470.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 46969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+480.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 47969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+490.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 48969 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+500.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 49970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+510.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 50970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+520.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 51970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+530.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 52970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+540.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 53970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+550.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 54970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+560.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 55970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+570.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 56970 35 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+580.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 57970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+590.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 58969 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+600.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 59969 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+610.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 60969 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+620.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 61969 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+630.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 62970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+640.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 63970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+650.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29167
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 64970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+660.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 65970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+670.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 66970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+680.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11158 0 0 0 67970 36 0 0 25 0 1 0 479351076 47906816 11083 4294967295 134512640 134672761 3221224624 3221223728 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11696 11083 603 41 0 11655 0
vsize: 46784
[startup+690.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11224 0 0 0 68970 36 0 0 25 0 1 0 479351076 48173056 11149 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11761 11149 603 41 0 11720 0
vsize: 47044
[startup+700.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11567 0 0 0 69970 37 0 0 25 0 1 0 479351076 49680384 11492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12129 11492 603 41 0 12088 0
vsize: 48516
[startup+710.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 11951 0 0 0 70969 38 0 0 25 0 1 0 479351076 51277824 11876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12519 11876 603 41 0 12478 0
vsize: 50076
[startup+720.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 12295 0 0 0 71969 38 0 0 25 0 1 0 479351076 52621312 12220 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12847 12220 603 41 0 12806 0
vsize: 51388
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 12624 0 0 0 72968 40 0 0 25 0 1 0 479351076 53952512 12549 4294967295 134512640 134672761 3221224624 3221223808 134558839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 12549 603 41 0 13131 0
vsize: 52688
[startup+740.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 12953 0 0 0 73967 40 0 0 25 0 1 0 479351076 55287808 12878 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13498 12878 603 41 0 13457 0
vsize: 53992
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13262 0 0 0 74966 41 0 0 25 0 1 0 479351076 56619008 13187 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13823 13187 603 41 0 13782 0
vsize: 55292
[startup+760.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13553 0 0 0 75966 42 0 0 25 0 1 0 479351076 58077184 13478 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14179 13478 603 41 0 14138 0
vsize: 56716
[startup+770.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 76965 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+780.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 77965 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+790.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 78965 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+800.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 79966 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+810.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 80966 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 81966 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+830.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 82966 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 83966 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+850.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 84967 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 85967 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+870.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 86967 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+880.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13782 0 0 0 87967 43 0 0 25 0 1 0 479351076 59011072 13707 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13707 603 41 0 14366 0
vsize: 57628
[startup+890.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 88967 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+900.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 89968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+910.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 90968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+920.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 91968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+930.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 92968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223728 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+940.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 93968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+950.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 94968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+960.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13783 0 0 0 95968 43 0 0 25 0 1 0 479351076 59011072 13708 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14407 13708 603 41 0 14366 0
vsize: 57628
[startup+970.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 13886 0 0 0 96968 43 0 0 25 0 1 0 479351076 59412480 13811 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14505 13811 603 41 0 14464 0
vsize: 58020
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 14242 0 0 0 97967 44 0 0 25 0 1 0 479351076 60891136 14167 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14866 14167 603 41 0 14825 0
vsize: 59464
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 14654 0 0 0 98966 45 0 0 25 0 1 0 479351076 62500864 14579 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14579 603 41 0 15218 0
vsize: 61036
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15078 0 0 0 99965 47 0 0 25 0 1 0 479351076 64237568 15003 4294967295 134512640 134672761 3221224624 3221223728 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15683 15003 603 41 0 15642 0
vsize: 62732
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15482 0 0 0 100964 48 0 0 25 0 1 0 479351076 65970176 15407 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16106 15408 603 41 0 16065 0
vsize: 64424
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 101963 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 102964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 103964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 104964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 105964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 106964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 107964 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 108965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 109965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 110965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 111965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 112965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 113965 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 114966 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 115966 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 116966 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 117966 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 118966 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29169
Raw data (stat): 29112 (minisat+) R 29111 26298 26297 0 -1 0 15769 0 0 0 119967 49 0 0 25 0 1 0 479351076 67039232 15694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15694 603 41 0 16326 0
vsize: 65468
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29169
Raw data (stat): 29112 (minisat+) Z 29111 26298 26297 0 -1 12 15772 0 0 0 119967 52 0 0 25 0 1 0 479351076 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.67
CPU system time (s): 0.52192
CPU usage (%): 100.012
Max. virtual memory (Kb): 65468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####