YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(a)
(f 1)
(g 1)
(h 1)
(b)
(c 1)
(fSNonEmpty)
)
(RULES
a -> b
f(x) -> h(x)
g(a) -> f(g(a))
g(b) -> c(a)
h(x) -> c(b)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
CSR Converter From Top u-Replacement Map Procedure [CSUR20]:


Original Replacement Map:
(a)
(f 1)
(g 1)
(h 1)
(b)
(c 1)
(fSNonEmpty)

New Replacement Maps:

Replacement Map number 1:
(a)
(f)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)

Replacement Map number 2:
(a)
(f)
(g 1)
(h 1)
(b)
(c)
(fSNonEmpty)

Replacement Map number 3:
(a)
(f)
(g 1)
(h 1)
(b)
(c 1)
(fSNonEmpty)

Replacement Map number 4:
(a)
(f 1)
(g 1)
(h)
(b)
(c)
(fSNonEmpty)

Replacement Map number 5:
(a)
(f 1)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)

Replacement Map number 6:
(a)
(f 1)
(g 1)
(h 1)
(b)
(c)
(fSNonEmpty)

Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x)
(STRATEGY CONTEXTSENSITIVE
(a)
(f)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)
)
(RULES
a -> b
f(x) -> h(x)
g(a) -> f(g(a))
g(b) -> c(a)
h(x) -> c(b)
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 F(x) -> H(x)
 G(a) -> F(g(a))
 G(b) -> A
-> Rules:
 a -> b
 f(x) -> h(x)
 g(a) -> f(g(a))
 g(b) -> c(a)
 h(x) -> c(b)
-> Unhiding Rules:
 Empty

Problem 1: 

SCC Processor:
-> Pairs:
 F(x) -> H(x)
 G(a) -> F(g(a))
 G(b) -> A
-> Rules:
 a -> b
 f(x) -> h(x)
 g(a) -> f(g(a))
 g(b) -> c(a)
 h(x) -> c(b)
-> Unhiding rules:
 Empty
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(a)
(f)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)
)
(RULES
a -> b
f(x) -> h(x)
g(a) -> f(g(a))
g(b) -> c(a)
h(x) -> c(b)
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy NW Procedure:
-> Rules:
 a -> b
 f(x) -> h(x)
 g(a) -> f(g(a))
 g(b) -> c(a)
 h(x) -> c(b)
-> Vars:
 x, x
-> UVars:
 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 2, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 5, UV-LActive: [x], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])

-> Rlps:
 (rule: a -> b, id: 1, possubterms: a->[])
 (rule: f(x) -> h(x), id: 2, possubterms: f(x)->[])
 (rule: g(a) -> f(g(a)), id: 3, possubterms: g(a)->[], a->[1])
 (rule: g(b) -> c(a), id: 4, possubterms: g(b)->[], b->[1])
 (rule: h(x) -> c(b), id: 5, possubterms: h(x)->[])

-> Unifications:
(R3 unifies with R1 at p: [1], l: g(a), lp: a, sig: {}, l': a, r: f(g(a)), r': b)

-> Critical pairs info:
<g(b),f(g(a))>   =>  Not trivial, Not overlay, Proper, NW0, N1

-> Problem conclusions:
 Left linear, Right linear, Linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a CS-TRS, Left-homogeneous u-replacing variables

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(a)
(f)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)
)
(RULES
a -> b
f(x) -> h(x)
g(a) -> f(g(a))
g(b) -> c(a)
h(x) -> c(b)
)
Critical Pairs:
<g(b),f(g(a))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet InfChecker Procedure:
Infeasible convergence?
NO

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(a)
(f)
(g 1)
(h)
(b)
(c 1)
(fSNonEmpty)
)
(RULES
a -> b
f(x) -> h(x)
g(a) -> f(g(a))
g(b) -> c(a)
h(x) -> c(b)
)]
Infeasibility Conditions:
g(b) \->* z0, f(g(a)) \->* z0

Problem 1: 

Obtaining a proof using Prover9:

 -> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 2689521 was started by shintani on shintani-XPS-13-9310,
Fri Jun  9 15:40:33 2023
The command was "./prover9 -f /tmp/prover92689509-0.in".
============================== end of head ===========================

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

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

assign(max_seconds,20).

formulas(assumptions).
\->_s0(x1,y) -> \->_s0(g(x1),g(y)) # label(cscongruence).
\->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence).
\->_s0(a,b) # label(csreplacement).
\->_s0(f(x1),h(x1)) # label(csreplacement).
\->_s0(g(a),f(g(a))) # label(csreplacement).
\->_s0(g(b),c(a)) # label(csreplacement).
\->_s0(h(x1),c(b)) # label(csreplacement).
\->*_s0(x,x) # label(csreflexivity).
\->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity).
end_of_list.

formulas(goals).
(exists x3 (\->*_s0(g(b),x3) & \->*_s0(f(g(a)),x3))) # label(goal).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 \->_s0(x1,y) -> \->_s0(g(x1),g(y)) # label(cscongruence) # label(non_clause).  [assumption].
2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause).  [assumption].
3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause).  [assumption].
4 (exists x3 (\->*_s0(g(b),x3) & \->*_s0(f(g(a)),x3))) # 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(g(x),g(y)) # label(cscongruence).  [clausify(1)].
-\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence).  [clausify(2)].
\->_s0(a,b) # label(csreplacement).  [assumption].
\->_s0(f(x),h(x)) # label(csreplacement).  [assumption].
\->_s0(g(a),f(g(a))) # label(csreplacement).  [assumption].
\->_s0(g(b),c(a)) # label(csreplacement).  [assumption].
\->_s0(h(x),c(b)) # label(csreplacement).  [assumption].
\->*_s0(x,x) # label(csreflexivity).  [assumption].
-\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity).  [clausify(3)].
-\->*_s0(g(b),x) | -\->*_s0(f(g(a)),x) # label(goal).  [deny(4)].
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([ a, b, g, c, f, h ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(neg_binary_resolution).  % (HNE depth_diff=-2)
  % clear(ordered_res).  % (HNE depth_diff=-2)
  % set(ur_resolution).  % (HNE depth_diff=-2)
    % 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:      5 -\->_s0(x,y) | \->_s0(g(x),g(y)) # label(cscongruence).  [clausify(1)].
kept:      6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence).  [clausify(2)].
kept:      7 \->_s0(a,b) # label(csreplacement).  [assumption].
kept:      8 \->_s0(f(x),h(x)) # label(csreplacement).  [assumption].
kept:      9 \->_s0(g(a),f(g(a))) # label(csreplacement).  [assumption].
kept:      10 \->_s0(g(b),c(a)) # label(csreplacement).  [assumption].
kept:      11 \->_s0(h(x),c(b)) # label(csreplacement).  [assumption].
kept:      12 \->*_s0(x,x) # label(csreflexivity).  [assumption].
kept:      13 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity).  [clausify(3)].
kept:      14 -\->*_s0(g(b),x) | -\->*_s0(f(g(a)),x) # label(goal) # answer(goal).  [deny(4)].

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
5 -\->_s0(x,y) | \->_s0(g(x),g(y)) # label(cscongruence).  [clausify(1)].
6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence).  [clausify(2)].
7 \->_s0(a,b) # label(csreplacement).  [assumption].
8 \->_s0(f(x),h(x)) # label(csreplacement).  [assumption].
9 \->_s0(g(a),f(g(a))) # label(csreplacement).  [assumption].
10 \->_s0(g(b),c(a)) # label(csreplacement).  [assumption].
11 \->_s0(h(x),c(b)) # label(csreplacement).  [assumption].
12 \->*_s0(x,x) # label(csreflexivity).  [assumption].
13 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity).  [clausify(3)].
14 -\->*_s0(g(b),x) | -\->*_s0(f(g(a)),x) # label(goal) # answer(goal).  [deny(4)].
end_of_list.

formulas(demodulators).
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=8): 5 -\->_s0(x,y) | \->_s0(g(x),g(y)) # label(cscongruence).  [clausify(1)].

given #2 (I,wt=8): 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence).  [clausify(2)].

given #3 (I,wt=3): 7 \->_s0(a,b) # label(csreplacement).  [assumption].

given #4 (I,wt=5): 8 \->_s0(f(x),h(x)) # label(csreplacement).  [assumption].

given #5 (I,wt=6): 9 \->_s0(g(a),f(g(a))) # label(csreplacement).  [assumption].

given #6 (I,wt=5): 10 \->_s0(g(b),c(a)) # label(csreplacement).  [assumption].

given #7 (I,wt=5): 11 \->_s0(h(x),c(b)) # label(csreplacement).  [assumption].

given #8 (I,wt=3): 12 \->*_s0(x,x) # label(csreflexivity).  [assumption].

given #9 (I,wt=9): 13 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity).  [clausify(3)].

given #10 (I,wt=9): 14 -\->*_s0(g(b),x) | -\->*_s0(f(g(a)),x) # label(goal) # answer(goal).  [deny(4)].

given #11 (A,wt=5): 15 \->_s0(c(a),c(b)).  [ur(6,a,7,a)].

given #12 (F,wt=6): 31 -\->*_s0(f(g(a)),g(b)) # answer(goal).  [resolve(14,a,12,a)].

given #13 (F,wt=6): 33 -\->*_s0(g(b),f(g(a))) # answer(goal).  [resolve(14,b,12,a)].

given #14 (F,wt=6): 38 -\->_s0(f(g(a)),g(b)) # answer(goal).  [ur(13,b,12,a,c,31,a)].

given #15 (F,wt=6): 39 -\->*_s0(h(g(a)),g(b)) # answer(goal).  [ur(13,a,8,a,c,31,a)].

given #16 (T,wt=3): 29 \->*_s0(a,b).  [ur(13,a,7,a,b,12,a)].

given #17 (T,wt=5): 16 \->_s0(g(a),g(b)).  [ur(5,a,7,a)].

given #18 (T,wt=5): 25 \->*_s0(h(x),c(b)).  [ur(13,a,11,a,b,12,a)].

given #19 (T,wt=5): 26 \->*_s0(g(b),c(a)).  [ur(13,a,10,a,b,12,a)].

given #20 (A,wt=7): 17 \->_s0(c(f(x)),c(h(x))).  [ur(6,a,8,a)].

given #21 (F,wt=5): 45 -\->*_s0(c(b),g(b)) # answer(goal).  [ur(13,a,11,a,c,39,a)].

given #22 (F,wt=5): 56 -\->_s0(c(b),g(b)) # answer(goal).  [ur(13,b,12,a,c,45,a)].

given #23 (F,wt=6): 41 -\->_s0(g(b),f(g(a))) # answer(goal).  [ur(13,b,12,a,c,33,a)].

given #24 (F,wt=6): 42 -\->*_s0(c(a),f(g(a))) # answer(goal).  [ur(13,a,10,a,c,33,a)].

given #25 (T,wt=5): 28 \->*_s0(f(x),h(x)).  [ur(13,a,8,a,b,12,a)].

given #26 (T,wt=5): 34 \->*_s0(c(a),c(b)).  [ur(13,a,15,a,b,12,a)].

given #27 (T,wt=5): 46 \->*_s0(g(a),g(b)).  [ur(13,a,16,a,b,12,a)].

given #28 (T,wt=5): 49 \->*_s0(f(x),c(b)).  [ur(13,a,8,a,b,25,a)].

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

% Proof 1 at 0.00 (+ 0.00) seconds: goal.
% Length of proof is 17.
% Level of proof is 5.
% Maximum clause weight is 9.000.
% Given clauses 28.

2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause).  [assumption].
3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause).  [assumption].
4 (exists x3 (\->*_s0(g(b),x3) & \->*_s0(f(g(a)),x3))) # label(goal) # label(non_clause) # label(goal).  [goal].
6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence).  [clausify(2)].
7 \->_s0(a,b) # label(csreplacement).  [assumption].
8 \->_s0(f(x),h(x)) # label(csreplacement).  [assumption].
10 \->_s0(g(b),c(a)) # label(csreplacement).  [assumption].
11 \->_s0(h(x),c(b)) # label(csreplacement).  [assumption].
12 \->*_s0(x,x) # label(csreflexivity).  [assumption].
13 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity).  [clausify(3)].
14 -\->*_s0(g(b),x) | -\->*_s0(f(g(a)),x) # label(goal) # answer(goal).  [deny(4)].
15 \->_s0(c(a),c(b)).  [ur(6,a,7,a)].
25 \->*_s0(h(x),c(b)).  [ur(13,a,11,a,b,12,a)].
34 \->*_s0(c(a),c(b)).  [ur(13,a,15,a,b,12,a)].
49 \->*_s0(f(x),c(b)).  [ur(13,a,8,a,b,25,a)].
62 \->*_s0(g(b),c(b)).  [ur(13,a,10,a,b,34,a)].
66 $F # answer(goal).  [resolve(49,a,14,b),unit_del(a,62)].

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

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

Given=28. Generated=66. Kept=61. proofs=1.
Usable=28. Sos=33. Demods=0. Limbo=0, Disabled=10. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=4. 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=36.
Megabytes=0.12.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 2689521 exit (max_proofs) Fri Jun  9 15:40:33 2023


The problem is feasible.


The problem is confluent.