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/primes-dimacs-cnf/normalized-ii8a2.opb
MD5SUM	6005a01d3f2ae55b0ca9c19f876c5827
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	139
Optimality of the best value was proved	NO
Number of terms in the objective function	360
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	360
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	360
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.02584
Number of variables	360
Total number of constraints	980
Number of constraints which are clauses	980
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	8
Trace number 5887

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 02:11:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4300 boxname=wulflinc9 idbench=164 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc9/normalized-ii8a2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-ii8a2.opb /oldhome/oroussel/tmp/wulflinc9/normalized-ii8a2.opb
IDLAUNCH: 4300
/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:        893912 kB
Buffers:         36228 kB
Cached:          84384 kB
SwapCached:        564 kB
Active:          53816 kB
Inactive:        70272 kB
HighTotal:      131008 kB
HighFree:        42672 kB
LowTotal:       903652 kB
LowFree:        851240 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11048 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:31:19 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 4300 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 980 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 |     980     2412 |     326       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 150[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13276     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   16839    39488 |    5613       3       20     6.7 |  0.000 % |
c |       103 |   16491    38744 |    6174      90     1250    13.9 |  1.915 % |
c |       254 |   16341    38418 |    6791     234     5528    23.6 |  2.729 % |
c |       479 |   16038    37759 |    7470     450    11949    26.6 |  4.320 % |
c |       817 |   15269    36066 |    8217     770    24110    31.3 |  8.575 % |
c |      1323 |   15221    35960 |    9039    1275    41757    32.8 |  8.844 % |
c |      2082 |   15221    35960 |    9943    2034    93705    46.1 |  8.844 % |
c ==============================================================================
c [1mFound solution: 148[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 |      2350 |   15217    35960 |    5072    2302   101593    44.1 |  8.844 % |
c |      2450 |   15217    35960 |    5579    2402   105288    43.8 |  9.084 % |
c |      2600 |   15217    35960 |    6137    2552   107574    42.2 |  9.084 % |
c ==============================================================================
c [1mFound solution: 142[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 |      2813 |   15257    36064 |    5085    2763   111341    40.3 |  9.084 % |
c |      2915 |   15257    36064 |    5593    2865   112507    39.3 |  9.266 % |
c |      3065 |   15257    36064 |    6152    3015   115583    38.3 |  9.266 % |
c |      3290 |   15213    35964 |    6768    3239   129038    39.8 |  9.524 % |
c |      3631 |   15119    35756 |    7444    3575   143929    40.3 | 10.048 % |
c |      4137 |   15119    35756 |    8189    4081   159776    39.2 | 10.048 % |
c |      4896 |   15119    35756 |    9008    4840   198324    41.0 | 10.048 % |
c |      6037 |   15119    35756 |    9909    5981   259812    43.4 | 10.048 % |
c |      7746 |   15119    35756 |   10900    7690   319662    41.6 | 10.048 % |
c |     10309 |   15020    35539 |   11990   10251   449968    43.9 | 10.590 % |
c |     14154 |   15020    35539 |   13189    7241   321460    44.4 | 10.590 % |
c |     19920 |   14964    35421 |   14508   13006   623303    47.9 | 10.875 % |
c ==============================================================================
c [1mFound solution: 141[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 |     27771 |   14986    35486 |    4995   11967   651063    54.4 | 10.875 % |
c |     27872 |   14986    35486 |    5494    6085   308059    50.6 | 10.927 % |
c |     28024 |   14931    35351 |    6043    6229   312203    50.1 | 11.294 % |
c |     28250 |   14825    35119 |    6648    6439   321374    49.9 | 11.853 % |
c |     28588 |   14825    35119 |    7313    6777   330987    48.8 | 11.853 % |
c |     29095 |   14825    35119 |    8044    7284   349008    47.9 | 11.853 % |
c |     29854 |   14825    35119 |    8848    8043   376752    46.8 | 11.853 % |
c |     30994 |   14825    35119 |    9733    9183   417078    45.4 | 11.853 % |
c |     32702 |   14791    35041 |   10707   10887   478885    44.0 | 12.055 % |
c |     35264 |   14791    35041 |   11777    7145   253382    35.5 | 12.055 % |
c |     39109 |   14791    35041 |   12955   10990   474654    43.2 | 12.055 % |
c |     44877 |   14791    35041 |   14251    9411   454007    48.2 | 12.055 % |
c |     53527 |   14791    35041 |   15676    9296   440843    47.4 | 12.055 % |
c |     66501 |   14791    35041 |   17244   12660   591539    46.7 | 12.055 % |
c |     85962 |   14752    34954 |   18968   12206   509154    41.7 | 12.275 % |
c |    115155 |   14752    34954 |   20865   19570   994956    50.8 | 12.275 % |
c |    158944 |   14752    34954 |   22951   15966   812506    50.9 | 12.275 % |
c |    224628 |   14752    34954 |   25247   16504   780085    47.3 | 12.275 % |
c ==============================================================================
c [1mFound solution: 139[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 |    273203 |   14737    34933 |    4912   22747  1178259    51.8 | 12.275 % |
c |    273303 |   14737    34933 |    5403    5787   220361    38.1 | 12.486 % |
c |    273453 |   14737    34933 |    5943    5937   224417    37.8 | 12.486 % |
c |    273678 |   14673    34785 |    6537    6143   232659    37.9 | 12.871 % |
c |    274016 |   14673    34785 |    7191    6481   247623    38.2 | 12.871 % |
c |    274524 |   14673    34785 |    7910    6989   269613    38.6 | 12.871 % |
c |    275284 |   14673    34785 |    8701    7749   306748    39.6 | 12.871 % |
c |    276423 |   14673    34785 |    9572    8888   356210    40.1 | 12.871 % |
c |    278132 |   14636    34702 |   10529   10596   451584    42.6 | 13.082 % |
c |    280694 |   14636    34702 |   11582    6651   294921    44.3 | 13.082 % |
c |    284538 |   14636    34702 |   12740   10495   503132    47.9 | 13.082 % |
c |    290305 |   14636    34702 |   14014    8572   373798    43.6 | 13.082 % |
c |    298954 |   14636    34702 |   15415    8671   427916    49.4 | 13.082 % |
c |    311928 |   14567    34547 |   16957   12461   746270    59.9 | 13.476 % |
c |    331389 |   14567    34547 |   18653   12412   552554    44.5 | 13.476 % |
c |    360584 |   14567    34547 |   20518   20300  1026218    50.6 | 13.476 % |
c |    404373 |   14567    34547 |   22570   17926   952975    53.2 | 13.476 % |
c |    470057 |   14567    34547 |   24827   21071  1096971    52.1 | 13.476 % |
c |    568587 |   14539    34481 |   27310   23204  1046969    45.1 | 13.650 % |
#### 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.86 0.97 0.92 2/54 3016
Raw data (stat): 3016 (runsolver) R 3015 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422668183 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0008 s]
Raw data (loadavg): 0.88 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 1617 0 0 0 995 3 0 0 25 0 1 0 422668183 8515584 1585 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2079 1585 603 41 0 2038 0
vsize: 8316
[startup+20.0015 s]
Raw data (loadavg): 0.90 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 1916 0 0 0 1994 4 0 0 25 0 1 0 422668183 9715712 1884 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2372 1884 603 41 0 2331 0
vsize: 9488
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2083 0 0 0 2992 5 0 0 25 0 1 0 422668183 10379264 2051 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2051 603 41 0 2493 0
vsize: 10136
[startup+40.0011 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2255 0 0 0 3992 6 0 0 25 0 1 0 422668183 11145216 2223 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2721 2223 603 41 0 2680 0
vsize: 10884
[startup+50.0018 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2262 0 0 0 4992 6 0 0 25 0 1 0 422668183 11145216 2230 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2721 2230 603 41 0 2680 0
vsize: 10884
[startup+60.0022 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2262 0 0 0 5992 6 0 0 25 0 1 0 422668183 11145216 2230 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2721 2230 603 41 0 2680 0
vsize: 10884
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2262 0 0 0 6993 6 0 0 25 0 1 0 422668183 11145216 2230 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2721 2230 603 41 0 2680 0
vsize: 10884
[startup+80.0041 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2275 0 0 0 7993 6 0 0 25 0 1 0 422668183 11280384 2243 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2243 603 41 0 2713 0
vsize: 11016
[startup+90.0046 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2375 0 0 0 8992 7 0 0 25 0 1 0 422668183 11677696 2343 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2851 2343 603 41 0 2810 0
vsize: 11404
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2403 0 0 0 9992 7 0 0 25 0 1 0 422668183 11825152 2371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2887 2371 603 41 0 2846 0
vsize: 11548
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2527 0 0 0 10992 7 0 0 25 0 1 0 422668183 12365824 2495 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3019 2495 603 41 0 2978 0
vsize: 12076
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2543 0 0 0 11992 7 0 0 25 0 1 0 422668183 12365824 2511 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3019 2511 603 41 0 2978 0
vsize: 12076
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2666 0 0 0 12992 8 0 0 25 0 1 0 422668183 12898304 2634 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3149 2634 603 41 0 3108 0
vsize: 12596
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2668 0 0 0 13992 8 0 0 25 0 1 0 422668183 12898304 2636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3149 2636 603 41 0 3108 0
vsize: 12596
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2672 0 0 0 14992 8 0 0 25 0 1 0 422668183 12898304 2640 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3149 2640 603 41 0 3108 0
vsize: 12596
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2672 0 0 0 15993 8 0 0 25 0 1 0 422668183 12898304 2640 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3149 2640 603 41 0 3108 0
vsize: 12596
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2709 0 0 0 16993 8 0 0 25 0 1 0 422668183 13033472 2677 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3182 2677 603 41 0 3141 0
vsize: 12728
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2723 0 0 0 17993 8 0 0 25 0 1 0 422668183 13172736 2691 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3216 2691 603 41 0 3175 0
vsize: 12864
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2880 0 0 0 18993 8 0 0 25 0 1 0 422668183 13709312 2848 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3347 2848 603 41 0 3306 0
vsize: 13388
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2903 0 0 0 19993 8 0 0 25 0 1 0 422668183 13856768 2871 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3383 2871 603 41 0 3342 0
vsize: 13532
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2919 0 0 0 20992 9 0 0 25 0 1 0 422668183 13856768 2887 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3383 2887 603 41 0 3342 0
vsize: 13532
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2941 0 0 0 21991 9 0 0 25 0 1 0 422668183 14004224 2909 4294967295 134512640 134672761 3221224560 3221223620 1075346557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3419 2909 603 41 0 3378 0
vsize: 13676
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 2945 0 0 0 22991 9 0 0 25 0 1 0 422668183 14004224 2913 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3419 2913 603 41 0 3378 0
vsize: 13676
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3047 0 0 0 23991 9 0 0 25 0 1 0 422668183 14401536 3015 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3015 603 41 0 3475 0
vsize: 14064
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3062 0 0 0 24991 9 0 0 25 0 1 0 422668183 14540800 3030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3550 3030 603 41 0 3509 0
vsize: 14200
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3159 0 0 0 25991 10 0 0 25 0 1 0 422668183 14950400 3127 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3650 3127 603 41 0 3609 0
vsize: 14600
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3255 0 0 0 26990 10 0 0 25 0 1 0 422668183 15343616 3223 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3746 3223 603 41 0 3705 0
vsize: 14984
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3257 0 0 0 27991 10 0 0 25 0 1 0 422668183 15343616 3225 4294967295 134512640 134672761 3221224560 3221223776 134558229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3746 3225 603 41 0 3705 0
vsize: 14984
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3268 0 0 0 28991 10 0 0 25 0 1 0 422668183 15343616 3236 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3746 3236 603 41 0 3705 0
vsize: 14984
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3272 0 0 0 29991 10 0 0 25 0 1 0 422668183 15491072 3240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3782 3240 603 41 0 3741 0
vsize: 15128
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3280 0 0 0 30990 11 0 0 25 0 1 0 422668183 15491072 3248 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3782 3248 603 41 0 3741 0
vsize: 15128
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3282 0 0 0 31990 11 0 0 25 0 1 0 422668183 15491072 3250 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3782 3250 603 41 0 3741 0
vsize: 15128
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3296 0 0 0 32990 11 0 0 25 0 1 0 422668183 15491072 3264 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3782 3264 603 41 0 3741 0
vsize: 15128
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3304 0 0 0 33990 11 0 0 25 0 1 0 422668183 15630336 3272 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3272 603 41 0 3775 0
vsize: 15264
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3308 0 0 0 34990 11 0 0 25 0 1 0 422668183 15630336 3276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3276 603 41 0 3775 0
vsize: 15264
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3319 0 0 0 35990 11 0 0 25 0 1 0 422668183 15630336 3287 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3287 603 41 0 3775 0
vsize: 15264
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3344 0 0 0 36990 11 0 0 25 0 1 0 422668183 15777792 3312 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3312 603 41 0 3811 0
vsize: 15408
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3347 0 0 0 37991 11 0 0 25 0 1 0 422668183 15777792 3315 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3315 603 41 0 3811 0
vsize: 15408
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3354 0 0 0 38990 11 0 0 25 0 1 0 422668183 15777792 3322 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3322 603 41 0 3811 0
vsize: 15408
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3357 0 0 0 39991 11 0 0 25 0 1 0 422668183 15777792 3325 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3325 603 41 0 3811 0
vsize: 15408
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3358 0 0 0 40991 11 0 0 25 0 1 0 422668183 15777792 3326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3326 603 41 0 3811 0
vsize: 15408
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3358 0 0 0 41991 11 0 0 25 0 1 0 422668183 15777792 3326 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3326 603 41 0 3811 0
vsize: 15408
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3365 0 0 0 42991 11 0 0 25 0 1 0 422668183 15925248 3333 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3888 3333 603 41 0 3847 0
vsize: 15552
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3365 0 0 0 43991 11 0 0 25 0 1 0 422668183 15925248 3333 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3888 3333 603 41 0 3847 0
vsize: 15552
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3373 0 0 0 44991 11 0 0 25 0 1 0 422668183 15925248 3341 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3888 3341 603 41 0 3847 0
vsize: 15552
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3386 0 0 0 45991 11 0 0 25 0 1 0 422668183 15925248 3354 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3888 3354 603 41 0 3847 0
vsize: 15552
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3527 0 0 0 46991 11 0 0 25 0 1 0 422668183 16584704 3495 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3495 603 41 0 4008 0
vsize: 16196
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3534 0 0 0 47991 11 0 0 25 0 1 0 422668183 16584704 3502 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3502 603 41 0 4008 0
vsize: 16196
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3538 0 0 0 48991 12 0 0 25 0 1 0 422668183 16584704 3506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3506 603 41 0 4008 0
vsize: 16196
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3668 0 0 0 49991 12 0 0 25 0 1 0 422668183 17117184 3636 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4179 3636 603 41 0 4138 0
vsize: 16716
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3668 0 0 0 50991 12 0 0 25 0 1 0 422668183 17117184 3636 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4179 3636 603 41 0 4138 0
vsize: 16716
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3669 0 0 0 51991 12 0 0 25 0 1 0 422668183 17117184 3637 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4179 3637 603 41 0 4138 0
vsize: 16716
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3783 0 0 0 52991 13 0 0 25 0 1 0 422668183 17649664 3751 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3751 603 41 0 4268 0
vsize: 17236
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 53991 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 54991 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 55991 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 56991 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 57991 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 58992 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 59992 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 60992 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 61992 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 62993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 63993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 64993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 65993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 66993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 67993 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 68994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 69994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 70994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 71994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 72994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 73994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 74994 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223216 134565736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 75995 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3799 0 0 0 76995 13 0 0 25 0 1 0 422668183 17649664 3767 4294967295 134512640 134672761 3221224560 3221223664 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3767 603 41 0 4268 0
vsize: 17236
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3800 0 0 0 77995 13 0 0 25 0 1 0 422668183 17649664 3768 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3768 603 41 0 4268 0
vsize: 17236
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3800 0 0 0 78995 13 0 0 25 0 1 0 422668183 17649664 3768 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3768 603 41 0 4268 0
vsize: 17236
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3811 0 0 0 79995 13 0 0 25 0 1 0 422668183 17813504 3779 4294967295 134512640 134672761 3221224560 3221223696 134560694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3779 603 41 0 4308 0
vsize: 17396
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3838 0 0 0 80996 13 0 0 25 0 1 0 422668183 17813504 3806 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3806 603 41 0 4308 0
vsize: 17396
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3849 0 0 0 81996 13 0 0 25 0 1 0 422668183 17952768 3817 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4383 3817 603 41 0 4342 0
vsize: 17532
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3849 0 0 0 82996 13 0 0 25 0 1 0 422668183 17952768 3817 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4383 3817 603 41 0 4342 0
vsize: 17532
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3849 0 0 0 83996 13 0 0 25 0 1 0 422668183 17952768 3817 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4383 3817 603 41 0 4342 0
vsize: 17532
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3852 0 0 0 84996 13 0 0 25 0 1 0 422668183 17952768 3820 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4383 3820 603 41 0 4342 0
vsize: 17532
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3948 0 0 0 85996 13 0 0 25 0 1 0 422668183 18350080 3916 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4480 3916 603 41 0 4439 0
vsize: 17920
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3962 0 0 0 86996 13 0 0 25 0 1 0 422668183 18350080 3930 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4480 3930 603 41 0 4439 0
vsize: 17920
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 3973 0 0 0 87997 13 0 0 25 0 1 0 422668183 18350080 3941 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4480 3941 603 41 0 4439 0
vsize: 17920
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4002 0 0 0 88997 13 0 0 25 0 1 0 422668183 18485248 3970 4294967295 134512640 134672761 3221224560 3221223664 134559824 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 3970 603 41 0 4472 0
vsize: 18052
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4002 0 0 0 89997 13 0 0 25 0 1 0 422668183 18485248 3970 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 3970 603 41 0 4472 0
vsize: 18052
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4006 0 0 0 90997 13 0 0 25 0 1 0 422668183 18632704 3974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 3974 603 41 0 4508 0
vsize: 18196
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4006 0 0 0 91997 13 0 0 25 0 1 0 422668183 18632704 3974 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 3974 603 41 0 4508 0
vsize: 18196
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4006 0 0 0 92997 13 0 0 25 0 1 0 422668183 18632704 3974 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 3974 603 41 0 4508 0
vsize: 18196
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4025 0 0 0 93996 14 0 0 25 0 1 0 422668183 18632704 3993 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4549 3993 603 41 0 4508 0
vsize: 18196
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4027 0 0 0 94996 14 0 0 25 0 1 0 422668183 18632704 3995 4294967295 134512640 134672761 3221224560 3221223728 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 3995 603 41 0 4508 0
vsize: 18196
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4027 0 0 0 95996 14 0 0 25 0 1 0 422668183 18632704 3995 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 3995 603 41 0 4508 0
vsize: 18196
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4032 0 0 0 96996 14 0 0 25 0 1 0 422668183 18780160 4000 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4585 4000 603 41 0 4544 0
vsize: 18340
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4060 0 0 0 97996 14 0 0 25 0 1 0 422668183 18944000 4028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 4028 603 41 0 4584 0
vsize: 18500
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4060 0 0 0 98997 14 0 0 25 0 1 0 422668183 18944000 4028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 4028 603 41 0 4584 0
vsize: 18500
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4072 0 0 0 99997 14 0 0 25 0 1 0 422668183 18944000 4040 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 4040 603 41 0 4584 0
vsize: 18500
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4075 0 0 0 100997 14 0 0 25 0 1 0 422668183 18944000 4043 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 4043 603 41 0 4584 0
vsize: 18500
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4078 0 0 0 101997 14 0 0 25 0 1 0 422668183 18944000 4046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 4046 603 41 0 4584 0
vsize: 18500
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4086 0 0 0 102997 14 0 0 25 0 1 0 422668183 19083264 4054 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4054 603 41 0 4618 0
vsize: 18636
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4090 0 0 0 103997 14 0 0 25 0 1 0 422668183 19083264 4058 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4058 603 41 0 4618 0
vsize: 18636
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4094 0 0 0 104998 14 0 0 25 0 1 0 422668183 19083264 4062 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4062 603 41 0 4618 0
vsize: 18636
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4099 0 0 0 105998 14 0 0 25 0 1 0 422668183 19083264 4067 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4067 603 41 0 4618 0
vsize: 18636
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4099 0 0 0 106998 14 0 0 25 0 1 0 422668183 19083264 4067 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4067 603 41 0 4618 0
vsize: 18636
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4099 0 0 0 107998 14 0 0 25 0 1 0 422668183 19083264 4067 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4067 603 41 0 4618 0
vsize: 18636
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4102 0 0 0 108998 14 0 0 25 0 1 0 422668183 19083264 4070 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4070 603 41 0 4618 0
vsize: 18636
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4110 0 0 0 109998 14 0 0 25 0 1 0 422668183 19083264 4078 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4078 603 41 0 4618 0
vsize: 18636
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4118 0 0 0 110999 14 0 0 25 0 1 0 422668183 19230720 4086 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4695 4086 603 41 0 4654 0
vsize: 18780
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4142 0 0 0 111999 14 0 0 25 0 1 0 422668183 19230720 4110 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4695 4110 603 41 0 4654 0
vsize: 18780
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4156 0 0 0 112999 14 0 0 25 0 1 0 422668183 19394560 4124 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4124 603 41 0 4694 0
vsize: 18940
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4157 0 0 0 113999 14 0 0 25 0 1 0 422668183 19394560 4125 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4125 603 41 0 4694 0
vsize: 18940
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4169 0 0 0 114998 14 0 0 25 0 1 0 422668183 19394560 4137 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4735 4137 603 41 0 4694 0
vsize: 18940
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4186 0 0 0 115998 14 0 0 25 0 1 0 422668183 19529728 4154 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4768 4154 603 41 0 4727 0
vsize: 19072
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4198 0 0 0 116998 14 0 0 25 0 1 0 422668183 19529728 4166 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4768 4166 603 41 0 4727 0
vsize: 19072
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4202 0 0 0 117998 14 0 0 25 0 1 0 422668183 19529728 4170 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4768 4170 603 41 0 4727 0
vsize: 19072
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4272 0 0 0 118998 15 0 0 25 0 1 0 422668183 19795968 4240 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4833 4240 603 41 0 4792 0
vsize: 19332
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3016
Raw data (stat): 3016 (minisat+) R 3015 30854 30853 0 -1 0 4335 0 0 0 119998 15 0 0 25 0 1 0 422668183 20058112 4303 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4897 4303 603 41 0 4856 0
vsize: 19588
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 3016
Raw data (stat): 3016 (minisat+) Z 3015 30854 30853 0 -1 12 4338 0 0 0 119998 16 0 0 25 0 1 0 422668183 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.04
CPU time (s): 1200.14
CPU user time (s): 1199.98
CPU system time (s): 0.161975
CPU usage (%): 100.009
Max. virtual memory (Kb): 19588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####