NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(b)
(c)
(d)
(f 1)
(g 1, 2, 3)
(h 1, 2)
(k)
(A)
(e)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Clean CTRS Procedure:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(b)
(c)
(d)
(f 1)
(g 1, 2, 3)
(h 1, 2)
(k)
(A)
(e)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

CRule InfChecker Info:
a -> c
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
a -> d
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
b -> c
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
b -> d
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
c -> e
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
c -> l
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
d -> m
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
f(x) -> x | x ->* e
Rule remains
Proof:
NO

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x vNonEmpty x)
(STRATEGY CONTEXTSENSITIVE
(a)
(b)
(c)
(d)
(f 1)
(g 1 2 3)
(h 1 2)
(k)
(A)
(e)
(fSNonEmpty)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)
]

Infeasibility Conditions:
x ->* e

Problem 1: 

Obtaining a proof using Prover9:

 -> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 2738064 was started by sandbox on z007.star.cs.uiowa.edu,
Thu Jun 27 11:11:08 2024
The command was "./prover9 -f /tmp/prover92738056-0.in".
============================== end of head ===========================

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

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

assign(max_seconds,20).

formulas(assumptions).
->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence).
->_s0(x1,y) -> ->_s0(g(x1,x2,x3),g(y,x2,x3)) # label(congruence).
->_s0(x2,y) -> ->_s0(g(x1,x2,x3),g(x1,y,x3)) # label(congruence).
->_s0(x3,y) -> ->_s0(g(x1,x2,x3),g(x1,x2,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence).
->_s0(a,c) # label(replacement).
->_s0(a,d) # label(replacement).
->_s0(b,c) # label(replacement).
->_s0(b,d) # label(replacement).
->_s0(c,e) # label(replacement).
->_s0(c,l) # label(replacement).
->_s0(d,m) # label(replacement).
->*_s0(x1,e) -> ->_s0(f(x1),x1) # label(replacement).
->_s0(g(d,x1,x1),A) # label(replacement).
->_s0(h(x1,x1),g(x1,x1,f(k))) # label(replacement).
->_s0(k,l) # label(replacement).
->_s0(k,m) # label(replacement).
->*_s0(x,x) # label(reflexivity).
->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
end_of_list.

formulas(goals).
(exists x3 ->*_s0(x3,e)) # label(goal).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
2 ->_s0(x1,y) -> ->_s0(g(x1,x2,x3),g(y,x2,x3)) # label(congruence) # label(non_clause).  [assumption].
3 ->_s0(x2,y) -> ->_s0(g(x1,x2,x3),g(x1,y,x3)) # label(congruence) # label(non_clause).  [assumption].
4 ->_s0(x3,y) -> ->_s0(g(x1,x2,x3),g(x1,x2,y)) # label(congruence) # label(non_clause).  [assumption].
5 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause).  [assumption].
6 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause).  [assumption].
7 ->*_s0(x1,e) -> ->_s0(f(x1),x1) # label(replacement) # label(non_clause).  [assumption].
8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
9 (exists x3 ->*_s0(x3,e)) # 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(f(x),f(y)) # label(congruence).  [clausify(1)].
-->_s0(x,y) | ->_s0(g(x,z,u),g(y,z,u)) # label(congruence).  [clausify(2)].
-->_s0(x,y) | ->_s0(g(z,x,u),g(z,y,u)) # label(congruence).  [clausify(3)].
-->_s0(x,y) | ->_s0(g(z,u,x),g(z,u,y)) # label(congruence).  [clausify(4)].
-->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence).  [clausify(5)].
-->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence).  [clausify(6)].
->_s0(a,c) # label(replacement).  [assumption].
->_s0(a,d) # label(replacement).  [assumption].
->_s0(b,c) # label(replacement).  [assumption].
->_s0(b,d) # label(replacement).  [assumption].
->_s0(c,e) # label(replacement).  [assumption].
->_s0(c,l) # label(replacement).  [assumption].
->_s0(d,m) # label(replacement).  [assumption].
-->*_s0(x,e) | ->_s0(f(x),x) # label(replacement).  [clausify(7)].
->_s0(g(d,x,x),A) # label(replacement).  [assumption].
->_s0(h(x,x),g(x,x,f(k))) # label(replacement).  [assumption].
->_s0(k,l) # label(replacement).  [assumption].
->_s0(k,m) # label(replacement).  [assumption].
->*_s0(x,x) # label(reflexivity).  [assumption].
-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(8)].
-->*_s0(x,e) # label(goal).  [deny(9)].
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([ c, d, k, e, l, m, a, b, A, h, f, g ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

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

Auto_process settings:  (no changes).

kept:      10 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(1)].
kept:      11 -->_s0(x,y) | ->_s0(g(x,z,u),g(y,z,u)) # label(congruence).  [clausify(2)].
kept:      12 -->_s0(x,y) | ->_s0(g(z,x,u),g(z,y,u)) # label(congruence).  [clausify(3)].
kept:      13 -->_s0(x,y) | ->_s0(g(z,u,x),g(z,u,y)) # label(congruence).  [clausify(4)].
kept:      14 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence).  [clausify(5)].
kept:      15 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence).  [clausify(6)].
kept:      16 ->_s0(a,c) # label(replacement).  [assumption].
kept:      17 ->_s0(a,d) # label(replacement).  [assumption].
kept:      18 ->_s0(b,c) # label(replacement).  [assumption].
kept:      19 ->_s0(b,d) # label(replacement).  [assumption].
kept:      20 ->_s0(c,e) # label(replacement).  [assumption].
kept:      21 ->_s0(c,l) # label(replacement).  [assumption].
kept:      22 ->_s0(d,m) # label(replacement).  [assumption].
kept:      23 -->*_s0(x,e) | ->_s0(f(x),x) # label(replacement).  [clausify(7)].
kept:      24 ->_s0(g(d,x,x),A) # label(replacement).  [assumption].
kept:      25 ->_s0(h(x,x),g(x,x,f(k))) # label(replacement).  [assumption].
kept:      26 ->_s0(k,l) # label(replacement).  [assumption].
kept:      27 ->_s0(k,m) # label(replacement).  [assumption].
kept:      28 ->*_s0(x,x) # label(reflexivity).  [assumption].
kept:      29 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(8)].
kept:      30 -->*_s0(x,e) # label(goal) # answer(goal).  [deny(9)].

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

% Proof 1 at 0.01 (+ 0.00) seconds: goal.
% Length of proof is 4.
% Level of proof is 2.
% Maximum clause weight is 3.000.
% Given clauses 0.

9 (exists x3 ->*_s0(x3,e)) # label(goal) # label(non_clause) # label(goal).  [goal].
28 ->*_s0(x,x) # label(reflexivity).  [assumption].
30 -->*_s0(x,e) # label(goal) # answer(goal).  [deny(9)].
31 $F # answer(goal).  [resolve(30,a,28,a)].

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

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

Given=0. Generated=21. Kept=21. proofs=1.
Usable=0. Sos=0. Demods=0. Limbo=20, Disabled=21. 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=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=0.
Megabytes=0.07.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 2738064 exit (max_proofs) Thu Jun 27 11:11:08 2024


The problem is feasible.


CRule InfChecker Info:
g(d,x,x) -> A
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
h(x,x) -> g(x,x,f(k))
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
k -> l
Rule remains
Proof:
NO_CONDS

CRule InfChecker Info:
k -> m
Rule remains
Proof:
NO_CONDS

Problem 1: 

Problem 1: 

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(b)
(c)
(d)
(f 1)
(g 1, 2, 3)
(h 1, 2)
(k)
(A)
(e)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Critical Pairs CProcedure:
-> Rules:
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
-> Vars:
"x"

-> Rlps:
crule: a -> c, id: 1, possubterms: a-> []
crule: a -> d, id: 2, possubterms: a-> []
crule: b -> c, id: 3, possubterms: b-> []
crule: b -> d, id: 4, possubterms: b-> []
crule: c -> e, id: 5, possubterms: c-> []
crule: c -> l, id: 6, possubterms: c-> []
crule: d -> m, id: 7, possubterms: d-> []
crule: f(x) -> x | x ->* e, id: 8, possubterms: f(x)-> []
crule: g(d,x,x) -> A, id: 9, possubterms: g(d,x,x)-> [], d-> [1]
crule: h(x,x) -> g(x,x,f(k)), id: 10, possubterms: h(x,x)-> []
crule: k -> l, id: 11, possubterms: k-> []
crule: k -> m, id: 12, possubterms: k-> []

-> Unifications:
R2 unifies with  R1 at  p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c
R4 unifies with  R3 at  p: [], l: b, lp: b, conds: {}, sig: {}, l': b, r: d, r': c
R6 unifies with  R5 at  p: [], l: c, lp: c, conds: {}, sig: {}, l': c, r: l, r': e
R9 unifies with  R7 at  p: [1], l: g(d,x,x), lp: d, conds: {}, sig: {}, l': d, r: A, r': m
R12 unifies with  R11 at  p: [], l: k, lp: k, conds: {}, sig: {}, l': k, r: m, r': l

-> Critical pairs info:
<e,l>   =>  Not trivial, Overlay, Proper, NW2, N1
<l,m>   =>  Not trivial, Overlay, Proper, NW2, N2
<g(m,x,x),A>   =>  Not trivial, Not overlay, Proper, NW1, N3
<c,d>   =>  Not trivial, Overlay, Proper, NW0, N4

-> Problem conclusions:
 Not left linear, Not right linear, Not linear, Not weakly left-linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
 CTRS Type: 1
 Deterministic, Strongly deterministic
 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS
 Maybe right-stable CTRS, Not overlay CTRS
 Maybe normal CTRS, Maybe almost normal CTRS
 ECCPs not considered
 Maybe terminating CTRS, Maybe operational terminating CTRS
 Maybe joinable CCPs
 Maybe level confluent, Maybe confluent

Problem 1: 

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(b)
(c)
(d)
(f 1)
(g 1, 2, 3)
(h 1, 2)
(k)
(A)
(e)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

Critical Pairs:
<e,l>   =>  Not trivial, Overlay, Proper, NW2, N1
<l,m>   =>  Not trivial, Overlay, Proper, NW2, N2
<g(m,x,x),A>   =>  Not trivial, Not overlay, Proper, NW1, N3
<c,d>   =>  Not trivial, Overlay, Proper, NW0, N4
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Conditional Critical Pairs Distributor Procedure

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(b)
(c)
(d)
(f 1)
(g 1, 2, 3)
(h 1, 2)
(k)
(A)
(e)
(l)
(m)
)
(RULES
a -> c
a -> d
b -> c
b -> d
c -> e
c -> l
d -> m
f(x) -> x | x ->* e
g(d,x,x) -> A
h(x,x) -> g(x,x,f(k))
k -> l
k -> m
)

Critical Pairs:
<e,l>   =>  Not trivial, Overlay, Proper, NW2, N1
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

InfChecker Different Ground and Normal No Conditions CCP Terms Procedure:
Proof:
Different, ground and normal terms (as normal weight is 2)

The problem is not confluent.