PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb
MD5SUM	feaa96df552ef9989407735877840272
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13
Optimality of the best value was proved	NO
Number of terms in the objective function	776
Biggest coefficient in the objective function	474
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	2127
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	474
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	2127
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	776
Total number of constraints	1642
Number of constraints which are clauses	701
Number of constraints which are cardinality constraints (but not clauses)	941
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 5691

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 01:24:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4129 boxname=wulflinc11 idbench=369 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc11/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-10:20:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc11/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 4129
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        910948 kB
Buffers:         35652 kB
Cached:          63796 kB
SwapCached:       4932 kB
Active:          56444 kB
Inactive:        50836 kB
HighTotal:      131008 kB
HighFree:        63420 kB
LowTotal:       903652 kB
LowFree:        847528 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10968 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:44:22 (client local time) WITH STATUS 10 IN 1209.79 SECONDS
stats: 4129 7 1209.79 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   44
c ---[ 161]---> BDD-cost:   44
c ---[ 160]---> BDD-cost:   50
c ---[ 159]---> BDD-cost:   44
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:   44
c ---[ 156]---> BDD-cost:   41
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   47
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   50
c ---[ 139]---> BDD-cost:   50
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   47
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   29
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   35
c ---[ 123]---> BDD-cost:   41
c ---[ 122]---> BDD-cost:   45
c ---[ 121]---> BDD-cost:   47
c ---[ 120]---> BDD-cost:   50
c ---[ 119]---> BDD-cost:   53
c ---[ 118]---> BDD-cost:   53
c ---[ 117]---> BDD-cost:   47
c ---[ 116]---> BDD-cost:   41
c ---[ 115]---> BDD-cost:   35
c ---[ 114]---> BDD-cost:   21
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   20
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:   41
c ---[ 101]---> BDD-cost:   47
c ---[ 100]---> BDD-cost:   45
c ---[  99]---> BDD-cost:   53
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   47
c ---[  96]---> BDD-cost:   41
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:    5
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   44
c ---[  78]---> BDD-cost:   38
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   29
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    7
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:    7
c ---[  38]---> BDD-cost:   14
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    7
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    7
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    8
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    0
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9119    26086 |    2735       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4273          
c   -- var.elim.:  2000/4273          
c   -- var.elim.:  3000/4273          
c   -- var.elim.:  4000/4273          
c   -- var.elim.:  4273/4273          
c   -- var.elim.:  1000/2084          
c   -- var.elim.:  2000/2084          
c   -- var.elim.:  2084/2084          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/1921          
c   -- var.elim.:  1921/1921          
c   -- var.elim.:  1000/1022          
c   -- var.elim.:  1022/1022          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  43/43          
c   -- var.elim.:  37/37          
c |         0 |    6670    25316 |      --       0       --      -- |     --   | -2449/-278
c |         0 |    6670    25316 |    2668       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.511922 s)
c ==============================================================================
c [1mFound solution: 727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:55538     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  102661   249779 |   30798       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/47420          
c   -- var.elim.:  2000/47420          
c   -- var.elim.:  3000/47420          
c   -- var.elim.:  4000/47420          
c   -- var.elim.:  5000/47420          
c   -- var.elim.:  6000/47420          
c   -- var.elim.:  7000/47420          
c   -- var.elim.:  8000/47420          
c   -- var.elim.:  9000/47420          
c   -- var.elim.:  10000/47420          
c   -- var.elim.:  11000/47420          
c   -- var.elim.:  12000/47420          
c   -- var.elim.:  13000/47420          
c   -- var.elim.:  14000/47420          
c   -- var.elim.:  15000/47420          
c   -- var.elim.:  16000/47420          
c   -- var.elim.:  17000/47420          
c   -- var.elim.:  18000/47420          
c   -- var.elim.:  19000/47420          
c   -- var.elim.:  20000/47420          
c   -- var.elim.:  21000/47420          
c   -- var.elim.:  22000/47420          
c   -- var.elim.:  23000/47420          
c   -- var.elim.:  24000/47420          
c   -- var.elim.:  25000/47420          
c   -- var.elim.:  26000/47420          
c   -- var.elim.:  27000/47420          
c   -- var.elim.:  28000/47420          
c   -- var.elim.:  29000/47420          
c   -- var.elim.:  30000/47420          
c   -- var.elim.:  31000/47420          
c   -- var.elim.:  32000/47420          
c   -- var.elim.:  33000/47420          
c   -- var.elim.:  34000/47420          
c   -- var.elim.:  35000/47420          
c   -- var.elim.:  36000/47420          
c   -- var.elim.:  37000/47420          
c   -- var.elim.:  38000/47420          
c   -- var.elim.:  39000/47420          
c   -- var.elim.:  40000/47420          
c   -- var.elim.:  41000/47420          
c   -- var.elim.:  42000/47420          
c   -- var.elim.:  43000/47420          
c   -- var.elim.:  44000/47420          
c   -- var.elim.:  45000/47420          
c   -- var.elim.:  46000/47420          
c   -- var.elim.:  47000/47420          
c   -- var.elim.:  47420/47420          
c   -- var.elim.:  1000/24629          
c   -- var.elim.:  2000/24629          
c   -- var.elim.:  3000/24629          
c   -- var.elim.:  4000/24629          
c   -- var.elim.:  5000/24629          
c   -- var.elim.:  6000/24629          
c   -- var.elim.:  7000/24629          
c   -- var.elim.:  8000/24629          
c   -- var.elim.:  9000/24629          
c   -- var.elim.:  10000/24629          
c   -- var.elim.:  11000/24629          
c   -- var.elim.:  12000/24629          
c   -- var.elim.:  13000/24629          
c   -- var.elim.:  14000/24629          
c   -- var.elim.:  15000/24629          
c   -- var.elim.:  16000/24629          
c   -- var.elim.:  17000/24629          
c   -- var.elim.:  18000/24629          
c   -- var.elim.:  19000/24629          
c   -- var.elim.:  20000/24629          
c   -- var.elim.:  21000/24629          
c   -- var.elim.:  22000/24629          
c   -- var.elim.:  23000/24629          
c   -- var.elim.:  24000/24629          
c   -- var.elim.:  24629/24629          
c   -- subsuming                       
c   -- var.elim.:  1000/15125          
c   -- var.elim.:  2000/15125          
c   -- var.elim.:  3000/15125          
c   -- var.elim.:  4000/15125          
c   -- var.elim.:  5000/15125          
c   -- var.elim.:  6000/15125          
c   -- var.elim.:  7000/15125          
c   -- var.elim.:  8000/15125          
c   -- var.elim.:  9000/15125          
c   -- var.elim.:  10000/15125          
c   -- var.elim.:  11000/15125          
c   -- var.elim.:  12000/15125          
c   -- var.elim.:  13000/15125          
c   -- var.elim.:  14000/15125          
c   -- var.elim.:  15000/15125          
c   -- var.elim.:  15125/15125          
c   -- var.elim.:  1000/1172          
c   -- var.elim.:  1172/1172          
c   -- subsuming                       
c   -- var.elim.:  161/161          
c |         0 |   83400   422067 |      --       0       --      -- |     --   | -19261/172289
c |         0 |   83400   422067 |   33360       0        0     nan |  0.000 % |
c |       100 |   83312   421367 |   36657      98      734     7.5 |  0.885 % |
c |       250 |   83005   420066 |   40174     241     1588     6.6 |  1.118 % |
c ==============================================================================
c (current CPU-time: 94.7186 s)
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       386 |   95039   453773 |   28511     376     2738     7.3 |  1.118 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22656          
c   -- var.elim.:  2000/22656          
c   -- var.elim.:  3000/22656          
c   -- var.elim.:  4000/22656          
c   -- var.elim.:  5000/22656          
c   -- var.elim.:  6000/22656          
c   -- var.elim.:  7000/22656          
c   -- var.elim.:  8000/22656          
c   -- var.elim.:  9000/22656          
c   -- var.elim.:  10000/22656          
c   -- var.elim.:  11000/22656          
c   -- var.elim.:  12000/22656          
c   -- var.elim.:  13000/22656          
c   -- var.elim.:  14000/22656          
c   -- var.elim.:  15000/22656          
c   -- var.elim.:  16000/22656          
c   -- var.elim.:  17000/22656          
c   -- var.elim.:  18000/22656          
c   -- var.elim.:  19000/22656          
c   -- var.elim.:  20000/22656          
c   -- var.elim.:  21000/22656          
c   -- var.elim.:  22000/22656          
c   -- var.elim.:  22656/22656          
c   -- var.elim.:  1000/10200          
c   -- var.elim.:  2000/10200          
c   -- var.elim.:  3000/10200          
c   -- var.elim.:  4000/10200          
c   -- var.elim.:  5000/10200          
c   -- var.elim.:  6000/10200          
c   -- var.elim.:  7000/10200          
c   -- var.elim.:  8000/10200          
c   -- var.elim.:  9000/10200          
c   -- var.elim.:  10000/10200          
c   -- var.elim.:  10200/10200          
c   -- subsuming                       
c   -- var.elim.:  1000/8310          
c   -- var.elim.:  2000/8310          
c   -- var.elim.:  3000/8310          
c   -- var.elim.:  4000/8310          
c   -- var.elim.:  5000/8310          
c   -- var.elim.:  6000/8310          
c   -- var.elim.:  7000/8310          
c   -- var.elim.:  8000/8310          
c   -- var.elim.:  8310/8310          
c |       386 |   84946   449081 |      --     376       --      -- |     --   | -10093/-4691
c |       386 |   84946   449081 |   33978     375     2735     7.3 |  1.118 % |
c |       488 |   84946   449081 |   37376     477     4153     8.7 |  1.253 % |
c |       639 |   84946   449081 |   41113     628     5445     8.7 |  1.253 % |
c |       864 |   84863   448796 |   45181     852    11334    13.3 |  1.297 % |
c |      1201 |   84632   447819 |   49563    1187    13355    11.3 |  1.470 % |
c |      1707 |   84456   446842 |   54406    1689    41437    24.5 |  1.635 % |
c |      2470 |   84216   445758 |   59677    2444    49936    20.4 |  1.822 % |
c |      3612 |   84004   444768 |   65480    3582    70379    19.6 |  1.972 % |
c |      5320 |   83996   444740 |   72021    5288    99428    18.8 |  1.976 % |
c |      7883 |   83343   441669 |   78607    7824   148658    19.0 |  2.511 % |
c ==============================================================================
c (current CPU-time: 156.371 s)
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8258 |   84455   444738 |   25336    8199   154051    18.8 |  2.511 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11405          
c   -- var.elim.:  2000/11405          
c   -- var.elim.:  3000/11405          
c   -- var.elim.:  4000/11405          
c   -- var.elim.:  5000/11405          
c   -- var.elim.:  6000/11405          
c   -- var.elim.:  7000/11405          
c   -- var.elim.:  8000/11405          
c   -- var.elim.:  9000/11405          
c   -- var.elim.:  10000/11405          
c   -- var.elim.:  11000/11405          
c   -- var.elim.:  11405/11405          
c   -- var.elim.:  1000/1261          
c   -- var.elim.:  1261/1261          
c   -- subsuming                       
c   -- var.elim.:  817/817          
c |      8258 |   83496   444029 |      --    8199       --      -- |     --   | -959/-708
c |      8258 |   83496   444029 |   33398    8106   151469    18.7 |  2.511 % |
c |      8360 |   83496   444029 |   36738    8208   152119    18.5 |  2.524 % |
c |      8511 |   83496   444029 |   40412    8359   155024    18.5 |  2.524 % |
c |      8736 |   83496   444029 |   44453    8584   160091    18.6 |  2.524 % |
c |      9074 |   83496   444029 |   48898    8922   166746    18.7 |  2.524 % |
c |      9580 |   83496   444029 |   53788    9428   178563    18.9 |  2.524 % |
c |     10339 |   83496   444029 |   59167   10187   191697    18.8 |  2.524 % |
c |     11479 |   83340   443474 |   64962   11323   219718    19.4 |  2.597 % |
c ==============================================================================
c (current CPU-time: 185.36 s)
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13011 |   83972   445229 |   25191   12852   268154    20.9 |  2.597 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1915          
c   -- var.elim.:  1915/1915          
c   -- var.elim.:  605/605          
c   -- var.elim.:  25/25          
c   -- subsuming                       
c   -- var.elim.:  75/75          
c |     13011 |   83452   444727 |      --   12852       --      -- |     --   | -520/-501
c |     13011 |   83452   444727 |   33380   12844   268083    20.9 |  2.597 % |
c |     13111 |   83452   444727 |   36718   12944   269044    20.8 |  2.602 % |
c |     13261 |   83452   444727 |   40390   13094   274469    21.0 |  2.602 % |
c |     13486 |   83358   444231 |   44379   13316   279713    21.0 |  2.668 % |
c |     13823 |   83358   444231 |   48817   13653   285989    20.9 |  2.668 % |
c |     14330 |   83324   443880 |   53677   14159   298128    21.1 |  2.727 % |
c |     15089 |   83128   442521 |   58906   14910   314552    21.1 |  2.940 % |
c ==============================================================================
c (current CPU-time: 192.168 s)
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15573 |   83164   442834 |   24949   15394   345756    22.5 |  2.940 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9481          
c   -- var.elim.:  2000/9481          
c   -- var.elim.:  3000/9481          
c   -- var.elim.:  4000/9481          
c   -- var.elim.:  5000/9481          
c   -- var.elim.:  6000/9481          
c   -- var.elim.:  7000/9481          
c   -- var.elim.:  8000/9481          
c   -- var.elim.:  9000/9481          
c   -- var.elim.:  9481/9481          
c   -- var.elim.:  320/320          
c |     15573 |   83116   443644 |      --   15394       --      -- |     --   | -48/811
c |     15573 |   83116   443644 |   33246   15272   342770    22.4 |  2.940 % |
c |     15676 |   83116   443644 |   36571   15375   344830    22.4 |  2.948 % |
c |     15826 |   83116   443644 |   40228   15525   352524    22.7 |  2.948 % |
c |     16051 |   82987   443013 |   44182   15742   354622    22.5 |  3.055 % |
c |     16390 |   82987   443013 |   48600   16081   357947    22.3 |  3.055 % |
c |     16897 |   82955   442678 |   53439   16586   387078    23.3 |  3.110 % |
c |     17656 |   82955   442678 |   58783   17345   400741    23.1 |  3.110 % |
c |     18795 |   82955   442678 |   64662   18484   482101    26.1 |  3.110 % |
c |     20503 |   82955   442678 |   71128   20192   530573    26.3 |  3.110 % |
c |     23066 |   82789   441903 |   78084   22751   631085    27.7 |  3.242 % |
c |     26912 |   82753   441531 |   85855   26592  1275215    48.0 |  3.308 % |
c ==============================================================================
c (current CPU-time: 237.902 s)
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     28122 |   82865   441473 |   24859   27795  1387318    49.9 |  3.308 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10683          
c   -- var.elim.:  2000/10683          
c   -- var.elim.:  3000/10683          
c   -- var.elim.:  4000/10683          
c   -- var.elim.:  5000/10683          
c   -- var.elim.:  6000/10683          
c   -- var.elim.:  7000/10683          
c   -- var.elim.:  8000/10683          
c   -- var.elim.:  9000/10683          
c   -- var.elim.:  10000/10683          
c   -- var.elim.:  10683/10683          
c   -- var.elim.:  399/399          
c   -- subsuming                       
c |     28122 |   82622   441249 |      --   27795       --      -- |     --   | -243/-223
c |     28122 |   82622   441249 |   33048   27625  1366725    49.5 |  3.308 % |
c |     28222 |   82622   441249 |   36353   27725  1367526    49.3 |  3.484 % |
c |     28372 |   82622   441249 |   39989   27875  1369981    49.1 |  3.484 % |
c |     28597 |   82622   441249 |   43987   28100  1372455    48.8 |  3.484 % |
c |     28934 |   82622   441249 |   48386   28437  1400239    49.2 |  3.484 % |
c |     29441 |   82544   440769 |   53175   28935  1445146    49.9 |  3.565 % |
c |     30201 |   82544   440769 |   58492   29695  1487439    50.1 |  3.565 % |
c |     31340 |   82512   440443 |   64317   30832  1538296    49.9 |  3.620 % |
c |     33048 |   82320   439599 |   70584   32528  1810047    55.6 |  3.785 % |
c |     35610 |   82320   439599 |   77642   35090  1928218    55.0 |  3.785 % |
c ==============================================================================
c (current CPU-time: 281.24 s)
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36296 |   82471   440222 |   24741   35776  2007819    56.1 |  3.785 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7660          
c   -- var.elim.:  2000/7660          
c   -- var.elim.:  3000/7660          
c   -- var.elim.:  4000/7660          
c   -- var.elim.:  5000/7660          
c   -- var.elim.:  6000/7660          
c   -- var.elim.:  7000/7660          
c   -- var.elim.:  7660/7660          
c   -- var.elim.:  421/421          
c   -- subsuming                       
c   -- var.elim.:  18/18          
c |     36296 |   82347   440906 |      --   35776       --      -- |     --   | -124/685
c |     36296 |   82347   440906 |   32938   35258  1987067    56.4 |  3.785 % |
c |     36396 |   82347   440906 |   36232   16367  1302344    79.6 |  3.792 % |
c |     36546 |   82347   440906 |   39855   16517  1303990    78.9 |  3.792 % |
c |     36772 |   82347   440906 |   43841   16743  1313704    78.5 |  3.792 % |
c |     37109 |   82347   440906 |   48225   17080  1317208    77.1 |  3.792 % |
c |     37616 |   82347   440906 |   53048   17587  1349698    76.7 |  3.792 % |
c |     38376 |   82311   440539 |   58327   18346  1360051    74.1 |  3.858 % |
c |     39516 |   82311   440539 |   64160   19486  1441530    74.0 |  3.858 % |
c |     41224 |   82311   440539 |   70576   21194  1482563    70.0 |  3.858 % |
c |     43786 |   82311   440539 |   77634   23756  1552748    65.4 |  3.858 % |
c |     47632 |   82216   440201 |   85298   27601  1733238    62.8 |  3.902 % |
c |     53398 |   82204   440060 |   93815   33365  2443799    73.2 |  3.924 % |
c ==============================================================================
c (current CPU-time: 346.794 s)
c ==============================================================================
c [1mFound solution: 46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     57290 |   82681   441393 |   24804   37257  2746097    73.7 |  3.924 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7745          
c   -- var.elim.:  2000/7745          
c   -- var.elim.:  3000/7745          
c   -- var.elim.:  4000/7745          
c   -- var.elim.:  5000/7745          
c   -- var.elim.:  6000/7745          
c   -- var.elim.:  7000/7745          
c   -- var.elim.:  7745/7745          
c   -- var.elim.:  473/473          
c   -- subsuming                       
c   -- var.elim.:  35/35          
c |     57290 |   82300   441120 |      --   37257       --      -- |     --   | -381/-272
c |     57290 |   82300   441120 |   32920   37253  2746074    73.7 |  3.924 % |
c |     57390 |   82300   441120 |   36212   17234  1136448    65.9 |  3.944 % |
c |     57540 |   82300   441120 |   39833   17384  1152841    66.3 |  3.944 % |
c |     57765 |   82300   441120 |   43816   17609  1156561    65.7 |  3.944 % |
c |     58103 |   82300   441120 |   48198   17947  1165095    64.9 |  3.944 % |
c |     58609 |   82300   441120 |   53017   18453  1174658    63.7 |  3.944 % |
c |     59368 |   82300   441120 |   58319   19212  1197033    62.3 |  3.944 % |
c |     60507 |   82282   440923 |   64137   20349  1270169    62.4 |  3.977 % |
c |     62215 |   82142   440159 |   70431   22051  1345881    61.0 |  4.105 % |
c |     64778 |   82045   439235 |   77383   24594  1453944    59.1 |  4.255 % |
c |     68624 |   82045   439235 |   85121   28440  1607536    56.5 |  4.255 % |
c |     74392 |   81923   438344 |   93494   34202  2511803    73.4 |  4.420 % |
c |     83043 |   81830   437953 |  102727   42839  4424804   103.3 |  4.479 % |
c |     96018 |   81830   437953 |  112999   55814  6047268   108.3 |  4.479 % |
c ==============================================================================
c (current CPU-time: 531.474 s)
c ==============================================================================
c [1mFound solution: 41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    109620 |   81978   438564 |   24593   69407  7498389   108.0 |  4.479 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8943          
c   -- var.elim.:  2000/8943          
c   -- var.elim.:  3000/8943          
c   -- var.elim.:  4000/8943          
c   -- var.elim.:  5000/8943          
c   -- var.elim.:  6000/8943          
c   -- var.elim.:  7000/8943          
c   -- var.elim.:  8000/8943          
c   -- var.elim.:  8943/8943          
c   -- var.elim.:  431/431          
c   -- subsuming                       
c   -- var.elim.:  742/742          
c |    109620 |   81858   439300 |      --   69407       --      -- |     --   | -120/737
c |    109620 |   81858   439300 |   32743   68497  6946562   101.4 |  4.479 % |
c |    109722 |   81858   439300 |   36017   19629  1123367    57.2 |  4.494 % |
c |    109872 |   81858   439300 |   39619   19779  1125176    56.9 |  4.494 % |
c |    110097 |   81858   439300 |   43581   20004  1131292    56.6 |  4.494 % |
c |    110435 |   81858   439300 |   47939   20342  1136969    55.9 |  4.494 % |
c |    110941 |   81858   439300 |   52733   20848  1189212    57.0 |  4.494 % |
c |    111700 |   81858   439300 |   58006   21607  1242495    57.5 |  4.494 % |
c |    112840 |   81858   439300 |   63807   22747  1329189    58.4 |  4.494 % |
c |    114549 |   81858   439300 |   70187   24456  1460330    59.7 |  4.494 % |
c |    117111 |   81858   439300 |   77206   27018  1573030    58.2 |  4.494 % |
c |    120956 |   81858   439300 |   84927   30863  2387609    77.4 |  4.494 % |
c |    126722 |   81856   439268 |   93417   36628  2593169    70.8 |  4.497 % |
c |    135371 |   81854   439247 |  102757   45276  6126307   135.3 |  4.501 % |
c |    148347 |   81854   439247 |  113032   58252 10102368   173.4 |  4.501 % |
c ==============================================================================
c (current CPU-time: 734.766 s)
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    161853 |   81884   439537 |   24565   71758 14656697   204.3 |  4.501 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1496          
c   -- var.elim.:  1496/1496          
c   -- var.elim.:  240/240          
c |    161853 |   81870   440424 |      --   71758       --      -- |     --   | -14/888
c |    161853 |   81870   440424 |   32748   71758 14656697   204.3 |  4.501 % |
c |    161953 |   81870   440424 |   36022   17554  4495811   256.1 |  4.504 % |
c |    162105 |   81870   440424 |   39625   17706  4498317   254.1 |  4.504 % |
c |    162330 |   81870   440424 |   43587   17931  4521853   252.2 |  4.504 % |
c |    162669 |   81870   440424 |   47946   18270  4527565   247.8 |  4.504 % |
c |    163175 |   81868   440400 |   52739   18775  4539035   241.8 |  4.508 % |
c |    163935 |   81868   440400 |   58013   19535  4571141   234.0 |  4.508 % |
c |    165075 |   81868   440400 |   63815   20675  4626983   223.8 |  4.508 % |
c |    166784 |   81856   440309 |   70186   22383  4727460   211.2 |  4.530 % |
c |    169346 |   81856   440309 |   77204   24945  4876408   195.5 |  4.530 % |
c |    173190 |   81856   440309 |   84925   28789  5101725   177.2 |  4.530 % |
c |    178956 |   81856   440309 |   93417   34555  5392547   156.1 |  4.530 % |
c |    187605 |   81856   440309 |  102759   43204  8555358   198.0 |  4.530 % |
c |    200580 |   81856   440309 |  113035   56179 10208615   181.7 |  4.530 % |
c |    220042 |   81856   440309 |  124339   75641 12082374   159.7 |  4.530 % |
c |    249236 |   81856   440309 |  136773  104835 22768202   217.2 |  4.530 % |
c ==============================================================================
c (current CPU-time: 1132.06 s)
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    273555 |   81850   439910 |   24554  129144 27511284   213.0 |  4.530 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6499          
c   -- var.elim.:  2000/6499          
c   -- var.elim.:  3000/6499          
c   -- var.elim.:  4000/6499          
c   -- var.elim.:  5000/6499          
c   -- var.elim.:  6000/6499          
c   -- var.elim.:  6499/6499          
c   -- var.elim.:  221/221          
c   -- var.elim.:  34/34          
c |    273555 |   81711   439664 |      --  129144       --      -- |     --   | -139/-245
c |    273555 |   81711   439664 |   32684  128832 27112157   210.4 |  4.530 % |
c |    273657 |   81711   439664 |   35952   22334  3273446   146.6 |  4.662 % |
c |    273807 |   81711   439664 |   39548   22484  3283523   146.0 |  4.662 % |
c |    274032 |   81711   439664 |   43502   22709  3286745   144.7 |  4.662 % |
c |    274369 |   81711   439664 |   47853   23046  3295691   143.0 |  4.662 % |
c |    274875 |   81711   439664 |   52638   23552  3305699   140.4 |  4.662 % |
c |    275635 |   81711   439664 |   57902   24312  3362618   138.3 |  4.662 % |
c |    276774 |   81711   439664 |   63692   25451  3400588   133.6 |  4.662 % |
c |    278482 |   81711   439664 |   70061   27159  3505241   129.1 |  4.662 % |
c |    281048 |   81711   439664 |   77068   29725  3635511   122.3 |  4.662 % |
c |    284892 |   81681   439298 |   84743   33567  3732731   111.2 |  4.717 % |
c |    290658 |   81681   439298 |   93218   39333  4491233   114.2 |  4.717 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v756 -v693 -v588 -v262 -v241 v56 v38 v692 -v590 -v486 -v263 -v246 -v55 v37 -v757 -v700 v589 -v485 -v439 -v266 v245 -v54 v39 -v758 -v694 -v594 -v487 v444 -v264 -v52 v40 -v761 -v695 -v612 -v593 -v488 v443 -v265 v248 -v53 v47 -v759 -v696 v611 -v591 v489 -v401 -v249 -v41 -v2 -v760 v613 -v592 -v496 v446 -v421 v400 -v252 -v198 -v171 -v42 -v1 -v734 v616 v490 v447 -v420 -v406 -v385 -v250 -v176 -v43 -v3 -v733 v615 -v491 v450 v422 -v405 v384 -v273 -v251 -v197 -v175 -v137 -v4 v620 -v492 -v448 -v425 -v407 v386 -v366 -v278 -v201 -v155 -v136 -v18 v5 -v735 v619 -v559 -v510 -v449 v424 -v411 v387 -v365 -v277 -v178 -v154 -v138 -v87 -v17 -v12 -v737 -v650 v617 -v515 -v429 -v410 v388 -v202 -v179 -v156 -v141 -v86 -v23 v6 -v649 v618 -v558 -v514 -v466 -v428 -v408 v395 -v367 -v280 -v182 -v157 -v140 -v88 -v66 -v22 v7 -v738 -v562 -v426 -v409 -v389 -v369 -v281 -v180 v158 -v145 -v91 -v71 v24 v8 -v740 -v651 v517 -v469 -v427 -v390 -v318 -v284 -v223 -v181 -v165 -v14#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.95 0.90 2/54 6186
Raw data (stat): 6186 (runsolver) R 6185 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422383120 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0015 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7780 0 0 0 969 29 0 0 25 0 1 0 422383120 33783808 7325 4294967295 134512640 134672761 3221224544 3221222992 134643493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8248 7325 603 41 0 8207 0
vsize: 32992
[startup+20.002 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7856 0 0 0 1963 34 0 0 25 0 1 0 422383120 34058240 7401 4294967295 134512640 134672761 3221224544 3221222720 134604069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 7401 603 41 0 8274 0
vsize: 33260
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.95 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7899 0 0 0 2958 38 0 0 25 0 1 0 422383120 34082816 7397 4294967295 134512640 134672761 3221224544 3221222992 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8321 7397 603 41 0 8280 0
vsize: 33284
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7899 0 0 0 3958 39 0 0 25 0 1 0 422383120 34082816 7397 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8321 7397 603 41 0 8280 0
vsize: 33284
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7899 0 0 0 4957 39 0 0 25 0 1 0 422383120 33820672 7350 4294967295 134512640 134672761 3221224544 3221223008 134644243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8257 7350 603 41 0 8216 0
vsize: 33028
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7899 0 0 0 5958 39 0 0 25 0 1 0 422383120 33820672 7350 4294967295 134512640 134672761 3221224544 3221222768 134621179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8257 7350 603 41 0 8216 0
vsize: 33028
[startup+70.003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 7899 0 0 0 6958 39 0 0 25 0 1 0 422383120 33820672 7350 4294967295 134512640 134672761 3221224544 3221223088 134621122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8257 7350 603 41 0 8216 0
vsize: 33028
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 8000 0 0 0 7958 39 0 0 25 0 1 0 422383120 34426880 7451 4294967295 134512640 134672761 3221224544 3221223088 134621081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8405 7451 603 41 0 8364 0
vsize: 33620
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 8020 0 0 0 8958 39 0 0 25 0 1 0 422383120 34017280 7370 4294967295 134512640 134672761 3221224544 3221222992 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8305 7370 603 41 0 8264 0
vsize: 33220
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10343 0 0 0 9931 66 0 0 25 0 1 0 422383120 35299328 7921 4294967295 134512640 134672761 3221224544 3221222864 134565212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8618 7921 603 41 0 8577 0
vsize: 34472
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10358 0 0 0 10875 83 0 0 25 0 1 0 422383120 35299328 7936 4294967295 134512640 134672761 3221224544 3221222992 134643483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8618 7936 603 41 0 8577 0
vsize: 34472
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10358 0 0 0 11874 83 0 0 25 0 1 0 422383120 35299328 7936 4294967295 134512640 134672761 3221224544 3221222992 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8618 7936 603 41 0 8577 0
vsize: 34472
[startup+130.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10560 0 0 0 12874 84 0 0 25 0 1 0 422383120 36159488 8138 4294967295 134512640 134672761 3221224544 3221222944 134605673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8828 8138 603 41 0 8787 0
vsize: 35312
[startup+140.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10560 0 0 0 13874 84 0 0 25 0 1 0 422383120 35299328 7936 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8618 7936 603 41 0 8577 0
vsize: 34472
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 10560 0 0 0 14874 84 0 0 25 0 1 0 422383120 35299328 7936 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8618 7936 603 41 0 8577 0
vsize: 34472
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 12825 0 0 0 15861 97 0 0 25 0 1 0 422383120 37167104 8257 4294967295 134512640 134672761 3221224544 3221223088 134621122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9074 8257 603 41 0 9033 0
vsize: 36296
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 12825 0 0 0 16860 97 0 0 25 0 1 0 422383120 35717120 8055 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8720 8055 603 41 0 8679 0
vsize: 34880
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 13049 0 0 0 17859 98 0 0 25 0 1 0 422383120 35717120 8055 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8720 8055 603 41 0 8679 0
vsize: 34880
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 15649 0 0 0 18843 115 0 0 25 0 1 0 422383120 36077568 8155 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8808 8155 603 41 0 8767 0
vsize: 35232
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 18051 0 0 0 19826 132 0 0 25 0 1 0 422383120 37941248 8450 4294967295 134512640 134672761 3221224544 3221223088 134621068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9263 8450 603 41 0 9222 0
vsize: 37052
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 18062 0 0 0 20826 132 0 0 25 0 1 0 422383120 36610048 8259 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8938 8259 603 41 0 8897 0
vsize: 35752
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 18080 0 0 0 21826 132 0 0 25 0 1 0 422383120 36679680 8267 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8955 8267 603 41 0 8914 0
vsize: 35820
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 18333 0 0 0 22825 133 0 0 25 0 1 0 422383120 37605376 8520 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9181 8520 603 41 0 9140 0
vsize: 36724
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 20810 0 0 0 23817 141 0 0 25 0 1 0 422383120 48373760 10997 4294967295 134512640 134672761 3221224544 3221222752 1075346529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11810 10997 603 41 0 11769 0
vsize: 47240
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 21489 0 0 0 24808 150 0 0 25 0 1 0 422383120 40955904 9334 4294967295 134512640 134672761 3221224544 3221222992 134643948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9999 9334 603 41 0 9958 0
vsize: 39996
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 21489 0 0 0 25807 150 0 0 25 0 1 0 422383120 40955904 9334 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9999 9334 603 41 0 9958 0
vsize: 39996
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 21892 0 0 0 26805 152 0 0 25 0 1 0 422383120 41480192 9479 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10127 9479 603 41 0 10086 0
vsize: 40508
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 22267 0 0 0 27804 153 0 0 25 0 1 0 422383120 43192320 9854 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10545 9854 603 41 0 10504 0
vsize: 42180
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 24830 0 0 0 28788 168 0 0 25 0 1 0 422383120 43737088 10013 4294967295 134512640 134672761 3221224544 3221222992 134643688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 10013 603 41 0 10637 0
vsize: 42712
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 24830 0 0 0 29788 168 0 0 25 0 1 0 422383120 43737088 10013 4294967295 134512640 134672761 3221224544 3221222992 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10678 10013 603 41 0 10637 0
vsize: 42712
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 25065 0 0 0 30788 169 0 0 25 0 1 0 422383120 43732992 10012 4294967295 134512640 134672761 3221224544 3221223696 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10677 10012 603 41 0 10636 0
vsize: 42708
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 25065 0 0 0 31788 169 0 0 25 0 1 0 422383120 43732992 10012 4294967295 134512640 134672761 3221224544 3221223584 134612821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10677 10012 603 41 0 10636 0
vsize: 42708
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 25065 0 0 0 32788 169 0 0 25 0 1 0 422383120 43732992 10012 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10677 10012 603 41 0 10636 0
vsize: 42708
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 25601 0 0 0 33786 171 0 0 25 0 1 0 422383120 45953024 10548 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11219 10548 603 41 0 11178 0
vsize: 44876
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28144 0 0 0 34770 188 0 0 25 0 1 0 422383120 47300608 10889 4294967295 134512640 134672761 3221224544 3221217812 134605085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11548 10889 603 41 0 11507 0
vsize: 46192
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28353 0 0 0 35769 188 0 0 25 0 1 0 422383120 47304704 10892 4294967295 134512640 134672761 3221224544 3221222992 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11549 10892 603 41 0 11508 0
vsize: 46196
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 36768 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 37768 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 38769 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 39769 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 40769 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28646 0 0 0 41768 189 0 0 25 0 1 0 422383120 47337472 10900 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11557 10900 603 41 0 11516 0
vsize: 46228
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 28911 0 0 0 42767 190 0 0 25 0 1 0 422383120 48517120 11165 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11845 11165 603 41 0 11804 0
vsize: 47380
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 29567 0 0 0 43765 192 0 0 25 0 1 0 422383120 51150848 11821 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12488 11821 603 41 0 12447 0
vsize: 49952
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 30294 0 0 0 44764 194 0 0 25 0 1 0 422383120 54063104 12548 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13199 12548 603 41 0 13158 0
vsize: 52796
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 30869 0 0 0 45763 195 0 0 25 0 1 0 422383120 56430592 13123 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13777 13123 603 41 0 13736 0
vsize: 55108
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 31288 0 0 0 46762 196 0 0 25 0 1 0 422383120 58150912 13542 4294967295 134512640 134672761 3221224544 3221223744 134610511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13542 603 41 0 14156 0
vsize: 56788
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 31621 0 0 0 47761 198 0 0 25 0 1 0 422383120 59478016 13875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14521 13875 603 41 0 14480 0
vsize: 58084
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 32148 0 0 0 48759 200 0 0 25 0 1 0 422383120 61722624 14402 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15069 14402 603 41 0 15028 0
vsize: 60276
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 32432 0 0 0 49758 201 0 0 25 0 1 0 422383120 62779392 14686 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15327 14686 603 41 0 15286 0
vsize: 61308
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 32939 0 0 0 50758 201 0 0 25 0 1 0 422383120 64897024 15193 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15844 15193 603 41 0 15803 0
vsize: 63376
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 33196 0 0 0 51757 202 0 0 25 0 1 0 422383120 66215936 15450 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16166 15450 603 41 0 16125 0
vsize: 64664
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 33620 0 0 0 52755 204 0 0 25 0 1 0 422383120 67923968 15874 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16583 15874 603 41 0 16542 0
vsize: 66332
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36161 0 0 0 53742 217 0 0 25 0 1 0 422383120 69967872 16229 4294967295 134512640 134672761 3221224544 3221223088 134621122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17082 16229 603 41 0 17041 0
vsize: 68328
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36170 0 0 0 54742 218 0 0 25 0 1 0 422383120 68472832 16005 4294967295 134512640 134672761 3221224544 3221222992 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 16005 603 41 0 16676 0
vsize: 66868
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 55741 218 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 56741 218 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 57741 218 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 58740 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 59740 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 60740 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 61741 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 62741 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 63741 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223680 134614721 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 64741 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 36493 0 0 0 65741 219 0 0 25 0 1 0 422383120 68648960 16060 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16760 16060 603 41 0 16719 0
vsize: 67040
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 37614 0 0 0 66739 222 0 0 25 0 1 0 422383120 73322496 17181 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17901 17181 603 41 0 17860 0
vsize: 71604
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 38460 0 0 0 67737 223 0 0 25 0 1 0 422383120 76746752 18027 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18737 18027 603 41 0 18696 0
vsize: 74948
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 39223 0 0 0 68734 226 0 0 25 0 1 0 422383120 79892480 18790 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19505 18791 603 41 0 19464 0
vsize: 78020
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 39519 0 0 0 69734 226 0 0 25 0 1 0 422383120 81068032 19086 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19792 19086 603 41 0 19751 0
vsize: 79168
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 40341 0 0 0 70733 228 0 0 25 0 1 0 422383120 84500480 19908 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20630 19908 603 41 0 20589 0
vsize: 82520
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 41507 0 0 0 71730 231 0 0 25 0 1 0 422383120 89288704 21074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21799 21074 603 41 0 21758 0
vsize: 87196
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 42903 0 0 0 72728 234 0 0 25 0 1 0 422383120 95006720 22470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23195 22470 603 41 0 23154 0
vsize: 92780
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46005 0 0 0 73709 252 0 0 25 0 1 0 422383120 98013184 23232 4294967295 134512640 134672761 3221224544 3221222992 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23929 23232 603 41 0 23888 0
vsize: 95716
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 74709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 75708 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 76708 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 77708 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 78709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 79709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 80709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 81709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 82709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 83709 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 84710 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 85710 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 86710 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 87710 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 88711 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46115 0 0 0 89711 252 0 0 25 0 1 0 422383120 98021376 23239 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23239 603 41 0 23890 0
vsize: 95724
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46117 0 0 0 90711 252 0 0 25 0 1 0 422383120 98021376 23241 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23241 603 41 0 23890 0
vsize: 95724
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46120 0 0 0 91711 252 0 0 25 0 1 0 422383120 98021376 23244 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23244 603 41 0 23890 0
vsize: 95724
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46122 0 0 0 92711 252 0 0 25 0 1 0 422383120 98021376 23246 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23246 603 41 0 23890 0
vsize: 95724
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46124 0 0 0 93712 252 0 0 25 0 1 0 422383120 98021376 23248 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23931 23248 603 41 0 23890 0
vsize: 95724
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46551 0 0 0 94711 253 0 0 25 0 1 0 422383120 99803136 23675 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24366 23675 603 41 0 24325 0
vsize: 97464
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 46965 0 0 0 95710 255 0 0 25 0 1 0 422383120 101519360 24089 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 24089 603 41 0 24744 0
vsize: 99140
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 47802 0 0 0 96708 257 0 0 25 0 1 0 422383120 104939520 24926 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25620 24926 603 41 0 25579 0
vsize: 102480
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 48716 0 0 0 97706 259 0 0 25 0 1 0 422383120 108613632 25840 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26517 25840 603 41 0 26476 0
vsize: 106068
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 50106 0 0 0 98703 262 0 0 25 0 1 0 422383120 114364416 27230 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27921 27230 603 41 0 27880 0
vsize: 111684
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 51347 0 0 0 99700 265 0 0 25 0 1 0 422383120 119390208 28471 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29148 28471 603 41 0 29107 0
vsize: 116592
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 52205 0 0 0 100698 268 0 0 25 0 1 0 422383120 122949632 29329 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30017 29329 603 41 0 29976 0
vsize: 120068
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 53057 0 0 0 101696 270 0 0 25 0 1 0 422383120 126414848 30181 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30863 30181 603 41 0 30822 0
vsize: 123452
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 54090 0 0 0 102693 272 0 0 25 0 1 0 422383120 130609152 31214 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31887 31214 603 41 0 31846 0
vsize: 127548
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 54565 0 0 0 103693 273 0 0 25 0 1 0 422383120 132591616 31689 4294967295 134512640 134672761 3221224544 3221223720 134615850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32371 31689 603 41 0 32330 0
vsize: 129484
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 55151 0 0 0 104692 274 0 0 25 0 1 0 422383120 134963200 32275 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32950 32275 603 41 0 32909 0
vsize: 131800
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 55610 0 0 0 105691 275 0 0 25 0 1 0 422383120 136806400 32734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33400 32734 603 41 0 33359 0
vsize: 133600
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 56033 0 0 0 106690 276 0 0 25 0 1 0 422383120 138526720 33157 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33820 33157 603 41 0 33779 0
vsize: 135280
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 56280 0 0 0 107690 277 0 0 25 0 1 0 422383120 139579392 33404 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34077 33404 603 41 0 34036 0
vsize: 136308
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 56665 0 0 0 108689 278 0 0 25 0 1 0 422383120 141139968 33789 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34458 33789 603 41 0 34417 0
vsize: 137832
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 56996 0 0 0 109689 278 0 0 25 0 1 0 422383120 142450688 34120 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34778 34120 603 41 0 34737 0
vsize: 139112
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 57313 0 0 0 110688 279 0 0 25 0 1 0 422383120 143761408 34437 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35098 34437 603 41 0 35057 0
vsize: 140392
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 58226 0 0 0 111686 282 0 0 25 0 1 0 422383120 147447808 35350 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35998 35350 603 41 0 35957 0
vsize: 143992
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 59111 0 0 0 112684 284 0 0 25 0 1 0 422383120 151093248 36235 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36888 36235 603 41 0 36847 0
vsize: 147552
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 61941 0 0 0 113667 301 0 0 25 0 1 0 422383120 152817664 36680 4294967295 134512640 134672761 3221224544 3221222992 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37309 36680 603 41 0 37268 0
vsize: 149236
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 61941 0 0 0 114667 301 0 0 25 0 1 0 422383120 152817664 36680 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37309 36680 603 41 0 37268 0
vsize: 149236
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 115667 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 116667 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 117666 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 118666 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 119667 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6186
Raw data (stat): 6186 (minisat+) R 6185 32461 32460 0 -1 0 62118 0 0 0 120667 301 0 0 25 0 1 0 422383120 153079808 36731 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37373 36731 603 41 0 37332 0
vsize: 149492
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 6186
Raw data (stat): 6186 (minisat+) Z 6185 32461 32460 0 -1 12 62119 0 0 0 120667 311 0 0 25 0 1 0 422383120 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: 10
Real time (s): 1210.13
CPU time (s): 1209.79
CPU user time (s): 1206.68
CPU system time (s): 3.11453
CPU usage (%): 99.9721
Max. virtual memory (Kb): 149492
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####