NO

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x y vNonEmpty x y)
(STRATEGY CONTEXTSENSITIVE
(+ 1 2)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
+(0,x) -> x
+(s(x),y) -> s(+(x,y))
)
]
Infeasibility Conditions:
+(s(x),y) ->* s(y)

Problem 1: 

Obtaining a proof using Prover9:

 -> Prover9 Output:
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 3413439 was started by sandbox2 on z021.star.cs.uiowa.edu,
Tue Jul 30 09:47:55 2024
The command was "./prover9 -f /tmp/prover93413430-0.in".
============================== end of head ===========================

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

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

assign(max_seconds,20).

formulas(assumptions).
->_s0(x1,y) -> ->_s0(+(x1,x2),+(y,x2)) # label(congruence).
->_s0(x2,y) -> ->_s0(+(x1,x2),+(x1,y)) # label(congruence).
->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
->_s0(+(0,x1),x1) # label(replacement).
->_s0(+(s(x1),x2),s(+(x1,x2))) # label(replacement).
->*_s0(x,x) # label(reflexivity).
->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
end_of_list.

formulas(goals).
(exists x4 exists x5 ->*_s0(+(s(x4),x5),s(x5))) # label(goal).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 ->_s0(x1,y) -> ->_s0(+(x1,x2),+(y,x2)) # label(congruence) # label(non_clause).  [assumption].
2 ->_s0(x2,y) -> ->_s0(+(x1,x2),+(x1,y)) # label(congruence) # label(non_clause).  [assumption].
3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
4 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
5 (exists x4 exists x5 ->*_s0(+(s(x4),x5),s(x5))) # 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(+(x,z),+(y,z)) # label(congruence).  [clausify(1)].
-->_s0(x,y) | ->_s0(+(z,x),+(z,y)) # label(congruence).  [clausify(2)].
-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(3)].
->_s0(+(0,x),x) # label(replacement).  [assumption].
->_s0(+(s(x),y),s(+(x,y))) # label(replacement).  [assumption].
->*_s0(x,x) # label(reflexivity).  [assumption].
-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(4)].
-->*_s0(+(s(x),y),s(y)) # label(goal).  [deny(5)].
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, +, s ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

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

Auto_process settings:  (no changes).

kept:      6 -->_s0(x,y) | ->_s0(+(x,z),+(y,z)) # label(congruence).  [clausify(1)].
kept:      7 -->_s0(x,y) | ->_s0(+(z,x),+(z,y)) # label(congruence).  [clausify(2)].
kept:      8 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(3)].
kept:      9 ->_s0(+(0,x),x) # label(replacement).  [assumption].
kept:      10 ->_s0(+(s(x),y),s(+(x,y))) # label(replacement).  [assumption].
kept:      11 ->*_s0(x,x) # label(reflexivity).  [assumption].
kept:      12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(4)].
kept:      13 -->*_s0(+(s(x),y),s(y)) # label(goal) # answer(goal).  [deny(5)].

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
6 -->_s0(x,y) | ->_s0(+(x,z),+(y,z)) # label(congruence).  [clausify(1)].
7 -->_s0(x,y) | ->_s0(+(z,x),+(z,y)) # label(congruence).  [clausify(2)].
8 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(3)].
9 ->_s0(+(0,x),x) # label(replacement).  [assumption].
10 ->_s0(+(s(x),y),s(+(x,y))) # label(replacement).  [assumption].
11 ->*_s0(x,x) # label(reflexivity).  [assumption].
12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(4)].
13 -->*_s0(+(s(x),y),s(y)) # label(goal) # answer(goal).  [deny(5)].
end_of_list.

formulas(demodulators).
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

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

given #4 (I,wt=5): 9 ->_s0(+(0,x),x) # label(replacement).  [assumption].

given #5 (I,wt=9): 10 ->_s0(+(s(x),y),s(+(x,y))) # label(replacement).  [assumption].

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

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

given #8 (I,wt=7): 13 -->*_s0(+(s(x),y),s(y)) # label(goal) # answer(goal).  [deny(5)].

given #9 (A,wt=7): 14 ->_s0(s(+(0,x)),s(x)).  [ur(8,a,9,a)].

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

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

3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
4 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
5 (exists x4 exists x5 ->*_s0(+(s(x4),x5),s(x5))) # label(goal) # label(non_clause) # label(goal).  [goal].
8 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(3)].
9 ->_s0(+(0,x),x) # label(replacement).  [assumption].
10 ->_s0(+(s(x),y),s(+(x,y))) # label(replacement).  [assumption].
11 ->*_s0(x,x) # label(reflexivity).  [assumption].
12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(4)].
13 -->*_s0(+(s(x),y),s(y)) # label(goal) # answer(goal).  [deny(5)].
14 ->_s0(s(+(0,x)),s(x)).  [ur(8,a,9,a)].
24 -->*_s0(s(+(x,y)),s(y)) # answer(goal).  [ur(12,a,10,a,c,13,a)].
25 ->*_s0(s(+(0,x)),s(x)).  [ur(12,a,14,a,b,11,a)].
26 $F # answer(goal).  [resolve(25,a,24,a)].

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

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

Given=9. Generated=20. Kept=20. proofs=1.
Usable=9. Sos=10. Demods=0. Limbo=0, Disabled=8. 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=1. Nonunit_bsub_feature_tests=9.
Megabytes=0.07.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3413439 exit (max_proofs) Tue Jul 30 09:47:55 2024


The problem is feasible.