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 5798

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 01:50:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4201 boxname=wulflinc15 idbench=65 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f13ba9c997276002b5bd6db1f679a6f5  /oldhome/oroussel/tmp/wulflinc15/normalized-count.b.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-count.b.opb /oldhome/oroussel/tmp/wulflinc15/normalized-count.b.opb
IDLAUNCH: 4201
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        899376 kB
Buffers:         36380 kB
Cached:          77348 kB
SwapCached:       2144 kB
Active:          63916 kB
Inactive:        54812 kB
HighTotal:      131008 kB
HighFree:        49756 kB
LowTotal:       903652 kB
LowFree:        849620 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11028 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:10:27 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 4201 7 1200.09 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.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (runsolver) R 3516 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422539892 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 1872 0 0 0 992 5 0 0 25 0 1 0 422539892 9707520 1846 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2370 1846 603 41 0 2329 0
vsize: 9480
[startup+20.0009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 2300 0 0 0 1989 8 0 0 25 0 1 0 422539892 11448320 2274 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2795 2274 603 41 0 2754 0
vsize: 11180
[startup+30.0009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 2566 0 0 0 2988 9 0 0 25 0 1 0 422539892 12525568 2540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3058 2540 603 41 0 3017 0
vsize: 12232
[startup+40.0006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 2973 0 0 0 3985 11 0 0 25 0 1 0 422539892 14249984 2947 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3479 2947 603 41 0 3438 0
vsize: 13916
[startup+50.0017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 4985 11 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+60.0012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 5985 11 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+70.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 6984 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+80.0022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 7985 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+90.0017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 8985 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+100.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 9985 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 10985 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3022 0 0 0 11985 12 0 0 25 0 1 0 422539892 14503936 2996 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2996 603 41 0 3500 0
vsize: 14164
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3025 0 0 0 12985 12 0 0 25 0 1 0 422539892 14503936 2999 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2999 603 41 0 3500 0
vsize: 14164
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3025 0 0 0 13985 12 0 0 25 0 1 0 422539892 14503936 2999 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2999 603 41 0 3500 0
vsize: 14164
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3025 0 0 0 14986 12 0 0 25 0 1 0 422539892 14503936 2999 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 2999 603 41 0 3500 0
vsize: 14164
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3026 0 0 0 15986 12 0 0 25 0 1 0 422539892 14503936 3000 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 3000 603 41 0 3500 0
vsize: 14164
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3026 0 0 0 16986 12 0 0 25 0 1 0 422539892 14503936 3000 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3541 3000 603 41 0 3500 0
vsize: 14164
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3049 0 0 0 17986 12 0 0 25 0 1 0 422539892 14667776 3023 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3581 3023 603 41 0 3540 0
vsize: 14324
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3050 0 0 0 18986 12 0 0 25 0 1 0 422539892 14667776 3024 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3581 3024 603 41 0 3540 0
vsize: 14324
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3050 0 0 0 19986 12 0 0 25 0 1 0 422539892 14667776 3024 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3581 3024 603 41 0 3540 0
vsize: 14324
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3136 0 0 0 20986 12 0 0 25 0 1 0 422539892 14934016 3110 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3646 3110 603 41 0 3605 0
vsize: 14584
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3215 0 0 0 21986 12 0 0 25 0 1 0 422539892 15339520 3189 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3189 603 41 0 3704 0
vsize: 14980
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3218 0 0 0 22986 13 0 0 25 0 1 0 422539892 15339520 3192 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3192 603 41 0 3704 0
vsize: 14980
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3232 0 0 0 23986 13 0 0 25 0 1 0 422539892 15339520 3206 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3206 603 41 0 3704 0
vsize: 14980
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3341 0 0 0 24986 13 0 0 25 0 1 0 422539892 15876096 3315 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3876 3315 603 41 0 3835 0
vsize: 15504
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3387 0 0 0 25986 13 0 0 25 0 1 0 422539892 16035840 3361 4294967295 134512640 134672761 3221224560 3221223696 134560720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3361 603 41 0 3874 0
vsize: 15660
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3394 0 0 0 26986 13 0 0 25 0 1 0 422539892 16035840 3368 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3368 603 41 0 3874 0
vsize: 15660
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3394 0 0 0 27986 13 0 0 25 0 1 0 422539892 16035840 3368 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3368 603 41 0 3874 0
vsize: 15660
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3395 0 0 0 28986 13 0 0 25 0 1 0 422539892 16035840 3369 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3369 603 41 0 3874 0
vsize: 15660
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3407 0 0 0 29986 13 0 0 25 0 1 0 422539892 16183296 3381 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3381 603 41 0 3910 0
vsize: 15804
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3417 0 0 0 30987 13 0 0 25 0 1 0 422539892 16183296 3391 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3391 603 41 0 3910 0
vsize: 15804
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3421 0 0 0 31987 13 0 0 25 0 1 0 422539892 16183296 3395 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3395 603 41 0 3910 0
vsize: 15804
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3432 0 0 0 32987 13 0 0 25 0 1 0 422539892 16347136 3406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3991 3406 603 41 0 3950 0
vsize: 15964
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3438 0 0 0 33987 13 0 0 25 0 1 0 422539892 16347136 3412 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3991 3412 603 41 0 3950 0
vsize: 15964
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3445 0 0 0 34987 13 0 0 25 0 1 0 422539892 16347136 3419 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3419 603 41 0 3950 0
vsize: 15964
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3448 0 0 0 35987 14 0 0 25 0 1 0 422539892 16347136 3422 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3422 603 41 0 3950 0
vsize: 15964
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3454 0 0 0 36986 14 0 0 25 0 1 0 422539892 16347136 3428 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3428 603 41 0 3950 0
vsize: 15964
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3462 0 0 0 37986 14 0 0 25 0 1 0 422539892 16347136 3436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3436 603 41 0 3950 0
vsize: 15964
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3472 0 0 0 38985 15 0 0 25 0 1 0 422539892 16543744 3446 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3446 603 41 0 3998 0
vsize: 16156
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3490 0 0 0 39985 15 0 0 25 0 1 0 422539892 16543744 3464 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3464 603 41 0 3998 0
vsize: 16156
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3523 0 0 0 40985 15 0 0 25 0 1 0 422539892 16674816 3497 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4071 3497 603 41 0 4030 0
vsize: 16284
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3523 0 0 0 41984 16 0 0 25 0 1 0 422539892 16674816 3497 4294967295 134512640 134672761 3221224560 3221223760 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4071 3497 603 41 0 4030 0
vsize: 16284
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3546 0 0 0 42984 16 0 0 25 0 1 0 422539892 16809984 3520 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3520 603 41 0 4063 0
vsize: 16416
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3687 0 0 0 43984 16 0 0 25 0 1 0 422539892 17350656 3661 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3661 603 41 0 4195 0
vsize: 16944
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3805 0 0 0 44983 17 0 0 25 0 1 0 422539892 17887232 3779 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3779 603 41 0 4326 0
vsize: 17468
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3805 0 0 0 45983 17 0 0 25 0 1 0 422539892 17887232 3779 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3779 603 41 0 4326 0
vsize: 17468
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3805 0 0 0 46982 17 0 0 25 0 1 0 422539892 17887232 3779 4294967295 134512640 134672761 3221224560 3221223744 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3779 603 41 0 4326 0
vsize: 17468
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3815 0 0 0 47982 18 0 0 25 0 1 0 422539892 17887232 3789 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3789 603 41 0 4326 0
vsize: 17468
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3829 0 0 0 48981 18 0 0 25 0 1 0 422539892 18026496 3803 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4401 3803 603 41 0 4360 0
vsize: 17604
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3829 0 0 0 49981 19 0 0 25 0 1 0 422539892 18026496 3803 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4401 3803 603 41 0 4360 0
vsize: 17604
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3830 0 0 0 50980 19 0 0 25 0 1 0 422539892 18026496 3804 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4401 3804 603 41 0 4360 0
vsize: 17604
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3858 0 0 0 51980 19 0 0 25 0 1 0 422539892 18190336 3832 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4441 3832 603 41 0 4400 0
vsize: 17764
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 3872 0 0 0 52980 20 0 0 25 0 1 0 422539892 18190336 3846 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4441 3846 603 41 0 4400 0
vsize: 17764
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4004 0 0 0 53979 20 0 0 25 0 1 0 422539892 18882560 3978 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4610 3978 603 41 0 4569 0
vsize: 18440
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4009 0 0 0 54978 21 0 0 25 0 1 0 422539892 18882560 3983 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4610 3983 603 41 0 4569 0
vsize: 18440
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4015 0 0 0 55978 21 0 0 25 0 1 0 422539892 18882560 3989 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4610 3989 603 41 0 4569 0
vsize: 18440
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3517
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4023 0 0 0 56978 21 0 0 25 0 1 0 422539892 19046400 3997 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4650 3997 603 41 0 4609 0
vsize: 18600
[startup+580.015 s]
Raw data (loadavg): 1.07 0.99 0.93 3/58 3521
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4047 0 0 0 57972 26 0 0 25 0 1 0 422539892 19046400 4021 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4650 4021 603 41 0 4609 0
vsize: 18600
[startup+590.014 s]
Raw data (loadavg): 1.14 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4058 0 0 0 58972 26 0 0 25 0 1 0 422539892 19238912 4032 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4032 603 41 0 4656 0
vsize: 18788
[startup+600.015 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4058 0 0 0 59972 26 0 0 25 0 1 0 422539892 19238912 4032 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4032 603 41 0 4656 0
vsize: 18788
[startup+610.014 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4058 0 0 0 60972 26 0 0 25 0 1 0 422539892 19238912 4032 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4032 603 41 0 4656 0
vsize: 18788
[startup+620.015 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4060 0 0 0 61973 26 0 0 25 0 1 0 422539892 19238912 4034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4034 603 41 0 4656 0
vsize: 18788
[startup+630.015 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4060 0 0 0 62973 26 0 0 25 0 1 0 422539892 19238912 4034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4034 603 41 0 4656 0
vsize: 18788
[startup+640.015 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 3570
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4060 0 0 0 63973 26 0 0 25 0 1 0 422539892 19238912 4034 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4034 603 41 0 4656 0
vsize: 18788
[startup+650.016 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4060 0 0 0 64973 26 0 0 25 0 1 0 422539892 19238912 4034 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4034 603 41 0 4656 0
vsize: 18788
[startup+660.016 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4060 0 0 0 65973 26 0 0 25 0 1 0 422539892 19238912 4034 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4034 603 41 0 4656 0
vsize: 18788
[startup+670.016 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4064 0 0 0 66974 26 0 0 25 0 1 0 422539892 19238912 4038 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4038 603 41 0 4656 0
vsize: 18788
[startup+680.016 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4066 0 0 0 67974 26 0 0 25 0 1 0 422539892 19238912 4040 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4040 603 41 0 4656 0
vsize: 18788
[startup+690.016 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4066 0 0 0 68974 26 0 0 25 0 1 0 422539892 19238912 4040 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4040 603 41 0 4656 0
vsize: 18788
[startup+700.017 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4066 0 0 0 69974 26 0 0 25 0 1 0 422539892 19238912 4040 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4040 603 41 0 4656 0
vsize: 18788
[startup+710.017 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4096 0 0 0 70974 26 0 0 25 0 1 0 422539892 19402752 4070 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4070 603 41 0 4696 0
vsize: 18948
[startup+720.017 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4099 0 0 0 71974 27 0 0 25 0 1 0 422539892 19402752 4073 4294967295 134512640 134672761 3221224560 3221223744 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4073 603 41 0 4696 0
vsize: 18948
[startup+730.016 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4100 0 0 0 72974 27 0 0 25 0 1 0 422539892 19402752 4074 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4074 603 41 0 4696 0
vsize: 18948
[startup+740.016 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4106 0 0 0 73974 27 0 0 25 0 1 0 422539892 19402752 4080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4080 603 41 0 4696 0
vsize: 18948
[startup+750.016 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4106 0 0 0 74975 27 0 0 25 0 1 0 422539892 19402752 4080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4080 603 41 0 4696 0
vsize: 18948
[startup+760.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4108 0 0 0 75975 27 0 0 25 0 1 0 422539892 19402752 4082 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4082 603 41 0 4696 0
vsize: 18948
[startup+770.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4129 0 0 0 76974 27 0 0 25 0 1 0 422539892 19566592 4103 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4103 603 41 0 4736 0
vsize: 19108
[startup+780.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 77974 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+790.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 78975 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+800.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 79975 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+810.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 80975 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+820.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 81975 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+830.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 82975 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+840.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4133 0 0 0 83976 27 0 0 25 0 1 0 422539892 19566592 4107 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4107 603 41 0 4736 0
vsize: 19108
[startup+850.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4145 0 0 0 84976 27 0 0 25 0 1 0 422539892 19566592 4119 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4119 603 41 0 4736 0
vsize: 19108
[startup+860.017 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4159 0 0 0 85976 27 0 0 25 0 1 0 422539892 19566592 4133 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4133 603 41 0 4736 0
vsize: 19108
[startup+870.017 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4162 0 0 0 86976 27 0 0 25 0 1 0 422539892 19566592 4136 4294967295 134512640 134672761 3221224560 3221223632 134553509 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4136 603 41 0 4736 0
vsize: 19108
[startup+880.017 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4166 0 0 0 87976 27 0 0 25 0 1 0 422539892 19566592 4140 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4140 603 41 0 4736 0
vsize: 19108
[startup+890.017 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4166 0 0 0 88976 27 0 0 25 0 1 0 422539892 19566592 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4140 603 41 0 4736 0
vsize: 19108
[startup+900.016 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4167 0 0 0 89976 27 0 0 25 0 1 0 422539892 19566592 4141 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4777 4141 603 41 0 4736 0
vsize: 19108
[startup+910.016 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4180 0 0 0 90977 27 0 0 25 0 1 0 422539892 19763200 4154 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4154 603 41 0 4784 0
vsize: 19300
[startup+920.017 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4182 0 0 0 91977 27 0 0 25 0 1 0 422539892 19763200 4156 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4156 603 41 0 4784 0
vsize: 19300
[startup+930.017 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 3572
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4183 0 0 0 92977 27 0 0 25 0 1 0 422539892 19763200 4157 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4157 603 41 0 4784 0
vsize: 19300
[startup+940.017 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4183 0 0 0 93977 27 0 0 25 0 1 0 422539892 19763200 4157 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4157 603 41 0 4784 0
vsize: 19300
[startup+950.018 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4183 0 0 0 94977 27 0 0 25 0 1 0 422539892 19763200 4157 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4157 603 41 0 4784 0
vsize: 19300
[startup+960.017 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4183 0 0 0 95977 27 0 0 25 0 1 0 422539892 19763200 4157 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4157 603 41 0 4784 0
vsize: 19300
[startup+970.017 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4192 0 0 0 96978 27 0 0 25 0 1 0 422539892 19763200 4166 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4166 603 41 0 4784 0
vsize: 19300
[startup+980.017 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4193 0 0 0 97978 27 0 0 25 0 1 0 422539892 19763200 4167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4167 603 41 0 4784 0
vsize: 19300
[startup+990.017 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4193 0 0 0 98978 27 0 0 25 0 1 0 422539892 19763200 4167 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4167 603 41 0 4784 0
vsize: 19300
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4193 0 0 0 99978 27 0 0 25 0 1 0 422539892 19763200 4167 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4167 603 41 0 4784 0
vsize: 19300
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4193 0 0 0 100978 27 0 0 25 0 1 0 422539892 19763200 4167 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4167 603 41 0 4784 0
vsize: 19300
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4196 0 0 0 101978 27 0 0 25 0 1 0 422539892 19763200 4170 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4170 603 41 0 4784 0
vsize: 19300
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4207 0 0 0 102978 27 0 0 25 0 1 0 422539892 19763200 4181 4294967295 134512640 134672761 3221224560 3221223616 1074972064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4181 603 41 0 4784 0
vsize: 19300
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4207 0 0 0 103978 27 0 0 25 0 1 0 422539892 19763200 4181 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4181 603 41 0 4784 0
vsize: 19300
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4216 0 0 0 104979 27 0 0 25 0 1 0 422539892 19959808 4190 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4190 603 41 0 4832 0
vsize: 19492
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4219 0 0 0 105979 27 0 0 25 0 1 0 422539892 19959808 4193 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4193 603 41 0 4832 0
vsize: 19492
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4220 0 0 0 106979 27 0 0 25 0 1 0 422539892 19959808 4194 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4194 603 41 0 4832 0
vsize: 19492
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4221 0 0 0 107979 27 0 0 25 0 1 0 422539892 19959808 4195 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4195 603 41 0 4832 0
vsize: 19492
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4223 0 0 0 108979 27 0 0 25 0 1 0 422539892 19959808 4197 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4197 603 41 0 4832 0
vsize: 19492
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4223 0 0 0 109979 27 0 0 25 0 1 0 422539892 19959808 4197 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4197 603 41 0 4832 0
vsize: 19492
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4223 0 0 0 110980 27 0 0 25 0 1 0 422539892 19959808 4197 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4197 603 41 0 4832 0
vsize: 19492
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4223 0 0 0 111980 27 0 0 25 0 1 0 422539892 19959808 4197 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4197 603 41 0 4832 0
vsize: 19492
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4236 0 0 0 112979 28 0 0 25 0 1 0 422539892 19959808 4210 4294967295 134512640 134672761 3221224560 3221223744 134559532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4210 603 41 0 4832 0
vsize: 19492
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4240 0 0 0 113979 28 0 0 25 0 1 0 422539892 19959808 4214 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4214 603 41 0 4832 0
vsize: 19492
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4247 0 0 0 114979 28 0 0 25 0 1 0 422539892 19959808 4221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4221 603 41 0 4832 0
vsize: 19492
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4248 0 0 0 115979 28 0 0 25 0 1 0 422539892 19959808 4222 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4222 603 41 0 4832 0
vsize: 19492
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4259 0 0 0 116979 28 0 0 25 0 1 0 422539892 20123648 4233 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4233 603 41 0 4872 0
vsize: 19652
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4260 0 0 0 117979 28 0 0 25 0 1 0 422539892 20123648 4234 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4234 603 41 0 4872 0
vsize: 19652
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4280 0 0 0 118979 28 0 0 25 0 1 0 422539892 20123648 4254 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4254 603 41 0 4872 0
vsize: 19652
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 3574
Raw data (stat): 3517 (minisat+) R 3516 29151 29150 0 -1 0 4284 0 0 0 119979 28 0 0 25 0 1 0 422539892 20123648 4258 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4258 603 41 0 4872 0
vsize: 19652
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 3574
Raw data (stat): 3517 (minisat+) Z 3516 29151 29150 0 -1 12 4287 0 0 0 119979 29 0 0 25 0 1 0 422539892 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.09
CPU user time (s): 1199.8
CPU system time (s): 0.294955
CPU usage (%): 100.006
Max. virtual memory (Kb): 19652
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####