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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-f2000.opb
MD5SUM4675a5d50c7e04c9a0597ae768da1a88
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 4000
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 4000
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 4000
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables4000
Total number of constraints10500
Number of constraints which are clauses10500
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 6191 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 03:47:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4640 boxname=wulflinc26 idbench=128 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4675a5d50c7e04c9a0597ae768da1a88  /oldhome/oroussel/tmp/wulflinc26/normalized-f2000.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc26/normalized-f2000.opb /oldhome/oroussel/tmp/wulflinc26/normalized-f2000.opb
IDLAUNCH: 4640
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        822740 kB
Buffers:         35724 kB
Cached:         135404 kB
SwapCached:       2476 kB
Active:          56696 kB
Inactive:       119768 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        822488 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29652 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:07:37 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4640 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 10500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10500    29500 |    3500       0        0     nan |  0.000 % |
c |       101 |   10500    29500 |    3850     101     5214    51.6 |  0.000 % |
c |       254 |   10500    29500 |    4235     254    16768    66.0 |  0.000 % |
c |       480 |   10500    29500 |    4658     480    31254    65.1 |  0.000 % |
c |       818 |   10500    29500 |    5124     818    54667    66.8 |  0.000 % |
c |      1325 |   10500    29500 |    5636    1325    91945    69.4 |  0.000 % |
c |      2085 |   10500    29500 |    6200    2085   147368    70.7 |  0.000 % |
c |      3224 |   10500    29500 |    6820    3224   227442    70.5 |  0.000 % |
c |      4933 |   10500    29500 |    7502    4933   356310    72.2 |  0.000 % |
c |      7498 |   10500    29500 |    8252    7498   558986    74.6 |  0.000 % |
c |     11342 |   10500    29500 |    9078    7035   532667    75.7 |  0.000 % |
c |     17110 |   10500    29500 |    9985    8082   628618    77.8 |  0.000 % |
c |     25760 |   10500    29500 |   10984    6399   501007    78.3 |  0.000 % |
c |     38734 |   10500    29500 |   12082    8099   680844    84.1 |  0.000 % |
c |     58195 |   10500    29500 |   13291    8833   695144    78.7 |  0.000 % |
c |     87387 |   10500    29500 |   14620   10633   872256    82.0 |  0.000 % |
c |    131179 |   10500    29500 |   16082    9098   714655    78.6 |  0.000 % |
c |    196863 |   10500    29500 |   17690    8808   654716    74.3 |  0.000 % |
c |    295391 |   10500    29500 |   19459   16874  1288385    76.4 |  0.000 % |
c |    443181 |   10500    29500 |   21405   15399  1144903    74.3 |  0.000 % |
c |    664864 |   10500    29500 |   23546   18740  1450858    77.4 |  0.000 % |
#### 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.36 0.69 0.81 2/54 32494
Raw data (stat): 32494 (runsolver) R 32493 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481471985 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.46 0.70 0.81 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 1400 0 0 0 993 5 0 0 25 0 1 0 481471985 7303168 1378 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1783 1378 603 41 0 1742 0
vsize: 7132
[startup+20.0019 s]
Raw data (loadavg): 0.54 0.71 0.81 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 1659 0 0 0 1992 6 0 0 25 0 1 0 481471985 8380416 1637 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2046 1637 603 41 0 2005 0
vsize: 8184
[startup+30.002 s]
Raw data (loadavg): 0.61 0.72 0.81 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 1823 0 0 0 2991 7 0 0 25 0 1 0 481471985 9052160 1801 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2210 1801 603 41 0 2169 0
vsize: 8840
[startup+40.002 s]
Raw data (loadavg): 0.67 0.73 0.81 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 1910 0 0 0 3991 7 0 0 25 0 1 0 481471985 9457664 1888 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2309 1888 603 41 0 2268 0
vsize: 9236
[startup+50.0016 s]
Raw data (loadavg): 0.72 0.74 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2016 0 0 0 4991 7 0 0 25 0 1 0 481471985 9859072 1994 4294967295 134512640 134672761 3221224576 3221223572 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 1994 603 41 0 2366 0
vsize: 9628
[startup+60.0023 s]
Raw data (loadavg): 0.76 0.75 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2038 0 0 0 5991 8 0 0 25 0 1 0 481471985 9859072 2016 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 2016 603 41 0 2366 0
vsize: 9628
[startup+70.003 s]
Raw data (loadavg): 0.80 0.75 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2149 0 0 0 6991 8 0 0 25 0 1 0 481471985 10387456 2127 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2536 2127 603 41 0 2495 0
vsize: 10144
[startup+80.0036 s]
Raw data (loadavg): 0.83 0.76 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2217 0 0 0 7991 8 0 0 25 0 1 0 481471985 10657792 2195 4294967295 134512640 134672761 3221224576 3221223812 134541796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2195 603 41 0 2561 0
vsize: 10408
[startup+90.0031 s]
Raw data (loadavg): 0.86 0.77 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2297 0 0 0 8990 9 0 0 25 0 1 0 481471985 10924032 2275 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2667 2275 603 41 0 2626 0
vsize: 10668
[startup+100.003 s]
Raw data (loadavg): 0.88 0.78 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2309 0 0 0 9990 9 0 0 25 0 1 0 481471985 11059200 2287 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2700 2287 603 41 0 2659 0
vsize: 10800
[startup+110.004 s]
Raw data (loadavg): 0.90 0.78 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2418 0 0 0 10989 10 0 0 25 0 1 0 481471985 11460608 2396 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2396 603 41 0 2757 0
vsize: 11192
[startup+120.004 s]
Raw data (loadavg): 0.91 0.79 0.82 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2445 0 0 0 11990 10 0 0 25 0 1 0 481471985 11595776 2423 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2423 603 41 0 2790 0
vsize: 11324
[startup+130.005 s]
Raw data (loadavg): 0.92 0.80 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2482 0 0 0 12990 10 0 0 25 0 1 0 481471985 11730944 2460 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2460 603 41 0 2823 0
vsize: 11456
[startup+140.005 s]
Raw data (loadavg): 0.94 0.80 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2489 0 0 0 13990 10 0 0 25 0 1 0 481471985 11730944 2467 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2467 603 41 0 2823 0
vsize: 11456
[startup+150.004 s]
Raw data (loadavg): 0.94 0.81 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2512 0 0 0 14990 10 0 0 25 0 1 0 481471985 11866112 2490 4294967295 134512640 134672761 3221224576 3221223712 134560694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2490 603 41 0 2856 0
vsize: 11588
[startup+160.004 s]
Raw data (loadavg): 0.95 0.81 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2531 0 0 0 15990 10 0 0 25 0 1 0 481471985 12001280 2509 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2509 603 41 0 2889 0
vsize: 11720
[startup+170.004 s]
Raw data (loadavg): 0.96 0.82 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2647 0 0 0 16990 11 0 0 25 0 1 0 481471985 12546048 2625 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+180.005 s]
Raw data (loadavg): 0.97 0.83 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2647 0 0 0 17990 11 0 0 25 0 1 0 481471985 12546048 2625 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+190.005 s]
Raw data (loadavg): 0.97 0.83 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2650 0 0 0 18990 11 0 0 25 0 1 0 481471985 12546048 2628 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2628 603 41 0 3022 0
vsize: 12252
[startup+200.005 s]
Raw data (loadavg): 0.97 0.83 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2657 0 0 0 19990 11 0 0 25 0 1 0 481471985 12546048 2635 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2635 603 41 0 3022 0
vsize: 12252
[startup+210.005 s]
Raw data (loadavg): 0.98 0.84 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2669 0 0 0 20990 11 0 0 25 0 1 0 481471985 12546048 2647 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2647 603 41 0 3022 0
vsize: 12252
[startup+220.005 s]
Raw data (loadavg): 0.98 0.84 0.83 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2710 0 0 0 21990 11 0 0 25 0 1 0 481471985 12824576 2688 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2688 603 41 0 3090 0
vsize: 12524
[startup+230.006 s]
Raw data (loadavg): 0.98 0.85 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2714 0 0 0 22991 11 0 0 25 0 1 0 481471985 12824576 2692 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+240.006 s]
Raw data (loadavg): 0.99 0.85 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2714 0 0 0 23991 11 0 0 25 0 1 0 481471985 12824576 2692 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+250.005 s]
Raw data (loadavg): 0.99 0.86 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2750 0 0 0 24991 11 0 0 25 0 1 0 481471985 12959744 2728 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3164 2728 603 41 0 3123 0
vsize: 12656
[startup+260.006 s]
Raw data (loadavg): 0.99 0.86 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2797 0 0 0 25991 11 0 0 25 0 1 0 481471985 13094912 2775 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3197 2775 603 41 0 3156 0
vsize: 12788
[startup+270.006 s]
Raw data (loadavg): 0.99 0.87 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2857 0 0 0 26991 11 0 0 25 0 1 0 481471985 13365248 2835 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3263 2835 603 41 0 3222 0
vsize: 13052
[startup+280.006 s]
Raw data (loadavg): 0.99 0.87 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2915 0 0 0 27991 11 0 0 25 0 1 0 481471985 13631488 2893 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3328 2893 603 41 0 3287 0
vsize: 13312
[startup+290.007 s]
Raw data (loadavg): 0.99 0.87 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2954 0 0 0 28991 11 0 0 25 0 1 0 481471985 13766656 2932 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3361 2932 603 41 0 3320 0
vsize: 13444
[startup+300.007 s]
Raw data (loadavg): 0.99 0.88 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2968 0 0 0 29992 11 0 0 25 0 1 0 481471985 13766656 2946 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3361 2946 603 41 0 3320 0
vsize: 13444
[startup+310.007 s]
Raw data (loadavg): 0.99 0.88 0.84 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2971 0 0 0 30992 11 0 0 25 0 1 0 481471985 13905920 2949 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+320.007 s]
Raw data (loadavg): 0.99 0.89 0.84 3/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2971 0 0 0 31992 11 0 0 25 0 1 0 481471985 13905920 2949 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+330.008 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2971 0 0 0 32992 11 0 0 25 0 1 0 481471985 13905920 2949 4294967295 134512640 134672761 3221224576 3221223712 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+340.008 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 2979 0 0 0 33992 11 0 0 25 0 1 0 481471985 13905920 2957 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2957 603 41 0 3354 0
vsize: 13580
[startup+350.007 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3008 0 0 0 34992 12 0 0 25 0 1 0 481471985 14041088 2986 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+360.008 s]
Raw data (loadavg): 0.99 0.90 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3008 0 0 0 35993 12 0 0 25 0 1 0 481471985 14041088 2986 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+370.009 s]
Raw data (loadavg): 0.99 0.90 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3008 0 0 0 36993 12 0 0 25 0 1 0 481471985 14041088 2986 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+380.009 s]
Raw data (loadavg): 0.99 0.90 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3048 0 0 0 37993 12 0 0 25 0 1 0 481471985 14172160 3026 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3460 3026 603 41 0 3419 0
vsize: 13840
[startup+390.01 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3101 0 0 0 38993 12 0 0 25 0 1 0 481471985 14442496 3079 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3526 3079 603 41 0 3485 0
vsize: 14104
[startup+400.01 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3177 0 0 0 39992 12 0 0 25 0 1 0 481471985 14708736 3155 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3155 603 41 0 3550 0
vsize: 14364
[startup+410.01 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3179 0 0 0 40992 12 0 0 25 0 1 0 481471985 14708736 3157 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3157 603 41 0 3550 0
vsize: 14364
[startup+420.01 s]
Raw data (loadavg): 0.99 0.91 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3197 0 0 0 41992 12 0 0 25 0 1 0 481471985 14843904 3175 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3624 3175 603 41 0 3583 0
vsize: 14496
[startup+430.011 s]
Raw data (loadavg): 0.99 0.92 0.85 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3206 0 0 0 42993 12 0 0 25 0 1 0 481471985 14843904 3184 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3624 3184 603 41 0 3583 0
vsize: 14496
[startup+440.01 s]
Raw data (loadavg): 0.99 0.92 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3221 0 0 0 43993 12 0 0 25 0 1 0 481471985 14843904 3199 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3624 3199 603 41 0 3583 0
vsize: 14496
[startup+450.01 s]
Raw data (loadavg): 0.99 0.92 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3249 0 0 0 44993 13 0 0 25 0 1 0 481471985 14979072 3227 4294967295 134512640 134672761 3221224576 3221223712 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3227 603 41 0 3616 0
vsize: 14628
[startup+460.011 s]
Raw data (loadavg): 0.99 0.92 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3255 0 0 0 45992 13 0 0 25 0 1 0 481471985 14979072 3233 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3233 603 41 0 3616 0
vsize: 14628
[startup+470.01 s]
Raw data (loadavg): 0.99 0.92 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3260 0 0 0 46992 13 0 0 25 0 1 0 481471985 15126528 3238 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3238 603 41 0 3652 0
vsize: 14772
[startup+480.011 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3278 0 0 0 47992 13 0 0 25 0 1 0 481471985 15126528 3256 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3256 603 41 0 3652 0
vsize: 14772
[startup+490.011 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3280 0 0 0 48992 13 0 0 25 0 1 0 481471985 15126528 3258 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+500.011 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3280 0 0 0 49992 13 0 0 25 0 1 0 481471985 15126528 3258 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+510.011 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3283 0 0 0 50993 13 0 0 25 0 1 0 481471985 15126528 3261 4294967295 134512640 134672761 3221224576 3221223744 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3261 603 41 0 3652 0
vsize: 14772
[startup+520.01 s]
Raw data (loadavg): 0.99 0.93 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3287 0 0 0 51993 13 0 0 25 0 1 0 481471985 15126528 3265 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3265 603 41 0 3652 0
vsize: 14772
[startup+530.011 s]
Raw data (loadavg): 0.99 0.94 0.86 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3293 0 0 0 52993 13 0 0 25 0 1 0 481471985 15257600 3271 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3271 603 41 0 3684 0
vsize: 14900
[startup+540.011 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3293 0 0 0 53993 13 0 0 25 0 1 0 481471985 15257600 3271 4294967295 134512640 134672761 3221224576 3221223760 134559392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3271 603 41 0 3684 0
vsize: 14900
[startup+550.011 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3321 0 0 0 54993 13 0 0 25 0 1 0 481471985 15257600 3299 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3299 603 41 0 3684 0
vsize: 14900
[startup+560.01 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3380 0 0 0 55993 14 0 0 25 0 1 0 481471985 15527936 3358 4294967295 134512640 134672761 3221224576 3221223680 134555197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3358 603 41 0 3750 0
vsize: 15164
[startup+570.01 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3387 0 0 0 56993 14 0 0 25 0 1 0 481471985 15527936 3365 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3365 603 41 0 3750 0
vsize: 15164
[startup+580.011 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3429 0 0 0 57993 14 0 0 25 0 1 0 481471985 15806464 3407 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3407 603 41 0 3818 0
vsize: 15436
[startup+590.01 s]
Raw data (loadavg): 0.99 0.94 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3435 0 0 0 58993 14 0 0 25 0 1 0 481471985 15806464 3413 4294967295 134512640 134672761 3221224576 3221223680 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+600.011 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3435 0 0 0 59993 14 0 0 25 0 1 0 481471985 15806464 3413 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+610.011 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3556 0 0 0 60993 14 0 0 25 0 1 0 481471985 16355328 3534 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3534 603 41 0 3952 0
vsize: 15972
[startup+620.01 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3589 0 0 0 61993 14 0 0 25 0 1 0 481471985 16486400 3567 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4025 3567 603 41 0 3984 0
vsize: 16100
[startup+630.011 s]
Raw data (loadavg): 0.99 0.95 0.87 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3656 0 0 0 62993 14 0 0 25 0 1 0 481471985 16777216 3634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4096 3634 603 41 0 4055 0
vsize: 16384
[startup+640.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3727 0 0 0 63993 15 0 0 25 0 1 0 481471985 17047552 3705 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3705 603 41 0 4121 0
vsize: 16648
[startup+650.011 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3727 0 0 0 64993 15 0 0 25 0 1 0 481471985 17047552 3705 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3705 603 41 0 4121 0
vsize: 16648
[startup+660.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3737 0 0 0 65993 15 0 0 25 0 1 0 481471985 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+670.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3737 0 0 0 66994 15 0 0 25 0 1 0 481471985 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+680.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3737 0 0 0 67994 15 0 0 25 0 1 0 481471985 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+690.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3740 0 0 0 68994 15 0 0 25 0 1 0 481471985 17047552 3718 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3718 603 41 0 4121 0
vsize: 16648
[startup+700.012 s]
Raw data (loadavg): 0.99 0.95 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3745 0 0 0 69994 15 0 0 25 0 1 0 481471985 17047552 3723 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3723 603 41 0 4121 0
vsize: 16648
[startup+710.013 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3745 0 0 0 70994 15 0 0 25 0 1 0 481471985 17047552 3723 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3723 603 41 0 4121 0
vsize: 16648
[startup+720.013 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3746 0 0 0 71994 15 0 0 25 0 1 0 481471985 17047552 3724 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3724 603 41 0 4121 0
vsize: 16648
[startup+730.013 s]
Raw data (loadavg): 0.99 0.96 0.88 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3751 0 0 0 72995 15 0 0 25 0 1 0 481471985 17190912 3729 4294967295 134512640 134672761 3221224576 3221223744 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+740.014 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 32494
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3751 0 0 0 73995 15 0 0 25 0 1 0 481471985 17190912 3729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+750.014 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 32497
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3785 0 0 0 74995 15 0 0 25 0 1 0 481471985 17326080 3763 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3763 603 41 0 4189 0
vsize: 16920
[startup+760.014 s]
Raw data (loadavg): 1.07 0.98 0.89 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3791 0 0 0 75994 16 0 0 25 0 1 0 481471985 17326080 3769 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3769 603 41 0 4189 0
vsize: 16920
[startup+770.014 s]
Raw data (loadavg): 1.06 0.98 0.89 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3810 0 0 0 76994 16 0 0 25 0 1 0 481471985 17326080 3788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3788 603 41 0 4189 0
vsize: 16920
[startup+780.015 s]
Raw data (loadavg): 1.05 0.98 0.89 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3813 0 0 0 77994 16 0 0 25 0 1 0 481471985 17326080 3791 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+790.015 s]
Raw data (loadavg): 1.04 0.98 0.90 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3813 0 0 0 78994 16 0 0 25 0 1 0 481471985 17326080 3791 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+800.015 s]
Raw data (loadavg): 1.03 0.98 0.90 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3813 0 0 0 79994 16 0 0 25 0 1 0 481471985 17326080 3791 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+810.015 s]
Raw data (loadavg): 1.03 0.98 0.90 2/54 32547
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3827 0 0 0 80995 16 0 0 25 0 1 0 481471985 17461248 3805 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3805 603 41 0 4222 0
vsize: 17052
[startup+820.015 s]
Raw data (loadavg): 1.02 0.98 0.90 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3834 0 0 0 81995 16 0 0 25 0 1 0 481471985 17461248 3812 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3812 603 41 0 4222 0
vsize: 17052
[startup+830.016 s]
Raw data (loadavg): 1.02 0.98 0.90 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3837 0 0 0 82995 16 0 0 25 0 1 0 481471985 17461248 3815 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3815 603 41 0 4222 0
vsize: 17052
[startup+840.016 s]
Raw data (loadavg): 1.02 0.98 0.90 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3838 0 0 0 83995 16 0 0 25 0 1 0 481471985 17461248 3816 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3816 603 41 0 4222 0
vsize: 17052
[startup+850.015 s]
Raw data (loadavg): 1.01 0.98 0.90 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3841 0 0 0 84995 16 0 0 25 0 1 0 481471985 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+860.016 s]
Raw data (loadavg): 1.01 0.98 0.90 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3841 0 0 0 85995 16 0 0 25 0 1 0 481471985 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+870.015 s]
Raw data (loadavg): 1.08 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3841 0 0 0 86995 17 0 0 25 0 1 0 481471985 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+880.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3841 0 0 0 87995 17 0 0 25 0 1 0 481471985 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+890.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3887 0 0 0 88996 17 0 0 25 0 1 0 481471985 17727488 3865 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4328 3865 603 41 0 4287 0
vsize: 17312
[startup+900.019 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3887 0 0 0 89996 17 0 0 25 0 1 0 481471985 17727488 3865 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4328 3865 603 41 0 4287 0
vsize: 17312
[startup+910.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3931 0 0 0 90996 17 0 0 25 0 1 0 481471985 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+920.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3931 0 0 0 91996 17 0 0 25 0 1 0 481471985 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+930.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3931 0 0 0 92996 17 0 0 25 0 1 0 481471985 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+940.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 3931 0 0 0 93996 17 0 0 25 0 1 0 481471985 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+950.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4015 0 0 0 94995 18 0 0 25 0 1 0 481471985 18284544 3993 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 3993 603 41 0 4423 0
vsize: 17856
[startup+960.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4021 0 0 0 95995 18 0 0 25 0 1 0 481471985 18284544 3999 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 3999 603 41 0 4423 0
vsize: 17856
[startup+970.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4025 0 0 0 96995 18 0 0 25 0 1 0 481471985 18284544 4003 4294967295 134512640 134672761 3221224576 3221223680 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 4003 603 41 0 4423 0
vsize: 17856
[startup+980.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4033 0 0 0 97995 18 0 0 25 0 1 0 481471985 18284544 4011 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 4011 603 41 0 4423 0
vsize: 17856
[startup+990.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4038 0 0 0 98995 18 0 0 25 0 1 0 481471985 18415616 4016 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4016 603 41 0 4455 0
vsize: 17984
[startup+1000.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4043 0 0 0 99995 18 0 0 25 0 1 0 481471985 18415616 4021 4294967295 134512640 134672761 3221224576 3221223760 134559156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4021 603 41 0 4455 0
vsize: 17984
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4047 0 0 0 100995 18 0 0 25 0 1 0 481471985 18415616 4025 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4025 603 41 0 4455 0
vsize: 17984
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4051 0 0 0 101995 18 0 0 25 0 1 0 481471985 18415616 4029 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4051 0 0 0 102996 18 0 0 25 0 1 0 481471985 18415616 4029 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4056 0 0 0 103996 18 0 0 25 0 1 0 481471985 18415616 4034 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4034 603 41 0 4455 0
vsize: 17984
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4056 0 0 0 104996 18 0 0 25 0 1 0 481471985 18415616 4034 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4034 603 41 0 4455 0
vsize: 17984
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4092 0 0 0 105996 18 0 0 25 0 1 0 481471985 18546688 4070 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4070 603 41 0 4487 0
vsize: 18112
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4099 0 0 0 106996 18 0 0 25 0 1 0 481471985 18546688 4077 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4077 603 41 0 4487 0
vsize: 18112
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4155 0 0 0 107996 19 0 0 25 0 1 0 481471985 18821120 4133 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4595 4133 603 41 0 4554 0
vsize: 18380
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32549
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4159 0 0 0 108996 19 0 0 25 0 1 0 481471985 18821120 4137 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4595 4137 603 41 0 4554 0
vsize: 18380
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4179 0 0 0 109997 19 0 0 25 0 1 0 481471985 18980864 4157 4294967295 134512640 134672761 3221224576 3221223760 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4179 0 0 0 110997 19 0 0 25 0 1 0 481471985 18980864 4157 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4184 0 0 0 111997 19 0 0 25 0 1 0 481471985 18980864 4162 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4184 0 0 0 112997 19 0 0 25 0 1 0 481471985 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4184 0 0 0 113997 19 0 0 25 0 1 0 481471985 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4184 0 0 0 114997 19 0 0 25 0 1 0 481471985 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4210 0 0 0 115997 19 0 0 25 0 1 0 481471985 19111936 4188 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4188 603 41 0 4625 0
vsize: 18664
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4210 0 0 0 116997 19 0 0 25 0 1 0 481471985 19111936 4188 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4188 603 41 0 4625 0
vsize: 18664
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4214 0 0 0 117997 19 0 0 25 0 1 0 481471985 19111936 4192 4294967295 134512640 134672761 3221224576 3221223744 134559670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4192 603 41 0 4625 0
vsize: 18664
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4214 0 0 0 118998 19 0 0 25 0 1 0 481471985 19111936 4192 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4192 603 41 0 4625 0
vsize: 18664
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32551
Raw data (stat): 32494 (minisat+) R 32493 22612 22611 0 -1 0 4246 0 0 0 119997 19 0 0 25 0 1 0 481471985 19247104 4224 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4699 4224 603 41 0 4658 0
vsize: 18796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32551
Raw data (stat): 32494 (minisat+) Z 32493 22612 22611 0 -1 12 4248 0 0 0 119998 20 0 0 25 0 1 0 481471985 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.19
CPU user time (s): 1199.98
CPU system time (s): 0.206968
CPU usage (%): 100.013
Max. virtual memory (Kb): 18796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####