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-ii32e1.opb
MD5SUM	33d46caaa6c22613488909eddb5a530f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	162
Optimality of the best value was proved	NO
Number of terms in the objective function	444
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	444
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	444
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02184
Number of variables	444
Total number of constraints	1408
Number of constraints which are clauses	1408
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	32
Trace number 4724

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 20:05:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3542 boxname=wulflinc5 idbench=158 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  33d46caaa6c22613488909eddb5a530f  /oldhome/oroussel/tmp/wulflinc5/normalized-ii32e1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-ii32e1.opb /oldhome/oroussel/tmp/wulflinc5/normalized-ii32e1.opb
IDLAUNCH: 3542
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        925392 kB
Buffers:         32988 kB
Cached:          54976 kB
SwapCached:       2272 kB
Active:          47912 kB
Inactive:        45148 kB
HighTotal:      131008 kB
HighFree:        72156 kB
LowTotal:       903652 kB
LowFree:        853236 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10552 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:25:06 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 3542 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1408 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 |    1408     6426 |     469       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 205[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 876   maxlim: 239   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7492    28138 |    2497       0        0     nan |  0.000 % |
c |       100 |    7492    28138 |    2746     100     2058    20.6 |  0.303 % |
c |       250 |    7492    28138 |    3021     250     3922    15.7 |  0.303 % |
c |       475 |    7492    28138 |    3323     475     8294    17.5 |  0.303 % |
c |       815 |    7492    28138 |    3655     815    15573    19.1 |  0.303 % |
c ==============================================================================
c [1mFound solution: 193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 251   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       902 |    7510    28217 |    2503     902    16660    18.5 |  0.303 % |
c |      1002 |    7510    28217 |    2753    1002    18586    18.5 |  0.453 % |
c ==============================================================================
c [1mFound solution: 178[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 266   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1106 |    7513    28228 |    2504    1105    19547    17.7 |  0.453 % |
c |      1206 |    7513    28228 |    2754    1205    21259    17.6 |  0.753 % |
c |      1357 |    7513    28228 |    3029    1356    23261    17.2 |  0.753 % |
c |      1582 |    7513    28228 |    3332    1581    27688    17.5 |  0.753 % |
c |      1920 |    7513    28228 |    3666    1919    33037    17.2 |  0.753 % |
c |      2427 |    7513    28228 |    4032    2426    48376    19.9 |  0.753 % |
c |      3186 |    7513    28228 |    4435    3185    80175    25.2 |  0.753 % |
c |      4326 |    7513    28228 |    4879    4325   167235    38.7 |  0.753 % |
c ==============================================================================
c [1mFound solution: 176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 268   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5194 |    7519    28260 |    2506    5193   187286    36.1 |  0.753 % |
c |      5294 |    7519    28260 |    2756    1399    23232    16.6 |  0.902 % |
c |      5444 |    7519    28260 |    3032    1549    27532    17.8 |  0.902 % |
c |      5670 |    7519    28260 |    3335    1775    31500    17.7 |  0.902 % |
c |      6008 |    7519    28260 |    3669    2113    41238    19.5 |  0.902 % |
c |      6514 |    7519    28260 |    4035    2619    55758    21.3 |  0.902 % |
c |      7273 |    7519    28260 |    4439    3378    92040    27.2 |  0.902 % |
c |      8412 |    7519    28260 |    4883    4517   140522    31.1 |  0.902 % |
c |     10123 |    7519    28260 |    5371    3405   153957    45.2 |  0.902 % |
c |     12686 |    7519    28260 |    5909    5968   302496    50.7 |  0.902 % |
c |     16530 |    7519    28260 |    6499    3712   110312    29.7 |  0.902 % |
c |     22296 |    7519    28260 |    7149    5830   464626    79.7 |  0.902 % |
c |     30947 |    7519    28260 |    7864    6568   515631    78.5 |  0.902 % |
c |     43922 |    7519    28260 |    8651    6475   459196    70.9 |  0.902 % |
c |     63383 |    7519    28260 |    9516    7082   442580    62.5 |  0.902 % |
c ==============================================================================
c [1mFound solution: 175[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 269   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74629 |    7520    28268 |    2506    8690   264938    30.5 |  0.902 % |
c |     74729 |    7520    28268 |    2756    2273    53022    23.3 |  0.976 % |
c |     74879 |    7520    28268 |    3032    2423    56935    23.5 |  0.976 % |
c |     75104 |    7520    28268 |    3335    2648    62170    23.5 |  0.976 % |
c |     75441 |    7520    28268 |    3669    2985    74936    25.1 |  0.976 % |
c |     75948 |    7520    28268 |    4035    3492    94537    27.1 |  0.976 % |
c |     76710 |    7520    28268 |    4439    2148    40103    18.7 |  0.976 % |
c |     77849 |    7520    28268 |    4883    3287    83586    25.4 |  0.976 % |
c |     79557 |    7520    28268 |    5371    2503    44659    17.8 |  0.976 % |
c |     82122 |    7520    28268 |    5909    5068   218634    43.1 |  0.976 % |
c |     85966 |    7520    28268 |    6499    5560   330199    59.4 |  0.976 % |
c |     91732 |    7520    28268 |    7149    4064   244047    60.1 |  0.976 % |
c |    100383 |    7520    28268 |    7864    4933   324727    65.8 |  0.977 % |
c |    113358 |    7520    28268 |    8651    4974   316057    63.5 |  0.976 % |
c ==============================================================================
c [1mFound solution: 174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 270   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    116927 |    7521    28277 |    2507    8543   496635    58.1 |  0.976 % |
c |    117027 |    7521    28277 |    2757    2236    63808    28.5 |  1.051 % |
c |    117177 |    7521    28277 |    3033    2386    66998    28.1 |  1.050 % |
c |    117403 |    7521    28277 |    3336    2612    74452    28.5 |  1.050 % |
c |    117740 |    7521    28277 |    3670    2949    81936    27.8 |  1.050 % |
c |    118248 |    7521    28277 |    4037    3457    99505    28.8 |  1.050 % |
c |    119007 |    7521    28277 |    4441    4216   125445    29.8 |  1.050 % |
c |    120146 |    7521    28277 |    4885    2761    87476    31.7 |  1.050 % |
c |    121857 |    7521    28277 |    5373    4472   177237    39.6 |  1.050 % |
c |    124421 |    7521    28277 |    5911    3959   173768    43.9 |  1.050 % |
c ==============================================================================
c [1mFound solution: 173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 271   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125220 |    7522    28282 |    2507    4758   191574    40.3 |  1.050 % |
c |    125320 |    7522    28282 |    2757    2479    52365    21.1 |  1.124 % |
c |    125470 |    7522    28282 |    3033    2629    57008    21.7 |  1.124 % |
c |    125695 |    7522    28282 |    3336    2854    63717    22.3 |  1.124 % |
c |    126032 |    7522    28282 |    3670    3191    69606    21.8 |  1.124 % |
c |    126541 |    7522    28282 |    4037    3700   105250    28.4 |  1.125 % |
c |    127301 |    7522    28282 |    4441    4460   137894    30.9 |  1.124 % |
c |    128442 |    7522    28282 |    4885    3371   106763    31.7 |  1.124 % |
c |    130150 |    7522    28282 |    5373    5079   206598    40.7 |  1.124 % |
c |    132712 |    7522    28282 |    5911    4581   209262    45.7 |  1.126 % |
c |    136557 |    7522    28282 |    6502    5313   228539    43.0 |  1.124 % |
c |    142324 |    7522    28282 |    7152    3811   206455    54.2 |  1.124 % |
c |    150975 |    7522    28282 |    7868    4514   235253    52.1 |  1.124 % |
c |    163949 |    7522    28282 |    8654    4656   248821    53.4 |  1.124 % |
c |    183410 |    7522    28282 |    9520    5478   532287    97.2 |  1.124 % |
c ==============================================================================
c [1mFound solution: 171[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 273   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    197894 |    7523    28290 |    2507    9656   831227    86.1 |  1.124 % |
c |    197995 |    7523    28290 |    2757    2515   112552    44.8 |  1.199 % |
c |    198145 |    7523    28290 |    3033    2665   116492    43.7 |  1.199 % |
c |    198370 |    7523    28290 |    3336    2890   122549    42.4 |  1.199 % |
c |    198707 |    7523    28290 |    3670    3227   131361    40.7 |  1.199 % |
c |    199215 |    7523    28290 |    4037    3735   145285    38.9 |  1.199 % |
c |    199977 |    7523    28290 |    4441    4497   177731    39.5 |  1.199 % |
c ==============================================================================
c [1mFound solution: 170[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 274   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200401 |    7525    28301 |    2508    2673    58225    21.8 |  1.199 % |
c |    200503 |    7525    28301 |    2758    1439    15785    11.0 |  1.272 % |
c |    200653 |    7525    28301 |    3034    1589    18160    11.4 |  1.272 % |
c |    200878 |    7525    28301 |    3338    1814    24394    13.4 |  1.272 % |
c |    201216 |    7525    28301 |    3671    2152    35034    16.3 |  1.272 % |
c |    201722 |    7525    28301 |    4039    2658    64441    24.2 |  1.272 % |
c |    202481 |    7525    28301 |    4443    3417   105525    30.9 |  1.272 % |
c |    203623 |    7525    28301 |    4887    4559   147748    32.4 |  1.272 % |
c |    205331 |    7525    28301 |    5376    3415   163262    47.8 |  1.272 % |
c |    207893 |    7525    28301 |    5913    5977   437949    73.3 |  1.272 % |
c |    211737 |    7525    28301 |    6505    6833   518168    75.8 |  1.272 % |
c |    217504 |    7525    28301 |    7155    5499   311155    56.6 |  1.272 % |
c |    226154 |    7525    28301 |    7871    6350   403081    63.5 |  1.272 % |
c |    239130 |    7525    28301 |    8658    6275   385259    61.4 |  1.272 % |
c |    258592 |    7525    28301 |    9524    6954   530168    76.2 |  1.272 % |
c |    287784 |    7525    28301 |   10476   10395  1014588    97.6 |  1.272 % |
c |    331573 |    7525    28301 |   11524    9128  1050326   115.1 |  1.272 % |
c |    397258 |    7525    28301 |   12676    6894   616115    89.4 |  1.272 % |
c |    495784 |    7525    28301 |   13944   10896  1035000    95.0 |  1.272 % |
c |    643575 |    7525    28301 |   15338    7969   346319    43.5 |  1.272 % |
c |    865259 |    7525    28301 |   16872   13199  1069733    81.0 |  1.272 % |
c |   1197784 |    7525    28301 |   18559   10992   812653    73.9 |  1.272 % |
#### 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.92 0.97 0.88 2/54 25895
Raw data (stat): 25895 (runsolver) R 25894 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420470785 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.97 0.88 2/54 25895
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1113 0 0 0 995 4 0 0 25 0 1 0 420470785 6107136 1091 4294967295 134512640 134672761 3221224576 3221223760 134559489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1491 1091 603 41 0 1450 0
vsize: 5964
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.88 2/54 25895
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1299 0 0 0 1994 4 0 0 25 0 1 0 420470785 6918144 1277 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1689 1277 603 41 0 1648 0
vsize: 6756
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.97 0.88 2/54 25895
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1300 0 0 0 2994 4 0 0 25 0 1 0 420470785 6918144 1278 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1689 1278 603 41 0 1648 0
vsize: 6756
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.97 0.88 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1376 0 0 0 3994 5 0 0 25 0 1 0 420470785 7188480 1354 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1755 1354 603 41 0 1714 0
vsize: 7020
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.97 0.88 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1376 0 0 0 4994 5 0 0 25 0 1 0 420470785 7188480 1354 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1755 1354 603 41 0 1714 0
vsize: 7020
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.88 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1376 0 0 0 5993 5 0 0 25 0 1 0 420470785 7188480 1354 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1755 1354 603 41 0 1714 0
vsize: 7020
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.88 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1459 0 0 0 6993 5 0 0 25 0 1 0 420470785 7454720 1437 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1820 1437 603 41 0 1779 0
vsize: 7280
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.97 0.88 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1459 0 0 0 7993 5 0 0 25 0 1 0 420470785 7454720 1437 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1820 1437 603 41 0 1779 0
vsize: 7280
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 1459 0 0 0 8993 5 0 0 25 0 1 0 420470785 7438336 1434 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1816 1434 603 41 0 1775 0
vsize: 7264
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2058 0 0 0 9992 7 0 0 25 0 1 0 420470785 9977856 2033 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2436 2033 603 41 0 2395 0
vsize: 9744
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2168 0 0 0 10992 7 0 0 25 0 1 0 420470785 10379264 2143 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2143 603 41 0 2493 0
vsize: 10136
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 11992 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 12992 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 13992 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 14990 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 15990 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2169 0 0 0 16991 7 0 0 25 0 1 0 420470785 10379264 2144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2144 603 41 0 2493 0
vsize: 10136
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2170 0 0 0 17991 7 0 0 25 0 1 0 420470785 10379264 2145 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2145 603 41 0 2493 0
vsize: 10136
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2170 0 0 0 18991 7 0 0 25 0 1 0 420470785 10379264 2145 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2145 603 41 0 2493 0
vsize: 10136
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2170 0 0 0 19991 7 0 0 25 0 1 0 420470785 10379264 2145 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2145 603 41 0 2493 0
vsize: 10136
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2285 0 0 0 20991 8 0 0 25 0 1 0 420470785 10911744 2260 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2664 2260 603 41 0 2623 0
vsize: 10656
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2446 0 0 0 21990 8 0 0 25 0 1 0 420470785 11579392 2421 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2827 2421 603 41 0 2786 0
vsize: 11308
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2446 0 0 0 22991 8 0 0 25 0 1 0 420470785 11579392 2421 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2827 2421 603 41 0 2786 0
vsize: 11308
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2563 0 0 0 23990 9 0 0 25 0 1 0 420470785 11976704 2538 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2924 2538 603 41 0 2883 0
vsize: 11696
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2568 0 0 0 24991 9 0 0 25 0 1 0 420470785 12111872 2543 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2957 2543 603 41 0 2916 0
vsize: 11828
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2658 0 0 0 25991 9 0 0 25 0 1 0 420470785 12378112 2633 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3022 2633 603 41 0 2981 0
vsize: 12088
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2661 0 0 0 26991 9 0 0 25 0 1 0 420470785 12513280 2636 4294967295 134512640 134672761 3221224576 3221223680 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2636 603 41 0 3014 0
vsize: 12220
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2661 0 0 0 27991 9 0 0 25 0 1 0 420470785 12513280 2636 4294967295 134512640 134672761 3221224576 3221223680 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2636 603 41 0 3014 0
vsize: 12220
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2661 0 0 0 28991 9 0 0 25 0 1 0 420470785 12513280 2636 4294967295 134512640 134672761 3221224576 3221223712 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2636 603 41 0 3014 0
vsize: 12220
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2662 0 0 0 29992 9 0 0 25 0 1 0 420470785 12513280 2637 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2637 603 41 0 3014 0
vsize: 12220
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2663 0 0 0 30992 9 0 0 25 0 1 0 420470785 12513280 2638 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2638 603 41 0 3014 0
vsize: 12220
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 31992 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 32992 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 33992 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 34993 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 35993 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 36993 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2664 0 0 0 37993 9 0 0 25 0 1 0 420470785 12513280 2639 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2639 603 41 0 3014 0
vsize: 12220
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 38993 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223760 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 39993 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 40994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 41994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 42994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 43994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 44994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 45994 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 46995 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 47995 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 48995 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 49995 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2665 0 0 0 50995 9 0 0 25 0 1 0 420470785 12513280 2640 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2666 0 0 0 51994 9 0 0 25 0 1 0 420470785 12513280 2641 4294967295 134512640 134672761 3221224576 3221223760 134559575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3055 2641 603 41 0 3014 0
vsize: 12220
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2666 0 0 0 52994 9 0 0 25 0 1 0 420470785 12513280 2641 4294967295 134512640 134672761 3221224576 3221223760 134558909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2641 603 41 0 3014 0
vsize: 12220
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2721 0 0 0 53994 9 0 0 25 0 1 0 420470785 12648448 2696 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3088 2696 603 41 0 3047 0
vsize: 12352
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2778 0 0 0 54994 9 0 0 25 0 1 0 420470785 12914688 2753 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2753 603 41 0 3112 0
vsize: 12612
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2780 0 0 0 55995 9 0 0 25 0 1 0 420470785 12914688 2755 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2755 603 41 0 3112 0
vsize: 12612
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2780 0 0 0 56995 9 0 0 25 0 1 0 420470785 12914688 2755 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2755 603 41 0 3112 0
vsize: 12612
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2783 0 0 0 57995 9 0 0 25 0 1 0 420470785 12914688 2758 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2758 603 41 0 3112 0
vsize: 12612
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2783 0 0 0 58995 9 0 0 25 0 1 0 420470785 12914688 2758 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2758 603 41 0 3112 0
vsize: 12612
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 59995 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 60996 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 61996 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223680 134555096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 62996 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 63996 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 64996 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2789 0 0 0 65997 9 0 0 25 0 1 0 420470785 12914688 2764 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3153 2764 603 41 0 3112 0
vsize: 12612
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2819 0 0 0 66997 9 0 0 25 0 1 0 420470785 13049856 2794 4294967295 134512640 134672761 3221224576 3221223680 134560125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3186 2794 603 41 0 3145 0
vsize: 12744
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2886 0 0 0 67997 10 0 0 25 0 1 0 420470785 13463552 2861 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2861 603 41 0 3246 0
vsize: 13148
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2886 0 0 0 68997 10 0 0 25 0 1 0 420470785 13463552 2861 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2861 603 41 0 3246 0
vsize: 13148
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2891 0 0 0 69997 10 0 0 25 0 1 0 420470785 13463552 2866 4294967295 134512640 134672761 3221224576 3221223760 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3287 2866 603 41 0 3246 0
vsize: 13148
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 2927 0 0 0 70997 10 0 0 25 0 1 0 420470785 13598720 2902 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3320 2902 603 41 0 3279 0
vsize: 13280
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3117 0 0 0 71997 10 0 0 25 0 1 0 420470785 14422016 3092 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3521 3092 603 41 0 3480 0
vsize: 14084
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3146 0 0 0 72997 10 0 0 25 0 1 0 420470785 14422016 3121 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3521 3121 603 41 0 3480 0
vsize: 14084
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3146 0 0 0 73997 10 0 0 25 0 1 0 420470785 14422016 3121 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3521 3121 603 41 0 3480 0
vsize: 14084
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3164 0 0 0 74997 11 0 0 25 0 1 0 420470785 14671872 3139 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3582 3139 603 41 0 3541 0
vsize: 14328
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3164 0 0 0 75996 11 0 0 25 0 1 0 420470785 14671872 3139 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3139 603 41 0 3541 0
vsize: 14328
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3164 0 0 0 76997 11 0 0 25 0 1 0 420470785 14671872 3139 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3139 603 41 0 3541 0
vsize: 14328
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3164 0 0 0 77997 11 0 0 25 0 1 0 420470785 14671872 3139 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3139 603 41 0 3541 0
vsize: 14328
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3165 0 0 0 78997 11 0 0 25 0 1 0 420470785 14671872 3140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3140 603 41 0 3541 0
vsize: 14328
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 79997 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 80997 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 81998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 82998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 83998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 84998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 85998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 86998 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223712 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3166 0 0 0 87999 11 0 0 25 0 1 0 420470785 14671872 3141 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3141 603 41 0 3541 0
vsize: 14328
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3201 0 0 0 88999 11 0 0 25 0 1 0 420470785 14807040 3176 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3176 603 41 0 3574 0
vsize: 14460
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3202 0 0 0 89999 11 0 0 25 0 1 0 420470785 14807040 3177 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3177 603 41 0 3574 0
vsize: 14460
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3203 0 0 0 90999 11 0 0 25 0 1 0 420470785 14807040 3178 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3178 603 41 0 3574 0
vsize: 14460
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3213 0 0 0 91999 11 0 0 25 0 1 0 420470785 14807040 3188 4294967295 134512640 134672761 3221224576 3221223680 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3188 603 41 0 3574 0
vsize: 14460
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3237 0 0 0 93000 11 0 0 25 0 1 0 420470785 14942208 3212 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3212 603 41 0 3607 0
vsize: 14592
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3247 0 0 0 94000 11 0 0 25 0 1 0 420470785 14942208 3222 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3222 603 41 0 3607 0
vsize: 14592
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3252 0 0 0 95000 11 0 0 25 0 1 0 420470785 14942208 3227 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3227 603 41 0 3607 0
vsize: 14592
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3252 0 0 0 96000 11 0 0 25 0 1 0 420470785 14942208 3227 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3227 603 41 0 3607 0
vsize: 14592
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3252 0 0 0 97000 11 0 0 25 0 1 0 420470785 14942208 3227 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3227 603 41 0 3607 0
vsize: 14592
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3252 0 0 0 98000 11 0 0 25 0 1 0 420470785 14942208 3227 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3227 603 41 0 3607 0
vsize: 14592
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3253 0 0 0 99001 11 0 0 25 0 1 0 420470785 14942208 3228 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3228 603 41 0 3607 0
vsize: 14592
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3282 0 0 0 100001 11 0 0 25 0 1 0 420470785 15077376 3257 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3257 603 41 0 3640 0
vsize: 14724
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3282 0 0 0 101001 11 0 0 25 0 1 0 420470785 15077376 3257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3257 603 41 0 3640 0
vsize: 14724
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 102001 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223760 134558977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 103001 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 104001 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 105002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 106002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 107002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 108002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 109002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3289 0 0 0 110002 11 0 0 25 0 1 0 420470785 15077376 3264 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3264 603 41 0 3640 0
vsize: 14724
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3358 0 0 0 111002 11 0 0 25 0 1 0 420470785 15478784 3333 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3333 603 41 0 3738 0
vsize: 15116
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3605 0 0 0 112001 12 0 0 25 0 1 0 420470785 16429056 3580 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4011 3580 603 41 0 3970 0
vsize: 16044
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3829 0 0 0 113001 13 0 0 25 0 1 0 420470785 17371136 3804 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4241 3804 603 41 0 4200 0
vsize: 16964
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 3829 0 0 0 114001 13 0 0 25 0 1 0 420470785 17371136 3804 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4241 3804 603 41 0 4200 0
vsize: 16964
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4035 0 0 0 115001 14 0 0 25 0 1 0 420470785 18169856 4010 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4436 4010 603 41 0 4395 0
vsize: 17744
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4180 0 0 0 116000 14 0 0 25 0 1 0 420470785 18841600 4155 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4600 4155 603 41 0 4559 0
vsize: 18400
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4180 0 0 0 117001 14 0 0 25 0 1 0 420470785 18841600 4155 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4600 4155 603 41 0 4559 0
vsize: 18400
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4180 0 0 0 118001 14 0 0 25 0 1 0 420470785 18841600 4155 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4600 4155 603 41 0 4559 0
vsize: 18400
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4180 0 0 0 119001 14 0 0 25 0 1 0 420470785 18841600 4155 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4600 4155 603 41 0 4559 0
vsize: 18400
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25897
Raw data (stat): 25895 (minisat+) R 25894 24215 24214 0 -1 0 4180 0 0 0 120001 14 0 0 25 0 1 0 420470785 18841600 4155 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4600 4155 603 41 0 4559 0
vsize: 18400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25897
Raw data (stat): 25895 (minisat+) Z 25894 24215 24214 0 -1 12 4183 0 0 0 120001 15 0 0 25 0 1 0 420470785 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.03
CPU time (s): 1200.17
CPU user time (s): 1200.02
CPU system time (s): 0.153976
CPU usage (%): 100.011
Max. virtual memory (Kb): 18400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####