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/een/normalized-p0548.opb
MD5SUM422c0da7d5380a26c4dac413428db5c9
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14670
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1230.14
Number of variables527
Total number of constraints156
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints116
Minimum length of a constraint2
Maximum length of a constraint134

Trace number 7156 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        821272 kB
Buffers:         38552 kB
Cached:         155112 kB
SwapCached:          0 kB
Active:          81104 kB
Inactive:       115420 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        821020 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11280 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 22:01:57 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 5239 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s.
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    5
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    6
c ---[  98]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   19
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:    4
c ---[  89]---> BDD-cost:   24
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   28
c ---[  85]---> BDD-cost:   13
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   19
c ---[  72]---> BDD-cost:   24
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:   27
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   56
c ---[  64]---> BDD-cost:   50
c ---[  63]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   33
c ---[  60]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:   34
c ---[  56]---> BDD-cost:   33
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   24
c ---[  52]---> BDD-cost:   37
c ---[  51]---> BDD-cost:   37
c ---[  50]---> BDD-cost:   95
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  115
c ---[  46]---> BDD-cost:  120
c ---[  45]---> BDD-cost:  104
c ---[  44]---> BDD-cost:   29
c ---[  43]---> BDD-cost:   51
c ---[  42]---> BDD-cost:   35
c ---[  41]---> BDD-cost:   24
c ---[  39]---> BDD-cost:   61
c ---[  38]---> BDD-cost:  109
c ---[  37]---> BDD-cost:  153
c ---[  36]---> BDD-cost:  120
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   25
c ---[  33]---> BDD-cost:  121
c ---[  32]---> BDD-cost:   32
c ---[  31]---> BDD-cost:   70
c ---[  30]---> BDD-cost:   56
c ---[  29]---> BDD-cost:   78
c ---[  28]---> BDD-cost:   84
c ---[  27]---> BDD-cost:   36
c ---[  26]---> BDD-cost:   91
c ---[  25]---> BDD-cost:   42
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:  128
c ---[  21]---> BDD-cost:   61
c ---[  19]---> BDD-cost:   85
c ---[  18]---> BDD-cost:   55
c ---[  17]---> BDD-cost:   79
c ---[  16]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  15]---> BDD-cost:   26
c ---[  14]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  13]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   49
c ---[  10]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[   9]---> BDD-cost:    2
c ---[   8]---> BDD-cost:    2
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    2
c ---[   5]---> BDD-cost:    4
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   11
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24240    72665 |    8080       0        0     nan |  0.000 % |
c |       100 |   24240    72665 |    8888     100      423     4.2 |  2.252 % |
c |       250 |   24195    72508 |    9776     241      968     4.0 |  2.325 % |
c |       475 |   24195    72508 |   10754     466     3788     8.1 |  2.325 % |
c |       812 |   24195    72508 |   11829     803    11179    13.9 |  2.325 % |
c |      1322 |   24156    72376 |   13012    1308    18060    13.8 |  2.379 % |
c |      2081 |   24117    72256 |   14314    2063    31627    15.3 |  2.452 % |
c |      3220 |   24117    72256 |   15745    3202    57528    18.0 |  2.452 % |
c |      4928 |   24117    72256 |   17320    4910    99011    20.2 |  2.452 % |
c |      7490 |   24117    72256 |   19052    7472   183731    24.6 |  2.452 % |
c |     11334 |   24117    72256 |   20957   11316   318128    28.1 |  2.452 % |
c |     17101 |   24099    72199 |   23053   17081   555186    32.5 |  2.488 % |
c |     25751 |   24054    72046 |   25358   13940   439186    31.5 |  2.579 % |
c |     38726 |   24028    71958 |   27894   14000   539530    38.5 |  2.652 % |
c |     58188 |   24024    71948 |   30683   17126   610577    35.7 |  2.670 % |
c |     87382 |   24020    71938 |   33752   28243  1126255    39.9 |  2.688 % |
c |    131171 |   24016    71928 |   37127   33207  1044551    31.5 |  2.706 % |
c |    196855 |   24002    71884 |   40840   30136  1015201    33.7 |  2.761 % |
c |    295382 |   23982    71834 |   44924   21576   646217    30.0 |  2.851 % |
c |    443171 |   23977    71819 |   49416   19976   621889    31.1 |  2.870 % |
c |    664854 |   23972    71804 |   54358   37695  1980650    52.5 |  2.888 % |
#### 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): 1.01 1.00 0.91 2/54 2468
Raw data (stat): 2468 (runsolver) R 2467 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429697273 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 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.0006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 1808 0 0 0 993 4 0 0 25 0 1 0 429697273 9064448 1778 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2213 1778 603 41 0 2172 0
vsize: 8852
[startup+20.0002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2007 0 0 0 1993 5 0 0 25 0 1 0 429697273 9871360 1977 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2410 1977 603 41 0 2369 0
vsize: 9640
[startup+30.0011 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2188 0 0 0 2993 5 0 0 25 0 1 0 429697273 10539008 2158 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2573 2158 603 41 0 2532 0
vsize: 10292
[startup+40.0004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2385 0 0 0 3993 5 0 0 25 0 1 0 429697273 11354112 2355 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2772 2355 603 41 0 2731 0
vsize: 11088
[startup+50.0001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2491 0 0 0 4993 5 0 0 25 0 1 0 429697273 11759616 2461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2871 2461 603 41 0 2830 0
vsize: 11484
[startup+60 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2491 0 0 0 5993 5 0 0 25 0 1 0 429697273 11759616 2461 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2871 2461 603 41 0 2830 0
vsize: 11484
[startup+70.0005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2770 0 0 0 6991 7 0 0 25 0 1 0 429697273 13094912 2740 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2740 603 41 0 3156 0
vsize: 12788
[startup+80.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2770 0 0 0 7990 7 0 0 25 0 1 0 429697273 13094912 2740 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3197 2740 603 41 0 3156 0
vsize: 12788
[startup+90.0009 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2792 0 0 0 8990 7 0 0 25 0 1 0 429697273 13246464 2762 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3234 2762 603 41 0 3193 0
vsize: 12936
[startup+100 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2810 0 0 0 9991 7 0 0 25 0 1 0 429697273 13246464 2780 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3234 2780 603 41 0 3193 0
vsize: 12936
[startup+110.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2823 0 0 0 10991 7 0 0 25 0 1 0 429697273 13393920 2793 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2793 603 41 0 3229 0
vsize: 13080
[startup+120.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2843 0 0 0 11991 7 0 0 25 0 1 0 429697273 13393920 2813 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2813 603 41 0 3229 0
vsize: 13080
[startup+130.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2880 0 0 0 12991 7 0 0 25 0 1 0 429697273 13529088 2850 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3303 2850 603 41 0 3262 0
vsize: 13212
[startup+140.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2917 0 0 0 13991 7 0 0 25 0 1 0 429697273 13668352 2887 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3337 2887 603 41 0 3296 0
vsize: 13348
[startup+150.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2934 0 0 0 14991 7 0 0 25 0 1 0 429697273 13803520 2904 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3370 2904 603 41 0 3329 0
vsize: 13480
[startup+160.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2948 0 0 0 15991 7 0 0 25 0 1 0 429697273 13803520 2918 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3370 2918 603 41 0 3329 0
vsize: 13480
[startup+170.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2966 0 0 0 16992 7 0 0 25 0 1 0 429697273 13967360 2936 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3410 2936 603 41 0 3369 0
vsize: 13640
[startup+180.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2968 0 0 0 17992 7 0 0 25 0 1 0 429697273 13967360 2938 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3410 2938 603 41 0 3369 0
vsize: 13640
[startup+190.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 2982 0 0 0 18992 7 0 0 25 0 1 0 429697273 14106624 2952 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3444 2952 603 41 0 3403 0
vsize: 13776
[startup+200.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3193 0 0 0 19991 8 0 0 25 0 1 0 429697273 14917632 3163 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3163 603 41 0 3601 0
vsize: 14568
[startup+210.001 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3193 0 0 0 20991 8 0 0 25 0 1 0 429697273 14917632 3163 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3163 603 41 0 3601 0
vsize: 14568
[startup+220.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3212 0 0 0 21992 8 0 0 25 0 1 0 429697273 15056896 3182 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3676 3182 603 41 0 3635 0
vsize: 14704
[startup+230.003 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3435 0 0 0 22991 9 0 0 25 0 1 0 429697273 15855616 3405 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3871 3405 603 41 0 3830 0
vsize: 15484
[startup+240.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3435 0 0 0 23991 9 0 0 25 0 1 0 429697273 15855616 3405 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3871 3405 603 41 0 3830 0
vsize: 15484
[startup+250.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3435 0 0 0 24991 9 0 0 25 0 1 0 429697273 15855616 3405 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3871 3405 603 41 0 3830 0
vsize: 15484
[startup+260.003 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3447 0 0 0 25991 9 0 0 25 0 1 0 429697273 15990784 3417 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3904 3417 603 41 0 3863 0
vsize: 15616
[startup+270.002 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3475 0 0 0 26991 9 0 0 25 0 1 0 429697273 16138240 3445 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3445 603 41 0 3899 0
vsize: 15760
[startup+280.003 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3515 0 0 0 27992 9 0 0 25 0 1 0 429697273 16302080 3485 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3485 603 41 0 3939 0
vsize: 15920
[startup+290.004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3527 0 0 0 28992 9 0 0 25 0 1 0 429697273 16302080 3497 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3497 603 41 0 3939 0
vsize: 15920
[startup+300.003 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3527 0 0 0 29992 9 0 0 25 0 1 0 429697273 16302080 3497 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3497 603 41 0 3939 0
vsize: 15920
[startup+310.004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3534 0 0 0 30992 10 0 0 25 0 1 0 429697273 16302080 3504 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3504 603 41 0 3939 0
vsize: 15920
[startup+320.004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3554 0 0 0 31992 10 0 0 25 0 1 0 429697273 16461824 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4019 3524 603 41 0 3978 0
vsize: 16076
[startup+330.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3568 0 0 0 32992 10 0 0 25 0 1 0 429697273 16461824 3538 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4019 3538 603 41 0 3978 0
vsize: 16076
[startup+340.004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3571 0 0 0 33992 10 0 0 25 0 1 0 429697273 16461824 3541 4294967295 134512640 134672761 3221224576 3221223744 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4019 3541 603 41 0 3978 0
vsize: 16076
[startup+350.004 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3579 0 0 0 34992 10 0 0 25 0 1 0 429697273 16625664 3549 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4059 3549 603 41 0 4018 0
vsize: 16236
[startup+360.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3594 0 0 0 35993 10 0 0 25 0 1 0 429697273 16625664 3564 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4059 3564 603 41 0 4018 0
vsize: 16236
[startup+370.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3658 0 0 0 36993 10 0 0 25 0 1 0 429697273 16896000 3628 4294967295 134512640 134672761 3221224576 3221223680 134560299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4125 3628 603 41 0 4084 0
vsize: 16500
[startup+380.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3671 0 0 0 37993 10 0 0 25 0 1 0 429697273 17039360 3641 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4160 3641 603 41 0 4119 0
vsize: 16640
[startup+390.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3687 0 0 0 38993 10 0 0 25 0 1 0 429697273 17039360 3657 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4160 3657 603 41 0 4119 0
vsize: 16640
[startup+400.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 3818 0 0 0 39993 10 0 0 25 0 1 0 429697273 17584128 3788 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4293 3788 603 41 0 4252 0
vsize: 17172
[startup+410.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4013 0 0 0 40993 10 0 0 25 0 1 0 429697273 18391040 3983 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4490 3983 603 41 0 4449 0
vsize: 17960
[startup+420.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4018 0 0 0 41993 10 0 0 25 0 1 0 429697273 18526208 3988 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4523 3988 603 41 0 4482 0
vsize: 18092
[startup+430.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4021 0 0 0 42993 10 0 0 25 0 1 0 429697273 18526208 3991 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4523 3991 603 41 0 4482 0
vsize: 18092
[startup+440.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4021 0 0 0 43993 10 0 0 25 0 1 0 429697273 18526208 3991 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4523 3991 603 41 0 4482 0
vsize: 18092
[startup+450.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4067 0 0 0 44993 10 0 0 25 0 1 0 429697273 18657280 4037 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4555 4037 603 41 0 4514 0
vsize: 18220
[startup+460.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4067 0 0 0 45994 10 0 0 25 0 1 0 429697273 18657280 4037 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4555 4037 603 41 0 4514 0
vsize: 18220
[startup+470.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4068 0 0 0 46994 10 0 0 25 0 1 0 429697273 18657280 4038 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4555 4038 603 41 0 4514 0
vsize: 18220
[startup+480.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4077 0 0 0 47994 10 0 0 25 0 1 0 429697273 18657280 4047 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4555 4047 603 41 0 4514 0
vsize: 18220
[startup+490.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4102 0 0 0 48994 10 0 0 25 0 1 0 429697273 18812928 4072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4593 4072 603 41 0 4552 0
vsize: 18372
[startup+500.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4102 0 0 0 49994 10 0 0 25 0 1 0 429697273 18812928 4072 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4593 4072 603 41 0 4552 0
vsize: 18372
[startup+510.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4102 0 0 0 50993 11 0 0 25 0 1 0 429697273 18812928 4072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4593 4072 603 41 0 4552 0
vsize: 18372
[startup+520.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4102 0 0 0 51993 11 0 0 25 0 1 0 429697273 18812928 4072 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4593 4072 603 41 0 4552 0
vsize: 18372
[startup+530.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4118 0 0 0 52993 11 0 0 25 0 1 0 429697273 18976768 4088 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4088 603 41 0 4592 0
vsize: 18532
[startup+540.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4125 0 0 0 53993 11 0 0 25 0 1 0 429697273 18976768 4095 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4095 603 41 0 4592 0
vsize: 18532
[startup+550.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4128 0 0 0 54993 11 0 0 25 0 1 0 429697273 18976768 4098 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4098 603 41 0 4592 0
vsize: 18532
[startup+560.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4136 0 0 0 55994 11 0 0 25 0 1 0 429697273 18976768 4106 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4106 603 41 0 4592 0
vsize: 18532
[startup+570.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4149 0 0 0 56994 11 0 0 25 0 1 0 429697273 18976768 4119 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4633 4119 603 41 0 4592 0
vsize: 18532
[startup+580.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4202 0 0 0 57994 11 0 0 25 0 1 0 429697273 19337216 4172 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4721 4172 603 41 0 4680 0
vsize: 18884
[startup+590.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4225 0 0 0 58994 11 0 0 25 0 1 0 429697273 19533824 4195 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4195 603 41 0 4728 0
vsize: 19076
[startup+600.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4227 0 0 0 59994 11 0 0 25 0 1 0 429697273 19533824 4197 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4197 603 41 0 4728 0
vsize: 19076
[startup+610.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4227 0 0 0 60994 11 0 0 25 0 1 0 429697273 19533824 4197 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4197 603 41 0 4728 0
vsize: 19076
[startup+620.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4228 0 0 0 61994 11 0 0 25 0 1 0 429697273 19533824 4198 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4198 603 41 0 4728 0
vsize: 19076
[startup+630.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4251 0 0 0 62994 12 0 0 25 0 1 0 429697273 19533824 4221 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4221 603 41 0 4728 0
vsize: 19076
[startup+640.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4252 0 0 0 63994 12 0 0 25 0 1 0 429697273 19533824 4222 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4222 603 41 0 4728 0
vsize: 19076
[startup+650.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4262 0 0 0 64995 12 0 0 25 0 1 0 429697273 19730432 4232 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4817 4232 603 41 0 4776 0
vsize: 19268
[startup+660.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4262 0 0 0 65995 12 0 0 25 0 1 0 429697273 19730432 4232 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4817 4232 603 41 0 4776 0
vsize: 19268
[startup+670.008 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4262 0 0 0 66995 12 0 0 25 0 1 0 429697273 19730432 4232 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4817 4232 603 41 0 4776 0
vsize: 19268
[startup+680.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4265 0 0 0 67995 12 0 0 25 0 1 0 429697273 19730432 4235 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4817 4235 603 41 0 4776 0
vsize: 19268
[startup+690.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4452 0 0 0 68995 12 0 0 25 0 1 0 429697273 20402176 4422 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4981 4422 603 41 0 4940 0
vsize: 19924
[startup+700.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4627 0 0 0 69995 12 0 0 25 0 1 0 429697273 21217280 4597 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5180 4597 603 41 0 5139 0
vsize: 20720
[startup+710.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4632 0 0 0 70995 12 0 0 25 0 1 0 429697273 21217280 4602 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5180 4602 603 41 0 5139 0
vsize: 20720
[startup+720.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4633 0 0 0 71995 12 0 0 25 0 1 0 429697273 21217280 4603 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5180 4603 603 41 0 5139 0
vsize: 20720
[startup+730.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4637 0 0 0 72995 12 0 0 25 0 1 0 429697273 21217280 4607 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5180 4607 603 41 0 5139 0
vsize: 20720
[startup+740.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4699 0 0 0 73995 13 0 0 25 0 1 0 429697273 21495808 4669 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4669 603 41 0 5207 0
vsize: 20992
[startup+750.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4918 0 0 0 74994 14 0 0 25 0 1 0 429697273 22421504 4888 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5474 4888 603 41 0 5433 0
vsize: 21896
[startup+760.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4918 0 0 0 75995 14 0 0 25 0 1 0 429697273 22421504 4888 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5474 4888 603 41 0 5433 0
vsize: 21896
[startup+770.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4920 0 0 0 76995 14 0 0 25 0 1 0 429697273 22421504 4890 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5474 4890 603 41 0 5433 0
vsize: 21896
[startup+780.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4920 0 0 0 77995 14 0 0 25 0 1 0 429697273 22421504 4890 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5474 4890 603 41 0 5433 0
vsize: 21896
[startup+790.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4936 0 0 0 78995 14 0 0 25 0 1 0 429697273 22577152 4906 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5512 4906 603 41 0 5471 0
vsize: 22048
[startup+800.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 4964 0 0 0 79995 14 0 0 25 0 1 0 429697273 22577152 4934 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5512 4934 603 41 0 5471 0
vsize: 22048
[startup+810.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5212 0 0 0 80995 14 0 0 25 0 1 0 429697273 23646208 5182 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5773 5182 603 41 0 5732 0
vsize: 23092
[startup+820.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5328 0 0 0 81994 15 0 0 25 0 1 0 429697273 24195072 5298 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5298 603 41 0 5866 0
vsize: 23628
[startup+830.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5331 0 0 0 82994 15 0 0 25 0 1 0 429697273 24195072 5301 4294967295 134512640 134672761 3221224576 3221223736 134559749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5301 603 41 0 5866 0
vsize: 23628
[startup+840.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5331 0 0 0 83994 15 0 0 25 0 1 0 429697273 24195072 5301 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5301 603 41 0 5866 0
vsize: 23628
[startup+850.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5336 0 0 0 84994 15 0 0 25 0 1 0 429697273 24195072 5306 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5907 5306 603 41 0 5866 0
vsize: 23628
[startup+860.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5339 0 0 0 85994 15 0 0 25 0 1 0 429697273 24195072 5309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5309 603 41 0 5866 0
vsize: 23628
[startup+870.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5343 0 0 0 86994 15 0 0 25 0 1 0 429697273 24195072 5313 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5313 603 41 0 5866 0
vsize: 23628
[startup+880.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5343 0 0 0 87995 15 0 0 25 0 1 0 429697273 24195072 5313 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5313 603 41 0 5866 0
vsize: 23628
[startup+890.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5345 0 0 0 88995 15 0 0 25 0 1 0 429697273 24195072 5315 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5315 603 41 0 5866 0
vsize: 23628
[startup+900.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5345 0 0 0 89995 15 0 0 25 0 1 0 429697273 24195072 5315 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5315 603 41 0 5866 0
vsize: 23628
[startup+910.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5346 0 0 0 90995 15 0 0 25 0 1 0 429697273 24195072 5316 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5316 603 41 0 5866 0
vsize: 23628
[startup+920.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5346 0 0 0 91995 15 0 0 25 0 1 0 429697273 24195072 5316 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5316 603 41 0 5866 0
vsize: 23628
[startup+930.007 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5346 0 0 0 92995 15 0 0 25 0 1 0 429697273 24195072 5316 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5316 603 41 0 5866 0
vsize: 23628
[startup+940.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5346 0 0 0 93996 15 0 0 25 0 1 0 429697273 24195072 5316 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5316 603 41 0 5866 0
vsize: 23628
[startup+950.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5355 0 0 0 94996 15 0 0 25 0 1 0 429697273 24195072 5325 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5325 603 41 0 5866 0
vsize: 23628
[startup+960.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5357 0 0 0 95996 15 0 0 25 0 1 0 429697273 24195072 5327 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5327 603 41 0 5866 0
vsize: 23628
[startup+970.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5357 0 0 0 96996 15 0 0 25 0 1 0 429697273 24195072 5327 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5327 603 41 0 5866 0
vsize: 23628
[startup+980.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 97996 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+990.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 98996 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 99996 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223728 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 100997 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 101997 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 102997 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 103997 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5358 0 0 0 104997 15 0 0 25 0 1 0 429697273 24195072 5328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5907 5328 603 41 0 5866 0
vsize: 23628
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5454 0 0 0 105997 16 0 0 25 0 1 0 429697273 24596480 5424 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6005 5424 603 41 0 5964 0
vsize: 24020
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5459 0 0 0 106997 16 0 0 25 0 1 0 429697273 24752128 5429 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5429 603 41 0 6002 0
vsize: 24172
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 2468
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5460 0 0 0 107997 16 0 0 25 0 1 0 429697273 24752128 5430 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5430 603 41 0 6002 0
vsize: 24172
[startup+1090.01 s]
Raw data (loadavg): 1.08 1.01 0.92 3/57 2507
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5460 0 0 0 108997 16 0 0 25 0 1 0 429697273 24752128 5430 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5430 603 41 0 6002 0
vsize: 24172
[startup+1100.01 s]
Raw data (loadavg): 1.07 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5468 0 0 0 109998 16 0 0 25 0 1 0 429697273 24752128 5438 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5438 603 41 0 6002 0
vsize: 24172
[startup+1110.01 s]
Raw data (loadavg): 1.06 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5479 0 0 0 110998 16 0 0 25 0 1 0 429697273 24752128 5449 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5449 603 41 0 6002 0
vsize: 24172
[startup+1120.01 s]
Raw data (loadavg): 1.05 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5494 0 0 0 111998 16 0 0 25 0 1 0 429697273 24915968 5464 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5464 603 41 0 6042 0
vsize: 24332
[startup+1130.01 s]
Raw data (loadavg): 1.04 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5504 0 0 0 112998 16 0 0 25 0 1 0 429697273 24915968 5474 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5474 603 41 0 6042 0
vsize: 24332
[startup+1140.01 s]
Raw data (loadavg): 1.03 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5505 0 0 0 113998 16 0 0 25 0 1 0 429697273 24915968 5475 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5475 603 41 0 6042 0
vsize: 24332
[startup+1150.01 s]
Raw data (loadavg): 1.03 1.01 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5505 0 0 0 114998 16 0 0 25 0 1 0 429697273 24915968 5475 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5475 603 41 0 6042 0
vsize: 24332
[startup+1160.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2521
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5505 0 0 0 115998 16 0 0 25 0 1 0 429697273 24915968 5475 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5475 603 41 0 6042 0
vsize: 24332
[startup+1170.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2523
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5505 0 0 0 116999 16 0 0 25 0 1 0 429697273 24915968 5475 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5475 603 41 0 6042 0
vsize: 24332
[startup+1180.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 2523
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5508 0 0 0 117999 16 0 0 25 0 1 0 429697273 24915968 5478 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5478 603 41 0 6042 0
vsize: 24332
[startup+1190.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2523
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5509 0 0 0 118999 16 0 0 25 0 1 0 429697273 24915968 5479 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6083 5479 603 41 0 6042 0
vsize: 24332
[startup+1200.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 2523
Raw data (stat): 2468 (minisat+) R 2467 22932 22931 0 -1 0 5519 0 0 0 119999 16 0 0 25 0 1 0 429697273 25063424 5489 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6119 5489 603 41 0 6078 0
vsize: 24476
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 2523
Raw data (stat): 2468 (minisat+) Z 2467 22932 22931 0 -1 12 5521 0 0 0 119999 17 0 0 25 0 1 0 429697273 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.02
CPU time (s): 1200.18
CPU user time (s): 1200
CPU system time (s): 0.179972
CPU usage (%): 100.013
Max. virtual memory (Kb): 24476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####