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/submitted/manquinho/logic-synthesis/normalized-count.b.opb
MD5SUM	f13ba9c997276002b5bd6db1f679a6f5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24
Optimality of the best value was proved	NO
Number of terms in the objective function	467
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	467
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	467
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	466
Total number of constraints	694
Number of constraints which are clauses	694
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	78
Trace number 4834

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        914200 kB
Buffers:         33932 kB
Cached:          66756 kB
SwapCached:        564 kB
Active:          49340 kB
Inactive:        54792 kB
HighTotal:      131008 kB
HighFree:        60312 kB
LowTotal:       903652 kB
LowFree:        853888 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10748 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:49:12 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 581 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 694 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     694    17335 |     231       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17658     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19647    61494 |    6549       0        0     nan |  0.000 % |
c |       101 |   19445    61064 |    7203      89     3487    39.2 |  1.289 % |
c |       257 |   19445    61064 |    7924     245     9767    39.9 |  1.289 % |
c |       484 |   19445    61064 |    8716     472    31182    66.1 |  1.289 % |
c |       822 |   19445    61064 |    9588     810    74289    91.7 |  1.289 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1166 |   19469    61124 |    6489    1154   114761    99.4 |  1.289 % |
c |      1267 |   19469    61124 |    7137    1255   124729    99.4 |  1.311 % |
c |      1418 |   19469    61124 |    7851    1406   135092    96.1 |  1.311 % |
c |      1643 |   19454    61093 |    8636    1630   144695    88.8 |  1.373 % |
c |      1982 |   19454    61093 |    9500    1969   167082    84.9 |  1.373 % |
c |      2489 |   19454    61093 |   10450    2476   202121    81.6 |  1.373 % |
c |      3249 |   19454    61093 |   11495    3236   266695    82.4 |  1.373 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4035 |   19146    60373 |    6382    3959   296660    74.9 |  1.373 % |
c |      4135 |   19146    60373 |    7020    4059   303620    74.8 |  3.040 % |
c |      4285 |   19146    60373 |    7722    4209   313768    74.5 |  3.040 % |
c |      4510 |   19146    60373 |    8494    4434   325949    73.5 |  3.040 % |
c |      4848 |   19101    60270 |    9343    4770   341762    71.6 |  3.265 % |
c |      5355 |   19101    60270 |   10278    5277   366069    69.4 |  3.265 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5912 |   19115    60306 |    6371    5834   399340    68.5 |  3.265 % |
c |      6015 |   19115    60306 |    7008    5937   406999    68.6 |  3.278 % |
c |      6166 |   19100    60273 |    7708    6087   413641    68.0 |  3.348 % |
c |      6393 |   19100    60273 |    8479    6314   428942    67.9 |  3.348 % |
c |      6730 |   19100    60273 |    9327    6651   444512    66.8 |  3.348 % |
c |      7237 |   19100    60273 |   10260    7158   469534    65.6 |  3.348 % |
c |      7996 |   19100    60273 |   11286    7917   505459    63.8 |  3.348 % |
c |      9135 |   19100    60273 |   12415    9056   570860    63.0 |  3.348 % |
c |     10843 |   19100    60273 |   13656   10764   693406    64.4 |  3.348 % |
c |     13407 |   19100    60273 |   15022   13328   804791    60.4 |  3.348 % |
c |     17252 |   19100    60273 |   16524    9015   600405    66.6 |  3.348 % |
c |     23019 |   19100    60273 |   18177   14782  1097525    74.2 |  3.348 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27329 |   19083    60230 |    6361   19088  1430862    75.0 |  3.348 % |
c |     27430 |   19083    60230 |    6997    4873   311386    63.9 |  3.486 % |
c |     27581 |   19083    60230 |    7696    5024   318135    63.3 |  3.486 % |
c |     27807 |   18979    59989 |    8466    5235   330614    63.2 |  4.006 % |
c |     28145 |   18979    59989 |    9313    5573   345816    62.1 |  4.006 % |
c |     28651 |   18979    59989 |   10244    6079   368825    60.7 |  4.006 % |
c |     29411 |   18979    59989 |   11268    6839   414066    60.5 |  4.006 % |
c |     30551 |   18979    59989 |   12395    7979   477554    59.9 |  4.006 % |
c |     32259 |   18979    59989 |   13635    9687   588178    60.7 |  4.006 % |
c |     34821 |   18979    59989 |   14998   12249   741563    60.5 |  4.006 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38313 |   18993    60024 |    6331   15741   911578    57.9 |  4.006 % |
c |     38413 |   18993    60024 |    6964    4036   167384    41.5 |  4.018 % |
c |     38563 |   18993    60024 |    7660    4186   172590    41.2 |  4.018 % |
c |     38791 |   18993    60024 |    8426    4414   179565    40.7 |  4.018 % |
c |     39128 |   18993    60024 |    9269    4751   186680    39.3 |  4.018 % |
c |     39638 |   18993    60024 |   10196    5261   201797    38.4 |  4.018 % |
c |     40398 |   18993    60024 |   11215    6021   227834    37.8 |  4.018 % |
c |     41537 |   18993    60024 |   12337    7160   281186    39.3 |  4.018 % |
c |     43245 |   18993    60024 |   13571    8868   361128    40.7 |  4.018 % |
c |     45807 |   18993    60024 |   14928   11430   472504    41.3 |  4.018 % |
c |     49652 |   18993    60024 |   16420   15275   637818    41.8 |  4.018 % |
c |     55420 |   18993    60024 |   18063   12289   467797    38.1 |  4.018 % |
c |     64073 |   18993    60024 |   19869   11350   439625    38.7 |  4.018 % |
c |     77047 |   18993    60024 |   21856   13267   640705    48.3 |  4.018 % |
c |     96509 |   18993    60024 |   24041   21195   872945    41.2 |  4.018 % |
c |    125704 |   18993    60024 |   26446   25028  1205586    48.2 |  4.018 % |
c |    169495 |   18978    59993 |   29090   27177  1048115    38.6 |  4.072 % |
c |    235179 |   18978    59993 |   31999   25525  1312075    51.4 |  4.072 % |
c |    333706 |   18978    59993 |   35199   32412  1339748    41.3 |  4.072 % |
c |    481495 |   18978    59993 |   38719   33150  1162730    35.1 |  4.072 % |
#### 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.88 0.95 0.90 2/54 32683
Raw data (stat): 32683 (runsolver) R 32682 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420615143 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.0005 s]
Raw data (loadavg): 0.90 0.96 0.90 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 1880 0 0 0 992 7 0 0 25 0 1 0 420615143 9785344 1855 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2389 1855 603 41 0 2348 0
vsize: 9556
[startup+20.0009 s]
Raw data (loadavg): 0.91 0.96 0.90 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 2287 0 0 0 1990 8 0 0 25 0 1 0 420615143 11395072 2262 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2782 2262 603 41 0 2741 0
vsize: 11128
[startup+30.0015 s]
Raw data (loadavg): 0.92 0.96 0.90 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 2587 0 0 0 2989 9 0 0 25 0 1 0 420615143 12607488 2562 4294967295 134512640 134672761 3221224640 3221223596 1075350178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2562 603 41 0 3037 0
vsize: 12312
[startup+40.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 2963 0 0 0 3986 11 0 0 25 0 1 0 420615143 14192640 2938 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3465 2938 603 41 0 3424 0
vsize: 13860
[startup+50.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 4986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+60.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 5986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+70.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 6985 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+80.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 7985 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+90.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 8986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 9986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 10986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3049 0 0 0 11986 12 0 0 25 0 1 0 420615143 14573568 3024 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3024 603 41 0 3517 0
vsize: 14232
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3052 0 0 0 12986 12 0 0 25 0 1 0 420615143 14573568 3027 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3027 603 41 0 3517 0
vsize: 14232
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3052 0 0 0 13986 12 0 0 25 0 1 0 420615143 14573568 3027 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3027 603 41 0 3517 0
vsize: 14232
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3052 0 0 0 14987 12 0 0 25 0 1 0 420615143 14573568 3027 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3027 603 41 0 3517 0
vsize: 14232
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3053 0 0 0 15987 12 0 0 25 0 1 0 420615143 14573568 3028 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3028 603 41 0 3517 0
vsize: 14232
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3053 0 0 0 16987 12 0 0 25 0 1 0 420615143 14573568 3028 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3558 3028 603 41 0 3517 0
vsize: 14232
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3070 0 0 0 17987 12 0 0 25 0 1 0 420615143 14737408 3045 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3598 3045 603 41 0 3557 0
vsize: 14392
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3071 0 0 0 18987 12 0 0 25 0 1 0 420615143 14737408 3046 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3598 3046 603 41 0 3557 0
vsize: 14392
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3071 0 0 0 19988 12 0 0 25 0 1 0 420615143 14737408 3046 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3598 3046 603 41 0 3557 0
vsize: 14392
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3178 0 0 0 20987 12 0 0 25 0 1 0 420615143 15138816 3153 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3153 603 41 0 3655 0
vsize: 14784
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3235 0 0 0 21987 13 0 0 25 0 1 0 420615143 15405056 3210 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3210 603 41 0 3720 0
vsize: 15044
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3244 0 0 0 22987 13 0 0 25 0 1 0 420615143 15405056 3219 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3219 603 41 0 3720 0
vsize: 15044
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3252 0 0 0 23987 13 0 0 25 0 1 0 420615143 15405056 3227 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3227 603 41 0 3720 0
vsize: 15044
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3366 0 0 0 24987 13 0 0 25 0 1 0 420615143 15945728 3341 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3893 3341 603 41 0 3852 0
vsize: 15572
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3408 0 0 0 25987 13 0 0 25 0 1 0 420615143 16101376 3383 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3931 3383 603 41 0 3890 0
vsize: 15724
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3415 0 0 0 26987 13 0 0 25 0 1 0 420615143 16101376 3390 4294967295 134512640 134672761 3221224640 3221223792 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3931 3390 603 41 0 3890 0
vsize: 15724
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3415 0 0 0 27988 13 0 0 25 0 1 0 420615143 16101376 3390 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3931 3390 603 41 0 3890 0
vsize: 15724
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3416 0 0 0 28988 13 0 0 25 0 1 0 420615143 16101376 3391 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3931 3391 603 41 0 3890 0
vsize: 15724
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3428 0 0 0 29988 13 0 0 25 0 1 0 420615143 16248832 3403 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3967 3403 603 41 0 3926 0
vsize: 15868
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3439 0 0 0 30988 13 0 0 25 0 1 0 420615143 16248832 3414 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3967 3414 603 41 0 3926 0
vsize: 15868
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3442 0 0 0 31988 13 0 0 25 0 1 0 420615143 16248832 3417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3967 3417 603 41 0 3926 0
vsize: 15868
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3454 0 0 0 32989 13 0 0 25 0 1 0 420615143 16412672 3429 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3429 603 41 0 3966 0
vsize: 16028
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3460 0 0 0 33989 13 0 0 25 0 1 0 420615143 16412672 3435 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3435 603 41 0 3966 0
vsize: 16028
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3467 0 0 0 34989 13 0 0 25 0 1 0 420615143 16412672 3442 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3442 603 41 0 3966 0
vsize: 16028
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3470 0 0 0 35989 13 0 0 25 0 1 0 420615143 16412672 3445 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3445 603 41 0 3966 0
vsize: 16028
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3476 0 0 0 36989 13 0 0 25 0 1 0 420615143 16412672 3451 4294967295 134512640 134672761 3221224640 3221223808 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3451 603 41 0 3966 0
vsize: 16028
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3493 0 0 0 37989 13 0 0 25 0 1 0 420615143 16609280 3468 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4055 3468 603 41 0 4014 0
vsize: 16220
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3494 0 0 0 38990 13 0 0 25 0 1 0 420615143 16609280 3469 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4055 3469 603 41 0 4014 0
vsize: 16220
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3547 0 0 0 39990 13 0 0 25 0 1 0 420615143 16744448 3522 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4088 3522 603 41 0 4047 0
vsize: 16352
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3547 0 0 0 40990 13 0 0 25 0 1 0 420615143 16744448 3522 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4088 3522 603 41 0 4047 0
vsize: 16352
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3547 0 0 0 41990 13 0 0 25 0 1 0 420615143 16744448 3522 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4088 3522 603 41 0 4047 0
vsize: 16352
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3572 0 0 0 42990 14 0 0 25 0 1 0 420615143 16879616 3547 4294967295 134512640 134672761 3221224640 3221223840 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4121 3547 603 41 0 4080 0
vsize: 16484
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3752 0 0 0 43990 14 0 0 25 0 1 0 420615143 17678336 3727 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4316 3727 603 41 0 4275 0
vsize: 17264
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3831 0 0 0 44989 15 0 0 25 0 1 0 420615143 17940480 3806 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3806 603 41 0 4339 0
vsize: 17520
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3831 0 0 0 45990 15 0 0 25 0 1 0 420615143 17940480 3806 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3806 603 41 0 4339 0
vsize: 17520
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3831 0 0 0 46990 15 0 0 25 0 1 0 420615143 17940480 3806 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3806 603 41 0 4339 0
vsize: 17520
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3841 0 0 0 47990 15 0 0 25 0 1 0 420615143 17940480 3816 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3816 603 41 0 4339 0
vsize: 17520
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3855 0 0 0 48990 15 0 0 25 0 1 0 420615143 18096128 3830 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4418 3830 603 41 0 4377 0
vsize: 17672
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3855 0 0 0 49990 15 0 0 25 0 1 0 420615143 18096128 3830 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4418 3830 603 41 0 4377 0
vsize: 17672
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3856 0 0 0 50990 15 0 0 25 0 1 0 420615143 18096128 3831 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4418 3831 603 41 0 4377 0
vsize: 17672
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3884 0 0 0 51990 15 0 0 25 0 1 0 420615143 18259968 3859 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4458 3859 603 41 0 4417 0
vsize: 17832
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 3897 0 0 0 52990 15 0 0 25 0 1 0 420615143 18259968 3872 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4458 3872 603 41 0 4417 0
vsize: 17832
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4030 0 0 0 53990 15 0 0 25 0 1 0 420615143 18952192 4005 4294967295 134512640 134672761 3221224640 3221223808 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 4005 603 41 0 4586 0
vsize: 18508
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4032 0 0 0 54990 15 0 0 25 0 1 0 420615143 18952192 4007 4294967295 134512640 134672761 3221224640 3221223808 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 4007 603 41 0 4586 0
vsize: 18508
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4038 0 0 0 55990 15 0 0 25 0 1 0 420615143 18952192 4013 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 4013 603 41 0 4586 0
vsize: 18508
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4047 0 0 0 56990 15 0 0 25 0 1 0 420615143 19111936 4022 4294967295 134512640 134672761 3221224640 3221223840 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4666 4022 603 41 0 4625 0
vsize: 18664
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4072 0 0 0 57990 15 0 0 25 0 1 0 420615143 19111936 4047 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4666 4047 603 41 0 4625 0
vsize: 18664
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4083 0 0 0 58991 15 0 0 25 0 1 0 420615143 19308544 4058 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4058 603 41 0 4673 0
vsize: 18856
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4083 0 0 0 59991 15 0 0 25 0 1 0 420615143 19308544 4058 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4058 603 41 0 4673 0
vsize: 18856
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4083 0 0 0 60991 15 0 0 25 0 1 0 420615143 19308544 4058 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4058 603 41 0 4673 0
vsize: 18856
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4085 0 0 0 61991 15 0 0 25 0 1 0 420615143 19308544 4060 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4060 603 41 0 4673 0
vsize: 18856
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4085 0 0 0 62991 15 0 0 25 0 1 0 420615143 19308544 4060 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4060 603 41 0 4673 0
vsize: 18856
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4085 0 0 0 63992 15 0 0 25 0 1 0 420615143 19308544 4060 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4060 603 41 0 4673 0
vsize: 18856
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4085 0 0 0 64992 15 0 0 25 0 1 0 420615143 19308544 4060 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4060 603 41 0 4673 0
vsize: 18856
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4085 0 0 0 65992 15 0 0 25 0 1 0 420615143 19308544 4060 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4060 603 41 0 4673 0
vsize: 18856
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4095 0 0 0 66992 15 0 0 25 0 1 0 420615143 19308544 4070 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4070 603 41 0 4673 0
vsize: 18856
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4095 0 0 0 67992 15 0 0 25 0 1 0 420615143 19308544 4070 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4070 603 41 0 4673 0
vsize: 18856
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4095 0 0 0 68992 15 0 0 25 0 1 0 420615143 19308544 4070 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4070 603 41 0 4673 0
vsize: 18856
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4095 0 0 0 69993 15 0 0 25 0 1 0 420615143 19308544 4070 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4714 4070 603 41 0 4673 0
vsize: 18856
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4126 0 0 0 70993 15 0 0 25 0 1 0 420615143 19472384 4101 4294967295 134512640 134672761 3221224640 3221223804 134560077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4101 603 41 0 4713 0
vsize: 19016
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4127 0 0 0 71993 16 0 0 25 0 1 0 420615143 19472384 4102 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4102 603 41 0 4713 0
vsize: 19016
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4127 0 0 0 72993 16 0 0 25 0 1 0 420615143 19472384 4102 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4102 603 41 0 4713 0
vsize: 19016
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4132 0 0 0 73993 16 0 0 25 0 1 0 420615143 19472384 4107 4294967295 134512640 134672761 3221224640 3221223824 134558382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4107 603 41 0 4713 0
vsize: 19016
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4132 0 0 0 74993 16 0 0 25 0 1 0 420615143 19472384 4107 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4107 603 41 0 4713 0
vsize: 19016
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4133 0 0 0 75994 16 0 0 25 0 1 0 420615143 19472384 4108 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4754 4108 603 41 0 4713 0
vsize: 19016
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4154 0 0 0 76993 16 0 0 25 0 1 0 420615143 19668992 4129 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4802 4129 603 41 0 4761 0
vsize: 19208
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 77992 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 78992 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 79993 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 80993 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 81993 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223824 134558354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 82993 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4157 0 0 0 83993 16 0 0 25 0 1 0 420615143 19668992 4132 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4132 603 41 0 4761 0
vsize: 19208
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4179 0 0 0 84994 16 0 0 25 0 1 0 420615143 19668992 4154 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4154 603 41 0 4761 0
vsize: 19208
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4184 0 0 0 85994 16 0 0 25 0 1 0 420615143 19668992 4159 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4159 603 41 0 4761 0
vsize: 19208
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4190 0 0 0 86994 16 0 0 25 0 1 0 420615143 19668992 4165 4294967295 134512640 134672761 3221224640 3221223744 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4165 603 41 0 4761 0
vsize: 19208
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4190 0 0 0 87994 16 0 0 25 0 1 0 420615143 19668992 4165 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4165 603 41 0 4761 0
vsize: 19208
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4190 0 0 0 88994 16 0 0 25 0 1 0 420615143 19668992 4165 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4165 603 41 0 4761 0
vsize: 19208
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4201 0 0 0 89995 16 0 0 25 0 1 0 420615143 19865600 4176 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4176 603 41 0 4809 0
vsize: 19400
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4205 0 0 0 90995 16 0 0 25 0 1 0 420615143 19865600 4180 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4180 603 41 0 4809 0
vsize: 19400
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4207 0 0 0 91995 16 0 0 25 0 1 0 420615143 19865600 4182 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4182 603 41 0 4809 0
vsize: 19400
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4207 0 0 0 92995 16 0 0 25 0 1 0 420615143 19865600 4182 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4182 603 41 0 4809 0
vsize: 19400
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4207 0 0 0 93995 16 0 0 25 0 1 0 420615143 19865600 4182 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4182 603 41 0 4809 0
vsize: 19400
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4207 0 0 0 94995 16 0 0 25 0 1 0 420615143 19865600 4182 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4182 603 41 0 4809 0
vsize: 19400
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4207 0 0 0 95996 16 0 0 25 0 1 0 420615143 19865600 4182 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4182 603 41 0 4809 0
vsize: 19400
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4216 0 0 0 96996 16 0 0 25 0 1 0 420615143 19865600 4191 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4191 603 41 0 4809 0
vsize: 19400
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4216 0 0 0 97996 16 0 0 25 0 1 0 420615143 19865600 4191 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4191 603 41 0 4809 0
vsize: 19400
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4216 0 0 0 98996 16 0 0 25 0 1 0 420615143 19865600 4191 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4191 603 41 0 4809 0
vsize: 19400
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4216 0 0 0 99996 16 0 0 25 0 1 0 420615143 19865600 4191 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4191 603 41 0 4809 0
vsize: 19400
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4219 0 0 0 100996 16 0 0 25 0 1 0 420615143 19865600 4194 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4194 603 41 0 4809 0
vsize: 19400
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4229 0 0 0 101997 16 0 0 25 0 1 0 420615143 19865600 4204 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4204 603 41 0 4809 0
vsize: 19400
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4229 0 0 0 102997 16 0 0 25 0 1 0 420615143 19865600 4204 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4204 603 41 0 4809 0
vsize: 19400
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4229 0 0 0 103997 16 0 0 25 0 1 0 420615143 19865600 4204 4294967295 134512640 134672761 3221224640 3221223800 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4204 603 41 0 4809 0
vsize: 19400
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4239 0 0 0 104997 16 0 0 25 0 1 0 420615143 20062208 4214 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4214 603 41 0 4857 0
vsize: 19592
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4241 0 0 0 105997 16 0 0 25 0 1 0 420615143 20062208 4216 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4216 603 41 0 4857 0
vsize: 19592
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4241 0 0 0 106997 16 0 0 25 0 1 0 420615143 20062208 4216 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4216 603 41 0 4857 0
vsize: 19592
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4242 0 0 0 107998 16 0 0 25 0 1 0 420615143 20062208 4217 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4217 603 41 0 4857 0
vsize: 19592
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4243 0 0 0 108998 16 0 0 25 0 1 0 420615143 20062208 4218 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4218 603 41 0 4857 0
vsize: 19592
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4243 0 0 0 109998 16 0 0 25 0 1 0 420615143 20062208 4218 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4218 603 41 0 4857 0
vsize: 19592
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4243 0 0 0 110998 16 0 0 25 0 1 0 420615143 20062208 4218 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4218 603 41 0 4857 0
vsize: 19592
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4256 0 0 0 111998 16 0 0 25 0 1 0 420615143 20062208 4231 4294967295 134512640 134672761 3221224640 3221223764 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4898 4231 603 41 0 4857 0
vsize: 19592
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4260 0 0 0 112997 16 0 0 25 0 1 0 420615143 20062208 4235 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4235 603 41 0 4857 0
vsize: 19592
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4260 0 0 0 113997 16 0 0 25 0 1 0 420615143 20062208 4235 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4235 603 41 0 4857 0
vsize: 19592
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4260 0 0 0 114998 16 0 0 25 0 1 0 420615143 20062208 4235 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4235 603 41 0 4857 0
vsize: 19592
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4260 0 0 0 115998 16 0 0 25 0 1 0 420615143 20062208 4235 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4235 603 41 0 4857 0
vsize: 19592
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4270 0 0 0 116998 16 0 0 25 0 1 0 420615143 20062208 4245 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4245 603 41 0 4857 0
vsize: 19592
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4278 0 0 0 117998 16 0 0 25 0 1 0 420615143 20062208 4253 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4253 603 41 0 4857 0
vsize: 19592
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4294 0 0 0 118998 16 0 0 25 0 1 0 420615143 20258816 4269 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4269 603 41 0 4905 0
vsize: 19784
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32683
Raw data (stat): 32683 (minisat+) R 32682 30854 30853 0 -1 0 4295 0 0 0 119999 16 0 0 25 0 1 0 420615143 20258816 4270 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4946 4270 603 41 0 4905 0
vsize: 19784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32683
Raw data (stat): 32683 (minisat+) Z 32682 30854 30853 0 -1 12 4298 0 0 0 119999 17 0 0 25 0 1 0 420615143 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.04
CPU time (s): 1200.17
CPU user time (s): 1199.99
CPU system time (s): 0.177972
CPU usage (%): 100.011
Max. virtual memory (Kb): 19784
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####