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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-3.opb
MD5SUM	25457db86ce3cc3b7604dfa37c8096b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
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	595
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	1175.05
Number of variables	595
Total number of constraints	27931
Number of constraints which are clauses	27931
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	2
Trace number 6365

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 04:37:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4833 boxname=wulflinc13 idbench=321 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  25457db86ce3cc3b7604dfa37c8096b4  /oldhome/oroussel/tmp/wulflinc13/normalized-frb35-17-3.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-frb35-17-3.opb /oldhome/oroussel/tmp/wulflinc13/normalized-frb35-17-3.opb
IDLAUNCH: 4833
/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:        889208 kB
Buffers:         35540 kB
Cached:          90072 kB
SwapCached:        392 kB
Active:          56592 kB
Inactive:        72228 kB
HighTotal:      131008 kB
HighFree:        37100 kB
LowTotal:       903652 kB
LowFree:        852108 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11220 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:57:30 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4833 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27931 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 |   27931    55862 |    9310       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   84836   189074 |   28278       0        0     nan |  0.000 % |
c |       100 |   84649   188653 |   31105      97      489     5.0 |  0.264 % |
c |       251 |   83195   185337 |   34216     212     1332     6.3 |  2.465 % |
c |       476 |   80550   179269 |   37638     381     2677     7.0 |  6.645 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       597 |   79952   177901 |   26650     492     3422     7.0 |  6.645 % |
c |       697 |   78808   175293 |   29315     568     4119     7.3 |  9.310 % |
c |       847 |   77450   172175 |   32246     691     5064     7.3 | 11.470 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       900 |   77595   172619 |   25865     740     5372     7.3 | 11.470 % |
c |      1000 |   76265   169563 |   28451     817     6467     7.9 | 13.858 % |
c |      1151 |   73727   163715 |   31296     893     7295     8.2 | 17.958 % |
c |      1376 |   71413   158360 |   34426    1058     8587     8.1 | 21.786 % |
c |      1714 |   68317   151203 |   37868    1301    11186     8.6 | 26.831 % |
c |      2220 |   63827   140766 |   41655    1601    13806     8.6 | 34.337 % |
c |      2980 |   56601   123824 |   45821    2051    17980     8.8 | 47.114 % |
c |      4119 |   50676   109968 |   50403    2759    27782    10.1 | 56.986 % |
c |      5827 |   46189    99456 |   55443    4083    56507    13.8 | 64.707 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7041 |   43684    93531 |   14561    4973    77119    15.5 | 64.707 % |
c |      7142 |   43468    93027 |   16017    5023    77689    15.5 | 69.545 % |
c |      7292 |   43242    92501 |   17618    5148    79828    15.5 | 69.931 % |
c |      7517 |   43242    92501 |   19380    5373    86254    16.1 | 69.931 % |
c |      7854 |   42671    91178 |   21318    5562   100305    18.0 | 70.898 % |
c |      8360 |   41569    88586 |   23450    5690   112874    19.8 | 73.084 % |
c |      9119 |   40646    86424 |   25795    6191   135035    21.8 | 74.524 % |
c |     10258 |   40241    85449 |   28375    7087   236319    33.3 | 75.301 % |
c ==============================================================================
c [1mFound solution: -29[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 |     10774 |   40170    85302 |   13390    7573   259805    34.3 | 75.301 % |
c |     10874 |   39996    84901 |   14729    7669   260726    34.0 | 75.772 % |
c |     11024 |   39934    84757 |   16201    7801   265272    34.0 | 75.875 % |
c |     11249 |   39640    84067 |   17822    7871   268743    34.1 | 76.398 % |
c |     11586 |   39628    84039 |   19604    8205   275469    33.6 | 76.419 % |
c |     12092 |   39519    83784 |   21564    8689   290797    33.5 | 76.614 % |
c |     12851 |   39299    83274 |   23721    9438   312171    33.1 | 76.984 % |
c |     13990 |   38968    82503 |   26093   10399   382374    36.8 | 77.554 % |
c ==============================================================================
c [1mFound solution: -30[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 |     14541 |   38929    82381 |   12976   10932   401713    36.7 | 77.554 % |
c |     14641 |   38829    82143 |   14273   10965   402064    36.7 | 77.788 % |
c |     14792 |   38829    82143 |   15700   11116   409361    36.8 | 77.788 % |
c |     15017 |   38774    82014 |   17271   11326   417411    36.9 | 77.880 % |
c |     15354 |   38471    81298 |   18998   11529   428300    37.1 | 78.429 % |
c |     15860 |   38445    81237 |   20897   12020   452908    37.7 | 78.476 % |
c |     16620 |   37876    79913 |   22987   12689   483173    38.1 | 79.436 % |
c |     17759 |   37876    79913 |   25286   13828   514733    37.2 | 79.436 % |
c |     19468 |   37622    79312 |   27815   15084   643195    42.6 | 79.893 % |
c ==============================================================================
c [1mFound solution: -31[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 |     21502 |   37506    79055 |   12502   16994   823142    48.4 | 79.893 % |
c |     21603 |   37506    79055 |   13752   17095   828347    48.5 | 80.224 % |
c |     21753 |   37382    78759 |   15127   17070   830111    48.6 | 80.459 % |
c |     21978 |   37232    78400 |   16640   17083   847247    49.6 | 80.746 % |
c |     22315 |   37232    78400 |   18304   17420   860224    49.4 | 80.746 % |
c |     22821 |   37232    78400 |   20134   17926   895877    50.0 | 80.746 % |
c |     23582 |   37232    78400 |   22148   18687   956743    51.2 | 80.746 % |
c |     24721 |   37232    78400 |   24362   19826  1037936    52.4 | 80.746 % |
c |     26429 |   36879    77570 |   26799   20885  1184221    56.7 | 81.390 % |
c |     28992 |   36879    77570 |   29479   23448  1374031    58.6 | 81.390 % |
c ==============================================================================
c [1mFound solution: -32[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 |     30702 |   36850    77490 |   12283   24884  1467144    59.0 | 81.390 % |
c |     30803 |   36850    77490 |   13511   24985  1473914    59.0 | 81.433 % |
c |     30954 |   36850    77490 |   14862   25136  1482237    59.0 | 81.433 % |
c |     31181 |   36850    77490 |   16348   25363  1491356    58.8 | 81.433 % |
c |     31518 |   36549    76783 |   17983   25323  1501735    59.3 | 81.975 % |
c |     32024 |   36549    76783 |   19781   25829  1533853    59.4 | 81.975 % |
c |     32783 |   36549    76783 |   21760   26588  1567874    59.0 | 81.975 % |
c |     33922 |   36527    76731 |   23936   27717  1630199    58.8 | 82.016 % |
c |     35631 |   36187    75938 |   26329   28661  1705443    59.5 | 82.599 % |
c |     38193 |   36156    75863 |   28962   31221  1821738    58.3 | 82.665 % |
c |     42037 |   36156    75863 |   31858   35065  1982905    56.5 | 82.665 % |
c ==============================================================================
c [1mFound solution: -33[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 |     44490 |   36106    75754 |   12035   37262  2087197    56.0 | 82.665 % |
c |     44590 |   36106    75754 |   13238   16395   571866    34.9 | 82.770 % |
c |     44742 |   36106    75754 |   14562   16547   581385    35.1 | 82.770 % |
c |     44967 |   36106    75754 |   16018   16772   592756    35.3 | 82.770 % |
c |     45304 |   36106    75754 |   17620   17109   605409    35.4 | 82.770 % |
c |     45810 |   36106    75754 |   19382   17615   632544    35.9 | 82.770 % |
c |     46570 |   35552    74454 |   21320   18338   663919    36.2 | 83.781 % |
c |     47709 |   35552    74454 |   23452   19477   717712    36.8 | 83.781 % |
c |     49417 |   35497    74320 |   25798   21181   820583    38.7 | 83.893 % |
c |     51979 |   35497    74320 |   28377   23743   945741    39.8 | 83.893 % |
c |     55823 |   35266    73782 |   31215   27578  1162021    42.1 | 84.281 % |
c |     61589 |   35201    73626 |   34337   33315  1449565    43.5 | 84.419 % |
c |     70240 |   35123    73442 |   37770   41954  1741015    41.5 | 84.562 % |
c ==============================================================================
c [1mFound solution: -34[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 |     71810 |   35091    73340 |   11697   43511  1800047    41.4 | 84.562 % |
c |     71910 |   35091    73340 |   12866   17253   462740    26.8 | 84.610 % |
c |     72060 |   35091    73340 |   14153   17403   465970    26.8 | 84.610 % |
c |     72285 |   35091    73340 |   15568   17628   471595    26.8 | 84.610 % |
c |     72623 |   35091    73340 |   17125   17966   479737    26.7 | 84.610 % |
c |     73129 |   35085    73326 |   18838   18470   490977    26.6 | 84.620 % |
c |     73888 |   35085    73326 |   20721   19229   508667    26.5 | 84.620 % |
c |     75027 |   35085    73326 |   22794   20368   543891    26.7 | 84.620 % |
c |     76735 |   35085    73326 |   25073   22076   592258    26.8 | 84.620 % |
c |     79300 |   35085    73326 |   27580   24641   654239    26.6 | 84.620 % |
c |     83144 |   35071    73292 |   30339   28483   814120    28.6 | 84.651 % |
c |     88910 |   35071    73292 |   33372   34249  1029665    30.1 | 84.651 % |
c |     97559 |   35061    73269 |   36710   42896  1457302    34.0 | 84.666 % |
c |    110533 |   35033    73203 |   40381   21630   456096    21.1 | 84.717 % |
c |    129995 |   35033    73203 |   44419   41092  1140107    27.7 | 84.717 % |
c |    159187 |   35009    73148 |   48861   26669   689614    25.9 | 84.753 % |
c |    202976 |   34767    72575 |   53747   23258   553945    23.8 | 85.223 % |
c |    268660 |   34721    72466 |   59122   39514  1155077    29.2 | 85.310 % |
c |    367188 |   33784    70346 |   65034   30364   815982    26.9 | 86.366 % |
c |    514977 |   33587    69927 |   71537   53411  1776762    33.3 | 86.494 % |
#### 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 0.98 0.91 2/54 5873
Raw data (stat): 5873 (runsolver) R 5872 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423548975 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 2414 0 0 0 990 8 0 0 25 0 1 0 423548975 12292096 2385 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2385 603 41 0 2960 0
vsize: 12004
[startup+20.0013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 2440 0 0 0 1989 8 0 0 25 0 1 0 423548975 12402688 2411 4294967295 134512640 134672761 3221224560 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3028 2411 603 41 0 2987 0
vsize: 12112
[startup+30.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 2868 0 0 0 2987 10 0 0 25 0 1 0 423548975 14147584 2839 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3454 2839 603 41 0 3413 0
vsize: 13816
[startup+40.0012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 3428 0 0 0 3985 12 0 0 25 0 1 0 423548975 16461824 3399 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4019 3399 603 41 0 3978 0
vsize: 16076
[startup+50.0022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 3956 0 0 0 4983 14 0 0 25 0 1 0 423548975 18599936 3927 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4541 3927 603 41 0 4500 0
vsize: 18164
[startup+60.0029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4267 0 0 0 5982 15 0 0 25 0 1 0 423548975 19959808 4238 4294967295 134512640 134672761 3221224560 3221223664 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4238 603 41 0 4832 0
vsize: 19492
[startup+70.0041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4534 0 0 0 6981 16 0 0 25 0 1 0 423548975 21147648 4505 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5163 4505 603 41 0 5122 0
vsize: 20652
[startup+80.0053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4735 0 0 0 7980 17 0 0 25 0 1 0 423548975 21950464 4706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4706 603 41 0 5318 0
vsize: 21436
[startup+90.0049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4735 0 0 0 8979 18 0 0 25 0 1 0 423548975 21950464 4706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4706 603 41 0 5318 0
vsize: 21436
[startup+100.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4735 0 0 0 9979 18 0 0 25 0 1 0 423548975 21950464 4706 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4706 603 41 0 5318 0
vsize: 21436
[startup+110.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4736 0 0 0 10979 18 0 0 25 0 1 0 423548975 21950464 4707 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4707 603 41 0 5318 0
vsize: 21436
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4741 0 0 0 11978 19 0 0 25 0 1 0 423548975 21950464 4712 4294967295 134512640 134672761 3221224560 3221223860 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4712 603 41 0 5318 0
vsize: 21436
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4741 0 0 0 12978 19 0 0 25 0 1 0 423548975 21950464 4712 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4712 603 41 0 5318 0
vsize: 21436
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4741 0 0 0 13977 20 0 0 25 0 1 0 423548975 21950464 4712 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4712 603 41 0 5318 0
vsize: 21436
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4741 0 0 0 14977 20 0 0 25 0 1 0 423548975 21950464 4712 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4712 603 41 0 5318 0
vsize: 21436
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4742 0 0 0 15976 20 0 0 25 0 1 0 423548975 21950464 4713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4713 603 41 0 5318 0
vsize: 21436
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4750 0 0 0 16976 21 0 0 25 0 1 0 423548975 21950464 4721 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5359 4721 603 41 0 5318 0
vsize: 21436
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4771 0 0 0 17975 21 0 0 25 0 1 0 423548975 22110208 4742 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4742 603 41 0 5357 0
vsize: 21592
[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 18974 22 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 19974 22 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+210.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 20974 22 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 21974 22 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 22974 23 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+240.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4776 0 0 0 23974 23 0 0 25 0 1 0 423548975 22110208 4747 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4747 603 41 0 5357 0
vsize: 21592
[startup+250.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4778 0 0 0 24974 23 0 0 25 0 1 0 423548975 22110208 4749 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4749 603 41 0 5357 0
vsize: 21592
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4783 0 0 0 25974 23 0 0 25 0 1 0 423548975 22110208 4754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4754 603 41 0 5357 0
vsize: 21592
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4784 0 0 0 26974 23 0 0 25 0 1 0 423548975 22110208 4755 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4755 603 41 0 5357 0
vsize: 21592
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4784 0 0 0 27974 23 0 0 25 0 1 0 423548975 22110208 4755 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4755 603 41 0 5357 0
vsize: 21592
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4789 0 0 0 28975 23 0 0 25 0 1 0 423548975 22110208 4760 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4760 603 41 0 5357 0
vsize: 21592
[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4789 0 0 0 29975 23 0 0 25 0 1 0 423548975 22110208 4760 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4760 603 41 0 5357 0
vsize: 21592
[startup+310.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4798 0 0 0 30975 23 0 0 25 0 1 0 423548975 22110208 4769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 4769 603 41 0 5357 0
vsize: 21592
[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4808 0 0 0 31975 23 0 0 25 0 1 0 423548975 22302720 4779 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5445 4779 603 41 0 5404 0
vsize: 21780
[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 4876 0 0 0 32975 23 0 0 25 0 1 0 423548975 22564864 4847 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5509 4847 603 41 0 5468 0
vsize: 22036
[startup+340.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5054 0 0 0 33975 24 0 0 25 0 1 0 423548975 23224320 5025 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5670 5025 603 41 0 5629 0
vsize: 22680
[startup+350.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5126 0 0 0 34975 24 0 0 25 0 1 0 423548975 23752704 5097 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5799 5097 603 41 0 5758 0
vsize: 23196
[startup+360.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5127 0 0 0 35975 24 0 0 25 0 1 0 423548975 23752704 5098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5799 5098 603 41 0 5758 0
vsize: 23196
[startup+370.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5130 0 0 0 36976 24 0 0 25 0 1 0 423548975 23752704 5101 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5799 5101 603 41 0 5758 0
vsize: 23196
[startup+380.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5131 0 0 0 37976 24 0 0 25 0 1 0 423548975 23752704 5102 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5799 5102 603 41 0 5758 0
vsize: 23196
[startup+390.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5133 0 0 0 38976 24 0 0 25 0 1 0 423548975 23887872 5104 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5832 5104 603 41 0 5791 0
vsize: 23328
[startup+400.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5138 0 0 0 39976 24 0 0 25 0 1 0 423548975 23887872 5109 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5832 5109 603 41 0 5791 0
vsize: 23328
[startup+410.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5146 0 0 0 40976 24 0 0 25 0 1 0 423548975 23887872 5117 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5832 5117 603 41 0 5791 0
vsize: 23328
[startup+420.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5153 0 0 0 41977 24 0 0 25 0 1 0 423548975 23887872 5124 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5832 5124 603 41 0 5791 0
vsize: 23328
[startup+430.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5347 0 0 0 42976 24 0 0 25 0 1 0 423548975 24690688 5318 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6028 5318 603 41 0 5987 0
vsize: 24112
[startup+440.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5465 0 0 0 43976 25 0 0 25 0 1 0 423548975 25223168 5436 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5436 603 41 0 6117 0
vsize: 24632
[startup+450.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5465 0 0 0 44976 25 0 0 25 0 1 0 423548975 25223168 5436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5436 603 41 0 6117 0
vsize: 24632
[startup+460.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5465 0 0 0 45976 25 0 0 25 0 1 0 423548975 25223168 5436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5436 603 41 0 6117 0
vsize: 24632
[startup+470.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5469 0 0 0 46977 25 0 0 25 0 1 0 423548975 25223168 5440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5440 603 41 0 6117 0
vsize: 24632
[startup+480.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5469 0 0 0 47977 25 0 0 25 0 1 0 423548975 25223168 5440 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5440 603 41 0 6117 0
vsize: 24632
[startup+490.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5470 0 0 0 48977 25 0 0 25 0 1 0 423548975 25223168 5441 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5441 603 41 0 6117 0
vsize: 24632
[startup+500.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5484 0 0 0 49977 25 0 0 25 0 1 0 423548975 25223168 5455 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6158 5455 603 41 0 6117 0
vsize: 24632
[startup+510.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5496 0 0 0 50977 25 0 0 25 0 1 0 423548975 25387008 5467 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5467 603 41 0 6157 0
vsize: 24792
[startup+520.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5506 0 0 0 51977 25 0 0 25 0 1 0 423548975 25387008 5477 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5477 603 41 0 6157 0
vsize: 24792
[startup+530.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5514 0 0 0 52978 25 0 0 25 0 1 0 423548975 25387008 5485 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5485 603 41 0 6157 0
vsize: 24792
[startup+540.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5514 0 0 0 53978 25 0 0 25 0 1 0 423548975 25387008 5485 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5485 603 41 0 6157 0
vsize: 24792
[startup+550.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5514 0 0 0 54978 25 0 0 25 0 1 0 423548975 25387008 5485 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5485 603 41 0 6157 0
vsize: 24792
[startup+560.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5523 0 0 0 55978 25 0 0 25 0 1 0 423548975 25534464 5494 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5494 603 41 0 6193 0
vsize: 24936
[startup+570.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5527 0 0 0 56978 25 0 0 25 0 1 0 423548975 25534464 5498 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5498 603 41 0 6193 0
vsize: 24936
[startup+580.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5532 0 0 0 57978 25 0 0 25 0 1 0 423548975 25534464 5503 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5503 603 41 0 6193 0
vsize: 24936
[startup+590.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5535 0 0 0 58979 25 0 0 25 0 1 0 423548975 25534464 5506 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5506 603 41 0 6193 0
vsize: 24936
[startup+600.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5568 0 0 0 59979 25 0 0 25 0 1 0 423548975 25673728 5539 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6268 5539 603 41 0 6227 0
vsize: 25072
[startup+610.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5618 0 0 0 60979 25 0 0 25 0 1 0 423548975 25935872 5589 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6332 5589 603 41 0 6291 0
vsize: 25328
[startup+620.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5800 0 0 0 61979 26 0 0 25 0 1 0 423548975 26599424 5771 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6494 5771 603 41 0 6453 0
vsize: 25976
[startup+630.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 5975 0 0 0 62978 27 0 0 25 0 1 0 423548975 27394048 5946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6688 5946 603 41 0 6647 0
vsize: 26752
[startup+640.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6103 0 0 0 63978 27 0 0 25 0 1 0 423548975 27791360 6074 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6785 6074 603 41 0 6744 0
vsize: 27140
[startup+650.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6103 0 0 0 64978 27 0 0 25 0 1 0 423548975 27791360 6074 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6785 6074 603 41 0 6744 0
vsize: 27140
[startup+660.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6106 0 0 0 65977 27 0 0 25 0 1 0 423548975 27791360 6077 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6785 6077 603 41 0 6744 0
vsize: 27140
[startup+670.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6108 0 0 0 66977 27 0 0 25 0 1 0 423548975 27791360 6079 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6785 6079 603 41 0 6744 0
vsize: 27140
[startup+680.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6108 0 0 0 67978 27 0 0 25 0 1 0 423548975 27791360 6079 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6785 6079 603 41 0 6744 0
vsize: 27140
[startup+690.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6115 0 0 0 68978 27 0 0 25 0 1 0 423548975 27955200 6086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6086 603 41 0 6784 0
vsize: 27300
[startup+700.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6121 0 0 0 69978 27 0 0 25 0 1 0 423548975 27955200 6092 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6092 603 41 0 6784 0
vsize: 27300
[startup+710.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6127 0 0 0 70978 27 0 0 25 0 1 0 423548975 27955200 6098 4294967295 134512640 134672761 3221224560 3221223744 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6098 603 41 0 6784 0
vsize: 27300
[startup+720.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6127 0 0 0 71978 27 0 0 25 0 1 0 423548975 27955200 6098 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6098 603 41 0 6784 0
vsize: 27300
[startup+730.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6127 0 0 0 72978 27 0 0 25 0 1 0 423548975 27955200 6098 4294967295 134512640 134672761 3221224560 3221223696 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6098 603 41 0 6784 0
vsize: 27300
[startup+740.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6128 0 0 0 73978 27 0 0 25 0 1 0 423548975 27955200 6099 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6099 603 41 0 6784 0
vsize: 27300
[startup+750.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6133 0 0 0 74979 27 0 0 25 0 1 0 423548975 27955200 6104 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6104 603 41 0 6784 0
vsize: 27300
[startup+760.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6133 0 0 0 75979 27 0 0 25 0 1 0 423548975 27955200 6104 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6825 6104 603 41 0 6784 0
vsize: 27300
[startup+770.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6197 0 0 0 76978 28 0 0 25 0 1 0 423548975 28217344 6168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6889 6168 603 41 0 6848 0
vsize: 27556
[startup+780.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6339 0 0 0 77978 28 0 0 25 0 1 0 423548975 28749824 6310 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6310 603 41 0 6978 0
vsize: 28076
[startup+790.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6339 0 0 0 78978 28 0 0 25 0 1 0 423548975 28749824 6310 4294967295 134512640 134672761 3221224560 3221223712 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6310 603 41 0 6978 0
vsize: 28076
[startup+800.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6339 0 0 0 79979 28 0 0 25 0 1 0 423548975 28749824 6310 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6310 603 41 0 6978 0
vsize: 28076
[startup+810.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6345 0 0 0 80979 28 0 0 25 0 1 0 423548975 28913664 6316 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6316 603 41 0 7018 0
vsize: 28236
[startup+820.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6351 0 0 0 81979 28 0 0 25 0 1 0 423548975 28913664 6322 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6322 603 41 0 7018 0
vsize: 28236
[startup+830.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6352 0 0 0 82979 28 0 0 25 0 1 0 423548975 28913664 6323 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6323 603 41 0 7018 0
vsize: 28236
[startup+840.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6352 0 0 0 83979 28 0 0 25 0 1 0 423548975 28913664 6323 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6323 603 41 0 7018 0
vsize: 28236
[startup+850.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6353 0 0 0 84979 28 0 0 25 0 1 0 423548975 28913664 6324 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6324 603 41 0 7018 0
vsize: 28236
[startup+860.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6353 0 0 0 85980 28 0 0 25 0 1 0 423548975 28913664 6324 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6324 603 41 0 7018 0
vsize: 28236
[startup+870.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6364 0 0 0 86980 28 0 0 25 0 1 0 423548975 28913664 6335 4294967295 134512640 134672761 3221224560 3221223712 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6335 603 41 0 7018 0
vsize: 28236
[startup+880.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6365 0 0 0 87980 28 0 0 25 0 1 0 423548975 28913664 6336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6336 603 41 0 7018 0
vsize: 28236
[startup+890.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6365 0 0 0 88980 28 0 0 25 0 1 0 423548975 28913664 6336 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6336 603 41 0 7018 0
vsize: 28236
[startup+900.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6465 0 0 0 89980 29 0 0 25 0 1 0 423548975 29327360 6436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7160 6436 603 41 0 7119 0
vsize: 28640
[startup+910.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6477 0 0 0 90980 29 0 0 25 0 1 0 423548975 29458432 6448 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6448 603 41 0 7151 0
vsize: 28768
[startup+920.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6477 0 0 0 91980 29 0 0 25 0 1 0 423548975 29458432 6448 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6448 603 41 0 7151 0
vsize: 28768
[startup+930.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6477 0 0 0 92980 29 0 0 25 0 1 0 423548975 29458432 6448 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6448 603 41 0 7151 0
vsize: 28768
[startup+940.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6477 0 0 0 93980 29 0 0 25 0 1 0 423548975 29458432 6448 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6448 603 41 0 7151 0
vsize: 28768
[startup+950.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6477 0 0 0 94981 29 0 0 25 0 1 0 423548975 29458432 6448 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6448 603 41 0 7151 0
vsize: 28768
[startup+960.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6482 0 0 0 95981 29 0 0 25 0 1 0 423548975 29458432 6453 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6453 603 41 0 7151 0
vsize: 28768
[startup+970.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6483 0 0 0 96981 29 0 0 25 0 1 0 423548975 29458432 6454 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6454 603 41 0 7151 0
vsize: 28768
[startup+980.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6483 0 0 0 97981 29 0 0 25 0 1 0 423548975 29458432 6454 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6454 603 41 0 7151 0
vsize: 28768
[startup+990.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6494 0 0 0 98981 29 0 0 25 0 1 0 423548975 29458432 6465 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6465 603 41 0 7151 0
vsize: 28768
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6503 0 0 0 99981 29 0 0 25 0 1 0 423548975 29593600 6474 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6474 603 41 0 7184 0
vsize: 28900
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6503 0 0 0 100981 29 0 0 25 0 1 0 423548975 29593600 6474 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6474 603 41 0 7184 0
vsize: 28900
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6504 0 0 0 101982 29 0 0 25 0 1 0 423548975 29593600 6475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6475 603 41 0 7184 0
vsize: 28900
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6605 0 0 0 102982 29 0 0 25 0 1 0 423548975 29990912 6576 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7322 6576 603 41 0 7281 0
vsize: 29288
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6749 0 0 0 103982 30 0 0 25 0 1 0 423548975 30523392 6720 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7452 6720 603 41 0 7411 0
vsize: 29808
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6849 0 0 0 104982 30 0 0 25 0 1 0 423548975 30924800 6820 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6820 603 41 0 7509 0
vsize: 30200
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6849 0 0 0 105982 30 0 0 25 0 1 0 423548975 30924800 6820 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6820 603 41 0 7509 0
vsize: 30200
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6857 0 0 0 106982 30 0 0 25 0 1 0 423548975 30924800 6828 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6828 603 41 0 7509 0
vsize: 30200
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6858 0 0 0 107982 30 0 0 25 0 1 0 423548975 30924800 6829 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6829 603 41 0 7509 0
vsize: 30200
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6858 0 0 0 108982 30 0 0 25 0 1 0 423548975 30924800 6829 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6829 603 41 0 7509 0
vsize: 30200
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 109982 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 110983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 111983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 112983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 113983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 114983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 115983 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 116984 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6859 0 0 0 117984 30 0 0 25 0 1 0 423548975 30924800 6830 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7550 6830 603 41 0 7509 0
vsize: 30200
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6863 0 0 0 118984 30 0 0 25 0 1 0 423548975 31068160 6834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7585 6834 603 41 0 7544 0
vsize: 30340
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 5873
Raw data (stat): 5873 (minisat+) R 5872 30701 30700 0 -1 0 6863 0 0 0 119984 30 0 0 25 0 1 0 423548975 31068160 6834 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7585 6834 603 41 0 7544 0
vsize: 30340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 5873
Raw data (stat): 5873 (minisat+) Z 5872 30701 30700 0 -1 12 6866 0 0 0 119984 31 0 0 25 0 1 0 423548975 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.16
CPU user time (s): 1199.85
CPU system time (s): 0.317951
CPU usage (%): 100.01
Max. virtual memory (Kb): 30340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####