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 18946

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 17:13:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17261 boxname=wulflinc8 idbench=1328 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb
IDLAUNCH: 17261
/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:        831540 kB
Buffers:          8944 kB
Cached:         172480 kB
SwapCached:          0 kB
Active:          30044 kB
Inactive:       154308 kB
HighTotal:      131008 kB
HighFree:        21504 kB
LowTotal:       903652 kB
LowFree:        810036 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13124 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:33:03 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 17261 7 1200.31 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]---> Adder-cost: 391   maxlim: 1341   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |   91914   328410 |   30638     191     1682     8.8 |  1.712 % |
c |       291 |   91914   328410 |   33701     291     5081    17.5 |  1.713 % |
c |       442 |   91914   328410 |   37071     442     6547    14.8 |  1.713 % |
c |       667 |   91914   328410 |   40779     667     9757    14.6 |  1.713 % |
c |      1005 |   91914   328410 |   44857    1005    25715    25.6 |  1.713 % |
c |      1512 |   91914   328410 |   49342    1512    35570    23.5 |  1.713 % |
c ==============================================================================
c [1mFound solution: -2964[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5   maxlim: 2964   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1687 |   91959   328591 |   30653    1687    40255    23.9 |  1.713 % |
c |      1789 |   91959   328591 |   33718    1789    41500    23.2 |  1.763 % |
c |      1939 |   91959   328591 |   37090    1939    49114    25.3 |  1.763 % |
c |      2164 |   91959   328591 |   40799    2164    53289    24.6 |  1.763 % |
c |      2502 |   91959   328591 |   44879    2502    65456    26.2 |  1.763 % |
c |      3008 |   91953   328574 |   49366    3007    82188    27.3 |  1.770 % |
c |      3767 |   91953   328574 |   54303    3766   119856    31.8 |  1.770 % |
c |      4906 |   91953   328574 |   59734    4905   138064    28.1 |  1.770 % |
c |      6614 |   91953   328574 |   65707    6613   213845    32.3 |  1.770 % |
c |      9177 |   91953   328574 |   72278    9176   324329    35.3 |  1.770 % |
c |     13023 |   91947   328557 |   79505   13021   494473    38.0 |  1.778 % |
c |     18790 |   91947   328557 |   87456   18788   814579    43.4 |  1.778 % |
c ==============================================================================
c [1mFound solution: -4257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4257   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23549 |   91961   328620 |   30653   23547  1019723    43.3 |  1.778 % |
c |     23649 |   91961   328620 |   33718   23647  1020545    43.2 |  1.806 % |
c |     23799 |   91961   328620 |   37090   23797  1025206    43.1 |  1.806 % |
c |     24024 |   91961   328620 |   40799   24022  1029449    42.9 |  1.806 % |
c |     24362 |   91961   328620 |   44879   24360  1043679    42.8 |  1.806 % |
c |     24868 |   91961   328620 |   49366   24866  1055658    42.5 |  1.806 % |
c |     25630 |   91961   328620 |   54303   25628  1083665    42.3 |  1.806 % |
c |     26770 |   91961   328620 |   59734   26768  1139583    42.6 |  1.806 % |
c |     28479 |   91961   328620 |   65707   28477  1195792    42.0 |  1.806 % |
c |     31041 |   91961   328620 |   72278   31039  1340127    43.2 |  1.806 % |
c |     34887 |   91961   328620 |   79505   34885  1524955    43.7 |  1.806 % |
c |     40654 |   91955   328603 |   87456   40651  1777207    43.7 |  1.813 % |
c |     49304 |   91955   328603 |   96202   49301  2369545    48.1 |  1.813 % |
c |     62280 |   91955   328603 |  105822   62277  3051067    49.0 |  1.813 % |
c |     81741 |   91955   328603 |  116404   81738  3924591    48.0 |  1.813 % |
c ==============================================================================
c [1mFound solution: -4363[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4363   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86781 |   91958   328635 |   30652   86778  4107084    47.3 |  1.813 % |
c |     86881 |   91958   328635 |   33717   15694   503426    32.1 |  1.835 % |
c |     87033 |   91958   328635 |   37088   15846   505886    31.9 |  1.835 % |
c |     87258 |   91958   328635 |   40797   16071   508525    31.6 |  1.835 % |
c |     87596 |   91958   328635 |   44877   16409   523526    31.9 |  1.835 % |
c |     88103 |   91958   328635 |   49365   16916   534759    31.6 |  1.835 % |
c |     88863 |   91958   328635 |   54301   17676   561876    31.8 |  1.835 % |
c |     90003 |   91958   328635 |   59732   18816   603645    32.1 |  1.835 % |
c |     91711 |   91958   328635 |   65705   20524   670414    32.7 |  1.835 % |
c |     94273 |   91958   328635 |   72275   23086   791440    34.3 |  1.835 % |
c |     98118 |   91958   328635 |   79503   26931   955009    35.5 |  1.835 % |
c |    103884 |   91958   328635 |   87453   32697  1219534    37.3 |  1.835 % |
c |    112534 |   91952   328618 |   96199   41346  1687230    40.8 |  1.842 % |
c |    125508 |   91952   328618 |  105819   54320  2269064    41.8 |  1.842 % |
c |    144969 |   91952   328618 |  116400   73781  3488461    47.3 |  1.842 % |
c |    174161 |   91952   328618 |  128041  102973  5276301    51.2 |  1.842 % |
c |    217950 |   91946   328601 |  140845   33573  1485357    44.2 |  1.850 % |
c ==============================================================================
c [1mFound solution: -4408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4408   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    219901 |   91953   328655 |   30651   35524  1564118    44.0 |  1.850 % |
c |    220004 |   91953   328655 |   33716   12785   498331    39.0 |  1.878 % |
c |    220154 |   91953   328655 |   37087   12935   501650    38.8 |  1.878 % |
c |    220379 |   91953   328655 |   40796   13160   506260    38.5 |  1.878 % |
c |    220716 |   91953   328655 |   44876   13497   515113    38.2 |  1.878 % |
c |    221224 |   91953   328655 |   49363   14005   526284    37.6 |  1.878 % |
c |    221983 |   91953   328655 |   54300   14764   548896    37.2 |  1.878 % |
c |    223122 |   91953   328655 |   59730   15903   584935    36.8 |  1.878 % |
c |    224832 |   91953   328655 |   65703   17613   641419    36.4 |  1.878 % |
#### 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.91 2/54 1335
Raw data (stat): 1335 (runsolver) R 1334 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 475002476 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0012 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2053 0 0 0 991 7 0 0 25 0 1 0 475002476 10334208 2022 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2523 2022 603 41 0 2482 0
vsize: 10092
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2183 0 0 0 1990 7 0 0 25 0 1 0 475002476 10895360 2152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2660 2152 603 41 0 2619 0
vsize: 10640
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2329 0 0 0 2989 8 0 0 25 0 1 0 475002476 11427840 2298 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2790 2298 603 41 0 2749 0
vsize: 11160
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2465 0 0 0 3989 8 0 0 25 0 1 0 475002476 11968512 2434 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2922 2434 603 41 0 2881 0
vsize: 11688
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2597 0 0 0 4989 8 0 0 25 0 1 0 475002476 12505088 2566 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3053 2566 603 41 0 3012 0
vsize: 12212
[startup+60.0037 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2689 0 0 0 5989 9 0 0 25 0 1 0 475002476 12910592 2658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3152 2658 603 41 0 3111 0
vsize: 12608
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2784 0 0 0 6989 9 0 0 25 0 1 0 475002476 13381632 2753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2753 603 41 0 3226 0
vsize: 13068
[startup+80.0049 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2885 0 0 0 7988 10 0 0 25 0 1 0 475002476 13787136 2854 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3366 2854 603 41 0 3325 0
vsize: 13464
[startup+90.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3012 0 0 0 8988 10 0 0 25 0 1 0 475002476 14327808 2981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3498 2981 603 41 0 3457 0
vsize: 13992
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3146 0 0 0 9988 10 0 0 25 0 1 0 475002476 14864384 3115 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3629 3115 603 41 0 3588 0
vsize: 14516
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3264 0 0 0 10988 11 0 0 25 0 1 0 475002476 15265792 3233 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3727 3233 603 41 0 3686 0
vsize: 14908
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3355 0 0 0 11988 11 0 0 25 0 1 0 475002476 15667200 3324 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3825 3324 603 41 0 3784 0
vsize: 15300
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3498 0 0 0 12987 12 0 0 25 0 1 0 475002476 16203776 3467 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3467 603 41 0 3915 0
vsize: 15824
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3617 0 0 0 13987 12 0 0 25 0 1 0 475002476 16736256 3586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4086 3586 603 41 0 4045 0
vsize: 16344
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3689 0 0 0 14987 12 0 0 25 0 1 0 475002476 17006592 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4152 3658 603 41 0 4111 0
vsize: 16608
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3775 0 0 0 15987 12 0 0 25 0 1 0 475002476 17399808 3744 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4248 3744 603 41 0 4207 0
vsize: 16992
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3880 0 0 0 16987 13 0 0 25 0 1 0 475002476 17936384 3849 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3849 603 41 0 4338 0
vsize: 17516
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3963 0 0 0 17986 13 0 0 25 0 1 0 475002476 18202624 3932 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 3932 603 41 0 4403 0
vsize: 17776
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4040 0 0 0 18986 13 0 0 25 0 1 0 475002476 18472960 4009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4510 4009 603 41 0 4469 0
vsize: 18040
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4121 0 0 0 19986 13 0 0 25 0 1 0 475002476 18878464 4090 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4609 4090 603 41 0 4568 0
vsize: 18436
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4219 0 0 0 20986 14 0 0 25 0 1 0 475002476 19283968 4188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4708 4188 603 41 0 4667 0
vsize: 18832
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4315 0 0 0 21986 14 0 0 25 0 1 0 475002476 19689472 4284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4807 4284 603 41 0 4766 0
vsize: 19228
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4416 0 0 0 22986 15 0 0 25 0 1 0 475002476 20094976 4385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4385 603 41 0 4865 0
vsize: 19624
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4515 0 0 0 23986 15 0 0 25 0 1 0 475002476 20496384 4484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5004 4484 603 41 0 4963 0
vsize: 20016
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4627 0 0 0 24986 15 0 0 25 0 1 0 475002476 20897792 4596 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5102 4596 603 41 0 5061 0
vsize: 20408
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4740 0 0 0 25986 15 0 0 25 0 1 0 475002476 21299200 4709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5200 4709 603 41 0 5159 0
vsize: 20800
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4866 0 0 0 26985 16 0 0 25 0 1 0 475002476 21835776 4835 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5331 4835 603 41 0 5290 0
vsize: 21324
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4964 0 0 0 27985 16 0 0 25 0 1 0 475002476 22245376 4933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5431 4933 603 41 0 5390 0
vsize: 21724
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5059 0 0 0 28985 16 0 0 25 0 1 0 475002476 22646784 5028 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5529 5028 603 41 0 5488 0
vsize: 22116
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5166 0 0 0 29985 16 0 0 25 0 1 0 475002476 23048192 5135 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5627 5135 603 41 0 5586 0
vsize: 22508
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5257 0 0 0 30985 16 0 0 25 0 1 0 475002476 23453696 5226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5726 5226 603 41 0 5685 0
vsize: 22904
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5345 0 0 0 31985 17 0 0 25 0 1 0 475002476 23855104 5314 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5824 5314 603 41 0 5783 0
vsize: 23296
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5440 0 0 0 32985 17 0 0 25 0 1 0 475002476 24121344 5409 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5889 5409 603 41 0 5848 0
vsize: 23556
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5533 0 0 0 33985 17 0 0 25 0 1 0 475002476 24522752 5502 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5987 5502 603 41 0 5946 0
vsize: 23948
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5665 0 0 0 34985 18 0 0 25 0 1 0 475002476 25063424 5634 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6119 5634 603 41 0 6078 0
vsize: 24476
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5804 0 0 0 35985 18 0 0 25 0 1 0 475002476 25862144 5773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6314 5773 603 41 0 6273 0
vsize: 25256
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5935 0 0 0 36985 18 0 0 25 0 1 0 475002476 26398720 5904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5904 603 41 0 6404 0
vsize: 25780
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6105 0 0 0 37984 19 0 0 25 0 1 0 475002476 27066368 6074 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6608 6074 603 41 0 6567 0
vsize: 26432
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6219 0 0 0 38984 19 0 0 25 0 1 0 475002476 27607040 6188 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6188 603 41 0 6699 0
vsize: 26960
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6354 0 0 0 39984 20 0 0 25 0 1 0 475002476 28139520 6323 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6323 603 41 0 6829 0
vsize: 27480
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6488 0 0 0 40984 20 0 0 25 0 1 0 475002476 28680192 6457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7002 6457 603 41 0 6961 0
vsize: 28008
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6614 0 0 0 41984 20 0 0 25 0 1 0 475002476 29216768 6583 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7133 6583 603 41 0 7092 0
vsize: 28532
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6760 0 0 0 42984 20 0 0 25 0 1 0 475002476 29753344 6729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7264 6729 603 41 0 7223 0
vsize: 29056
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6896 0 0 0 43984 20 0 0 25 0 1 0 475002476 30289920 6865 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6865 603 41 0 7354 0
vsize: 29580
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 44984 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 45985 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+470.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 46995 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+480.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 47995 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+490.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 48996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+500.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 49996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+510.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 50996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+520.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 51996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+530.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 52996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+540.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 53997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+550.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 54997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+560.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 55997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+570.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 56997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+580.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 57997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+590.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 58998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+600.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 59998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+610.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 60998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+620.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 61998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+630.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 62998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+640.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 63999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+650.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 64999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+660.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 65999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+670.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 66999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+680.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 67999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+690.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 69000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+700.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 70000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+710.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 71000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+720.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 72000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+730.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 73000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+740.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 74001 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+750.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 75001 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+760.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 76000 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+770.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 76999 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+780.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 77999 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+790.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 79000 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+800.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6972 0 0 0 80000 21 0 0 25 0 1 0 475002476 30756864 6941 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7509 6941 603 41 0 7468 0
vsize: 30036
[startup+810.134 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7084 0 0 0 81000 21 0 0 25 0 1 0 475002476 31293440 7053 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7053 603 41 0 7599 0
vsize: 30560
[startup+820.135 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7216 0 0 0 82000 21 0 0 25 0 1 0 475002476 31834112 7185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7772 7185 603 41 0 7731 0
vsize: 31088
[startup+830.135 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7298 0 0 0 83000 22 0 0 25 0 1 0 475002476 32096256 7267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7836 7267 603 41 0 7795 0
vsize: 31344
[startup+840.135 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7361 0 0 0 84000 22 0 0 25 0 1 0 475002476 32366592 7330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7902 7330 603 41 0 7861 0
vsize: 31608
[startup+850.136 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7431 0 0 0 85000 22 0 0 25 0 1 0 475002476 32636928 7400 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7968 7400 603 41 0 7927 0
vsize: 31872
[startup+860.137 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7517 0 0 0 86000 22 0 0 25 0 1 0 475002476 33034240 7486 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7486 603 41 0 8024 0
vsize: 32260
[startup+870.137 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7602 0 0 0 87000 23 0 0 25 0 1 0 475002476 33435648 7571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 7571 603 41 0 8122 0
vsize: 32652
[startup+880.137 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7685 0 0 0 88000 23 0 0 25 0 1 0 475002476 33705984 7654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8229 7654 603 41 0 8188 0
vsize: 32916
[startup+890.137 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7759 0 0 0 89000 23 0 0 25 0 1 0 475002476 33968128 7728 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8293 7728 603 41 0 8252 0
vsize: 33172
[startup+900.137 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7858 0 0 0 90000 23 0 0 25 0 1 0 475002476 34369536 7827 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8391 7827 603 41 0 8350 0
vsize: 33564
[startup+910.138 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7975 0 0 0 91000 23 0 0 25 0 1 0 475002476 34910208 7944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8523 7944 603 41 0 8482 0
vsize: 34092
[startup+920.138 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8076 0 0 0 92000 23 0 0 25 0 1 0 475002476 35311616 8045 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8621 8045 603 41 0 8580 0
vsize: 34484
[startup+930.138 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8160 0 0 0 93000 24 0 0 25 0 1 0 475002476 35581952 8129 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8687 8129 603 41 0 8646 0
vsize: 34748
[startup+940.139 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8249 0 0 0 94000 24 0 0 25 0 1 0 475002476 35979264 8218 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8784 8218 603 41 0 8743 0
vsize: 35136
[startup+950.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8341 0 0 0 95000 24 0 0 25 0 1 0 475002476 36380672 8310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8882 8310 603 41 0 8841 0
vsize: 35528
[startup+960.141 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8435 0 0 0 96000 25 0 0 25 0 1 0 475002476 36777984 8404 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8979 8404 603 41 0 8938 0
vsize: 35916
[startup+970.142 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8588 0 0 0 96999 25 0 0 25 0 1 0 475002476 37318656 8557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8557 603 41 0 9070 0
vsize: 36444
[startup+980.141 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8805 0 0 0 97998 26 0 0 25 0 1 0 475002476 38260736 8774 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9341 8774 603 41 0 9300 0
vsize: 37364
[startup+990.142 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8933 0 0 0 98997 27 0 0 25 0 1 0 475002476 38801408 8902 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9473 8902 603 41 0 9432 0
vsize: 37892
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9027 0 0 0 99997 27 0 0 25 0 1 0 475002476 39067648 8996 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9538 8996 603 41 0 9497 0
vsize: 38152
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9127 0 0 0 100997 27 0 0 25 0 1 0 475002476 39473152 9096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9637 9096 603 41 0 9596 0
vsize: 38548
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9204 0 0 0 101997 28 0 0 25 0 1 0 475002476 39874560 9173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9735 9173 603 41 0 9694 0
vsize: 38940
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9273 0 0 0 102997 28 0 0 25 0 1 0 475002476 40144896 9242 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9801 9242 603 41 0 9760 0
vsize: 39204
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9353 0 0 0 103997 28 0 0 25 0 1 0 475002476 40415232 9322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9867 9322 603 41 0 9826 0
vsize: 39468
[startup+1050.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9431 0 0 0 104997 29 0 0 25 0 1 0 475002476 40820736 9400 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9966 9400 603 41 0 9925 0
vsize: 39864
[startup+1060.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9520 0 0 0 105997 29 0 0 25 0 1 0 475002476 41091072 9489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10032 9489 603 41 0 9991 0
vsize: 40128
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9607 0 0 0 106997 29 0 0 25 0 1 0 475002476 41488384 9576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10129 9576 603 41 0 10088 0
vsize: 40516
[startup+1080.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9683 0 0 0 107997 29 0 0 25 0 1 0 475002476 41754624 9652 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10194 9652 603 41 0 10153 0
vsize: 40776
[startup+1090.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9765 0 0 0 108997 30 0 0 25 0 1 0 475002476 42160128 9734 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10293 9734 603 41 0 10252 0
vsize: 41172
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9853 0 0 0 109996 30 0 0 25 0 1 0 475002476 42422272 9822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10357 9822 603 41 0 10316 0
vsize: 41428
[startup+1110.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 110997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1120.14 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 111997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1130.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 112997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1140.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 113997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1150.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 114997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1160.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 115998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1170.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 116998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223544 1075350251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1180.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 117997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1190.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 118998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1335
Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 119998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1335
Raw data (stat): 1335 (minisat+) Z 1334 26667 26666 0 -1 12 9910 0 0 0 119998 32 0 0 25 0 1 0 475002476 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.17
CPU time (s): 1200.31
CPU user time (s): 1199.98
CPU system time (s): 0.328949
CPU usage (%): 100.012
Max. virtual memory (Kb): 41684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####