NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y ys vNonEmpty x x1 x2) (STRATEGY CONTEXTSENSITIVE (cons 1 2) (lt 1 2) (0) (fSNonEmpty) (false) (s 1) (true) ) (RULES cons(x,cons(y,ys)) -> cons(y,cons(x,ys)) | lt(x,y) ->* true lt(0,s(y)) -> true lt(s(x),s(y)) -> lt(x,y) lt(x,0) -> false ) ] Infeasibility Conditions: lt(x,x1) ->* true, lt(x1,x2) ->* true Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 3344595 was started by sandbox on z020.star.cs.uiowa.edu, Tue Jul 30 09:31:10 2024 The command was "./prover9 -f /tmp/prover93344585-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover93344585-0.in assign(max_seconds,20). formulas(assumptions). ->_s0(x1,y) -> ->_s0(cons(x1,x2),cons(y,x2)) # label(congruence). ->_s0(x2,y) -> ->_s0(cons(x1,x2),cons(x1,y)) # label(congruence). ->_s0(x1,y) -> ->_s0(lt(x1,x2),lt(y,x2)) # label(congruence). ->_s0(x2,y) -> ->_s0(lt(x1,x2),lt(x1,y)) # label(congruence). ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). ->*_s0(lt(x1,x2),true) -> ->_s0(cons(x1,cons(x2,x3)),cons(x2,cons(x1,x3))) # label(replacement). ->_s0(lt(0,s(x2)),true) # label(replacement). ->_s0(lt(s(x1),s(x2)),lt(x1,x2)) # label(replacement). ->_s0(lt(x1,0),false) # label(replacement). ->*_s0(x,x) # label(reflexivity). ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). end_of_list. formulas(goals). (exists x5 exists x6 exists x7 (->*_s0(lt(x5,x6),true) & ->*_s0(lt(x6,x7),true))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 ->_s0(x1,y) -> ->_s0(cons(x1,x2),cons(y,x2)) # label(congruence) # label(non_clause). [assumption]. 2 ->_s0(x2,y) -> ->_s0(cons(x1,x2),cons(x1,y)) # label(congruence) # label(non_clause). [assumption]. 3 ->_s0(x1,y) -> ->_s0(lt(x1,x2),lt(y,x2)) # label(congruence) # label(non_clause). [assumption]. 4 ->_s0(x2,y) -> ->_s0(lt(x1,x2),lt(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 6 ->*_s0(lt(x1,x2),true) -> ->_s0(cons(x1,cons(x2,x3)),cons(x2,cons(x1,x3))) # label(replacement) # label(non_clause). [assumption]. 7 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 8 (exists x5 exists x6 exists x7 (->*_s0(lt(x5,x6),true) & ->*_s0(lt(x6,x7),true))) # 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(cons(x,z),cons(y,z)) # label(congruence). [clausify(1)]. -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(2)]. -->_s0(x,y) | ->_s0(lt(x,z),lt(y,z)) # label(congruence). [clausify(3)]. -->_s0(x,y) | ->_s0(lt(z,x),lt(z,y)) # label(congruence). [clausify(4)]. -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. -->*_s0(lt(x,y),true) | ->_s0(cons(x,cons(y,z)),cons(y,cons(x,z))) # label(replacement). [clausify(6)]. ->_s0(lt(0,s(x)),true) # label(replacement). [assumption]. ->_s0(lt(s(x),s(y)),lt(x,y)) # label(replacement). [assumption]. ->_s0(lt(x,0),false) # label(replacement). [assumption]. ->*_s0(x,x) # label(reflexivity). [assumption]. -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. -->*_s0(lt(x,y),true) | -->*_s0(lt(y,z),true) # label(goal). [deny(8)]. 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, true, false, lt, cons, s ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-6) % clear(ordered_res). % (HNE depth_diff=-6) % set(ur_resolution). % (HNE depth_diff=-6) % 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: 9 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(1)]. kept: 10 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(2)]. kept: 11 -->_s0(x,y) | ->_s0(lt(x,z),lt(y,z)) # label(congruence). [clausify(3)]. kept: 12 -->_s0(x,y) | ->_s0(lt(z,x),lt(z,y)) # label(congruence). [clausify(4)]. kept: 13 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. kept: 14 -->*_s0(lt(x,y),true) | ->_s0(cons(x,cons(y,z)),cons(y,cons(x,z))) # label(replacement). [clausify(6)]. kept: 15 ->_s0(lt(0,s(x)),true) # label(replacement). [assumption]. kept: 16 ->_s0(lt(s(x),s(y)),lt(x,y)) # label(replacement). [assumption]. kept: 17 ->_s0(lt(x,0),false) # label(replacement). [assumption]. kept: 18 ->*_s0(x,x) # label(reflexivity). [assumption]. kept: 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. kept: 20 -->*_s0(lt(x,y),true) | -->*_s0(lt(y,z),true) # label(goal) # answer(goal). [deny(8)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 9 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(1)]. 10 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(2)]. 11 -->_s0(x,y) | ->_s0(lt(x,z),lt(y,z)) # label(congruence). [clausify(3)]. 12 -->_s0(x,y) | ->_s0(lt(z,x),lt(z,y)) # label(congruence). [clausify(4)]. 13 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 14 -->*_s0(lt(x,y),true) | ->_s0(cons(x,cons(y,z)),cons(y,cons(x,z))) # label(replacement). [clausify(6)]. 15 ->_s0(lt(0,s(x)),true) # label(replacement). [assumption]. 16 ->_s0(lt(s(x),s(y)),lt(x,y)) # label(replacement). [assumption]. 17 ->_s0(lt(x,0),false) # label(replacement). [assumption]. 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 20 -->*_s0(lt(x,y),true) | -->*_s0(lt(y,z),true) # label(goal) # answer(goal). [deny(8)]. 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): 9 -->_s0(x,y) | ->_s0(cons(x,z),cons(y,z)) # label(congruence). [clausify(1)]. given #2 (I,wt=10): 10 -->_s0(x,y) | ->_s0(cons(z,x),cons(z,y)) # label(congruence). [clausify(2)]. given #3 (I,wt=10): 11 -->_s0(x,y) | ->_s0(lt(x,z),lt(y,z)) # label(congruence). [clausify(3)]. given #4 (I,wt=10): 12 -->_s0(x,y) | ->_s0(lt(z,x),lt(z,y)) # label(congruence). [clausify(4)]. given #5 (I,wt=8): 13 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. given #6 (I,wt=16): 14 -->*_s0(lt(x,y),true) | ->_s0(cons(x,cons(y,z)),cons(y,cons(x,z))) # label(replacement). [clausify(6)]. given #7 (I,wt=6): 15 ->_s0(lt(0,s(x)),true) # label(replacement). [assumption]. given #8 (I,wt=9): 16 ->_s0(lt(s(x),s(y)),lt(x,y)) # label(replacement). [assumption]. given #9 (I,wt=5): 17 ->_s0(lt(x,0),false) # label(replacement). [assumption]. given #10 (I,wt=3): 18 ->*_s0(x,x) # label(reflexivity). [assumption]. given #11 (I,wt=9): 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. given #12 (I,wt=10): 20 -->*_s0(lt(x,y),true) | -->*_s0(lt(y,z),true) # label(goal) # answer(goal). [deny(8)]. given #13 (A,wt=8): 21 ->_s0(s(lt(0,s(x))),s(true)). [ur(13,a,15,a)]. given #14 (F,wt=13): 39 -->*_s0(lt(x,y),true) | -->_s0(lt(z,x),u) | -->*_s0(u,true) # answer(goal). [resolve(20,a,19,c)]. given #15 (F,wt=6): 50 -->*_s0(lt(s(x),y),true) # answer(goal). [resolve(39,b,15,a),unit_del(b,18)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.01) seconds: goal. % Length of proof is 12. % Level of proof is 5. % Maximum clause weight is 13.000. % Given clauses 15. 7 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 8 (exists x5 exists x6 exists x7 (->*_s0(lt(x5,x6),true) & ->*_s0(lt(x6,x7),true))) # label(goal) # label(non_clause) # label(goal). [goal]. 15 ->_s0(lt(0,s(x)),true) # label(replacement). [assumption]. 16 ->_s0(lt(s(x),s(y)),lt(x,y)) # label(replacement). [assumption]. 18 ->*_s0(x,x) # label(reflexivity). [assumption]. 19 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 20 -->*_s0(lt(x,y),true) | -->*_s0(lt(y,z),true) # label(goal) # answer(goal). [deny(8)]. 38 ->*_s0(lt(0,s(x)),true). [ur(19,a,15,a,b,18,a)]. 39 -->*_s0(lt(x,y),true) | -->_s0(lt(z,x),u) | -->*_s0(u,true) # answer(goal). [resolve(20,a,19,c)]. 50 -->*_s0(lt(s(x),y),true) # answer(goal). [resolve(39,b,15,a),unit_del(b,18)]. 57 -->*_s0(lt(x,y),true) # answer(goal). [ur(19,a,16,a,c,50,a)]. 58 $F # answer(goal). [resolve(57,a,38,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=15. Generated=51. Kept=49. proofs=1. Usable=15. Sos=29. Demods=0. Limbo=3, Disabled=13. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=2. Back_subsumed=1. 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=18. Nonunit_bsub_feature_tests=35. Megabytes=0.14. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3344595 exit (max_proofs) Tue Jul 30 09:31:10 2024 The problem is feasible.