%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:38:06 PM UTC 2026 % Result : Unsatisfiable 18.94s 19.22s % Output : Refutation 18.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.34 % Computer : n017.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Wed Apr 29 01:24:27 EDT 2026 % 0.17/0.34 % CPUTime : % 18.94/19.22 ============================== Prover9 =============================== % 18.94/19.22 Prover9 (32) version 2009-11A, November 2009. % 18.94/19.22 Process 7533 was started by sandbox2 on n017.cluster.edu, % 18.94/19.22 Wed Apr 29 01:24:28 2026 % 18.94/19.22 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_7380_n017.cluster.edu". % 18.94/19.22 ============================== end of head =========================== % 18.94/19.22 % 18.94/19.22 ============================== INPUT ================================= % 18.94/19.22 % 18.94/19.22 % Reading from file /tmp/Prover9_7380_n017.cluster.edu % 18.94/19.22 % 18.94/19.22 set(prolog_style_variables). % 18.94/19.22 set(auto2). % 18.94/19.22 % set(auto2) -> set(auto). % 18.94/19.22 % set(auto) -> set(auto_inference). % 18.94/19.22 % set(auto) -> set(auto_setup). % 18.94/19.22 % set(auto_setup) -> set(predicate_elim). % 18.94/19.22 % set(auto_setup) -> assign(eq_defs, unfold). % 18.94/19.22 % set(auto) -> set(auto_limits). % 18.94/19.22 % set(auto_limits) -> assign(max_weight, "100.000"). % 18.94/19.22 % set(auto_limits) -> assign(sos_limit, 20000). % 18.94/19.22 % set(auto) -> set(auto_denials). % 18.94/19.22 % set(auto) -> set(auto_process). % 18.94/19.22 % set(auto2) -> assign(new_constants, 1). % 18.94/19.22 % set(auto2) -> assign(fold_denial_max, 3). % 18.94/19.22 % set(auto2) -> assign(max_weight, "200.000"). % 18.94/19.22 % set(auto2) -> assign(max_hours, 1). % 18.94/19.22 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 18.94/19.22 % set(auto2) -> assign(max_seconds, 0). % 18.94/19.22 % set(auto2) -> assign(max_minutes, 5). % 18.94/19.22 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 18.94/19.22 % set(auto2) -> set(sort_initial_sos). % 18.94/19.22 % set(auto2) -> assign(sos_limit, -1). % 18.94/19.22 % set(auto2) -> assign(lrs_ticks, 3000). % 18.94/19.22 % set(auto2) -> assign(max_megs, 400). % 18.94/19.22 % set(auto2) -> assign(stats, some). % 18.94/19.22 % set(auto2) -> clear(echo_input). % 18.94/19.22 % set(auto2) -> set(quiet). % 18.94/19.22 % set(auto2) -> clear(print_initial_clauses). % 18.94/19.22 % set(auto2) -> clear(print_given). % 18.94/19.22 assign(lrs_ticks,-1). % 18.94/19.22 assign(sos_limit,10000). % 18.94/19.22 assign(order,kbo). % 18.94/19.22 set(lex_order_vars). % 18.94/19.22 clear(print_given). % 18.94/19.22 % 18.94/19.22 % formulas(sos). % not echoed (91 formulas) % 18.94/19.22 % 18.94/19.22 ============================== end of input ========================== % 18.94/19.22 % 18.94/19.22 % From the command line: assign(max_seconds, 300). % 18.94/19.22 % 18.94/19.22 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 18.94/19.22 % 18.94/19.22 % Formulas that are not ordinary clauses: % 18.94/19.22 % 18.94/19.22 ============================== end of process non-clausal formulas === % 18.94/19.22 % 18.94/19.22 ============================== PROCESS INITIAL CLAUSES =============== % 18.94/19.22 % 18.94/19.22 ============================== PREDICATE ELIMINATION ================= % 18.94/19.22 % 18.94/19.22 ============================== end predicate elimination ============= % 18.94/19.22 % 18.94/19.22 Auto_denials: % 18.94/19.22 % copying label goal to answer in negative clause % 18.94/19.22 % 18.94/19.22 Term ordering decisions: % 18.94/19.22 Function symbol KB weights: eps=1. nil2=1. bfalse=1. btrue=1. a=1. b=1. c=1. nil=1. x=1. y=1. x2=1. z=1. step=1. eq=1. rec=1. eq2=1. andb=1. orb=1. cons=1. star=1. atom=1. eps2=1. aux=1. prop_koen=1. aux2=1. % 18.94/19.22 % 18.94/19.22 ============================== end of process initial clauses ======== % 18.94/19.22 % 18.94/19.22 ============================== CLAUSES FOR SEARCH ==================== % 18.94/19.22 % 18.94/19.22 ============================== end of clauses for search ============= % 18.94/19.22 % 18.94/19.22 ============================== SEARCH ================================ % 18.94/19.22 % 18.94/19.22 % Starting search at 0.02 seconds. % 18.94/19.22 % 18.94/19.22 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 1385 (0.00 of 0.37 sec). % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=25.000, iters=3420 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=23.000, iters=3402 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=22.000, iters=3354 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=21.000, iters=3334 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=20.000, iters=3357 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=19.000, iters=3334 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=11446, wt=44.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=11546, wt=42.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=10003, wt=41.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=10853, wt=39.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=10774, wt=38.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=11527, wt=36.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=10782, wt=35.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=4953, wt=27.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=5134, wt=26.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=4937, wt=25.000 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=18.000, iters=3364 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=17045, wt=24.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=17442, wt=17.000 % 18.94/19.22 % 18.94/19.22 Low Water (displace): id=18938, wt=16.000 % 18.94/19.22 % 18.94/19.22 Low Water (keep): wt=17.000, iters=3335 % 18.94/19.22 % 18.94/19.22 ============================== PROOF ================================= % 18.94/19.22 % SZS status Unsatisfiable % 18.94/19.22 % SZS output start Refutation % 18.94/19.22 % 18.94/19.22 % Proof 1 at 17.82 (+ 0.39) seconds: goal. % 18.94/19.22 % Length of proof is 124. % 18.94/19.22 % Level of proof is 17. % 18.94/19.22 % Maximum clause weight is 22.000. % 18.94/19.22 % Given clauses 5576. % 18.94/19.22 % 18.94/19.22 1 eps2(eps) = btrue # label(axiom_065) # label(axiom). [assumption]. % 18.94/19.22 2 btrue = eps2(eps). [copy(1),flip(a)]. % 18.94/19.22 3 eps2(nil2) = bfalse # label(axiom_069) # label(axiom). [assumption]. % 18.94/19.22 4 bfalse = eps2(nil2). [copy(3),flip(a)]. % 18.94/19.22 9 orb(btrue,A) = btrue # label(axiom_061) # label(axiom). [assumption]. % 18.94/19.22 10 orb(eps2(eps),A) = eps2(eps). [copy(9),rewrite([2(1),2(4)])]. % 18.94/19.22 11 orb(bfalse,A) = A # label(axiom_062) # label(axiom). [assumption]. % 18.94/19.22 12 orb(eps2(nil2),A) = A. [copy(11),rewrite([4(1)])]. % 18.94/19.22 15 andb(bfalse,A) = bfalse # label(axiom_064) # label(axiom). [assumption]. % 18.94/19.22 16 andb(eps2(nil2),A) = eps2(nil2). [copy(15),rewrite([4(1),4(4)])]. % 18.94/19.22 19 eps2(atom(A)) = bfalse # label(axiom_070) # label(axiom). [assumption]. % 18.94/19.22 20 eps2(atom(A)) = eps2(nil2). [copy(19),rewrite([4(3)])]. % 18.94/19.22 21 step(nil2,A) = nil2 # label(axiom_075) # label(axiom). [assumption]. % 18.94/19.22 22 step(eps,A) = nil2 # label(axiom_076) # label(axiom). [assumption]. % 18.94/19.22 23 eq(a,b) = bfalse # label(axiom_080) # label(axiom). [assumption]. % 18.94/19.22 24 eq(a,b) = eps2(nil2). [copy(23),rewrite([4(4)])]. % 18.94/19.22 25 eq(a,c) = bfalse # label(axiom_081) # label(axiom). [assumption]. % 18.94/19.22 26 eq(a,c) = eps2(nil2). [copy(25),rewrite([4(4)])]. % 18.94/19.22 27 eq(b,a) = bfalse # label(axiom_082) # label(axiom). [assumption]. % 18.94/19.22 28 eq(b,a) = eps2(nil2). [copy(27),rewrite([4(4)])]. % 18.94/19.22 29 eq(b,c) = bfalse # label(axiom_083) # label(axiom). [assumption]. % 18.94/19.22 30 eq(b,c) = eps2(nil2). [copy(29),rewrite([4(4)])]. % 18.94/19.22 31 eq(c,a) = bfalse # label(axiom_084) # label(axiom). [assumption]. % 18.94/19.22 32 eq(c,a) = eps2(nil2). [copy(31),rewrite([4(4)])]. % 18.94/19.22 33 eq(c,b) = bfalse # label(axiom_085) # label(axiom). [assumption]. % 18.94/19.22 34 eq(c,b) = eps2(nil2). [copy(33),rewrite([4(4)])]. % 18.94/19.22 35 eq2(bfalse,btrue) = bfalse # label(axiom_086) # label(axiom). [assumption]. % 18.94/19.22 36 eq2(eps2(nil2),eps2(eps)) = eps2(nil2). [copy(35),rewrite([4(1),2(3),4(6)])]. % 18.94/19.22 39 eq(A,A) = btrue # label(axiom_088) # label(axiom). [assumption]. % 18.94/19.22 40 eq(A,A) = eps2(eps). [copy(39),rewrite([2(2)])]. % 18.94/19.22 41 eq2(A,A) = btrue # label(axiom_089) # label(axiom). [assumption]. % 18.94/19.22 42 eq2(A,A) = eps2(eps). [copy(41),rewrite([2(2)])]. % 18.94/19.22 43 aux(A,B,btrue) = eps # label(axiom) # label(axiom). [assumption]. % 18.94/19.22 44 aux(A,B,eps2(eps)) = eps. [copy(43),rewrite([2(1)])]. % 18.94/19.22 45 aux(A,B,bfalse) = nil2 # label(axiom_001) # label(axiom). [assumption]. % 18.94/19.22 46 aux(A,B,eps2(nil2)) = nil2. [copy(45),rewrite([4(1)])]. % 18.94/19.22 49 rec(A,nil) = eps2(A) # label(axiom_077) # label(axiom). [assumption]. % 18.94/19.22 50 eps2(A) = rec(A,nil). [copy(49),flip(a)]. % 18.94/19.22 66 eps2(x(A,B)) = orb(eps2(A),eps2(B)) # label(axiom_066) # label(axiom). [assumption]. % 18.94/19.22 67 orb(rec(A,nil),rec(B,nil)) = rec(x(A,B),nil). [copy(66),rewrite([50(2),50(4),50(6)]),flip(a)]. % 18.94/19.22 68 eps2(y(A,B)) = andb(eps2(A),eps2(B)) # label(axiom_067) # label(axiom). [assumption]. % 18.94/19.22 69 andb(rec(A,nil),rec(B,nil)) = rec(y(A,B),nil). [copy(68),rewrite([50(2),50(4),50(6)]),flip(a)]. % 18.94/19.22 82 step(atom(A),B) = aux(B,A,eq(A,B)) # label(axiom_071) # label(axiom). [assumption]. % 18.94/19.22 83 aux(A,B,eq(B,A)) = step(atom(B),A). [copy(82),flip(a)]. % 18.94/19.22 86 rec(A,cons(B,C)) = rec(step(A,B),C) # label(axiom_078) # label(axiom). [assumption]. % 18.94/19.22 87 rec(step(A,B),C) = rec(A,cons(B,C)). [copy(86),flip(a)]. % 18.94/19.22 88 step(y(A,B),C) = aux2(C,A,B,eps2(A)) # label(axiom_073) # label(axiom). [assumption]. % 18.94/19.22 89 aux2(A,B,C,rec(B,nil)) = step(y(B,C),A). [copy(88),rewrite([50(3)]),flip(a)]. % 18.94/19.22 90 aux2(A,B,C,bfalse) = x(y(step(B,A),C),nil2) # label(axiom_003) # label(axiom). [assumption]. % 18.94/19.22 91 aux2(A,B,C,rec(nil2,nil)) = x(y(step(B,A),C),nil2). [copy(90),rewrite([4(1),50(2)])]. % 18.94/19.22 108 step(x(A,B),C) = x(step(A,C),step(B,C)) # label(axiom_072) # label(axiom). [assumption]. % 18.94/19.22 109 x(step(A,B),step(C,B)) = step(x(A,C),B). [copy(108),flip(a)]. % 18.94/19.22 110 aux2(A,B,C,btrue) = x(y(step(B,A),C),step(C,A)) # label(axiom_002) # label(axiom). [assumption]. % 18.94/19.22 111 x(y(step(A,B),C),step(C,B)) = aux2(B,A,C,rec(eps,nil)). [copy(110),rewrite([2(1),50(2)]),flip(a)]. % 18.94/19.22 120 prop_koen(A,B,C) = eq2(rec(y(A,B),C),rec(y(B,A),C)) # label(axiom_079) # label(axiom). [assumption]. % 18.94/19.22 121 eq2(prop_koen(A,B,C),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 18.94/19.22 122 eq2(eq2(rec(y(A,B),C),rec(y(B,A),C)),rec(nil2,nil)) != rec(eps,nil) # answer(goal). [copy(121),rewrite([120(1),4(6),50(7),2(10),50(11)])]. % 18.94/19.22 123 aux(A,B,rec(nil2,nil)) = nil2. [back_rewrite(46),rewrite([50(2)])]. % 18.94/19.22 124 aux(A,B,rec(eps,nil)) = eps. [back_rewrite(44),rewrite([50(2)])]. % 18.94/19.22 125 eq2(A,A) = rec(eps,nil). [back_rewrite(42),rewrite([50(3)])]. % 18.94/19.22 126 rec(eps,nil) = eq(A,A). [back_rewrite(40),rewrite([50(3)]),flip(a)]. % 18.94/19.22 128 eq2(rec(nil2,nil),rec(eps,nil)) = rec(nil2,nil). [back_rewrite(36),rewrite([50(2),50(5),50(9)])]. % 18.94/19.22 129 rec(nil2,nil) = eq(c,b). [back_rewrite(34),rewrite([50(5)]),flip(a)]. % 18.94/19.22 130 eq(c,b) = eq(c,a). [back_rewrite(32),rewrite([50(5),129(6)]),flip(a)]. % 18.94/19.22 131 eq(c,a) = eq(b,c). [back_rewrite(30),rewrite([50(5),129(6),130(6)]),flip(a)]. % 18.94/19.22 132 eq(b,c) = eq(b,a). [back_rewrite(28),rewrite([50(5),129(6),130(6),131(6)]),flip(a)]. % 18.94/19.22 133 eq(b,a) = eq(a,c). [back_rewrite(26),rewrite([50(5),129(6),130(6),131(6),132(6)]),flip(a)]. % 18.94/19.22 134 eq(a,c) = eq(a,b). [back_rewrite(24),rewrite([50(5),129(6),130(6),131(6),132(6),133(6)]),flip(a)]. % 18.94/19.22 135 rec(atom(A),nil) = eq(a,b). [back_rewrite(20),rewrite([50(2),50(5),129(6),130(6),131(6),132(6),133(6),134(6)])]. % 18.94/19.22 137 andb(eq(a,b),A) = eq(a,b). [back_rewrite(16),rewrite([50(2),129(3),130(3),131(3),132(3),133(3),134(3),50(6),129(7),130(7),131(7),132(7),133(7),134(7)])]. % 18.94/19.22 139 orb(eq(a,b),A) = A. [back_rewrite(12),rewrite([50(2),129(3),130(3),131(3),132(3),133(3),134(3)])]. % 18.94/19.22 140 orb(rec(eps,nil),A) = rec(eps,nil). [back_rewrite(10),rewrite([50(2),50(6)])]. % 18.94/19.22 143 eq2(eq(a,b),rec(eps,nil)) = eq(a,b). [back_rewrite(128),rewrite([129(3),130(3),131(3),132(3),133(3),134(3),129(10),130(10),131(10),132(10),133(10),134(10)])]. % 18.94/19.22 145 aux(A,B,eq(a,b)) = nil2. [back_rewrite(123),rewrite([129(3),130(3),131(3),132(3),133(3),134(3)])]. % 18.94/19.22 146 eq2(eq2(rec(y(A,B),C),rec(y(B,A),C)),eq(a,b)) != rec(eps,nil) # answer(goal). [back_rewrite(122),rewrite([129(8),130(8),131(8),132(8),133(8),134(8)])]. % 18.94/19.22 147 aux2(A,B,C,eq(a,b)) = x(y(step(B,A),C),nil2). [back_rewrite(91),rewrite([129(3),130(3),131(3),132(3),133(3),134(3)])]. % 18.94/19.22 148 rec(nil2,nil) = eq(a,b). [back_rewrite(129),rewrite([130(6),131(6),132(6),133(6),134(6)])]. % 18.94/19.22 161 rec(nil2,cons(A,B)) = rec(nil2,B). [para(21(a,1),87(a,1,1)),flip(a)]. % 18.94/19.22 163 orb(rec(A,cons(B,nil)),rec(C,nil)) = rec(x(step(A,B),C),nil). [para(87(a,1),67(a,1,1))]. % 18.94/19.22 179 step(x(A,nil2),B) = x(step(A,B),nil2). [para(21(a,1),109(a,1,2)),flip(a)]. % 18.94/19.22 181 step(x(A,eps),B) = x(step(A,B),nil2). [para(22(a,1),109(a,1,2)),flip(a)]. % 18.94/19.22 198 x(y(nil2,A),step(A,B)) = step(y(eps,A),B). [para(22(a,1),111(a,1,1,1)),rewrite([89(9)])]. % 18.94/19.22 239 orb(eq2(A,A),rec(B,nil)) = rec(x(eps,B),nil). [para(125(a,2),67(a,1,1))]. % 18.94/19.22 245 aux(A,B,eq2(C,C)) = eps. [para(125(a,2),124(a,1,3))]. % 18.94/19.22 246 eq2(A,A) = eq2(B,B). [para(125(a,2),125(a,2))]. % 18.94/19.22 247 eq2(A,A) = c_0. [new_symbol(246)]. % 18.94/19.22 248 aux(A,B,c_0) = eps. [back_rewrite(245),rewrite([247(1)])]. % 18.94/19.22 254 orb(c_0,rec(A,nil)) = rec(x(eps,A),nil). [back_rewrite(239),rewrite([247(1)])]. % 18.94/19.22 255 rec(eps,nil) = c_0. [back_rewrite(125),rewrite([247(1)]),flip(a)]. % 18.94/19.22 282 eq2(eq2(rec(y(A,B),C),rec(y(B,A),C)),eq(a,b)) != c_0 # answer(goal). [back_rewrite(146),rewrite([255(12)])]. % 18.94/19.22 284 eq2(eq(a,b),c_0) = eq(a,b). [back_rewrite(143),rewrite([255(6)])]. % 18.94/19.22 286 orb(c_0,A) = c_0. [back_rewrite(140),rewrite([255(3),255(5)])]. % 18.94/19.22 289 eq(A,A) = c_0. [back_rewrite(126),rewrite([255(3)]),flip(a)]. % 18.94/19.22 290 rec(x(eps,A),nil) = c_0. [back_rewrite(254),rewrite([286(4)]),flip(a)]. % 18.94/19.22 292 step(atom(a),c) = nil2. [para(134(a,1),83(a,1,3)),rewrite([145(6)]),flip(a)]. % 18.94/19.22 294 rec(x(A,atom(B)),nil) = orb(rec(A,nil),eq(a,b)). [para(135(a,1),67(a,1,2)),flip(a)]. % 18.94/19.22 297 x(y(step(atom(A),B),C),nil2) = step(y(atom(A),C),B). [para(135(a,1),89(a,1,4)),rewrite([147(5)])]. % 18.94/19.22 300 orb(rec(A,nil),eq(a,b)) = rec(x(A,nil2),nil). [para(148(a,1),67(a,1,2))]. % 18.94/19.22 301 rec(y(nil2,A),nil) = eq(a,b). [para(148(a,1),69(a,1,1)),rewrite([137(6)]),flip(a)]. % 18.94/19.22 303 x(y(nil2,A),nil2) = step(y(nil2,A),B). [para(148(a,1),89(a,1,4)),rewrite([147(5),21(2)])]. % 18.94/19.22 304 rec(x(A,atom(B)),nil) = rec(x(A,nil2),nil). [back_rewrite(294),rewrite([300(10)])]. % 18.94/19.22 377 step(atom(A),A) = eps. [para(289(a,1),83(a,1,3)),rewrite([248(2)]),flip(a)]. % 18.94/19.22 425 step(x(atom(A),B),A) = x(eps,step(B,A)). [para(377(a,1),109(a,1,1)),flip(a)]. % 18.94/19.22 479 orb(rec(A,cons(B,nil)),eq(a,b)) = rec(x(step(A,B),nil2),nil). [para(135(a,1),163(a,1,2)),rewrite([304(12)])]. % 18.94/19.22 561 rec(x(step(A,B),nil2),C) = rec(x(A,nil2),cons(B,C)). [para(179(a,1),87(a,1,1))]. % 18.94/19.22 572 orb(rec(A,cons(B,nil)),eq(a,b)) = rec(x(A,nil2),cons(B,nil)). [back_rewrite(479),rewrite([561(12)])]. % 18.94/19.22 610 rec(x(A,nil2),cons(B,C)) = rec(x(A,eps),cons(B,C)). [para(181(a,1),87(a,1,1)),rewrite([561(4)])]. % 18.94/19.22 618 orb(rec(A,cons(B,nil)),eq(a,b)) = rec(x(A,eps),cons(B,nil)). [back_rewrite(572),rewrite([610(12)])]. % 18.94/19.22 639 rec(y(nil2,A),cons(B,nil)) = eq(a,b). [para(303(a,1),67(a,2,1)),rewrite([301(4),148(6),139(7),87(8)]),flip(a)]. % 18.94/19.22 698 step(y(nil2,A),B) = step(y(nil2,A),C). [para(303(a,1),303(a,1))]. % 18.94/19.22 934 rec(x(step(y(nil2,A),B),C),nil) = rec(C,nil). [para(639(a,1),163(a,1,1)),rewrite([139(6)]),flip(a)]. % 18.94/19.22 947 x(step(y(nil2,A),B),step(C,D)) = step(x(y(nil2,A),C),D). [para(698(a,1),109(a,1,1))]. % 18.94/19.22 1131 rec(x(atom(A),B),cons(A,C)) = rec(x(eps,step(B,A)),C). [para(425(a,1),87(a,1,1)),flip(a)]. % 18.94/19.22 1278 rec(y(eps,A),cons(B,nil)) = rec(A,cons(B,nil)). [para(198(a,1),67(a,2,1)),rewrite([301(4),87(6),139(7),87(8)]),flip(a)]. % 18.94/19.22 3685 rec(x(y(nil2,A),B),cons(C,nil)) = rec(B,cons(C,nil)). [para(87(a,1),934(a,2)),rewrite([947(5),87(6)])]. % 18.94/19.22 5207 step(y(atom(a),A),c) = x(y(nil2,A),nil2). [para(292(a,1),297(a,1,1,1)),flip(a)]. % 18.94/19.22 5213 step(y(atom(A),B),A) = x(y(eps,B),nil2). [para(377(a,1),297(a,1,1,1)),flip(a)]. % 18.94/19.22 5336 rec(y(atom(a),A),cons(c,B)) = rec(x(y(nil2,A),nil2),B). [para(5207(a,1),87(a,1,1)),flip(a)]. % 18.94/19.22 5489 rec(y(atom(A),B),cons(A,C)) = rec(x(y(eps,B),nil2),C). [para(5213(a,1),87(a,1,1)),flip(a)]. % 18.94/19.22 10854 rec(x(y(eps,A),eps),cons(B,nil)) = rec(x(A,eps),cons(B,nil)). [para(1278(a,1),618(a,1,1)),rewrite([618(7)]),flip(a)]. % 18.94/19.22 22732 eq2(eq2(rec(x(y(nil2,A),nil2),B),rec(y(A,atom(a)),cons(c,B))),eq(a,b)) != c_0 # answer(goal). [para(5336(a,1),282(a,1,1,1))]. % 18.94/19.22 23551 eq2(eq2(eq(a,b),rec(y(A,atom(a)),cons(c,cons(B,nil)))),eq(a,b)) != c_0 # answer(goal). [para(3685(a,1),22732(a,1,1,1)),rewrite([161(4),148(3)])]. % 18.94/19.22 23555 eq2(eq2(eq(a,b),rec(x(atom(a),eps),cons(A,nil))),eq(a,b)) != c_0 # answer(goal). [para(5489(a,1),23551(a,1,1,2)),rewrite([610(12),10854(12)])]. % 18.94/19.22 23556 $F # answer(goal). [para(1131(a,1),23555(a,1,1,2)),rewrite([22(7),290(8),284(5),247(7)]),xx(a)]. % 18.94/19.22 % 18.94/19.22 % SZS output end Refutation % 18.94/19.22 ============================== end of proof ========================== % 18.94/19.22 % 18.94/19.22 ============================== STATISTICS ============================ % 18.94/19.22 % 18.94/19.22 Given=5576. Generated=658778. Kept=23524. proofs=1. % 18.94/19.22 Usable=4793. Sos=9825. Demods=6355. Limbo=0, Disabled=8997. Hints=0. % 18.94/19.22 Megabytes=26.19. % 18.94/19.22 User_CPU=17.82, System_CPU=0.39, Wall_clock=18. % 18.94/19.22 % 18.94/19.22 ============================== end of statistics ===================== % 18.94/19.22 % 18.94/19.22 ============================== end of search ========================= % 18.94/19.22 % 18.94/19.22 THEOREM PROVED % 18.94/19.22 % SZS status Unsatisfiable % 18.94/19.22 % 18.94/19.22 Exiting with 1 proof. % 18.94/19.22 % 18.94/19.22 Process 7533 exit (max_proofs) Wed Apr 29 01:24:46 2026 % 18.94/19.22 Prover9 interrupted %------------------------------------------------------------------------------