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:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5668

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        888608 kB
Buffers:         35440 kB
Cached:          73764 kB
SwapCached:          4 kB
Active:          52552 kB
Inactive:        60448 kB
HighTotal:      131008 kB
HighFree:        52640 kB
LowTotal:       903652 kB
LowFree:        835968 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27464 kB
Committed_AS:    63516 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:42:28 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4126 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4084    11649 |    1225       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1919          
c   -- var.elim.:  1919/1919          
c   -- var.elim.:  942/942          
c   -- subsuming                       
c   -- var.elim.:  873/873          
c   -- var.elim.:  479/479          
c   -- subsuming                       
c |         0 |    3026    11001 |      --       0       --      -- |     --   | -1058/-423
c |         0 |    3026    11001 |    1210       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.209968 s)
c ==============================================================================
c [1mFound solution: 343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20800     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   38676    94407 |   11602       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17481          
c   -- var.elim.:  2000/17481          
c   -- var.elim.:  3000/17481          
c   -- var.elim.:  4000/17481          
c   -- var.elim.:  5000/17481          
c   -- var.elim.:  6000/17481          
c   -- var.elim.:  7000/17481          
c   -- var.elim.:  8000/17481          
c   -- var.elim.:  9000/17481          
c   -- var.elim.:  10000/17481          
c   -- var.elim.:  11000/17481          
c   -- var.elim.:  12000/17481          
c   -- var.elim.:  13000/17481          
c   -- var.elim.:  14000/17481          
c   -- var.elim.:  15000/17481          
c   -- var.elim.:  16000/17481          
c   -- var.elim.:  17000/17481          
c   -- var.elim.:  17481/17481          
c   -- var.elim.:  1000/9142          
c   -- var.elim.:  2000/9142          
c   -- var.elim.:  3000/9142          
c   -- var.elim.:  4000/9142          
c   -- var.elim.:  5000/9142          
c   -- var.elim.:  6000/9142          
c   -- var.elim.:  7000/9142          
c   -- var.elim.:  8000/9142          
c   -- var.elim.:  9000/9142          
c   -- var.elim.:  9142/9142          
c   -- subsuming                       
c   -- var.elim.:  1000/5523          
c   -- var.elim.:  2000/5523          
c   -- var.elim.:  3000/5523          
c   -- var.elim.:  4000/5523          
c   -- var.elim.:  5000/5523          
c   -- var.elim.:  5523/5523          
c   -- var.elim.:  594/594          
c   -- subsuming                       
c   -- var.elim.:  114/114          
c |         0 |   31672   144168 |      --       0       --      -- |     --   | -7004/49762
c |         0 |   31672   144168 |   12668       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 15.3337 s)
c ==============================================================================
c [1mFound solution: 100[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 |        37 |   38023   161120 |   11406      30      336    11.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11633          
c   -- var.elim.:  2000/11633          
c   -- var.elim.:  3000/11633          
c   -- var.elim.:  4000/11633          
c   -- var.elim.:  5000/11633          
c   -- var.elim.:  6000/11633          
c   -- var.elim.:  7000/11633          
c   -- var.elim.:  8000/11633          
c   -- var.elim.:  9000/11633          
c   -- var.elim.:  10000/11633          
c   -- var.elim.:  11000/11633          
c   -- var.elim.:  11633/11633          
c   -- var.elim.:  1000/5681          
c   -- var.elim.:  2000/5681          
c   -- var.elim.:  3000/5681          
c   -- var.elim.:  4000/5681          
c   -- var.elim.:  5000/5681          
c   -- var.elim.:  5681/5681          
c   -- var.elim.:  10/10          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  1000/4667          
c   -- var.elim.:  2000/4667          
c   -- var.elim.:  3000/4667          
c   -- var.elim.:  4000/4667          
c   -- var.elim.:  4667/4667          
c   -- var.elim.:  8/8          
c |        37 |   32221   156512 |      --      30       --      -- |     --   | -5800/-4603
c |        37 |   32221   156512 |   12888      30      336    11.2 |  0.000 % |
c |       137 |   32221   156512 |   14177     130     1264     9.7 |  1.647 % |
c ==============================================================================
c (current CPU-time: 28.5007 s)
c ==============================================================================
c [1mFound solution: 61[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 |       173 |   33915   161409 |   10174     166     1570     9.5 |  1.647 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3067          
c   -- var.elim.:  2000/3067          
c   -- var.elim.:  3000/3067          
c   -- var.elim.:  3067/3067          
c   -- var.elim.:  1000/1619          
c   -- var.elim.:  1619/1619          
c   -- subsuming                       
c   -- var.elim.:  1000/1413          
c   -- var.elim.:  1413/1413          
c   -- var.elim.:  8/8          
c |       173 |   32497   161051 |      --     166       --      -- |     --   | -1418/-357
c |       173 |   32497   161051 |   12998     166     1570     9.5 |  1.647 % |
c ==============================================================================
c (current CPU-time: 31.3972 s)
c ==============================================================================
c [1mFound solution: 47[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 |       253 |   33282   163272 |    9984     245     7144    29.2 |  1.647 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3631          
c   -- var.elim.:  2000/3631          
c   -- var.elim.:  3000/3631          
c   -- var.elim.:  3631/3631          
c   -- var.elim.:  856/856          
c   -- var.elim.:  19/19          
c |       253 |   32595   163214 |      --     245       --      -- |     --   | -685/-53
c |       253 |   32595   163214 |   13038     245     7144    29.2 |  1.647 % |
c |       353 |   32595   163214 |   14341     345     8173    23.7 |  1.756 % |
c |       503 |   32463   162586 |   15712     493    14107    28.6 |  2.053 % |
c |       728 |   32463   162586 |   17283     718    39224    54.6 |  2.053 % |
c |      1065 |   32463   162586 |   19011    1055    47730    45.2 |  2.053 % |
c ==============================================================================
c (current CPU-time: 36.1865 s)
c ==============================================================================
c [1mFound solution: 43[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 |      1110 |   32659   163225 |    9797    1100    48162    43.8 |  2.053 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2665          
c   -- var.elim.:  2000/2665          
c   -- var.elim.:  2665/2665          
c   -- var.elim.:  336/336          
c   -- var.elim.:  18/18          
c |      1110 |   32511   163894 |      --    1100       --      -- |     --   | -147/672
c |      1110 |   32511   163894 |   13004    1087    47857    44.0 |  2.053 % |
c |      1210 |   32511   163894 |   14304    1187    53084    44.7 |  2.072 % |
c |      1360 |   32511   163894 |   15735    1337    54560    40.8 |  2.072 % |
c |      1585 |   32511   163894 |   17308    1562    84633    54.2 |  2.072 % |
c |      1922 |   32425   163447 |   18989    1895    98677    52.1 |  2.254 % |
c |      2429 |   32425   163447 |   20888    2402   118235    49.2 |  2.254 % |
c ==============================================================================
c (current CPU-time: 39.522 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 |      2499 |   32877   164747 |    9863    2472   119627    48.4 |  2.254 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2187          
c   -- var.elim.:  2000/2187          
c   -- var.elim.:  2187/2187          
c   -- var.elim.:  483/483          
c   -- var.elim.:  30/30          
c |      2499 |   32491   164217 |      --    2472       --      -- |     --   | -386/-529
c |      2499 |   32491   164217 |   12996    2472   119627    48.4 |  2.254 % |
c |      2600 |   32491   164217 |   14296    2573   136009    52.9 |  2.261 % |
c |      2750 |   32332   163298 |   15648    2717   141695    52.2 |  2.644 % |
c |      2977 |   32310   163069 |   17201    2943   153487    52.2 |  2.750 % |
c |      3314 |   32310   163069 |   18922    3280   157062    47.9 |  2.750 % |
c |      3820 |   32310   163069 |   20814    3786   203178    53.7 |  2.750 % |
c ==============================================================================
c (current CPU-time: 43.5064 s)
c ==============================================================================
c [1mFound solution: 33[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 |      4548 |   33092   165240 |    9927    4511   265580    58.9 |  2.750 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3937          
c   -- var.elim.:  2000/3937          
c   -- var.elim.:  3000/3937          
c   -- var.elim.:  3937/3937          
c   -- var.elim.:  953/953          
c   -- subsuming                       
c   -- var.elim.:  662/662          
c |      4548 |   32329   165452 |      --    4511       --      -- |     --   | -763/213
c |      4548 |   32329   165452 |   12931    4407   240891    54.7 |  2.750 % |
c |      4649 |   32329   165452 |   14224    4508   243288    54.0 |  2.942 % |
c |      4799 |   32329   165452 |   15647    4658   246123    52.8 |  2.942 % |
c |      5024 |   32329   165452 |   17211    4883   252615    51.7 |  2.942 % |
c |      5362 |   32312   165398 |   18923    5219   275196    52.7 |  2.961 % |
c |      5871 |   32312   165398 |   20815    5728   302744    52.9 |  2.961 % |
c ==============================================================================
c (current CPU-time: 49.8074 s)
c ==============================================================================
c [1mFound solution: 29[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 |      6226 |   32637   166418 |    9791    6083   320415    52.7 |  2.961 % |
c   -- subsuming                       
c   -- var.elim.:  708/708          
c   -- var.elim.:  419/419          
c |      6226 |   32355   166783 |      --    6083       --      -- |     --   | -282/366
c |      6226 |   32355   166783 |   12942    6020   304715    50.6 |  2.961 % |
c |      6327 |   32264   166212 |   14196    6120   305592    49.9 |  3.179 % |
c |      6477 |   32264   166212 |   15615    6270   312492    49.8 |  3.179 % |
c |      6704 |   32264   166212 |   17177    6497   337678    52.0 |  3.179 % |
c |      7041 |   32264   166212 |   18895    6834   378597    55.4 |  3.179 % |
c |      7547 |   32211   165980 |   20750    7335   390322    53.2 |  3.256 % |
c |      8308 |   32146   165612 |   22779    8091   410212    50.7 |  3.438 % |
c |      9447 |   32146   165612 |   25057    9230   476164    51.6 |  3.438 % |
c ==============================================================================
c (current CPU-time: 55.9795 s)
c ==============================================================================
c [1mFound solution: 24[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 |      9887 |   32432   166435 |    9729    9670   493004    51.0 |  3.438 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3546          
c   -- var.elim.:  2000/3546          
c   -- var.elim.:  3000/3546          
c   -- var.elim.:  3546/3546          
c   -- var.elim.:  359/359          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  213/213          
c |      9887 |   32153   165931 |      --    9670       --      -- |     --   | -279/-503
c |      9887 |   32153   165931 |   12861    9543   474522    49.7 |  3.438 % |
c |      9990 |   32153   165931 |   14147    9646   477631    49.5 |  3.478 % |
c |     10141 |   32153   165931 |   15562    9797   484381    49.4 |  3.478 % |
c |     10366 |   32153   165931 |   17118   10022   502117    50.1 |  3.478 % |
c |     10705 |   32153   165931 |   18830   10361   507676    49.0 |  3.478 % |
c |     11211 |   32153   165931 |   20713   10867   570119    52.5 |  3.478 % |
c |     11972 |   32153   165931 |   22784   11628   653385    56.2 |  3.478 % |
c |     13111 |   32110   165728 |   25029   12760   764017    59.9 |  3.545 % |
c |     14820 |   32110   165728 |   27532   14469   849513    58.7 |  3.545 % |
c ==============================================================================
c (current CPU-time: 68.1186 s)
c ==============================================================================
c [1mFound solution: 21[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 |     15495 |   32256   166217 |    9676   15144   971047    64.1 |  3.545 % |
c   -- subsuming                       
c   -- var.elim.:  597/597          
c   -- var.elim.:  237/237          
c |     15495 |   32149   166949 |      --   15144       --      -- |     --   | -107/733
c |     15495 |   32149   166949 |   12859   14920   919336    61.6 |  3.545 % |
c |     15595 |   32149   166949 |   14145   10047   623851    62.1 |  3.553 % |
c |     15745 |   32149   166949 |   15560   10197   625462    61.3 |  3.553 % |
c |     15971 |   32149   166949 |   17116   10423   642120    61.6 |  3.553 % |
c |     16308 |   32149   166949 |   18827   10760   660324    61.4 |  3.553 % |
c |     16816 |   32149   166949 |   20710   11268   708595    62.9 |  3.553 % |
c |     17578 |   32085   166651 |   22736   12024   775703    64.5 |  3.629 % |
c |     18718 |   32085   166651 |   25009   13164   968206    73.5 |  3.629 % |
c |     20426 |   32085   166651 |   27510   14872  1241185    83.5 |  3.629 % |
c |     22989 |   32085   166651 |   30261   17435  1444714    82.9 |  3.629 % |
c |     26833 |   32085   166651 |   33288   21279  1891245    88.9 |  3.629 % |
c |     32599 |   32067   166452 |   36596   27044  3550248   131.3 |  3.715 % |
c |     41248 |   32067   166452 |   40255   35693  3966461   111.1 |  3.715 % |
c |     54223 |   32067   166452 |   44281   17359  5610700   323.2 |  3.715 % |
c |     73684 |   32067   166452 |   48709   36820 11136485   302.5 |  3.715 % |
c |    102877 |   32067   166452 |   53580   26763  7044362   263.2 |  3.715 % |
c ==============================================================================
c (current CPU-time: 420.112 s)
c ==============================================================================
c [1mFound solution: 16[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 |    132461 |   32219   166882 |    9665   56347 18423273   327.0 |  3.715 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1951          
c   -- var.elim.:  1951/1951          
c   -- var.elim.:  168/168          
c   -- var.elim.:  31/31          
c |    132461 |   32087   166662 |      --   56347       --      -- |     --   | -132/-219
c |    132461 |   32087   166662 |   12834   56347 18423273   327.0 |  3.715 % |
c |    132564 |   32087   166662 |   14118    9069  3336554   367.9 |  3.733 % |
c |    132714 |   32087   166662 |   15530    9219  3342220   362.5 |  3.733 % |
c |    132939 |   32087   166662 |   17083    9444  3350223   354.7 |  3.734 % |
c |    133276 |   32087   166662 |   18791    9781  3362491   343.8 |  3.734 % |
c |    133782 |   32087   166662 |   20670   10287  3404451   330.9 |  3.733 % |
c |    134541 |   32087   166662 |   22737   11046  3525231   319.1 |  3.733 % |
c |    135680 |   32087   166662 |   25011   12185  3745740   307.4 |  3.733 % |
c |    137388 |   32087   166662 |   27512   13893  3984228   286.8 |  3.733 % |
c |    139950 |   32087   166662 |   30263   16455  4343450   264.0 |  3.734 % |
c |    143794 |   32087   166662 |   33290   20299  5186665   255.5 |  3.733 % |
c |    149562 |   32087   166662 |   36619   26067  5590943   214.5 |  3.733 % |
c |    158212 |   32087   166662 |   40281   34717  6958308   200.4 |  3.733 % |
c |    171187 |   32087   166662 |   44309   16651  3547741   213.1 |  3.733 % |
c |    190648 |   32074   166619 |   48720   36111  5479816   151.7 |  3.743 % |
c |    219842 |   32056   166459 |   53562   26330  6293134   239.0 |  3.829 % |
c |    263631 |   32056   166459 |   58918   26870  9946245   370.2 |  3.829 % |
c |    329318 |   32056   166459 |   64810   43707 14083004   322.2 |  3.829 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v287 -v229 v148 -v112 -v97 v75 -v45 v23 -v285 -v270 v233 v147 -v128 -v113 -v44 -v28 -v269 v232 -v196 v149 -v127 -v117 -#### 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.85 0.97 0.93 2/54 18511
Raw data (stat): 18511 (runsolver) R 18510 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480600688 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 3098 0 0 0 984 13 0 0 25 0 1 0 480600688 15478784 2953 4294967295 134512640 134672761 3221224544 3221222880 134565588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3779 2953 603 41 0 3738 0
vsize: 15116
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 4029 0 0 0 1971 27 0 0 25 0 1 0 480600688 16596992 3367 4294967295 134512640 134672761 3221224544 3221222904 1075347366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4052 3367 603 41 0 4011 0
vsize: 16208
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 4867 0 0 0 2966 31 0 0 25 0 1 0 480600688 18092032 3733 4294967295 134512640 134672761 3221224544 3221223012 134643898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4417 3733 603 41 0 4376 0
vsize: 17668
[startup+40.0004 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 6254 0 0 0 3956 41 0 0 25 0 1 0 480600688 18972672 3971 4294967295 134512640 134672761 3221224544 3221222792 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 3971 603 41 0 4591 0
vsize: 18528
[startup+50.001 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 7263 0 0 0 4946 52 0 0 25 0 1 0 480600688 19984384 4219 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4879 4219 603 41 0 4838 0
vsize: 19516
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 8394 0 0 0 5936 61 0 0 25 0 1 0 480600688 21348352 4558 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5212 4558 603 41 0 5171 0
vsize: 20848
[startup+70.0023 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 9335 0 0 0 6930 68 0 0 25 0 1 0 480600688 23347200 5039 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5700 5039 603 41 0 5659 0
vsize: 22800
[startup+80.002 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 9368 0 0 0 7929 69 0 0 25 0 1 0 480600688 23347200 5072 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5700 5072 603 41 0 5659 0
vsize: 22800
[startup+90.0027 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 10071 0 0 0 8927 71 0 0 25 0 1 0 480600688 26107904 5775 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6374 5775 603 41 0 6333 0
vsize: 25496
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 11158 0 0 0 9923 75 0 0 25 0 1 0 480600688 30564352 6862 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7462 6862 603 41 0 7421 0
vsize: 29848
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 11707 0 0 0 10922 77 0 0 25 0 1 0 480600688 32780288 7411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8003 7411 603 41 0 7962 0
vsize: 32012
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 12305 0 0 0 11920 78 0 0 25 0 1 0 480600688 35430400 8009 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8650 8009 603 41 0 8609 0
vsize: 34600
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 13499 0 0 0 12918 81 0 0 25 0 1 0 480600688 40288256 9203 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9836 9203 603 41 0 9795 0
vsize: 39344
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 14679 0 0 0 13915 84 0 0 25 0 1 0 480600688 45129728 10383 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11018 10383 603 41 0 10977 0
vsize: 44072
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 15872 0 0 0 14911 88 0 0 25 0 1 0 480600688 50053120 11576 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12220 11576 603 41 0 12179 0
vsize: 48880
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 15872 0 0 0 15911 88 0 0 25 0 1 0 480600688 50053120 11576 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12220 11576 603 41 0 12179 0
vsize: 48880
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 15872 0 0 0 16911 89 0 0 25 0 1 0 480600688 50053120 11576 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12220 11576 603 41 0 12179 0
vsize: 48880
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 15872 0 0 0 17911 89 0 0 25 0 1 0 480600688 50053120 11576 4294967295 134512640 134672761 3221224544 3221223584 134603490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12220 11576 603 41 0 12179 0
vsize: 48880
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 16853 0 0 0 18908 92 0 0 25 0 1 0 480600688 53997568 12557 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13183 12557 603 41 0 13142 0
vsize: 52732
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 17892 0 0 0 19905 95 0 0 25 0 1 0 480600688 58208256 13596 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14211 13596 603 41 0 14170 0
vsize: 56844
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 18698 0 0 0 20903 97 0 0 25 0 1 0 480600688 61513728 14402 4294967295 134512640 134672761 3221224544 3221223408 1075349719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15018 14402 603 41 0 14977 0
vsize: 60072
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 19588 0 0 0 21901 99 0 0 25 0 1 0 480600688 65183744 15292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15914 15292 603 41 0 15873 0
vsize: 63656
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 20035 0 0 0 22900 101 0 0 25 0 1 0 480600688 67031040 15739 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16365 15739 603 41 0 16324 0
vsize: 65460
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 20644 0 0 0 23898 102 0 0 25 0 1 0 480600688 69537792 16348 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16977 16348 603 41 0 16936 0
vsize: 67908
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 21469 0 0 0 24896 105 0 0 25 0 1 0 480600688 72937472 17173 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17807 17173 603 41 0 17766 0
vsize: 71228
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22183 0 0 0 25893 108 0 0 25 0 1 0 480600688 75833344 17887 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18514 17887 603 41 0 18473 0
vsize: 74056
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 26892 109 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 27892 109 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 28892 110 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 29892 110 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 30891 110 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 31891 110 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 32891 111 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 33891 111 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 34891 111 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 35891 111 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22710 0 0 0 36890 112 0 0 25 0 1 0 480600688 77791232 18362 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18992 18362 603 41 0 18951 0
vsize: 75968
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 22733 0 0 0 37890 112 0 0 25 0 1 0 480600688 77922304 18385 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19024 18385 603 41 0 18983 0
vsize: 76096
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 23850 0 0 0 38887 116 0 0 25 0 1 0 480600688 82522112 19502 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20147 19502 603 41 0 20106 0
vsize: 80588
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 24920 0 0 0 39885 118 0 0 25 0 1 0 480600688 86855680 20572 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21205 20572 603 41 0 21164 0
vsize: 84820
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 25845 0 0 0 40882 121 0 0 25 0 1 0 480600688 90693632 21497 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22142 21497 603 41 0 22101 0
vsize: 88568
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 26785 0 0 0 41880 124 0 0 25 0 1 0 480600688 94531584 22437 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23079 22437 603 41 0 23038 0
vsize: 92316
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 42873 131 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223480 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 43872 131 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 44872 132 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 45872 132 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 46872 132 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 47872 132 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223636 1075351154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 48872 133 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 49872 133 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223432 1074972061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 50872 133 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 51871 133 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 52871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 53871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 54871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 55871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 56871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 57871 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 58872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 59872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 60872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 61872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 62872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 63872 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 64873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 65873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 66873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 67873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 68873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 69873 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 70874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223556 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 71874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 72874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 73874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 74874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 75874 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 76875 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 77875 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 78875 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 79875 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 27934 0 0 0 80875 134 0 0 25 0 1 0 480600688 97210368 23095 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23095 603 41 0 23692 0
vsize: 94932
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 81875 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 82875 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 83876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 84876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223584 134603615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 85876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 86876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 87876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 88876 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 89877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 90877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 91877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 92877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 93877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28053 0 0 0 94877 135 0 0 25 0 1 0 480600688 97497088 23188 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23803 23188 603 41 0 23762 0
vsize: 95212
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 28516 0 0 0 95877 135 0 0 25 0 1 0 480600688 99483648 23651 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24288 23651 603 41 0 24247 0
vsize: 97152
[startup+970.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29486 0 0 0 96875 137 0 0 25 0 1 0 480600688 103407616 24621 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25246 24621 603 41 0 25205 0
vsize: 100984
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 97875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 98875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 99875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 100875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 101875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 102875 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 103876 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 104876 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 105876 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 106876 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 107876 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 108877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 109877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 110877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 111877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 112877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 113877 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29581 0 0 0 114878 138 0 0 25 0 1 0 480600688 103489536 24655 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24655 603 41 0 25225 0
vsize: 101064
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29582 0 0 0 115879 138 0 0 25 0 1 0 480600688 103489536 24656 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24656 603 41 0 25225 0
vsize: 101064
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29584 0 0 0 116879 138 0 0 25 0 1 0 480600688 103489536 24658 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25266 24658 603 41 0 25225 0
vsize: 101064
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 29976 0 0 0 117878 139 0 0 25 0 1 0 480600688 105439232 25050 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25742 25050 603 41 0 25701 0
vsize: 102968
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 30605 0 0 0 118876 141 0 0 25 0 1 0 480600688 107614208 25611 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26273 25611 603 41 0 26232 0
vsize: 105092
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18511
Raw data (stat): 18511 (minisat+) R 18510 10614 10613 0 -1 0 30605 0 0 0 119877 141 0 0 25 0 1 0 480600688 107614208 25611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26273 25611 603 41 0 26232 0
vsize: 105092
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 18511
Raw data (stat): 18511 (minisat+) Z 18510 10614 10613 0 -1 12 30606 0 0 0 119877 146 0 0 25 0 1 0 480600688 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1198.77
CPU system time (s): 1.46878
CPU usage (%): 100.013
Max. virtual memory (Kb): 105092
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####