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 4916

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 20:50:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1472 boxname=wulflinc13 idbench=164 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc13/normalized-ii8a2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-ii8a2.opb
IDLAUNCH: 1472
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924312 kB
Buffers:         34036 kB
Cached:          56692 kB
SwapCached:        392 kB
Active:          49948 kB
Inactive:        44052 kB
HighTotal:      131008 kB
HighFree:        70420 kB
LowTotal:       903652 kB
LowFree:        853892 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10764 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:10:16 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 1472 7 1200.17 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.85 0.95 0.90 2/54 1145
Raw data (stat): 1145 (runsolver) R 1144 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420745166 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0013 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 1633 0 0 0 993 5 0 0 25 0 1 0 420745166 8556544 1602 4294967295 134512640 134672761 3221224640 3221223824 134558380 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2089 1602 603 41 0 2048 0
vsize: 8356
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 1929 0 0 0 1992 6 0 0 25 0 1 0 420745166 9756672 1898 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2382 1898 603 41 0 2341 0
vsize: 9528
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2099 0 0 0 2991 7 0 0 25 0 1 0 420745166 10420224 2068 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2544 2068 603 41 0 2503 0
vsize: 10176
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2268 0 0 0 3990 7 0 0 25 0 1 0 420745166 11186176 2237 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2731 2237 603 41 0 2690 0
vsize: 10924
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2273 0 0 0 4990 7 0 0 25 0 1 0 420745166 11186176 2242 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2731 2242 603 41 0 2690 0
vsize: 10924
[startup+60.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2273 0 0 0 5991 7 0 0 25 0 1 0 420745166 11186176 2242 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2731 2242 603 41 0 2690 0
vsize: 10924
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2273 0 0 0 6991 7 0 0 25 0 1 0 420745166 11186176 2242 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2731 2242 603 41 0 2690 0
vsize: 10924
[startup+80.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2297 0 0 0 7991 7 0 0 25 0 1 0 420745166 11321344 2266 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2764 2266 603 41 0 2723 0
vsize: 11056
[startup+90.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2392 0 0 0 8991 8 0 0 25 0 1 0 420745166 11726848 2361 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2361 603 41 0 2822 0
vsize: 11452
[startup+100.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2421 0 0 0 9991 8 0 0 25 0 1 0 420745166 11874304 2390 4294967295 134512640 134672761 3221224640 3221223824 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2899 2390 603 41 0 2858 0
vsize: 11596
[startup+110.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2544 0 0 0 10990 8 0 0 25 0 1 0 420745166 12410880 2513 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3030 2513 603 41 0 2989 0
vsize: 12120
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2557 0 0 0 11991 8 0 0 25 0 1 0 420745166 12410880 2526 4294967295 134512640 134672761 3221224640 3221223744 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3030 2526 603 41 0 2989 0
vsize: 12120
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2680 0 0 0 12990 9 0 0 25 0 1 0 420745166 12935168 2649 4294967295 134512640 134672761 3221224640 3221223824 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2649 603 41 0 3117 0
vsize: 12632
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2686 0 0 0 13991 9 0 0 25 0 1 0 420745166 12935168 2655 4294967295 134512640 134672761 3221224640 3221223824 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2655 603 41 0 3117 0
vsize: 12632
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2687 0 0 0 14991 9 0 0 25 0 1 0 420745166 12935168 2656 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2656 603 41 0 3117 0
vsize: 12632
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2687 0 0 0 15991 9 0 0 25 0 1 0 420745166 12935168 2656 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2656 603 41 0 3117 0
vsize: 12632
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2726 0 0 0 16991 9 0 0 25 0 1 0 420745166 13070336 2695 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3191 2695 603 41 0 3150 0
vsize: 12764
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2739 0 0 0 17991 9 0 0 25 0 1 0 420745166 13213696 2708 4294967295 134512640 134672761 3221224640 3221223744 134555205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3226 2708 603 41 0 3185 0
vsize: 12904
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2900 0 0 0 18991 10 0 0 25 0 1 0 420745166 13750272 2869 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3357 2869 603 41 0 3316 0
vsize: 13428
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2924 0 0 0 19991 10 0 0 25 0 1 0 420745166 13897728 2893 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3393 2893 603 41 0 3352 0
vsize: 13572
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2945 0 0 0 20990 10 0 0 25 0 1 0 420745166 14045184 2914 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3429 2914 603 41 0 3388 0
vsize: 13716
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2959 0 0 0 21990 10 0 0 25 0 1 0 420745166 14045184 2928 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2928 603 41 0 3388 0
vsize: 13716
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 2963 0 0 0 22990 10 0 0 25 0 1 0 420745166 14045184 2932 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2932 603 41 0 3388 0
vsize: 13716
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3063 0 0 0 23990 11 0 0 25 0 1 0 420745166 14446592 3032 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3527 3032 603 41 0 3486 0
vsize: 14108
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3080 0 0 0 24990 11 0 0 25 0 1 0 420745166 14581760 3049 4294967295 134512640 134672761 3221224640 3221223744 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3560 3049 603 41 0 3519 0
vsize: 14240
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3193 0 0 0 25990 11 0 0 25 0 1 0 420745166 15126528 3162 4294967295 134512640 134672761 3221224640 3221223808 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3162 603 41 0 3652 0
vsize: 14772
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3271 0 0 0 26990 11 0 0 25 0 1 0 420745166 15392768 3240 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3240 603 41 0 3717 0
vsize: 15032
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3274 0 0 0 27990 11 0 0 25 0 1 0 420745166 15392768 3243 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3243 603 41 0 3717 0
vsize: 15032
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3285 0 0 0 28990 11 0 0 25 0 1 0 420745166 15392768 3254 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3254 603 41 0 3717 0
vsize: 15032
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3286 0 0 0 29990 11 0 0 25 0 1 0 420745166 15392768 3255 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3758 3255 603 41 0 3717 0
vsize: 15032
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3294 0 0 0 30990 12 0 0 25 0 1 0 420745166 15556608 3263 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3263 603 41 0 3757 0
vsize: 15192
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3307 0 0 0 31990 12 0 0 25 0 1 0 420745166 15556608 3276 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3276 603 41 0 3757 0
vsize: 15192
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3324 0 0 0 32990 12 0 0 25 0 1 0 420745166 15556608 3293 4294967295 134512640 134672761 3221224640 3221223596 1075349975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3293 603 41 0 3757 0
vsize: 15192
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3329 0 0 0 33990 12 0 0 25 0 1 0 420745166 15556608 3298 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3298 603 41 0 3757 0
vsize: 15192
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3333 0 0 0 34990 12 0 0 25 0 1 0 420745166 15704064 3302 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3834 3302 603 41 0 3793 0
vsize: 15336
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3347 0 0 0 35991 12 0 0 25 0 1 0 420745166 15704064 3316 4294967295 134512640 134672761 3221224640 3221223824 134558378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3834 3316 603 41 0 3793 0
vsize: 15336
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3369 0 0 0 36991 12 0 0 25 0 1 0 420745166 15867904 3338 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3338 603 41 0 3833 0
vsize: 15496
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3372 0 0 0 37991 12 0 0 25 0 1 0 420745166 15867904 3341 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3341 603 41 0 3833 0
vsize: 15496
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3379 0 0 0 38991 12 0 0 25 0 1 0 420745166 15867904 3348 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3348 603 41 0 3833 0
vsize: 15496
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3382 0 0 0 39991 12 0 0 25 0 1 0 420745166 15867904 3351 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3351 603 41 0 3833 0
vsize: 15496
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3382 0 0 0 40992 12 0 0 25 0 1 0 420745166 15867904 3351 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3351 603 41 0 3833 0
vsize: 15496
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3382 0 0 0 41992 12 0 0 25 0 1 0 420745166 15867904 3351 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3351 603 41 0 3833 0
vsize: 15496
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3390 0 0 0 42992 12 0 0 25 0 1 0 420745166 15867904 3359 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3359 603 41 0 3833 0
vsize: 15496
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3394 0 0 0 43992 12 0 0 25 0 1 0 420745166 15867904 3363 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3363 603 41 0 3833 0
vsize: 15496
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3396 0 0 0 44992 12 0 0 25 0 1 0 420745166 16015360 3365 4294967295 134512640 134672761 3221224640 3221223744 134559818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3910 3365 603 41 0 3869 0
vsize: 15640
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3406 0 0 0 45992 12 0 0 25 0 1 0 420745166 16015360 3375 4294967295 134512640 134672761 3221224640 3221223744 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3910 3375 603 41 0 3869 0
vsize: 15640
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3547 0 0 0 46992 13 0 0 25 0 1 0 420745166 16613376 3516 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3516 603 41 0 4015 0
vsize: 16224
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3554 0 0 0 47992 13 0 0 25 0 1 0 420745166 16613376 3523 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3523 603 41 0 4015 0
vsize: 16224
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3558 0 0 0 48992 13 0 0 25 0 1 0 420745166 16613376 3527 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3527 603 41 0 4015 0
vsize: 16224
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3688 0 0 0 49992 13 0 0 25 0 1 0 420745166 17145856 3657 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4186 3657 603 41 0 4145 0
vsize: 16744
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3688 0 0 0 50992 13 0 0 25 0 1 0 420745166 17145856 3657 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4186 3657 603 41 0 4145 0
vsize: 16744
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3689 0 0 0 51992 13 0 0 25 0 1 0 420745166 17145856 3658 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4186 3658 603 41 0 4145 0
vsize: 16744
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3817 0 0 0 52992 14 0 0 25 0 1 0 420745166 17678336 3786 4294967295 134512640 134672761 3221224640 3221223840 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3786 603 41 0 4275 0
vsize: 17264
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3817 0 0 0 53992 14 0 0 25 0 1 0 420745166 17678336 3786 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3786 603 41 0 4275 0
vsize: 17264
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 54992 14 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 55992 14 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 56992 14 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1145
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 57992 14 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1148
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 58992 14 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+600.008 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 59987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+610.008 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 60987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+620.008 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 61987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+630.009 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 62987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+640.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 63987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+650.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1198
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 64987 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+660.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 65988 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+670.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 66988 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+680.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 67988 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+690.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 68988 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+700.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 69988 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+710.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 70989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+720.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 71989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 72989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+740.009 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 73989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223744 134559787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+750.009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 74989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+760.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3820 0 0 0 75989 19 0 0 25 0 1 0 420745166 17678336 3789 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3789 603 41 0 4275 0
vsize: 17264
[startup+770.008 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3825 0 0 0 76990 19 0 0 25 0 1 0 420745166 17813504 3794 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3794 603 41 0 4308 0
vsize: 17396
[startup+780.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3833 0 0 0 77990 19 0 0 25 0 1 0 420745166 17813504 3802 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3802 603 41 0 4308 0
vsize: 17396
[startup+790.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3844 0 0 0 78990 19 0 0 25 0 1 0 420745166 17813504 3813 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3813 603 41 0 4308 0
vsize: 17396
[startup+800.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3850 0 0 0 79990 19 0 0 25 0 1 0 420745166 17977344 3819 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3819 603 41 0 4348 0
vsize: 17556
[startup+810.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3851 0 0 0 80990 19 0 0 25 0 1 0 420745166 17977344 3820 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3820 603 41 0 4348 0
vsize: 17556
[startup+820.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3858 0 0 0 81991 19 0 0 25 0 1 0 420745166 17977344 3827 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3827 603 41 0 4348 0
vsize: 17556
[startup+830.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3858 0 0 0 82991 19 0 0 25 0 1 0 420745166 17977344 3827 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3827 603 41 0 4348 0
vsize: 17556
[startup+840.011 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3858 0 0 0 83991 19 0 0 25 0 1 0 420745166 17977344 3827 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3827 603 41 0 4348 0
vsize: 17556
[startup+850.01 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3865 0 0 0 84991 19 0 0 25 0 1 0 420745166 17977344 3834 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3834 603 41 0 4348 0
vsize: 17556
[startup+860.01 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3956 0 0 0 85991 20 0 0 25 0 1 0 420745166 18370560 3925 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4485 3925 603 41 0 4444 0
vsize: 17940
[startup+870.01 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3974 0 0 0 86991 20 0 0 25 0 1 0 420745166 18370560 3943 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4485 3943 603 41 0 4444 0
vsize: 17940
[startup+880.01 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 3981 0 0 0 87990 20 0 0 25 0 1 0 420745166 18518016 3950 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4521 3950 603 41 0 4480 0
vsize: 18084
[startup+890.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4010 0 0 0 88991 20 0 0 25 0 1 0 420745166 18653184 3979 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3979 603 41 0 4513 0
vsize: 18216
[startup+900.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 1200
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4010 0 0 0 89991 20 0 0 25 0 1 0 420745166 18653184 3979 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3979 603 41 0 4513 0
vsize: 18216
[startup+910.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4014 0 0 0 90991 20 0 0 25 0 1 0 420745166 18653184 3983 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3983 603 41 0 4513 0
vsize: 18216
[startup+920.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4014 0 0 0 91991 20 0 0 25 0 1 0 420745166 18653184 3983 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3983 603 41 0 4513 0
vsize: 18216
[startup+930.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4014 0 0 0 92991 20 0 0 25 0 1 0 420745166 18653184 3983 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4554 3983 603 41 0 4513 0
vsize: 18216
[startup+940.011 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4035 0 0 0 93991 20 0 0 25 0 1 0 420745166 18788352 4004 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4004 603 41 0 4546 0
vsize: 18348
[startup+950.011 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4036 0 0 0 94991 20 0 0 25 0 1 0 420745166 18788352 4005 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4005 603 41 0 4546 0
vsize: 18348
[startup+960.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4036 0 0 0 95991 20 0 0 25 0 1 0 420745166 18788352 4005 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4005 603 41 0 4546 0
vsize: 18348
[startup+970.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4044 0 0 0 96991 20 0 0 25 0 1 0 420745166 18788352 4013 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4013 603 41 0 4546 0
vsize: 18348
[startup+980.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4080 0 0 0 97992 21 0 0 25 0 1 0 420745166 18935808 4049 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4623 4049 603 41 0 4582 0
vsize: 18492
[startup+990.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4085 0 0 0 98992 21 0 0 25 0 1 0 420745166 18935808 4054 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4623 4054 603 41 0 4582 0
vsize: 18492
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4099 0 0 0 99992 21 0 0 25 0 1 0 420745166 19083264 4068 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4068 603 41 0 4618 0
vsize: 18636
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4102 0 0 0 100992 21 0 0 25 0 1 0 420745166 19083264 4071 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4071 603 41 0 4618 0
vsize: 18636
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4109 0 0 0 101992 21 0 0 25 0 1 0 420745166 19083264 4078 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4078 603 41 0 4618 0
vsize: 18636
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4115 0 0 0 102992 21 0 0 25 0 1 0 420745166 19083264 4084 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4084 603 41 0 4618 0
vsize: 18636
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4115 0 0 0 103992 21 0 0 25 0 1 0 420745166 19083264 4084 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4084 603 41 0 4618 0
vsize: 18636
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4117 0 0 0 104992 21 0 0 25 0 1 0 420745166 19083264 4086 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4086 603 41 0 4618 0
vsize: 18636
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4122 0 0 0 105992 21 0 0 25 0 1 0 420745166 19083264 4091 4294967295 134512640 134672761 3221224640 3221223776 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4091 603 41 0 4618 0
vsize: 18636
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4122 0 0 0 106993 21 0 0 25 0 1 0 420745166 19083264 4091 4294967295 134512640 134672761 3221224640 3221223824 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4091 603 41 0 4618 0
vsize: 18636
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4122 0 0 0 107993 21 0 0 25 0 1 0 420745166 19083264 4091 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4659 4091 603 41 0 4618 0
vsize: 18636
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4125 0 0 0 108993 21 0 0 25 0 1 0 420745166 19230720 4094 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4695 4094 603 41 0 4654 0
vsize: 18780
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4134 0 0 0 109993 21 0 0 25 0 1 0 420745166 19230720 4103 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4695 4103 603 41 0 4654 0
vsize: 18780
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4147 0 0 0 110993 21 0 0 25 0 1 0 420745166 19230720 4116 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4695 4116 603 41 0 4654 0
vsize: 18780
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4163 0 0 0 111993 21 0 0 25 0 1 0 420745166 19394560 4132 4294967295 134512640 134672761 3221224640 3221223824 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4132 603 41 0 4694 0
vsize: 18940
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4175 0 0 0 112994 21 0 0 25 0 1 0 420745166 19394560 4144 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4144 603 41 0 4694 0
vsize: 18940
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4176 0 0 0 113994 21 0 0 25 0 1 0 420745166 19394560 4145 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4145 603 41 0 4694 0
vsize: 18940
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4188 0 0 0 114994 21 0 0 25 0 1 0 420745166 19394560 4157 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4735 4157 603 41 0 4694 0
vsize: 18940
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4209 0 0 0 115994 21 0 0 25 0 1 0 420745166 19591168 4178 4294967295 134512640 134672761 3221224640 3221223840 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4178 603 41 0 4742 0
vsize: 19132
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4209 0 0 0 116994 21 0 0 25 0 1 0 420745166 19591168 4178 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4178 603 41 0 4742 0
vsize: 19132
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4212 0 0 0 117994 21 0 0 25 0 1 0 420745166 19591168 4181 4294967295 134512640 134672761 3221224640 3221223744 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4783 4181 603 41 0 4742 0
vsize: 19132
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4326 0 0 0 118994 21 0 0 25 0 1 0 420745166 20119552 4295 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4295 603 41 0 4871 0
vsize: 19648
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1202
Raw data (stat): 1145 (minisat+) R 1144 30701 30700 0 -1 0 4346 0 0 0 119994 21 0 0 25 0 1 0 420745166 20119552 4315 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4315 603 41 0 4871 0
vsize: 19648
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 1202
Raw data (stat): 1145 (minisat+) Z 1144 30701 30700 0 -1 12 4349 0 0 0 119994 22 0 0 25 0 1 0 420745166 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.02
CPU time (s): 1200.17
CPU user time (s): 1199.95
CPU system time (s): 0.224965
CPU usage (%): 100.013
Max. virtual memory (Kb): 19648
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####