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-ii8b1.opb
MD5SUM	812314147c77e28d5e428080c7a2412d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	672
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03684
Number of variables	672
Total number of constraints	2404
Number of constraints which are clauses	2404
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 6258

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 04:01:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4679 boxname=wulflinc31 idbench=167 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc31/normalized-ii8b1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-ii8b1.opb /oldhome/oroussel/tmp/wulflinc31/normalized-ii8b1.opb
IDLAUNCH: 4679
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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:        888388 kB
Buffers:         36332 kB
Cached:          71328 kB
SwapCached:        392 kB
Active:          53440 kB
Inactive:        57404 kB
HighTotal:      131008 kB
HighFree:        56056 kB
LowTotal:       903652 kB
LowFree:        832332 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29844 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:21:30 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 4679 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2404 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 |    2404     5328 |     801       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   76108   177735 |   25369       2       14     7.0 |  0.000 % |
c |       103 |   75947   177374 |   27905     100      535     5.3 |  0.263 % |
c |       253 |   69390   162323 |   30696     109      907     8.3 |  8.247 % |
c |       480 |   66361   155366 |   33766     260     2337     9.0 | 11.941 % |
c |       817 |   65382   153130 |   37142     577     8256    14.3 | 13.094 % |
c |      1323 |   63923   149769 |   40857    1054    27160    25.8 | 14.905 % |
c |      2082 |   59911   140553 |   44942    1726    55692    32.3 | 19.789 % |
c |      3221 |   59007   138484 |   49437    2852   101752    35.7 | 20.862 % |
c |      4929 |   46771   110215 |   54380    4322   159356    36.9 | 36.290 % |
c |      7491 |   42928   101346 |   59818    6803   243501    35.8 | 41.145 % |
c |     11336 |   33980    80612 |   65800   10296   361426    35.1 | 52.803 % |
c |     17102 |   33350    79156 |   72380   16044   750385    46.8 | 53.441 % |
c ==============================================================================
c [1mFound solution: 223[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 |     18772 |   33386    79253 |   11128   17711   789754    44.6 | 53.441 % |
c |     18872 |   33386    79253 |   12240   17811   792925    44.5 | 53.437 % |
c |     19023 |   33029    78429 |   13464   17954   794194    44.2 | 53.879 % |
c |     19249 |   33021    78411 |   14811   18174   798439    43.9 | 53.887 % |
c ==============================================================================
c [1mFound solution: 222[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 |     19537 |   32857    78021 |   10952   18457   807493    43.7 | 53.887 % |
c |     19639 |   32857    78021 |   12047   18559   809230    43.6 | 54.098 % |
c |     19789 |   32651    77543 |   13251   18696   814151    43.5 | 54.369 % |
c |     20014 |   32526    77252 |   14577   18913   819787    43.3 | 54.537 % |
c |     20351 |   32526    77252 |   16034   19250   842693    43.8 | 54.537 % |
c |     20858 |   32526    77252 |   17638   19757   861817    43.6 | 54.537 % |
c ==============================================================================
c [1mFound solution: 221[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 |     21294 |   32584    77400 |   10861   20193   880026    43.6 | 54.537 % |
c |     21396 |   32443    77075 |   11947   20291   880595    43.4 | 54.694 % |
c |     21546 |   32443    77075 |   13141   20441   888422    43.5 | 54.694 % |
c |     21772 |   32443    77075 |   14455   20667   891805    43.2 | 54.694 % |
c |     22110 |   32366    76895 |   15901   20994   896903    42.7 | 54.801 % |
c |     22617 |   32249    76623 |   17491   21498   916007    42.6 | 54.956 % |
c |     23377 |   31993    76030 |   19240   22250   944473    42.4 | 55.287 % |
c |     24517 |   31993    76030 |   21165   23390  1028002    44.0 | 55.287 % |
c |     26226 |   31878    75765 |   23281   25098  1142650    45.5 | 55.430 % |
c ==============================================================================
c [1mFound solution: 220[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 |     26447 |   31703    75351 |   10567   25271  1146091    45.4 | 55.430 % |
c |     26547 |   31703    75351 |   11623   12736   405569    31.8 | 55.649 % |
c |     26699 |   31703    75351 |   12786   12888   407991    31.7 | 55.649 % |
c ==============================================================================
c [1mFound solution: 218[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 |     26893 |   31686    75320 |   10562   12991   403977    31.1 | 55.649 % |
c |     26993 |   31686    75320 |   11618   13091   405759    31.0 | 55.699 % |
c |     27145 |   31686    75320 |   12780   13243   410982    31.0 | 55.699 % |
c |     27370 |   31464    74808 |   14058   13438   417018    31.0 | 55.969 % |
c |     27707 |   31464    74808 |   15463   13775   431915    31.4 | 55.969 % |
c |     28213 |   31464    74808 |   17010   14281   451666    31.6 | 55.969 % |
c |     28972 |   31464    74808 |   18711   15040   488809    32.5 | 55.969 % |
c |     30111 |   31464    74808 |   20582   16179   556319    34.4 | 55.969 % |
c |     31822 |   31464    74808 |   22640   17890   652949    36.5 | 55.969 % |
c |     34384 |   31464    74808 |   24904   20452   891680    43.6 | 55.969 % |
c |     38228 |   31464    74808 |   27395   24296  1068057    44.0 | 55.969 % |
c |     43994 |   31464    74808 |   30134   30062  1479271    49.2 | 55.969 % |
c |     52643 |   31464    74808 |   33148   38711  2041715    52.7 | 55.969 % |
c |     65618 |   31464    74808 |   36462   20054   845131    42.1 | 55.969 % |
c |     85079 |   31464    74808 |   40109   39515  2190132    55.4 | 55.969 % |
c |    114271 |   31068    73887 |   44120   33115  1501405    45.3 | 56.499 % |
c |    158060 |   31068    73887 |   48532   34983  1879325    53.7 | 56.499 % |
c |    223744 |   30989    73703 |   53385   58034  2755875    47.5 | 56.606 % |
#### 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.98 1.02 0.94 2/54 31051
Raw data (stat): 31051 (runsolver) R 31050 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481537714 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.99 1.02 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 2511 0 0 0 992 5 0 0 25 0 1 0 481537714 12075008 2423 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2948 2423 603 41 0 2907 0
vsize: 11792
[startup+20.0014 s]
Raw data (loadavg): 0.99 1.02 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 2615 0 0 0 1992 6 0 0 25 0 1 0 481537714 12611584 2527 4294967295 134512640 134672761 3221224576 3221223748 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3079 2527 603 41 0 3038 0
vsize: 12316
[startup+30.0019 s]
Raw data (loadavg): 0.99 1.02 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 2735 0 0 0 2991 7 0 0 25 0 1 0 481537714 13008896 2647 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3176 2647 603 41 0 3135 0
vsize: 12704
[startup+40.0022 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 2868 0 0 0 3990 7 0 0 25 0 1 0 481537714 13537280 2780 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3305 2780 603 41 0 3264 0
vsize: 13220
[startup+50.0049 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3129 0 0 0 4990 8 0 0 25 0 1 0 481537714 14610432 3041 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3567 3041 603 41 0 3526 0
vsize: 14268
[startup+60.0047 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3407 0 0 0 5989 9 0 0 25 0 1 0 481537714 16359424 3319 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3319 603 41 0 3953 0
vsize: 15976
[startup+70.005 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3543 0 0 0 6989 9 0 0 25 0 1 0 481537714 16982016 3455 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4146 3455 603 41 0 4105 0
vsize: 16584
[startup+80.0059 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3777 0 0 0 7988 10 0 0 25 0 1 0 481537714 17891328 3689 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4368 3689 603 41 0 4327 0
vsize: 17472
[startup+90.0062 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3777 0 0 0 8988 10 0 0 25 0 1 0 481537714 17891328 3689 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4368 3689 603 41 0 4327 0
vsize: 17472
[startup+100.007 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3777 0 0 0 9987 11 0 0 25 0 1 0 481537714 17891328 3689 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4368 3689 603 41 0 4327 0
vsize: 17472
[startup+110.008 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3777 0 0 0 10988 11 0 0 25 0 1 0 481537714 17891328 3689 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4368 3689 603 41 0 4327 0
vsize: 17472
[startup+120.007 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 3869 0 0 0 11987 11 0 0 25 0 1 0 481537714 18296832 3781 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4467 3781 603 41 0 4426 0
vsize: 17868
[startup+130.008 s]
Raw data (loadavg): 0.99 1.01 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 4088 0 0 0 12987 12 0 0 25 0 1 0 481537714 19099648 4000 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4000 603 41 0 4622 0
vsize: 18652
[startup+140.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 4300 0 0 0 13986 13 0 0 25 0 1 0 481537714 20021248 4212 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4888 4212 603 41 0 4847 0
vsize: 19552
[startup+150.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 4496 0 0 0 14986 13 0 0 25 0 1 0 481537714 20946944 4408 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4408 603 41 0 5073 0
vsize: 20456
[startup+160.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 4687 0 0 0 15985 14 0 0 25 0 1 0 481537714 21745664 4599 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5309 4599 603 41 0 5268 0
vsize: 21236
[startup+170.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 4882 0 0 0 16985 15 0 0 25 0 1 0 481537714 22536192 4794 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5502 4794 603 41 0 5461 0
vsize: 22008
[startup+180.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5066 0 0 0 17984 15 0 0 25 0 1 0 481537714 23207936 4978 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5666 4978 603 41 0 5625 0
vsize: 22664
[startup+190.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5254 0 0 0 18984 16 0 0 25 0 1 0 481537714 24006656 5166 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5861 5166 603 41 0 5820 0
vsize: 23444
[startup+200.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5411 0 0 0 19984 16 0 0 25 0 1 0 481537714 24674304 5323 4294967295 134512640 134672761 3221224576 3221223760 134558880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6024 5323 603 41 0 5983 0
vsize: 24096
[startup+210.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5584 0 0 0 20983 17 0 0 25 0 1 0 481537714 25350144 5496 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5496 603 41 0 6148 0
vsize: 24756
[startup+220.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31051
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 21983 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+230.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 22984 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223776 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+240.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 23984 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+250.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 24984 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+260.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 25984 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+270.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 26984 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+280.018 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 27985 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+290.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5604 0 0 0 28985 17 0 0 25 0 1 0 481537714 25350144 5516 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6189 5516 603 41 0 6148 0
vsize: 24756
[startup+300.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5609 0 0 0 29985 17 0 0 25 0 1 0 481537714 25497600 5521 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6225 5521 603 41 0 6184 0
vsize: 24900
[startup+310.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5609 0 0 0 30985 17 0 0 25 0 1 0 481537714 25497600 5521 4294967295 134512640 134672761 3221224576 3221223840 134562196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6225 5521 603 41 0 6184 0
vsize: 24900
[startup+320.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5616 0 0 0 31985 17 0 0 25 0 1 0 481537714 25497600 5528 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6225 5528 603 41 0 6184 0
vsize: 24900
[startup+330.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5745 0 0 0 32985 18 0 0 25 0 1 0 481537714 26034176 5657 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6356 5657 603 41 0 6315 0
vsize: 25424
[startup+340.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 5873 0 0 0 33985 18 0 0 25 0 1 0 481537714 26570752 5785 4294967295 134512640 134672761 3221224576 3221223760 134559514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6487 5785 603 41 0 6446 0
vsize: 25948
[startup+350.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6028 0 0 0 34985 18 0 0 25 0 1 0 481537714 27111424 5940 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 5940 603 41 0 6578 0
vsize: 26476
[startup+360.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 35985 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+370.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 36986 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+380.022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 37986 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+390.022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 38986 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+400.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 39986 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+410.024 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6117 0 0 0 40986 18 0 0 25 0 1 0 481537714 27508736 6029 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6716 6029 603 41 0 6675 0
vsize: 26864
[startup+420.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6119 0 0 0 41985 19 0 0 25 0 1 0 481537714 27508736 6031 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6031 603 41 0 6675 0
vsize: 26864
[startup+430.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 42985 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+440.024 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 43985 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+450.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 44985 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+460.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 45986 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+470.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 46986 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+480.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 47986 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+490.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6120 0 0 0 48986 19 0 0 25 0 1 0 481537714 27508736 6032 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6716 6032 603 41 0 6675 0
vsize: 26864
[startup+500.027 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6264 0 0 0 49986 19 0 0 25 0 1 0 481537714 28172288 6176 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6878 6176 603 41 0 6837 0
vsize: 27512
[startup+510.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6425 0 0 0 50986 19 0 0 25 0 1 0 481537714 28835840 6337 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7040 6337 603 41 0 6999 0
vsize: 28160
[startup+520.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6591 0 0 0 51985 20 0 0 25 0 1 0 481537714 29499392 6503 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7202 6503 603 41 0 7161 0
vsize: 28808
[startup+530.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6708 0 0 0 52985 20 0 0 25 0 1 0 481537714 29900800 6620 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6620 603 41 0 7259 0
vsize: 29200
[startup+540.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6708 0 0 0 53985 20 0 0 25 0 1 0 481537714 29900800 6620 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6620 603 41 0 7259 0
vsize: 29200
[startup+550.031 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6712 0 0 0 54986 20 0 0 25 0 1 0 481537714 29900800 6624 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6624 603 41 0 7259 0
vsize: 29200
[startup+560.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6713 0 0 0 55986 20 0 0 25 0 1 0 481537714 29900800 6625 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6625 603 41 0 7259 0
vsize: 29200
[startup+570.031 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6713 0 0 0 56986 20 0 0 25 0 1 0 481537714 29900800 6625 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6625 603 41 0 7259 0
vsize: 29200
[startup+580.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6713 0 0 0 57986 20 0 0 25 0 1 0 481537714 29900800 6625 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7300 6625 603 41 0 7259 0
vsize: 29200
[startup+590.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6713 0 0 0 58986 21 0 0 25 0 1 0 481537714 29900800 6625 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7300 6625 603 41 0 7259 0
vsize: 29200
[startup+600.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6724 0 0 0 59985 21 0 0 25 0 1 0 481537714 30060544 6636 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6636 603 41 0 7298 0
vsize: 29356
[startup+610.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6724 0 0 0 60986 21 0 0 25 0 1 0 481537714 30060544 6636 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6636 603 41 0 7298 0
vsize: 29356
[startup+620.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6724 0 0 0 61986 21 0 0 25 0 1 0 481537714 30060544 6636 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6636 603 41 0 7298 0
vsize: 29356
[startup+630.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6724 0 0 0 62986 21 0 0 25 0 1 0 481537714 30060544 6636 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6636 603 41 0 7298 0
vsize: 29356
[startup+640.039 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6724 0 0 0 63987 21 0 0 25 0 1 0 481537714 30060544 6636 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6636 603 41 0 7298 0
vsize: 29356
[startup+650.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6727 0 0 0 64987 21 0 0 25 0 1 0 481537714 30060544 6639 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6639 603 41 0 7298 0
vsize: 29356
[startup+660.041 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6727 0 0 0 65987 21 0 0 25 0 1 0 481537714 30060544 6639 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6639 603 41 0 7298 0
vsize: 29356
[startup+670.041 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6727 0 0 0 66987 21 0 0 25 0 1 0 481537714 30060544 6639 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6639 603 41 0 7298 0
vsize: 29356
[startup+680.042 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6750 0 0 0 67988 21 0 0 25 0 1 0 481537714 30208000 6662 4294967295 134512640 134672761 3221224576 3221223680 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7375 6662 603 41 0 7334 0
vsize: 29500
[startup+690.042 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6777 0 0 0 68988 21 0 0 25 0 1 0 481537714 30355456 6689 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7411 6689 603 41 0 7370 0
vsize: 29644
[startup+700.043 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6791 0 0 0 69988 21 0 0 25 0 1 0 481537714 30355456 6703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7411 6703 603 41 0 7370 0
vsize: 29644
[startup+710.044 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6791 0 0 0 70988 21 0 0 25 0 1 0 481537714 30355456 6703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7411 6703 603 41 0 7370 0
vsize: 29644
[startup+720.043 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6893 0 0 0 71988 21 0 0 25 0 1 0 481537714 30756864 6805 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7509 6805 603 41 0 7468 0
vsize: 30036
[startup+730.043 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 6999 0 0 0 72988 22 0 0 25 0 1 0 481537714 31150080 6911 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7605 6911 603 41 0 7564 0
vsize: 30420
[startup+740.044 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7032 0 0 0 73988 22 0 0 25 0 1 0 481537714 31281152 6944 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6944 603 41 0 7596 0
vsize: 30548
[startup+750.045 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7032 0 0 0 74988 22 0 0 25 0 1 0 481537714 31281152 6944 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6944 603 41 0 7596 0
vsize: 30548
[startup+760.045 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 75988 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+770.045 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 76988 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+780.046 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 77988 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+790.046 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 78989 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+800.047 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 79989 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+810.048 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 80989 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+820.048 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7033 0 0 0 81989 22 0 0 25 0 1 0 481537714 31281152 6945 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7637 6945 603 41 0 7596 0
vsize: 30548
[startup+830.049 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7053 0 0 0 82989 22 0 0 25 0 1 0 481537714 31449088 6965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6965 603 41 0 7637 0
vsize: 30712
[startup+840.049 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7055 0 0 0 83990 22 0 0 25 0 1 0 481537714 31449088 6967 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6967 603 41 0 7637 0
vsize: 30712
[startup+850.051 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7055 0 0 0 84990 22 0 0 25 0 1 0 481537714 31449088 6967 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6967 603 41 0 7637 0
vsize: 30712
[startup+860.052 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7055 0 0 0 85990 22 0 0 25 0 1 0 481537714 31449088 6967 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6967 603 41 0 7637 0
vsize: 30712
[startup+870.052 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7055 0 0 0 86990 22 0 0 25 0 1 0 481537714 31449088 6967 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6967 603 41 0 7637 0
vsize: 30712
[startup+880.053 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7055 0 0 0 87990 22 0 0 25 0 1 0 481537714 31449088 6967 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6967 603 41 0 7637 0
vsize: 30712
[startup+890.052 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7057 0 0 0 88991 22 0 0 25 0 1 0 481537714 31449088 6969 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6969 603 41 0 7637 0
vsize: 30712
[startup+900.053 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7057 0 0 0 89990 22 0 0 25 0 1 0 481537714 31449088 6969 4294967295 134512640 134672761 3221224576 3221223776 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6969 603 41 0 7637 0
vsize: 30712
[startup+910.054 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7057 0 0 0 90990 22 0 0 25 0 1 0 481537714 31449088 6969 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6969 603 41 0 7637 0
vsize: 30712
[startup+920.054 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7057 0 0 0 91991 22 0 0 25 0 1 0 481537714 31449088 6969 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6969 603 41 0 7637 0
vsize: 30712
[startup+930.055 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7057 0 0 0 92991 22 0 0 25 0 1 0 481537714 31449088 6969 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7678 6969 603 41 0 7637 0
vsize: 30712
[startup+940.056 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7058 0 0 0 93991 22 0 0 25 0 1 0 481537714 31711232 6970 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 6970 603 41 0 7701 0
vsize: 30968
[startup+950.057 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7060 0 0 0 94991 22 0 0 25 0 1 0 481537714 31711232 6972 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 6972 603 41 0 7701 0
vsize: 30968
[startup+960.058 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7066 0 0 0 95991 22 0 0 25 0 1 0 481537714 31711232 6978 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 6978 603 41 0 7701 0
vsize: 30968
[startup+970.075 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7069 0 0 0 96993 22 0 0 25 0 1 0 481537714 31711232 6981 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 6981 603 41 0 7701 0
vsize: 30968
[startup+980.082 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7078 0 0 0 97994 22 0 0 25 0 1 0 481537714 31875072 6990 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6990 603 41 0 7741 0
vsize: 31128
[startup+990.083 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7078 0 0 0 98994 22 0 0 25 0 1 0 481537714 31875072 6990 4294967295 134512640 134672761 3221224576 3221223680 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6990 603 41 0 7741 0
vsize: 31128
[startup+1000.08 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7078 0 0 0 99994 22 0 0 25 0 1 0 481537714 31875072 6990 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6990 603 41 0 7741 0
vsize: 31128
[startup+1010.08 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 100995 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1020.08 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 101995 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223680 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1030.08 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 102995 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1040.08 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 103995 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1050.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 104995 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1060.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7079 0 0 0 105996 22 0 0 25 0 1 0 481537714 31875072 6991 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6991 603 41 0 7741 0
vsize: 31128
[startup+1070.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7081 0 0 0 106996 23 0 0 25 0 1 0 481537714 31875072 6993 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6993 603 41 0 7741 0
vsize: 31128
[startup+1080.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7081 0 0 0 107996 23 0 0 25 0 1 0 481537714 31875072 6993 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6993 603 41 0 7741 0
vsize: 31128
[startup+1090.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7082 0 0 0 108996 23 0 0 25 0 1 0 481537714 31875072 6994 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6994 603 41 0 7741 0
vsize: 31128
[startup+1100.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7082 0 0 0 109996 23 0 0 25 0 1 0 481537714 31875072 6994 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6994 603 41 0 7741 0
vsize: 31128
[startup+1110.11 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7082 0 0 0 110999 23 0 0 25 0 1 0 481537714 31875072 6994 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6994 603 41 0 7741 0
vsize: 31128
[startup+1120.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7082 0 0 0 112002 23 0 0 25 0 1 0 481537714 31875072 6994 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 6994 603 41 0 7741 0
vsize: 31128
[startup+1130.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7092 0 0 0 113003 23 0 0 25 0 1 0 481537714 31875072 7004 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 7004 603 41 0 7741 0
vsize: 31128
[startup+1140.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7109 0 0 0 114003 23 0 0 25 0 1 0 481537714 31875072 7021 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7782 7021 603 41 0 7741 0
vsize: 31128
[startup+1150.15 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7231 0 0 0 115003 23 0 0 25 0 1 0 481537714 32468992 7143 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7927 7143 603 41 0 7886 0
vsize: 31708
[startup+1160.19 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7355 0 0 0 116007 23 0 0 25 0 1 0 481537714 32993280 7267 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7267 603 41 0 8014 0
vsize: 32220
[startup+1170.19 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7473 0 0 0 117007 24 0 0 25 0 1 0 481537714 33525760 7385 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7385 603 41 0 8144 0
vsize: 32740
[startup+1180.2 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7473 0 0 0 118007 24 0 0 25 0 1 0 481537714 33525760 7385 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7385 603 41 0 8144 0
vsize: 32740
[startup+1190.2 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7473 0 0 0 119007 24 0 0 25 0 1 0 481537714 33525760 7385 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7385 603 41 0 8144 0
vsize: 32740
[startup+1200.2 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 31053
Raw data (stat): 31051 (minisat+) R 31050 23176 23175 0 -1 0 7473 0 0 0 120007 24 0 0 25 0 1 0 481537714 33525760 7385 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7385 603 41 0 8144 0
vsize: 32740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 0.99 1.00 0.94 1/54 31053
Raw data (stat): 31051 (minisat+) Z 31050 23176 23175 0 -1 12 7476 0 0 0 120007 25 0 0 25 0 1 0 481537714 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.21
CPU time (s): 1200.34
CPU user time (s): 1200.08
CPU system time (s): 0.25896
CPU usage (%): 100.01
Max. virtual memory (Kb): 32740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####