NO

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x y q n z vNonEmpty x1 x3)
(STRATEGY CONTEXTSENSITIVE
(add 1 2)
(div 1 2)
(lte 1 2)
(minus 1 2)
(mod 1 2)
(mult 1 2)
(power 1 2)
(0)
(fSNonEmpty)
(false)
(s 1)
(true)
)
(RULES
add(0,x) -> x
add(s(x),y) -> s(add(x,y))
div(0,s(x)) -> 0
div(s(x),s(y)) -> 0 | lte(s(x),y) ->* true
div(s(x),s(y)) -> s(q) | lte(s(x),y) ->* false, div(minus(x,y),s(y)) ->* q
lte(0,y) -> true
lte(s(x),0) -> false
lte(s(x),s(y)) -> lte(x,y)
minus(0,s(y)) -> 0
minus(s(x),s(y)) -> minus(x,y)
minus(x,0) -> x
mod(0,y) -> 0
mod(x,0) -> x
mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) ->* true
mod(x,s(y)) -> x | lte(s(y),x) ->* false
mult(0,y) -> 0
mult(s(x),y) -> add(mult(x,y),y)
power(x,0) -> s(0)
power(x,n) -> mult(mult(y,y),s(0)) | mod(n,s(s(0))) ->* 0, power(x,div(n,s(s(0)))) ->* y
power(x,n) -> mult(mult(y,y),x) | mod(n,s(s(0))) ->* s(z), power(x,div(n,s(s(0)))) ->* y
)
]

Infeasibility Conditions:
mod(0,s(s(0))) ->* 0, power(x1,div(0,s(s(0)))) ->* x3

Problem 1: 

Obtaining a proof using Prover9:

 -> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 3143668 was started by sandbox2 on z032.star.cs.uiowa.edu,
Tue Jul 30 08:22:40 2024
The command was "./prover9 -f /tmp/prover93143657-0.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file /tmp/prover93143657-0.in

assign(max_seconds,20).

formulas(assumptions).
->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(div(x1,x2),div(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(div(x1,x2),div(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(lte(x1,x2),lte(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(lte(x1,x2),lte(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(minus(x1,x2),minus(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(minus(x1,x2),minus(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(mod(x1,x2),mod(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(mod(x1,x2),mod(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(mult(x1,x2),mult(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(mult(x1,x2),mult(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(power(x1,x2),power(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(power(x1,x2),power(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
->_s0(add(0,x1),x1) # label(replacement).
->_s0(add(s(x1),x2),s(add(x1,x2))) # label(replacement).
->_s0(div(0,s(x1)),0) # label(replacement).
->*_s0(lte(s(x1),x2),true) -> ->_s0(div(s(x1),s(x2)),0) # label(replacement).
->*_s0(lte(s(x1),x2),false) & ->*_s0(div(minus(x1,x2),s(x2)),x3) -> ->_s0(div(s(x1),s(x2)),s(x3)) # label(replacement).
->_s0(lte(0,x2),true) # label(replacement).
->_s0(lte(s(x1),0),false) # label(replacement).
->_s0(lte(s(x1),s(x2)),lte(x1,x2)) # label(replacement).
->_s0(minus(0,s(x2)),0) # label(replacement).
->_s0(minus(s(x1),s(x2)),minus(x1,x2)) # label(replacement).
->_s0(minus(x1,0),x1) # label(replacement).
->_s0(mod(0,x2),0) # label(replacement).
->_s0(mod(x1,0),x1) # label(replacement).
->*_s0(lte(s(x2),x1),true) -> ->_s0(mod(x1,s(x2)),mod(minus(x1,s(x2)),s(x2))) # label(replacement).
->*_s0(lte(s(x2),x1),false) -> ->_s0(mod(x1,s(x2)),x1) # label(replacement).
->_s0(mult(0,x2),0) # label(replacement).
->_s0(mult(s(x1),x2),add(mult(x1,x2),x2)) # label(replacement).
->_s0(power(x1,0),s(0)) # label(replacement).
->*_s0(mod(x4,s(s(0))),0) & ->*_s0(power(x1,div(x4,s(s(0)))),x2) -> ->_s0(power(x1,x4),mult(mult(x2,x2),s(0))) # label(replacement).
->*_s0(mod(x4,s(s(0))),s(x5)) & ->*_s0(power(x1,div(x4,s(s(0)))),x2) -> ->_s0(power(x1,x4),mult(mult(x2,x2),x1)) # label(replacement).
->*_s0(x,x) # label(reflexivity).
->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
end_of_list.

formulas(goals).
(exists x7 exists x8 (->*_s0(mod(0,s(s(0))),0) & ->*_s0(power(x7,div(0,s(s(0)))),x8))) # label(goal).
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 ->_s0(x1,y) -> ->_s0(add(x1,x2),add(y,x2)) # label(congruence) # label(non_clause).  [assumption].
2 ->_s0(x2,y) -> ->_s0(add(x1,x2),add(x1,y)) # label(congruence) # label(non_clause).  [assumption].
3 ->_s0(x1,y) -> ->_s0(div(x1,x2),div(y,x2)) # label(congruence) # label(non_clause).  [assumption].
4 ->_s0(x2,y) -> ->_s0(div(x1,x2),div(x1,y)) # label(congruence) # label(non_clause).  [assumption].
5 ->_s0(x1,y) -> ->_s0(lte(x1,x2),lte(y,x2)) # label(congruence) # label(non_clause).  [assumption].
6 ->_s0(x2,y) -> ->_s0(lte(x1,x2),lte(x1,y)) # label(congruence) # label(non_clause).  [assumption].
7 ->_s0(x1,y) -> ->_s0(minus(x1,x2),minus(y,x2)) # label(congruence) # label(non_clause).  [assumption].
8 ->_s0(x2,y) -> ->_s0(minus(x1,x2),minus(x1,y)) # label(congruence) # label(non_clause).  [assumption].
9 ->_s0(x1,y) -> ->_s0(mod(x1,x2),mod(y,x2)) # label(congruence) # label(non_clause).  [assumption].
10 ->_s0(x2,y) -> ->_s0(mod(x1,x2),mod(x1,y)) # label(congruence) # label(non_clause).  [assumption].
11 ->_s0(x1,y) -> ->_s0(mult(x1,x2),mult(y,x2)) # label(congruence) # label(non_clause).  [assumption].
12 ->_s0(x2,y) -> ->_s0(mult(x1,x2),mult(x1,y)) # label(congruence) # label(non_clause).  [assumption].
13 ->_s0(x1,y) -> ->_s0(power(x1,x2),power(y,x2)) # label(congruence) # label(non_clause).  [assumption].
14 ->_s0(x2,y) -> ->_s0(power(x1,x2),power(x1,y)) # label(congruence) # label(non_clause).  [assumption].
15 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
16 ->*_s0(lte(s(x1),x2),true) -> ->_s0(div(s(x1),s(x2)),0) # label(replacement) # label(non_clause).  [assumption].
17 ->*_s0(lte(s(x1),x2),false) & ->*_s0(div(minus(x1,x2),s(x2)),x3) -> ->_s0(div(s(x1),s(x2)),s(x3)) # label(replacement) # label(non_clause).  [assumption].
18 ->*_s0(lte(s(x2),x1),true) -> ->_s0(mod(x1,s(x2)),mod(minus(x1,s(x2)),s(x2))) # label(replacement) # label(non_clause).  [assumption].
19 ->*_s0(lte(s(x2),x1),false) -> ->_s0(mod(x1,s(x2)),x1) # label(replacement) # label(non_clause).  [assumption].
20 ->*_s0(mod(x4,s(s(0))),0) & ->*_s0(power(x1,div(x4,s(s(0)))),x2) -> ->_s0(power(x1,x4),mult(mult(x2,x2),s(0))) # label(replacement) # label(non_clause).  [assumption].
21 ->*_s0(mod(x4,s(s(0))),s(x5)) & ->*_s0(power(x1,div(x4,s(s(0)))),x2) -> ->_s0(power(x1,x4),mult(mult(x2,x2),x1)) # label(replacement) # label(non_clause).  [assumption].
22 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
23 (exists x7 exists x8 (->*_s0(mod(0,s(s(0))),0) & ->*_s0(power(x7,div(0,s(s(0)))),x8))) # label(goal) # label(non_clause) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
-->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(1)].
-->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(2)].
-->_s0(x,y) | ->_s0(div(x,z),div(y,z)) # label(congruence).  [clausify(3)].
-->_s0(x,y) | ->_s0(div(z,x),div(z,y)) # label(congruence).  [clausify(4)].
-->_s0(x,y) | ->_s0(lte(x,z),lte(y,z)) # label(congruence).  [clausify(5)].
-->_s0(x,y) | ->_s0(lte(z,x),lte(z,y)) # label(congruence).  [clausify(6)].
-->_s0(x,y) | ->_s0(minus(x,z),minus(y,z)) # label(congruence).  [clausify(7)].
-->_s0(x,y) | ->_s0(minus(z,x),minus(z,y)) # label(congruence).  [clausify(8)].
-->_s0(x,y) | ->_s0(mod(x,z),mod(y,z)) # label(congruence).  [clausify(9)].
-->_s0(x,y) | ->_s0(mod(z,x),mod(z,y)) # label(congruence).  [clausify(10)].
-->_s0(x,y) | ->_s0(mult(x,z),mult(y,z)) # label(congruence).  [clausify(11)].
-->_s0(x,y) | ->_s0(mult(z,x),mult(z,y)) # label(congruence).  [clausify(12)].
-->_s0(x,y) | ->_s0(power(x,z),power(y,z)) # label(congruence).  [clausify(13)].
-->_s0(x,y) | ->_s0(power(z,x),power(z,y)) # label(congruence).  [clausify(14)].
-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(15)].
->_s0(add(0,x),x) # label(replacement).  [assumption].
->_s0(add(s(x),y),s(add(x,y))) # label(replacement).  [assumption].
->_s0(div(0,s(x)),0) # label(replacement).  [assumption].
-->*_s0(lte(s(x),y),true) | ->_s0(div(s(x),s(y)),0) # label(replacement).  [clausify(16)].
-->*_s0(lte(s(x),y),false) | -->*_s0(div(minus(x,y),s(y)),z) | ->_s0(div(s(x),s(y)),s(z)) # label(replacement).  [clausify(17)].
->_s0(lte(0,x),true) # label(replacement).  [assumption].
->_s0(lte(s(x),0),false) # label(replacement).  [assumption].
->_s0(lte(s(x),s(y)),lte(x,y)) # label(replacement).  [assumption].
->_s0(minus(0,s(x)),0) # label(replacement).  [assumption].
->_s0(minus(s(x),s(y)),minus(x,y)) # label(replacement).  [assumption].
->_s0(minus(x,0),x) # label(replacement).  [assumption].
->_s0(mod(0,x),0) # label(replacement).  [assumption].
->_s0(mod(x,0),x) # label(replacement).  [assumption].
-->*_s0(lte(s(x),y),true) | ->_s0(mod(y,s(x)),mod(minus(y,s(x)),s(x))) # label(replacement).  [clausify(18)].
-->*_s0(lte(s(x),y),false) | ->_s0(mod(y,s(x)),y) # label(replacement).  [clausify(19)].
->_s0(mult(0,x),0) # label(replacement).  [assumption].
->_s0(mult(s(x),y),add(mult(x,y),y)) # label(replacement).  [assumption].
->_s0(power(x,0),s(0)) # label(replacement).  [assumption].
-->*_s0(mod(x,s(s(0))),0) | -->*_s0(power(y,div(x,s(s(0)))),z) | ->_s0(power(y,x),mult(mult(z,z),s(0))) # label(replacement).  [clausify(20)].
-->*_s0(mod(x,s(s(0))),s(y)) | -->*_s0(power(z,div(x,s(s(0)))),u) | ->_s0(power(z,x),mult(mult(u,u),z)) # label(replacement).  [clausify(21)].
->*_s0(x,x) # label(reflexivity).  [assumption].
-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(22)].
-->*_s0(mod(0,s(s(0))),0) | -->*_s0(power(x,div(0,s(s(0)))),y) # label(goal).  [deny(23)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:
  % copying label goal to answer in negative clause

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
Function symbol precedence:  function_order([ 0, false, true, lte, mod, mult, div, minus, power, add, s ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(neg_binary_resolution).  % (HNE depth_diff=-12)
  % clear(ordered_res).  % (HNE depth_diff=-12)
  % set(ur_resolution).  % (HNE depth_diff=-12)
    % set(ur_resolution) -> set(pos_ur_resolution).
    % set(ur_resolution) -> set(neg_ur_resolution).

Auto_process settings:
  % set(unit_deletion).  % (Horn set with negative nonunits)

kept:      24 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(1)].
kept:      25 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(2)].
kept:      26 -->_s0(x,y) | ->_s0(div(x,z),div(y,z)) # label(congruence).  [clausify(3)].
kept:      27 -->_s0(x,y) | ->_s0(div(z,x),div(z,y)) # label(congruence).  [clausify(4)].
kept:      28 -->_s0(x,y) | ->_s0(lte(x,z),lte(y,z)) # label(congruence).  [clausify(5)].
kept:      29 -->_s0(x,y) | ->_s0(lte(z,x),lte(z,y)) # label(congruence).  [clausify(6)].
kept:      30 -->_s0(x,y) | ->_s0(minus(x,z),minus(y,z)) # label(congruence).  [clausify(7)].
kept:      31 -->_s0(x,y) | ->_s0(minus(z,x),minus(z,y)) # label(congruence).  [clausify(8)].
kept:      32 -->_s0(x,y) | ->_s0(mod(x,z),mod(y,z)) # label(congruence).  [clausify(9)].
kept:      33 -->_s0(x,y) | ->_s0(mod(z,x),mod(z,y)) # label(congruence).  [clausify(10)].
kept:      34 -->_s0(x,y) | ->_s0(mult(x,z),mult(y,z)) # label(congruence).  [clausify(11)].
kept:      35 -->_s0(x,y) | ->_s0(mult(z,x),mult(z,y)) # label(congruence).  [clausify(12)].
kept:      36 -->_s0(x,y) | ->_s0(power(x,z),power(y,z)) # label(congruence).  [clausify(13)].
kept:      37 -->_s0(x,y) | ->_s0(power(z,x),power(z,y)) # label(congruence).  [clausify(14)].
kept:      38 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(15)].
kept:      39 ->_s0(add(0,x),x) # label(replacement).  [assumption].
kept:      40 ->_s0(add(s(x),y),s(add(x,y))) # label(replacement).  [assumption].
kept:      41 ->_s0(div(0,s(x)),0) # label(replacement).  [assumption].
kept:      42 -->*_s0(lte(s(x),y),true) | ->_s0(div(s(x),s(y)),0) # label(replacement).  [clausify(16)].
kept:      43 -->*_s0(lte(s(x),y),false) | -->*_s0(div(minus(x,y),s(y)),z) | ->_s0(div(s(x),s(y)),s(z)) # label(replacement).  [clausify(17)].
kept:      44 ->_s0(lte(0,x),true) # label(replacement).  [assumption].
kept:      45 ->_s0(lte(s(x),0),false) # label(replacement).  [assumption].
kept:      46 ->_s0(lte(s(x),s(y)),lte(x,y)) # label(replacement).  [assumption].
kept:      47 ->_s0(minus(0,s(x)),0) # label(replacement).  [assumption].
kept:      48 ->_s0(minus(s(x),s(y)),minus(x,y)) # label(replacement).  [assumption].
kept:      49 ->_s0(minus(x,0),x) # label(replacement).  [assumption].
kept:      50 ->_s0(mod(0,x),0) # label(replacement).  [assumption].
kept:      51 ->_s0(mod(x,0),x) # label(replacement).  [assumption].
kept:      52 -->*_s0(lte(s(x),y),true) | ->_s0(mod(y,s(x)),mod(minus(y,s(x)),s(x))) # label(replacement).  [clausify(18)].
kept:      53 -->*_s0(lte(s(x),y),false) | ->_s0(mod(y,s(x)),y) # label(replacement).  [clausify(19)].
kept:      54 ->_s0(mult(0,x),0) # label(replacement).  [assumption].
kept:      55 ->_s0(mult(s(x),y),add(mult(x,y),y)) # label(replacement).  [assumption].
kept:      56 ->_s0(power(x,0),s(0)) # label(replacement).  [assumption].
kept:      57 -->*_s0(mod(x,s(s(0))),0) | -->*_s0(power(y,div(x,s(s(0)))),z) | ->_s0(power(y,x),mult(mult(z,z),s(0))) # label(replacement).  [clausify(20)].
kept:      58 -->*_s0(mod(x,s(s(0))),s(y)) | -->*_s0(power(z,div(x,s(s(0)))),u) | ->_s0(power(z,x),mult(mult(u,u),z)) # label(replacement).  [clausify(21)].
kept:      59 ->*_s0(x,x) # label(reflexivity).  [assumption].
kept:      60 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(22)].
kept:      61 -->*_s0(mod(0,s(s(0))),0) | -->*_s0(power(x,div(0,s(s(0)))),y) # label(goal) # answer(goal).  [deny(23)].

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
24 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(1)].
25 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(2)].
26 -->_s0(x,y) | ->_s0(div(x,z),div(y,z)) # label(congruence).  [clausify(3)].
27 -->_s0(x,y) | ->_s0(div(z,x),div(z,y)) # label(congruence).  [clausify(4)].
28 -->_s0(x,y) | ->_s0(lte(x,z),lte(y,z)) # label(congruence).  [clausify(5)].
29 -->_s0(x,y) | ->_s0(lte(z,x),lte(z,y)) # label(congruence).  [clausify(6)].
30 -->_s0(x,y) | ->_s0(minus(x,z),minus(y,z)) # label(congruence).  [clausify(7)].
31 -->_s0(x,y) | ->_s0(minus(z,x),minus(z,y)) # label(congruence).  [clausify(8)].
32 -->_s0(x,y) | ->_s0(mod(x,z),mod(y,z)) # label(congruence).  [clausify(9)].
33 -->_s0(x,y) | ->_s0(mod(z,x),mod(z,y)) # label(congruence).  [clausify(10)].
34 -->_s0(x,y) | ->_s0(mult(x,z),mult(y,z)) # label(congruence).  [clausify(11)].
35 -->_s0(x,y) | ->_s0(mult(z,x),mult(z,y)) # label(congruence).  [clausify(12)].
36 -->_s0(x,y) | ->_s0(power(x,z),power(y,z)) # label(congruence).  [clausify(13)].
37 -->_s0(x,y) | ->_s0(power(z,x),power(z,y)) # label(congruence).  [clausify(14)].
38 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(15)].
39 ->_s0(add(0,x),x) # label(replacement).  [assumption].
40 ->_s0(add(s(x),y),s(add(x,y))) # label(replacement).  [assumption].
41 ->_s0(div(0,s(x)),0) # label(replacement).  [assumption].
42 -->*_s0(lte(s(x),y),true) | ->_s0(div(s(x),s(y)),0) # label(replacement).  [clausify(16)].
43 -->*_s0(lte(s(x),y),false) | -->*_s0(div(minus(x,y),s(y)),z) | ->_s0(div(s(x),s(y)),s(z)) # label(replacement).  [clausify(17)].
44 ->_s0(lte(0,x),true) # label(replacement).  [assumption].
45 ->_s0(lte(s(x),0),false) # label(replacement).  [assumption].
46 ->_s0(lte(s(x),s(y)),lte(x,y)) # label(replacement).  [assumption].
47 ->_s0(minus(0,s(x)),0) # label(replacement).  [assumption].
48 ->_s0(minus(s(x),s(y)),minus(x,y)) # label(replacement).  [assumption].
49 ->_s0(minus(x,0),x) # label(replacement).  [assumption].
50 ->_s0(mod(0,x),0) # label(replacement).  [assumption].
51 ->_s0(mod(x,0),x) # label(replacement).  [assumption].
52 -->*_s0(lte(s(x),y),true) | ->_s0(mod(y,s(x)),mod(minus(y,s(x)),s(x))) # label(replacement).  [clausify(18)].
53 -->*_s0(lte(s(x),y),false) | ->_s0(mod(y,s(x)),y) # label(replacement).  [clausify(19)].
54 ->_s0(mult(0,x),0) # label(replacement).  [assumption].
55 ->_s0(mult(s(x),y),add(mult(x,y),y)) # label(replacement).  [assumption].
56 ->_s0(power(x,0),s(0)) # label(replacement).  [assumption].
57 -->*_s0(mod(x,s(s(0))),0) | -->*_s0(power(y,div(x,s(s(0)))),z) | ->_s0(power(y,x),mult(mult(z,z),s(0))) # label(replacement).  [clausify(20)].
58 -->*_s0(mod(x,s(s(0))),s(y)) | -->*_s0(power(z,div(x,s(s(0)))),u) | ->_s0(power(z,x),mult(mult(u,u),z)) # label(replacement).  [clausify(21)].
59 ->*_s0(x,x) # label(reflexivity).  [assumption].
60 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(22)].
61 -->*_s0(mod(0,s(s(0))),0) | -->*_s0(power(x,div(0,s(s(0)))),y) # label(goal) # answer(goal).  [deny(23)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.01 seconds.

given #1 (I,wt=10): 24 -->_s0(x,y) | ->_s0(add(x,z),add(y,z)) # label(congruence).  [clausify(1)].

given #2 (I,wt=10): 25 -->_s0(x,y) | ->_s0(add(z,x),add(z,y)) # label(congruence).  [clausify(2)].

given #3 (I,wt=10): 26 -->_s0(x,y) | ->_s0(div(x,z),div(y,z)) # label(congruence).  [clausify(3)].

given #4 (I,wt=10): 27 -->_s0(x,y) | ->_s0(div(z,x),div(z,y)) # label(congruence).  [clausify(4)].

given #5 (I,wt=10): 28 -->_s0(x,y) | ->_s0(lte(x,z),lte(y,z)) # label(congruence).  [clausify(5)].

given #6 (I,wt=10): 29 -->_s0(x,y) | ->_s0(lte(z,x),lte(z,y)) # label(congruence).  [clausify(6)].

given #7 (I,wt=10): 30 -->_s0(x,y) | ->_s0(minus(x,z),minus(y,z)) # label(congruence).  [clausify(7)].

given #8 (I,wt=10): 31 -->_s0(x,y) | ->_s0(minus(z,x),minus(z,y)) # label(congruence).  [clausify(8)].

given #9 (I,wt=10): 32 -->_s0(x,y) | ->_s0(mod(x,z),mod(y,z)) # label(congruence).  [clausify(9)].

given #10 (I,wt=10): 33 -->_s0(x,y) | ->_s0(mod(z,x),mod(z,y)) # label(congruence).  [clausify(10)].

given #11 (I,wt=10): 34 -->_s0(x,y) | ->_s0(mult(x,z),mult(y,z)) # label(congruence).  [clausify(11)].

given #12 (I,wt=10): 35 -->_s0(x,y) | ->_s0(mult(z,x),mult(z,y)) # label(congruence).  [clausify(12)].

given #13 (I,wt=10): 36 -->_s0(x,y) | ->_s0(power(x,z),power(y,z)) # label(congruence).  [clausify(13)].

given #14 (I,wt=10): 37 -->_s0(x,y) | ->_s0(power(z,x),power(z,y)) # label(congruence).  [clausify(14)].

given #15 (I,wt=8): 38 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(15)].

given #16 (I,wt=5): 39 ->_s0(add(0,x),x) # label(replacement).  [assumption].

given #17 (I,wt=9): 40 ->_s0(add(s(x),y),s(add(x,y))) # label(replacement).  [assumption].

given #18 (I,wt=6): 41 ->_s0(div(0,s(x)),0) # label(replacement).  [assumption].

given #19 (I,wt=13): 42 -->*_s0(lte(s(x),y),true) | ->_s0(div(s(x),s(y)),0) # label(replacement).  [clausify(16)].

given #20 (I,wt=22): 43 -->*_s0(lte(s(x),y),false) | -->*_s0(div(minus(x,y),s(y)),z) | ->_s0(div(s(x),s(y)),s(z)) # label(replacement).  [clausify(17)].

given #21 (I,wt=5): 44 ->_s0(lte(0,x),true) # label(replacement).  [assumption].

given #22 (I,wt=6): 45 ->_s0(lte(s(x),0),false) # label(replacement).  [assumption].

given #23 (I,wt=9): 46 ->_s0(lte(s(x),s(y)),lte(x,y)) # label(replacement).  [assumption].

given #24 (I,wt=6): 47 ->_s0(minus(0,s(x)),0) # label(replacement).  [assumption].

given #25 (I,wt=9): 48 ->_s0(minus(s(x),s(y)),minus(x,y)) # label(replacement).  [assumption].

given #26 (I,wt=5): 49 ->_s0(minus(x,0),x) # label(replacement).  [assumption].

given #27 (I,wt=5): 50 ->_s0(mod(0,x),0) # label(replacement).  [assumption].

given #28 (I,wt=5): 51 ->_s0(mod(x,0),x) # label(replacement).  [assumption].

given #29 (I,wt=18): 52 -->*_s0(lte(s(x),y),true) | ->_s0(mod(y,s(x)),mod(minus(y,s(x)),s(x))) # label(replacement).  [clausify(18)].

given #30 (I,wt=12): 53 -->*_s0(lte(s(x),y),false) | ->_s0(mod(y,s(x)),y) # label(replacement).  [clausify(19)].

given #31 (I,wt=5): 54 ->_s0(mult(0,x),0) # label(replacement).  [assumption].

given #32 (I,wt=10): 55 ->_s0(mult(s(x),y),add(mult(x,y),y)) # label(replacement).  [assumption].

given #33 (I,wt=6): 56 ->_s0(power(x,0),s(0)) # label(replacement).  [assumption].

given #34 (I,wt=26): 57 -->*_s0(mod(x,s(s(0))),0) | -->*_s0(power(y,div(x,s(s(0)))),z) | ->_s0(power(y,x),mult(mult(z,z),s(0))) # label(replacement).  [clausify(20)].

given #35 (I,wt=26): 58 -->*_s0(mod(x,s(s(0))),s(y)) | -->*_s0(power(z,div(x,s(s(0)))),u) | ->_s0(power(z,x),mult(mult(u,u),z)) # label(replacement).  [clausify(21)].

given #36 (I,wt=3): 59 ->*_s0(x,x) # label(reflexivity).  [assumption].

given #37 (I,wt=9): 60 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(22)].

============================== PROOF =================================

% Proof 1 at 0.02 (+ 0.00) seconds: goal.
% Length of proof is 9.
% Level of proof is 4.
% Maximum clause weight is 16.000.
% Given clauses 37.

22 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
23 (exists x7 exists x8 (->*_s0(mod(0,s(s(0))),0) & ->*_s0(power(x7,div(0,s(s(0)))),x8))) # label(goal) # label(non_clause) # label(goal).  [goal].
50 ->_s0(mod(0,x),0) # label(replacement).  [assumption].
59 ->*_s0(x,x) # label(reflexivity).  [assumption].
60 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(22)].
61 -->*_s0(mod(0,s(s(0))),0) | -->*_s0(power(x,div(0,s(s(0)))),y) # label(goal) # answer(goal).  [deny(23)].
276 ->*_s0(mod(0,x),0).  [ur(60,a,50,a,b,59,a)].
286 -->*_s0(power(x,div(0,s(s(0)))),y) # answer(goal).  [back_unit_del(61),unit_del(a,276)].
287 $F # answer(goal).  [resolve(286,a,59,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=37. Generated=263. Kept=263. proofs=1.
Usable=37. Sos=214. Demods=0. Limbo=10, Disabled=39. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=0. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=38.
Megabytes=0.58.
User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3143668 exit (max_proofs) Tue Jul 30 08:22:40 2024


The problem is feasible.