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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 15545

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 04:58:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17256 boxname=wulflinc15 idbench=1328 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-sentoy.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-sentoy.opb
IDLAUNCH: 17256
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        717060 kB
Buffers:         32960 kB
Cached:         263248 kB
SwapCached:        408 kB
Active:          30692 kB
Inactive:       267640 kB
HighTotal:      131008 kB
HighFree:        31640 kB
LowTotal:       903652 kB
LowFree:        685420 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13628 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:18:52 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17256 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89253   318894 |   29751       0        0     nan |  0.000 % |
c |       100 |   89253   318894 |   32726     100     1024    10.2 |  1.712 % |
c ==============================================================================
c [1mFound solution: -1341[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6599     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |  106220   358591 |   35406     191     1682     8.8 |  1.712 % |
c |       291 |  106220   358591 |   38946     291     5111    17.6 |  1.192 % |
c |       443 |  106220   358591 |   42841     443     9280    20.9 |  1.192 % |
c |       669 |  106220   358591 |   47125     669    14719    22.0 |  1.192 % |
c |      1007 |  106214   358574 |   51837    1006    19436    19.3 |  1.197 % |
c ==============================================================================
c [1mFound solution: -1485[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1190 |  106519   359320 |   35506    1189    21596    18.2 |  1.197 % |
c |      1293 |  106519   359320 |   39056    1292    22436    17.4 |  1.191 % |
c |      1445 |  106519   359320 |   42962    1444    24976    17.3 |  1.191 % |
c |      1670 |  106519   359320 |   47258    1669    29751    17.8 |  1.191 % |
c |      2007 |  106519   359320 |   51984    2006    35780    17.8 |  1.191 % |
c ==============================================================================
c [1mFound solution: -1703[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2104 |  106596   359531 |   35532    2103    37022    17.6 |  1.191 % |
c |      2204 |  106596   359531 |   39085    2203    38425    17.4 |  1.194 % |
c |      2357 |  106596   359531 |   42993    2356    40994    17.4 |  1.194 % |
c |      2582 |  106596   359531 |   47293    2581    48161    18.7 |  1.194 % |
c |      2920 |  106596   359531 |   52022    2919    55040    18.9 |  1.194 % |
c ==============================================================================
c [1mFound solution: -2044[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3041 |  106710   359836 |   35570    3040    59039    19.4 |  1.194 % |
c |      3141 |  106710   359836 |   39127    3140    59910    19.1 |  1.195 % |
c |      3291 |  106704   359819 |   43039    3289    62063    18.9 |  1.200 % |
c |      3516 |  106704   359819 |   47343    3514    64855    18.5 |  1.200 % |
c ==============================================================================
c [1mFound solution: -2051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3838 |  106709   359842 |   35569    3836    75916    19.8 |  1.200 % |
c |      3938 |  106709   359842 |   39125    3936    77693    19.7 |  1.205 % |
c |      4088 |  106709   359842 |   43038    4086    78884    19.3 |  1.205 % |
c ==============================================================================
c [1mFound solution: -2441[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4105 |  106730   359904 |   35576    4103    79182    19.3 |  1.205 % |
c |      4205 |  106730   359904 |   39133    4203    85074    20.2 |  1.209 % |
c |      4356 |  106730   359904 |   43046    4354    87121    20.0 |  1.209 % |
c ==============================================================================
c [1mFound solution: -2545[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4437 |  106743   359939 |   35581    4435    91419    20.6 |  1.209 % |
c |      4537 |  106743   359939 |   39139    4535    93846    20.7 |  1.214 % |
c |      4687 |  106743   359939 |   43053    4685    97645    20.8 |  1.214 % |
c |      4912 |  106743   359939 |   47358    4910   102902    21.0 |  1.214 % |
c |      5249 |  106743   359939 |   52094    5247   110257    21.0 |  1.213 % |
c |      5755 |  106743   359939 |   57303    5753   131413    22.8 |  1.214 % |
c |      6514 |  106743   359939 |   63033    6512   170601    26.2 |  1.214 % |
c |      7653 |  106743   359939 |   69337    7651   215921    28.2 |  1.214 % |
c ==============================================================================
c [1mFound solution: -2651[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7953 |  106748   359952 |   35582    7951   223593    28.1 |  1.214 % |
c |      8055 |  106748   359952 |   39140    8053   225854    28.0 |  1.218 % |
c |      8205 |  106748   359952 |   43054    8203   228739    27.9 |  1.218 % |
c ==============================================================================
c [1mFound solution: -2952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8246 |  106757   359976 |   35585    8244   230421    28.0 |  1.218 % |
c |      8346 |  106757   359976 |   39143    8344   232767    27.9 |  1.223 % |
c |      8496 |  106757   359976 |   43057    8494   236015    27.8 |  1.223 % |
c |      8721 |  106757   359976 |   47363    8719   243030    27.9 |  1.223 % |
c |      9058 |  106757   359976 |   52099    9056   255321    28.2 |  1.223 % |
c |      9566 |  106757   359976 |   57309    9564   270673    28.3 |  1.223 % |
c ==============================================================================
c [1mFound solution: -3309[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9599 |  106798   360082 |   35599    9597   271200    28.3 |  1.223 % |
c |      9699 |  106798   360082 |   39158    9697   276476    28.5 |  1.227 % |
c |      9849 |  106798   360082 |   43074    9847   279294    28.4 |  1.227 % |
c |     10074 |  106798   360082 |   47382   10072   291867    29.0 |  1.227 % |
c |     10412 |  106798   360082 |   52120   10410   298988    28.7 |  1.227 % |
c |     10919 |  106798   360082 |   57332   10917   331053    30.3 |  1.227 % |
c |     11680 |  106792   360065 |   63065   11677   353489    30.3 |  1.232 % |
c |     12819 |  106792   360065 |   69372   12816   416224    32.5 |  1.232 % |
c |     14527 |  106792   360065 |   76309   14524   500281    34.4 |  1.232 % |
c |     17090 |  106786   360048 |   83940   17086   621843    36.4 |  1.237 % |
c |     20934 |  106786   360048 |   92334   20930   766604    36.6 |  1.237 % |
c |     26700 |  106786   360048 |  101568   26696   976667    36.6 |  1.237 % |
c |     35352 |  106786   360048 |  111724   35348  1373187    38.8 |  1.237 % |
c |     48326 |  106786   360048 |  122897   48322  2301426    47.6 |  1.237 % |
c ==============================================================================
c [1mFound solution: -5491[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49564 |  106852   360209 |   35617   49560  2348470    47.4 |  1.237 % |
c |     49664 |  106852   360209 |   39178   13139   877063    66.8 |  1.239 % |
c |     49815 |  106852   360209 |   43096   13290   878830    66.1 |  1.239 % |
c |     50040 |  106852   360209 |   47406   13515   892196    66.0 |  1.239 % |
c |     50379 |  106852   360209 |   52146   13854   895991    64.7 |  1.239 % |
c |     50887 |  106852   360209 |   57361   14362   901416    62.8 |  1.239 % |
c |     51646 |  106852   360209 |   63097   15121   912500    60.3 |  1.239 % |
c |     52787 |  106852   360209 |   69407   16262   956151    58.8 |  1.239 % |
c |     54495 |  106852   360209 |   76348   17970  1040942    57.9 |  1.239 % |
c |     57057 |  106852   360209 |   83983   20532  1211813    59.0 |  1.239 % |
c |     60902 |  106852   360209 |   92381   24377  1475337    60.5 |  1.239 % |
c |     66669 |  106846   360192 |  101619   30143  1911942    63.4 |  1.245 % |
c |     75319 |  106846   360192 |  111781   38793  2562755    66.1 |  1.245 % |
c |     88295 |  106846   360192 |  122959   51769  3109322    60.1 |  1.245 % |
c |    107756 |  106846   360192 |  135255   71230  4469811    62.8 |  1.245 % |
c |    136950 |  106846   360192 |  148781  100424  6087573    60.6 |  1.245 % |
c |    180739 |  106840   360175 |  163659  144212  8423431    58.4 |  1.250 % |
#### 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.84 0.94 0.94 2/54 28701
Raw data (stat): 28701 (runsolver) R 28700 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484158221 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 2607 0 0 0 991 7 0 0 25 0 1 0 484158221 12935168 2531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3158 2531 603 41 0 3117 0
vsize: 12632
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 2715 0 0 0 1990 7 0 0 25 0 1 0 484158221 13471744 2639 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3289 2639 603 41 0 3248 0
vsize: 13156
[startup+30.0034 s]
Raw data (loadavg): 0.90 0.94 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 2842 0 0 0 2989 8 0 0 25 0 1 0 484158221 14020608 2766 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3423 2766 603 41 0 3382 0
vsize: 13692
[startup+40.0031 s]
Raw data (loadavg): 0.92 0.94 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 2951 0 0 0 3988 8 0 0 25 0 1 0 484158221 14422016 2875 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3521 2875 603 41 0 3480 0
vsize: 14084
[startup+50.0034 s]
Raw data (loadavg): 0.93 0.94 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3073 0 0 0 4987 9 0 0 25 0 1 0 484158221 14946304 2997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3649 2997 603 41 0 3608 0
vsize: 14596
[startup+60.0038 s]
Raw data (loadavg): 0.94 0.95 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3191 0 0 0 5987 10 0 0 25 0 1 0 484158221 15343616 3115 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3746 3115 603 41 0 3705 0
vsize: 14984
[startup+70.0045 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 28701
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3294 0 0 0 6986 10 0 0 25 0 1 0 484158221 15876096 3218 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3876 3218 603 41 0 3835 0
vsize: 15504
[startup+80.059 s]
Raw data (loadavg): 1.04 0.96 0.94 3/58 28746
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3398 0 0 0 7991 10 0 0 25 0 1 0 484158221 16273408 3322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3973 3322 603 41 0 3932 0
vsize: 15892
[startup+90.0587 s]
Raw data (loadavg): 1.03 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3526 0 0 0 8991 11 0 0 25 0 1 0 484158221 16814080 3450 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4105 3450 603 41 0 4064 0
vsize: 16420
[startup+100.059 s]
Raw data (loadavg): 1.02 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3654 0 0 0 9991 11 0 0 25 0 1 0 484158221 17350656 3578 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3578 603 41 0 4195 0
vsize: 16944
[startup+110.059 s]
Raw data (loadavg): 1.02 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3786 0 0 0 10990 12 0 0 25 0 1 0 484158221 17895424 3710 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4369 3710 603 41 0 4328 0
vsize: 17476
[startup+120.06 s]
Raw data (loadavg): 1.02 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 3929 0 0 0 11990 12 0 0 25 0 1 0 484158221 18427904 3853 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4499 3853 603 41 0 4458 0
vsize: 17996
[startup+130.06 s]
Raw data (loadavg): 1.01 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4117 0 0 0 12989 13 0 0 25 0 1 0 484158221 19361792 4041 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4727 4041 603 41 0 4686 0
vsize: 18908
[startup+140.06 s]
Raw data (loadavg): 1.01 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4288 0 0 0 13989 14 0 0 25 0 1 0 484158221 20029440 4212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4890 4212 603 41 0 4849 0
vsize: 19560
[startup+150.064 s]
Raw data (loadavg): 1.01 0.97 0.94 2/54 28754
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4379 0 0 0 14989 14 0 0 25 0 1 0 484158221 20430848 4303 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4303 603 41 0 4947 0
vsize: 19952
[startup+160.063 s]
Raw data (loadavg): 1.01 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4497 0 0 0 15989 15 0 0 25 0 1 0 484158221 20832256 4421 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5086 4421 603 41 0 5045 0
vsize: 20344
[startup+170.064 s]
Raw data (loadavg): 1.01 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4650 0 0 0 16988 16 0 0 25 0 1 0 484158221 21508096 4574 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5251 4574 603 41 0 5210 0
vsize: 21004
[startup+180.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4755 0 0 0 17988 16 0 0 25 0 1 0 484158221 21905408 4679 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5348 4679 603 41 0 5307 0
vsize: 21392
[startup+190.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 4889 0 0 0 18988 16 0 0 25 0 1 0 484158221 22441984 4813 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5479 4813 603 41 0 5438 0
vsize: 21916
[startup+200.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5015 0 0 0 19987 17 0 0 25 0 1 0 484158221 22974464 4939 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5609 4939 603 41 0 5568 0
vsize: 22436
[startup+210.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5143 0 0 0 20987 18 0 0 25 0 1 0 484158221 23511040 5067 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5740 5067 603 41 0 5699 0
vsize: 22960
[startup+220.065 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5268 0 0 0 21986 18 0 0 25 0 1 0 484158221 23908352 5192 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5837 5192 603 41 0 5796 0
vsize: 23348
[startup+230.065 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 22986 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+240.065 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 23986 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+250.066 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 24987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+260.066 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 25987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+270.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 26987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+280.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 27987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+290.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 28987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+300.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 29987 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+310.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5380 0 0 0 30988 18 0 0 25 0 1 0 484158221 24440832 5304 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5967 5304 603 41 0 5926 0
vsize: 23868
[startup+320.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5412 0 0 0 31988 18 0 0 25 0 1 0 484158221 24576000 5336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6000 5336 603 41 0 5959 0
vsize: 24000
[startup+330.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5591 0 0 0 32987 20 0 0 25 0 1 0 484158221 25239552 5515 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6162 5515 603 41 0 6121 0
vsize: 24648
[startup+340.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5720 0 0 0 33986 20 0 0 25 0 1 0 484158221 25767936 5644 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6291 5644 603 41 0 6250 0
vsize: 25164
[startup+350.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5870 0 0 0 34986 21 0 0 25 0 1 0 484158221 26435584 5794 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6454 5794 603 41 0 6413 0
vsize: 25816
[startup+360.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 5981 0 0 0 35986 21 0 0 25 0 1 0 484158221 26836992 5905 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6552 5905 603 41 0 6511 0
vsize: 26208
[startup+370.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6096 0 0 0 36985 22 0 0 25 0 1 0 484158221 27365376 6020 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6681 6020 603 41 0 6640 0
vsize: 26724
[startup+380.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6212 0 0 0 37985 22 0 0 25 0 1 0 484158221 27901952 6136 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6812 6136 603 41 0 6771 0
vsize: 27248
[startup+390.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6335 0 0 0 38985 22 0 0 25 0 1 0 484158221 28299264 6259 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6259 603 41 0 6868 0
vsize: 27636
[startup+400.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6424 0 0 0 39985 23 0 0 25 0 1 0 484158221 28696576 6348 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7006 6348 603 41 0 6965 0
vsize: 28024
[startup+410.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6506 0 0 0 40985 23 0 0 25 0 1 0 484158221 29093888 6430 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7103 6430 603 41 0 7062 0
vsize: 28412
[startup+420.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6612 0 0 0 41985 23 0 0 25 0 1 0 484158221 29491200 6536 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7200 6536 603 41 0 7159 0
vsize: 28800
[startup+430.071 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28756
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6749 0 0 0 42985 24 0 0 25 0 1 0 484158221 30019584 6673 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7329 6673 603 41 0 7288 0
vsize: 29316
[startup+440.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 6891 0 0 0 43984 24 0 0 25 0 1 0 484158221 30556160 6815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7460 6815 603 41 0 7419 0
vsize: 29840
[startup+450.071 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7003 0 0 0 44984 25 0 0 25 0 1 0 484158221 31096832 6927 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7592 6927 603 41 0 7551 0
vsize: 30368
[startup+460.071 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7120 0 0 0 45984 25 0 0 25 0 1 0 484158221 31494144 7044 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7689 7044 603 41 0 7648 0
vsize: 30756
[startup+470.072 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7242 0 0 0 46984 25 0 0 25 0 1 0 484158221 32022528 7166 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7818 7166 603 41 0 7777 0
vsize: 31272
[startup+480.072 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7370 0 0 0 47984 26 0 0 25 0 1 0 484158221 32808960 7294 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8010 7294 603 41 0 7969 0
vsize: 32040
[startup+490.072 s]
Raw data (loadavg): 1.00 0.97 0.94 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7510 0 0 0 48983 26 0 0 25 0 1 0 484158221 33337344 7434 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8139 7434 603 41 0 8098 0
vsize: 32556
[startup+500.072 s]
Raw data (loadavg): 1.08 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7639 0 0 0 49983 26 0 0 25 0 1 0 484158221 33865728 7563 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8268 7563 603 41 0 8227 0
vsize: 33072
[startup+510.073 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7714 0 0 0 50982 27 0 0 25 0 1 0 484158221 34127872 7638 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8332 7638 603 41 0 8291 0
vsize: 33328
[startup+520.073 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7790 0 0 0 51982 27 0 0 25 0 1 0 484158221 34525184 7714 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7714 603 41 0 8388 0
vsize: 33716
[startup+530.074 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 7894 0 0 0 52981 28 0 0 25 0 1 0 484158221 34922496 7818 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8526 7818 603 41 0 8485 0
vsize: 34104
[startup+540.074 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8050 0 0 0 53980 29 0 0 25 0 1 0 484158221 35586048 7974 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8688 7974 603 41 0 8647 0
vsize: 34752
[startup+550.074 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8206 0 0 0 54980 30 0 0 25 0 1 0 484158221 36118528 8130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8818 8130 603 41 0 8777 0
vsize: 35272
[startup+560.074 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8304 0 0 0 55980 30 0 0 25 0 1 0 484158221 36528128 8228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8918 8228 603 41 0 8877 0
vsize: 35672
[startup+570.076 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8383 0 0 0 56980 30 0 0 25 0 1 0 484158221 36941824 8307 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9019 8307 603 41 0 8978 0
vsize: 36076
[startup+580.076 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8457 0 0 0 57980 30 0 0 25 0 1 0 484158221 37208064 8381 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9084 8381 603 41 0 9043 0
vsize: 36336
[startup+590.076 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8538 0 0 0 58980 30 0 0 25 0 1 0 484158221 37474304 8462 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9149 8462 603 41 0 9108 0
vsize: 36596
[startup+600.077 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8632 0 0 0 59979 31 0 0 25 0 1 0 484158221 37875712 8556 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9247 8556 603 41 0 9206 0
vsize: 36988
[startup+610.076 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8726 0 0 0 60980 31 0 0 25 0 1 0 484158221 38285312 8650 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9347 8650 603 41 0 9306 0
vsize: 37388
[startup+620.077 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8821 0 0 0 61980 31 0 0 25 0 1 0 484158221 38682624 8745 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9444 8745 603 41 0 9403 0
vsize: 37776
[startup+630.078 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 8918 0 0 0 62979 32 0 0 25 0 1 0 484158221 39088128 8842 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9543 8842 603 41 0 9502 0
vsize: 38172
[startup+640.078 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9000 0 0 0 63979 32 0 0 25 0 1 0 484158221 39354368 8924 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9608 8924 603 41 0 9567 0
vsize: 38432
[startup+650.078 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9065 0 0 0 64979 32 0 0 25 0 1 0 484158221 39616512 8989 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9672 8989 603 41 0 9631 0
vsize: 38688
[startup+660.078 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9134 0 0 0 65979 33 0 0 25 0 1 0 484158221 39878656 9058 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9736 9058 603 41 0 9695 0
vsize: 38944
[startup+670.078 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9201 0 0 0 66979 33 0 0 25 0 1 0 484158221 40144896 9125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9801 9125 603 41 0 9760 0
vsize: 39204
[startup+680.078 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9274 0 0 0 67979 33 0 0 25 0 1 0 484158221 40550400 9198 4294967295 134512640 134672761 3221224624 3221223580 1075349791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9900 9198 603 41 0 9859 0
vsize: 39600
[startup+690.079 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9347 0 0 0 68979 33 0 0 25 0 1 0 484158221 40820736 9271 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9966 9271 603 41 0 9925 0
vsize: 39864
[startup+700.079 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9417 0 0 0 69979 33 0 0 25 0 1 0 484158221 41082880 9341 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10030 9341 603 41 0 9989 0
vsize: 40120
[startup+710.079 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9492 0 0 0 70979 34 0 0 25 0 1 0 484158221 41353216 9416 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10096 9416 603 41 0 10055 0
vsize: 40384
[startup+720.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9574 0 0 0 71978 34 0 0 25 0 1 0 484158221 41754624 9498 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10194 9498 603 41 0 10153 0
vsize: 40776
[startup+730.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9646 0 0 0 72979 34 0 0 25 0 1 0 484158221 42020864 9570 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10259 9570 603 41 0 10218 0
vsize: 41036
[startup+740.08 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9738 0 0 0 73977 35 0 0 25 0 1 0 484158221 42438656 9662 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9662 603 41 0 10320 0
vsize: 41444
[startup+750.082 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9821 0 0 0 74977 35 0 0 25 0 1 0 484158221 42704896 9745 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10426 9745 603 41 0 10385 0
vsize: 41704
[startup+760.082 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9906 0 0 0 75976 36 0 0 25 0 1 0 484158221 43102208 9830 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10523 9830 603 41 0 10482 0
vsize: 42092
[startup+770.082 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 9996 0 0 0 76976 36 0 0 25 0 1 0 484158221 43499520 9920 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10620 9920 603 41 0 10579 0
vsize: 42480
[startup+780.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10100 0 0 0 77976 37 0 0 25 0 1 0 484158221 43896832 10024 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10717 10024 603 41 0 10676 0
vsize: 42868
[startup+790.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10186 0 0 0 78975 37 0 0 25 0 1 0 484158221 44163072 10110 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10782 10110 603 41 0 10741 0
vsize: 43128
[startup+800.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10311 0 0 0 79975 38 0 0 25 0 1 0 484158221 44699648 10235 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10913 10235 603 41 0 10872 0
vsize: 43652
[startup+810.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10446 0 0 0 80975 38 0 0 25 0 1 0 484158221 45240320 10370 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11045 10370 603 41 0 11004 0
vsize: 44180
[startup+820.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10573 0 0 0 81975 38 0 0 25 0 1 0 484158221 45785088 10497 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11178 10497 603 41 0 11137 0
vsize: 44712
[startup+830.083 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10705 0 0 0 82975 39 0 0 25 0 1 0 484158221 46317568 10629 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11308 10629 603 41 0 11267 0
vsize: 45232
[startup+840.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10829 0 0 0 83974 39 0 0 25 0 1 0 484158221 46854144 10753 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11439 10753 603 41 0 11398 0
vsize: 45756
[startup+850.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 10942 0 0 0 84974 40 0 0 25 0 1 0 484158221 47251456 10866 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11536 10866 603 41 0 11495 0
vsize: 46144
[startup+860.084 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11026 0 0 0 85974 40 0 0 25 0 1 0 484158221 47648768 10950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11633 10950 603 41 0 11592 0
vsize: 46532
[startup+870.085 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11150 0 0 0 86974 40 0 0 25 0 1 0 484158221 48185344 11074 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11764 11074 603 41 0 11723 0
vsize: 47056
[startup+880.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11243 0 0 0 87974 41 0 0 25 0 1 0 484158221 48578560 11167 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11860 11167 603 41 0 11819 0
vsize: 47440
[startup+890.085 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11344 0 0 0 88973 41 0 0 25 0 1 0 484158221 48979968 11268 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11958 11268 603 41 0 11917 0
vsize: 47832
[startup+900.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11429 0 0 0 89973 41 0 0 25 0 1 0 484158221 49262592 11353 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12027 11353 603 41 0 11986 0
vsize: 48108
[startup+910.085 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11490 0 0 0 90974 41 0 0 25 0 1 0 484158221 49528832 11414 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12092 11414 603 41 0 12051 0
vsize: 48368
[startup+920.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11574 0 0 0 91974 42 0 0 25 0 1 0 484158221 49926144 11498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12189 11498 603 41 0 12148 0
vsize: 48756
[startup+930.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11664 0 0 0 92973 42 0 0 25 0 1 0 484158221 50855936 11588 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12416 11588 603 41 0 12375 0
vsize: 49664
[startup+940.085 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11751 0 0 0 93973 42 0 0 25 0 1 0 484158221 51118080 11675 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12480 11675 603 41 0 12439 0
vsize: 49920
[startup+950.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11846 0 0 0 94973 42 0 0 25 0 1 0 484158221 51515392 11770 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12577 11770 603 41 0 12536 0
vsize: 50308
[startup+960.086 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11917 0 0 0 95973 42 0 0 25 0 1 0 484158221 51789824 11841 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12644 11841 603 41 0 12603 0
vsize: 50576
[startup+970.087 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 11990 0 0 0 96973 43 0 0 25 0 1 0 484158221 52195328 11914 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12743 11914 603 41 0 12702 0
vsize: 50972
[startup+980.087 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12061 0 0 0 97973 43 0 0 25 0 1 0 484158221 52457472 11985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12807 11985 603 41 0 12766 0
vsize: 51228
[startup+990.087 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12130 0 0 0 98973 43 0 0 25 0 1 0 484158221 52723712 12054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12872 12054 603 41 0 12831 0
vsize: 51488
[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12205 0 0 0 99973 43 0 0 25 0 1 0 484158221 52985856 12129 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12936 12129 603 41 0 12895 0
vsize: 51744
[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12274 0 0 0 100973 43 0 0 25 0 1 0 484158221 53252096 12198 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13001 12198 603 41 0 12960 0
vsize: 52004
[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12340 0 0 0 101973 44 0 0 25 0 1 0 484158221 53526528 12264 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13068 12264 603 41 0 13027 0
vsize: 52272
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12411 0 0 0 102973 44 0 0 25 0 1 0 484158221 53792768 12335 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13133 12335 603 41 0 13092 0
vsize: 52532
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12493 0 0 0 103973 44 0 0 25 0 1 0 484158221 54206464 12417 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13234 12417 603 41 0 13193 0
vsize: 52936
[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12576 0 0 0 104973 44 0 0 25 0 1 0 484158221 54476800 12500 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12500 603 41 0 13259 0
vsize: 53200
[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12674 0 0 0 105973 45 0 0 25 0 1 0 484158221 54874112 12598 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13397 12598 603 41 0 13356 0
vsize: 53588
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12773 0 0 0 106972 45 0 0 25 0 1 0 484158221 55279616 12697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13496 12697 603 41 0 13455 0
vsize: 53984
[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12852 0 0 0 107972 45 0 0 25 0 1 0 484158221 55545856 12776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13561 12776 603 41 0 13520 0
vsize: 54244
[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 12930 0 0 0 108973 45 0 0 25 0 1 0 484158221 55951360 12854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13660 12854 603 41 0 13619 0
vsize: 54640
[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13023 0 0 0 109972 46 0 0 25 0 1 0 484158221 56352768 12947 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12947 603 41 0 13717 0
vsize: 55032
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13113 0 0 0 110972 46 0 0 25 0 1 0 484158221 56614912 13037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13822 13037 603 41 0 13781 0
vsize: 55288
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13202 0 0 0 111972 46 0 0 25 0 1 0 484158221 57024512 13126 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13922 13126 603 41 0 13881 0
vsize: 55688
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13287 0 0 0 112972 46 0 0 25 0 1 0 484158221 57294848 13211 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13988 13211 603 41 0 13947 0
vsize: 55952
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13376 0 0 0 113972 47 0 0 25 0 1 0 484158221 57692160 13300 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14085 13300 603 41 0 14044 0
vsize: 56340
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13453 0 0 0 114972 47 0 0 25 0 1 0 484158221 57962496 13377 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14151 13377 603 41 0 14110 0
vsize: 56604
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13537 0 0 0 115972 47 0 0 25 0 1 0 484158221 58363904 13461 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13461 603 41 0 14208 0
vsize: 56996
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13613 0 0 0 116972 48 0 0 25 0 1 0 484158221 58630144 13537 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14314 13537 603 41 0 14273 0
vsize: 57256
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13685 0 0 0 117972 48 0 0 25 0 1 0 484158221 59031552 13609 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14412 13609 603 41 0 14371 0
vsize: 57648
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13746 0 0 0 118972 48 0 0 25 0 1 0 484158221 59162624 13670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14444 13670 603 41 0 14403 0
vsize: 57776
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 28758
Raw data (stat): 28701 (minisat+) R 28700 29151 29150 0 -1 0 13814 0 0 0 119972 48 0 0 25 0 1 0 484158221 59428864 13738 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14542 13739 603 41 0 14501 0
vsize: 58036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 28758
Raw data (stat): 28701 (minisat+) Z 28700 29151 29150 0 -1 12 13818 0 0 0 119972 51 0 0 25 0 1 0 484158221 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.12
CPU time (s): 1200.24
CPU user time (s): 1199.73
CPU system time (s): 0.510922
CPU usage (%): 100.009
Max. virtual memory (Kb): 58036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####