%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX207+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n001.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:05 PM UTC 2026 % Result : Theorem 0.75s 1.05s % Output : Refutation 0.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX207+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.33 % Computer : n001.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Wed Apr 29 00:59:48 EDT 2026 % 0.17/0.34 % CPUTime : % 0.75/1.04 ============================== Prover9 =============================== % 0.75/1.04 Prover9 (32) version 2009-11A, November 2009. % 0.75/1.04 Process 21384 was started by sandbox2 on n001.cluster.edu, % 0.75/1.04 Wed Apr 29 00:59:49 2026 % 0.75/1.04 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_21027_n001.cluster.edu". % 0.75/1.04 ============================== end of head =========================== % 0.75/1.04 % 0.75/1.04 ============================== INPUT ================================= % 0.75/1.04 % 0.75/1.04 % Reading from file /tmp/Prover9_21027_n001.cluster.edu % 0.75/1.04 % 0.75/1.04 set(prolog_style_variables). % 0.75/1.04 set(auto2). % 0.75/1.04 % set(auto2) -> set(auto). % 0.75/1.04 % set(auto) -> set(auto_inference). % 0.75/1.04 % set(auto) -> set(auto_setup). % 0.75/1.04 % set(auto_setup) -> set(predicate_elim). % 0.75/1.04 % set(auto_setup) -> assign(eq_defs, unfold). % 0.75/1.04 % set(auto) -> set(auto_limits). % 0.75/1.04 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.75/1.04 % set(auto_limits) -> assign(sos_limit, 20000). % 0.75/1.04 % set(auto) -> set(auto_denials). % 0.75/1.04 % set(auto) -> set(auto_process). % 0.75/1.04 % set(auto2) -> assign(new_constants, 1). % 0.75/1.04 % set(auto2) -> assign(fold_denial_max, 3). % 0.75/1.04 % set(auto2) -> assign(max_weight, "200.000"). % 0.75/1.04 % set(auto2) -> assign(max_hours, 1). % 0.75/1.04 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.75/1.04 % set(auto2) -> assign(max_seconds, 0). % 0.75/1.04 % set(auto2) -> assign(max_minutes, 5). % 0.75/1.04 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.75/1.04 % set(auto2) -> set(sort_initial_sos). % 0.75/1.04 % set(auto2) -> assign(sos_limit, -1). % 0.75/1.04 % set(auto2) -> assign(lrs_ticks, 3000). % 0.75/1.04 % set(auto2) -> assign(max_megs, 400). % 0.75/1.04 % set(auto2) -> assign(stats, some). % 0.75/1.04 % set(auto2) -> clear(echo_input). % 0.75/1.04 % set(auto2) -> set(quiet). % 0.75/1.04 % set(auto2) -> clear(print_initial_clauses). % 0.75/1.04 % set(auto2) -> clear(print_given). % 0.75/1.04 assign(lrs_ticks,-1). % 0.75/1.04 assign(sos_limit,10000). % 0.75/1.04 assign(order,kbo). % 0.75/1.04 set(lex_order_vars). % 0.75/1.04 clear(print_given). % 0.75/1.04 % 0.75/1.04 % formulas(sos). % not echoed (27 formulas) % 0.75/1.04 % 0.75/1.04 ============================== end of input ========================== % 0.75/1.04 % 0.75/1.04 % From the command line: assign(max_seconds, 300). % 0.75/1.04 % 0.75/1.04 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.75/1.04 % 0.75/1.04 % Formulas that are not ordinary clauses: % 0.75/1.04 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 4 (all X proj1AP(aP(X)) = X) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 5 (all X proj1BP(bP(X)) = X) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 6 (all X all X2 aP(X) != bP(X2)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 7 (all X aP(X) != pA) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 8 (all X aP(X) != pB) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 9 (all X aP(X) != pE) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 10 (all X bP(X) != pA) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 11 (all X bP(X) != pB) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 12 (all X bP(X) != pE) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 14 (all X all X2 proj2C(c2(X,X2)) = X2) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 18 (all Q linP(bP(Q)) = append(cons(b,nil),append(linP(Q),cons(b,nil)))) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.04 19 (all P all Q linC(c2(P,Q)) = append(l % 0.75/1.04 WARNING: denials share constants (see output). % 0.75/1.04 % 0.75/1.05 inP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.05 % 0.75/1.05 ============================== end of process non-clausal formulas === % 0.75/1.05 % 0.75/1.05 ============================== PROCESS INITIAL CLAUSES =============== % 0.75/1.05 % 0.75/1.05 ============================== PREDICATE ELIMINATION ================= % 0.75/1.05 % 0.75/1.05 ============================== end predicate elimination ============= % 0.75/1.05 % 0.75/1.05 Auto_denials: % 0.75/1.05 % copying label axiom_004 to answer in negative clause % 0.75/1.05 % copying label axiom_014 to answer in negative clause % 0.75/1.05 % copying label axiom_015 to answer in negative clause % 0.75/1.05 % copying label axiom_016 to answer in negative clause % 0.75/1.05 % copying label axiom_008 to answer in negative clause % 0.75/1.05 % copying label axiom_009 to answer in negative clause % 0.75/1.05 % copying label axiom_010 to answer in negative clause % 0.75/1.05 % copying label axiom_011 to answer in negative clause % 0.75/1.05 % copying label axiom_012 to answer in negative clause % 0.75/1.05 % copying label axiom_013 to answer in negative clause % 0.75/1.05 % copying label axiom_003 to answer in negative clause % 0.75/1.05 % copying label axiom_007 to answer in negative clause % 0.75/1.05 % assign(max_proofs, 12). % (Horn set with more than one neg. clause) % 0.75/1.05 % 0.75/1.05 WARNING, because some of the denials share constants, % 0.75/1.05 some of the denials or their descendents may be subsumed, % 0.75/1.05 preventing the target number of proofs from being found. % 0.75/1.05 The shared constants are: pE, pB, pA. % 0.75/1.05 % 0.75/1.05 Term ordering decisions: % 0.75/1.05 Function symbol KB weights: nil=1. a=1. b=1. pA=1. pB=1. pE=1. cons=1. append=1. c2=1. linP=1. linC=1. aP=1. bP=1. head=1. proj1AP=1. proj1BP=1. proj1C=1. proj2C=1. tail=1. % 0.75/1.05 % 0.75/1.05 ============================== end of process initial clauses ======== % 0.75/1.05 % 0.75/1.05 ============================== CLAUSES FOR SEARCH ==================== % 0.75/1.05 % 0.75/1.05 ============================== end of clauses for search ============= % 0.75/1.05 % 0.75/1.05 ============================== SEARCH ================================ % 0.75/1.05 % 0.75/1.05 % Starting search at 0.01 seconds. % 0.75/1.05 % 0.75/1.05 ============================== PROOF ================================= % 0.75/1.05 % SZS status Theorem % 0.75/1.05 % SZS output start Refutation % 0.75/1.05 % 0.75/1.05 % Proof 1 at 0.02 (+ 0.00) seconds: axiom_010. % 0.75/1.05 % Length of proof is 31. % 0.75/1.05 % Level of proof is 10. % 0.75/1.05 % Maximum clause weight is 11.000. % 0.75/1.05 % Given clauses 78. % 0.75/1.05 % 0.75/1.05 9 (all X aP(X) != pE) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.05 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.05 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.05 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.05 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.05 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.05 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.05 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.05 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.05 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.05 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.05 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.05 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.05 52 aP(A) != pE # label(axiom_010) # label(axiom) # answer(axiom_010). [clausify(9)]. % 0.75/1.05 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.05 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.05 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.05 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.05 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.05 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.05 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.05 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.05 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.05 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.05 151 $F # answer(axiom_010). [resolve(150,a,52,a)]. % 0.75/1.05 % 0.75/1.05 % SZS output end Refutation % 0.75/1.05 ============================== end of proof ========================== % 0.75/1.05 % 0.75/1.05 ============================== PROOF ================================= % 0.75/1.05 % SZS status Theorem % 0.75/1.05 % SZS output start Refutation % 0.75/1.05 % 0.75/1.05 % Proof 2 at 0.02 (+ 0.00) seconds: axiom_003. % 0.75/1.05 % Length of proof is 37. % 0.75/1.05 % Level of proof is 11. % 0.75/1.05 % Maximum clause weight is 11.000. % 0.75/1.05 % Given clauses 78. % 0.75/1.05 % 0.75/1.05 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.05 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.05 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.05 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.05 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.05 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.05 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.05 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.05 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.05 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.05 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.05 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.05 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.05 56 cons(A,B) != nil # label(axiom_003) # label(axiom) # answer(axiom_003). [clausify(3)]. % 0.75/1.05 57 cons(A,B) != linP(pE) # answer(axiom_003). [copy(56),rewrite([22(2)])]. % 0.75/1.05 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.05 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.05 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.05 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.05 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.05 89 linC(c2(pA,A)) = cons(a,linP(A)). [para(65(a,1),36(a,1)),flip(a)]. % 0.75/1.05 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.05 103 cons(a,linP(aP(pE))) = linP(aP(pA)). [para(89(a,1),67(a,1,2)),rewrite([102(5)])]. % 0.75/1.05 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.05 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.05 137 linC(c2(aP(pE),pA)) = linP(aP(pA)). [para(102(a,1),116(a,2,2)),rewrite([36(6),103(10)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 147 cons(a,linP(aP(pA))) = linP(aP(aP(pE))). [para(137(a,1),67(a,1,2))]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 152 cons(a,linP(aP(pA))) = linP(pE). [back_rewrite(147),rewrite([150(7),150(7)])]. % 0.75/1.06 153 $F # answer(axiom_003). [resolve(152,a,57,a)]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % Redundant proof: 157 $F # answer(axiom_003). [resolve(156,a,57,a)]. % 0.75/1.06 % Redundant proof: 159 $F # answer(axiom_003). [resolve(158,a,57,a)]. % 0.75/1.06 % Redundant proof: 162 $F # answer(axiom_003). [resolve(161,a,57,a)]. % 0.75/1.06 % 0.75/1.06 % Disable descendants (x means already disabled): % 0.75/1.06 56x 57 69 70 72 83 84 101 108 119 % 0.75/1.06 120 121 122 125 52 76 113 142 % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 3 at 0.03 (+ 0.00) seconds: axiom_004. % 0.75/1.06 % Length of proof is 44. % 0.75/1.06 % Level of proof is 13. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 94. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 18 (all Q linP(bP(Q)) = append(cons(b,nil),append(linP(Q),cons(b,nil)))) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 33 linP(pB) = cons(b,nil) # label(axiom_024) # label(axiom). [assumption]. % 0.75/1.06 34 cons(b,linP(pE)) = linP(pB). [copy(33),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 40 linP(bP(A)) = append(cons(b,nil),append(linP(A),cons(b,nil))) # label(axiom_022) # label(axiom). [clausify(18)]. % 0.75/1.06 41 append(linP(pB),linC(c2(A,pB))) = linP(bP(A)). [copy(40),rewrite([22(4),34(6),22(7),34(9),36(8)]),flip(a)]. % 0.75/1.06 42 a != b # label(axiom_004) # label(axiom) # answer(axiom_004). [assumption]. % 0.75/1.06 43 b != a # answer(axiom_004). [copy(42),flip(a)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 66 append(linP(pB),A) = cons(b,A). [para(34(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 68 cons(b,linC(c2(A,pB))) = linP(bP(A)). [back_rewrite(41),rewrite([66(6)])]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 105 head(linP(bP(A))) = b. [para(68(a,1),27(a,1,1))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 190 b = a. [back_rewrite(105),rewrite([186(3)]),flip(a)]. % 0.75/1.06 191 $F # answer(axiom_004). [resolve(190,a,43,a)]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % Redundant proof: 193 $F # answer(axiom_004). [resolve(192,a,43,a(flip))]. % 0.75/1.06 % Redundant proof: 207 $F # answer(axiom_004). [back_rewrite(183),rewrite([190(1)]),xx(a)]. % 0.75/1.06 % Redundant proof: 211 $F # answer(axiom_004). [back_rewrite(129),rewrite([190(1)]),xx(a)]. % 0.75/1.06 % Redundant proof: 219 $F # answer(axiom_004). [back_rewrite(91),rewrite([190(1)]),xx(a)]. % 0.75/1.06 % Redundant proof: 220 $F # answer(axiom_004). [back_rewrite(82),rewrite([190(1)]),xx(a)]. % 0.75/1.06 % Redundant proof: 223 $F # answer(axiom_004). [back_rewrite(43),rewrite([190(1)]),xx(a)]. % 0.75/1.06 % 0.75/1.06 % Disable descendants (x means already disabled): % 0.75/1.06 42x 43x 82x 91x 129x 183x % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 4 at 0.03 (+ 0.00) seconds: axiom_014. % 0.75/1.06 % Length of proof is 37. % 0.75/1.06 % Level of proof is 14. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 44 pA != pB # label(axiom_014) # label(axiom) # answer(axiom_014). [assumption]. % 0.75/1.06 45 pB != pA # answer(axiom_014). [copy(44),flip(a)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.06 243 pA != a # answer(axiom_014). [para(192(a,2),45(a,1)),flip(a)]. % 0.75/1.06 244 $F # answer(axiom_014). [resolve(243,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % Redundant proof: 246 $F # answer(axiom_014). [resolve(245,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 5 at 0.03 (+ 0.00) seconds: axiom_015. % 0.75/1.06 % Length of proof is 37. % 0.75/1.06 % Level of proof is 14. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 46 pA != pE # label(axiom_015) # label(axiom) # answer(axiom_015). [assumption]. % 0.75/1.06 47 pE != pA # answer(axiom_015). [copy(46),flip(a)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.06 247 pE != a # answer(axiom_015). [para(192(a,2),47(a,2))]. % 0.75/1.06 248 $F # answer(axiom_015). [resolve(247,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 6 at 0.03 (+ 0.00) seconds: axiom_008. % 0.75/1.06 % Length of proof is 37. % 0.75/1.06 % Level of proof is 14. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 7 (all X aP(X) != pA) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 50 aP(A) != pA # label(axiom_008) # label(axiom) # answer(axiom_008). [clausify(7)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.06 249 aP(A) != a # answer(axiom_008). [para(192(a,2),50(a,2))]. % 0.75/1.06 250 $F # answer(axiom_008). [resolve(249,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 7 at 0.03 (+ 0.00) seconds: axiom_011. % 0.75/1.06 % Length of proof is 37. % 0.75/1.06 % Level of proof is 14. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 10 (all X bP(X) != pA) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 53 bP(A) != pA # label(axiom_011) # label(axiom) # answer(axiom_011). [clausify(10)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.06 251 bP(A) != a # answer(axiom_011). [para(192(a,2),53(a,2))]. % 0.75/1.06 252 $F # answer(axiom_011). [resolve(251,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 8 at 0.03 (+ 0.00) seconds: axiom_016. % 0.75/1.06 % Length of proof is 44. % 0.75/1.06 % Level of proof is 20. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.06 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.06 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.06 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.06 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.06 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.06 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.06 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.06 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.06 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.06 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.06 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.06 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.06 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.06 48 pB != pE # label(axiom_016) # label(axiom) # answer(axiom_016). [assumption]. % 0.75/1.06 49 pE != pB # answer(axiom_016). [copy(48),flip(a)]. % 0.75/1.06 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.06 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.06 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.06 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.06 79 linC(pE) != linC(pB) # answer(axiom_016). [ur(59,b,49,a)]. % 0.75/1.06 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.06 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.06 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.06 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.06 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.06 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.06 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.06 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.06 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.06 229 linP(pE) = a. [para(192(a,2),22(a,1)),flip(a)]. % 0.75/1.06 230 linP(a) = a. [para(192(a,2),22(a,2,1)),rewrite([22(1),229(2)]),flip(a)]. % 0.75/1.06 233 append(a,A) = A. [para(192(a,2),26(a,1,1,1)),rewrite([230(2)])]. % 0.75/1.06 237 linC(c2(A,B)) = linP(B). [para(192(a,2),36(a,1,1)),rewrite([233(3)]),flip(a)]. % 0.75/1.06 239 linP(A) = a. [para(192(a,2),36(a,1)),rewrite([237(3)]),flip(a)]. % 0.75/1.06 240 linC(a) = a. [para(192(a,2),36(a,2,1)),rewrite([239(1),239(2),233(3)]),flip(a)]. % 0.75/1.06 255 linC(pB) != a # answer(axiom_016). [para(192(a,2),79(a,1,1)),rewrite([240(2)]),flip(a)]. % 0.75/1.06 256 $F # answer(axiom_016). [resolve(255,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 % SZS output end Refutation % 0.75/1.06 ============================== end of proof ========================== % 0.75/1.06 % Redundant proof: 258 $F # answer(axiom_016). [resolve(257,a,192,a(flip))]. % 0.75/1.06 % Redundant proof: 260 $F # answer(axiom_015). [resolve(259,a,192,a(flip))]. % 0.75/1.06 % 0.75/1.06 ============================== PROOF ================================= % 0.75/1.06 % SZS status Theorem % 0.75/1.06 % SZS output start Refutation % 0.75/1.06 % 0.75/1.06 % Proof 9 at 0.04 (+ 0.00) seconds: axiom_013. % 0.75/1.06 % Length of proof is 44. % 0.75/1.06 % Level of proof is 20. % 0.75/1.06 % Maximum clause weight is 11.000. % 0.75/1.06 % Given clauses 96. % 0.75/1.06 % 0.75/1.06 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 12 (all X bP(X) != pE) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.06 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.07 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.07 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.07 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.07 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.07 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.07 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.07 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.07 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.07 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.07 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.07 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.07 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.07 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.07 55 bP(A) != pE # label(axiom_013) # label(axiom) # answer(axiom_013). [clausify(12)]. % 0.75/1.07 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.07 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.07 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.07 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.07 73 linC(bP(A)) != linC(pE) # answer(axiom_013). [ur(59,b,55,a)]. % 0.75/1.07 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.07 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.07 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.07 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.07 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.07 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.07 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.07 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.07 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.07 229 linP(pE) = a. [para(192(a,2),22(a,1)),flip(a)]. % 0.75/1.07 230 linP(a) = a. [para(192(a,2),22(a,2,1)),rewrite([22(1),229(2)]),flip(a)]. % 0.75/1.07 233 append(a,A) = A. [para(192(a,2),26(a,1,1,1)),rewrite([230(2)])]. % 0.75/1.07 237 linC(c2(A,B)) = linP(B). [para(192(a,2),36(a,1,1)),rewrite([233(3)]),flip(a)]. % 0.75/1.07 239 linP(A) = a. [para(192(a,2),36(a,1)),rewrite([237(3)]),flip(a)]. % 0.75/1.07 240 linC(a) = a. [para(192(a,2),36(a,2,1)),rewrite([239(1),239(2),233(3)]),flip(a)]. % 0.75/1.07 261 linC(bP(A)) != a # answer(axiom_013). [para(192(a,2),73(a,2,1)),rewrite([240(4)])]. % 0.75/1.07 262 $F # answer(axiom_013). [resolve(261,a,192,a(flip))]. % 0.75/1.07 % 0.75/1.07 % SZS output end Refutation % 0.75/1.07 ============================== end of proof ========================== % 0.75/1.07 % 0.75/1.07 ============================== PROOF ================================= % 0.75/1.07 % SZS status Theorem % 0.75/1.07 % SZS output start Refutation % 0.75/1.07 % 0.75/1.07 % Proof 10 at 0.04 (+ 0.00) seconds: axiom_009. % 0.75/1.07 % Length of proof is 44. % 0.75/1.07 % Level of proof is 20. % 0.75/1.07 % Maximum clause weight is 11.000. % 0.75/1.07 % Given clauses 96. % 0.75/1.07 % 0.75/1.07 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 8 (all X aP(X) != pB) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.07 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.07 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.07 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.07 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.07 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.07 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.07 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.07 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.07 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.07 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.07 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.07 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.07 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.07 51 aP(A) != pB # label(axiom_009) # label(axiom) # answer(axiom_009). [clausify(8)]. % 0.75/1.07 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.07 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.07 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.07 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.07 77 linC(aP(A)) != linC(pB) # answer(axiom_009). [ur(59,b,51,a)]. % 0.75/1.07 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.07 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.07 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.07 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.07 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.07 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.07 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.07 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.07 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.07 229 linP(pE) = a. [para(192(a,2),22(a,1)),flip(a)]. % 0.75/1.07 230 linP(a) = a. [para(192(a,2),22(a,2,1)),rewrite([22(1),229(2)]),flip(a)]. % 0.75/1.07 233 append(a,A) = A. [para(192(a,2),26(a,1,1,1)),rewrite([230(2)])]. % 0.75/1.07 237 linC(c2(A,B)) = linP(B). [para(192(a,2),36(a,1,1)),rewrite([233(3)]),flip(a)]. % 0.75/1.07 239 linP(A) = a. [para(192(a,2),36(a,1)),rewrite([237(3)]),flip(a)]. % 0.75/1.07 240 linC(a) = a. [para(192(a,2),36(a,2,1)),rewrite([239(1),239(2),233(3)]),flip(a)]. % 0.75/1.07 263 linC(aP(A)) != a # answer(axiom_009). [para(192(a,2),77(a,2,1)),rewrite([240(4)])]. % 0.75/1.07 264 $F # answer(axiom_009). [resolve(263,a,192,a(flip))]. % 0.75/1.07 % 0.75/1.07 % SZS output end Refutation % 0.75/1.07 ============================== end of proof ========================== % 0.75/1.07 % Redundant proof: 266 $F # answer(axiom_016). [resolve(265,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 268 $F # answer(axiom_016). [resolve(267,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 270 $F # answer(axiom_015). [resolve(269,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 273 $F # answer(axiom_013). [resolve(272,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 275 $F # answer(axiom_009). [resolve(274,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 278 $F # answer(axiom_015). [resolve(277,a,247,a)]. % 0.75/1.07 % Redundant proof: 280 $F # answer(axiom_016). [resolve(279,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 281 $F # answer(axiom_016). [para(192(a,2),126(a,2,1,1,1)),rewrite([277(1),240(2),240(2),240(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 282 $F # answer(axiom_016). [para(192(a,2),126(a,2,1,1)),rewrite([277(1),240(2),240(2),240(2),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 283 $F # answer(axiom_016). [para(192(a,2),126(a,2,1)),rewrite([277(1),240(2),240(2),240(2),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 284 $F # answer(axiom_016). [para(192(a,2),126(a,2)),rewrite([277(1),240(2),240(2),240(2)]),xx(a)]. % 0.75/1.07 % Redundant proof: 286 $F # answer(axiom_015). [resolve(285,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 287 $F # answer(axiom_015). [para(192(a,2),127(a,2,1,1,1)),rewrite([277(1),240(2),240(2),240(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 288 $F # answer(axiom_015). [para(192(a,2),127(a,2,1,1)),rewrite([277(1),240(2),240(2),240(2),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 289 $F # answer(axiom_015). [para(192(a,2),127(a,2,1)),rewrite([277(1),240(2),240(2),240(2),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 290 $F # answer(axiom_015). [para(192(a,2),127(a,2)),rewrite([277(1),240(2),240(2),240(2)]),xx(a)]. % 0.75/1.07 % Redundant proof: 291 $F # answer(axiom_013). [para(192(a,2),139(a,1,1,1,1)),rewrite([240(2),240(2),240(2),277(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 292 $F # answer(axiom_013). [para(192(a,2),139(a,1,1,1)),rewrite([240(2),240(2),277(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 293 $F # answer(axiom_013). [para(192(a,2),139(a,1,1)),rewrite([240(2),277(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 294 $F # answer(axiom_013). [para(192(a,2),139(a,1)),rewrite([277(2),240(3),240(3),240(3)]),xx(a)]. % 0.75/1.07 % Redundant proof: 296 $F # answer(axiom_013). [resolve(295,a,192,a(flip))]. % 0.75/1.07 % Redundant proof: 298 $F # answer(axiom_013). [resolve(297,a,295,a)]. % 0.75/1.07 % Redundant proof: 299 $F # answer(axiom_015). [resolve(297,a,285,a)]. % 0.75/1.07 % Redundant proof: 300 $F # answer(axiom_016). [resolve(297,a,279,a)]. % 0.75/1.07 % Redundant proof: 301 $F # answer(axiom_009). [resolve(297,a,274,a)]. % 0.75/1.07 % Redundant proof: 302 $F # answer(axiom_013). [resolve(297,a,272,a)]. % 0.75/1.07 % Redundant proof: 303 $F # answer(axiom_015). [resolve(297,a,269,a)]. % 0.75/1.07 % Redundant proof: 304 $F # answer(axiom_016). [resolve(297,a,267,a)]. % 0.75/1.07 % Redundant proof: 305 $F # answer(axiom_016). [resolve(297,a,265,a)]. % 0.75/1.07 % Redundant proof: 306 $F # answer(axiom_009). [resolve(297,a,263,a)]. % 0.75/1.07 % Redundant proof: 307 $F # answer(axiom_013). [resolve(297,a,261,a)]. % 0.75/1.07 % Redundant proof: 308 $F # answer(axiom_015). [resolve(297,a,259,a)]. % 0.75/1.07 % Redundant proof: 309 $F # answer(axiom_016). [resolve(297,a,257,a)]. % 0.75/1.07 % Redundant proof: 310 $F # answer(axiom_016). [resolve(297,a,255,a)]. % 0.75/1.07 % Redundant proof: 311 $F # answer(axiom_011). [resolve(297,a,251,a)]. % 0.75/1.07 % Redundant proof: 312 $F # answer(axiom_008). [resolve(297,a,249,a)]. % 0.75/1.07 % Redundant proof: 313 $F # answer(axiom_015). [resolve(297,a,247,a)]. % 0.75/1.07 % Redundant proof: 314 $F # answer(axiom_014). [resolve(297,a,245,a)]. % 0.75/1.07 % Redundant proof: 315 $F # answer(axiom_014). [resolve(297,a,243,a)]. % 0.75/1.07 % 0.75/1.07 ============================== PROOF ================================= % 0.75/1.07 % SZS status Theorem % 0.75/1.07 % SZS output start Refutation % 0.75/1.07 % 0.75/1.07 % Proof 11 at 0.04 (+ 0.00) seconds: axiom_012. % 0.75/1.07 % Length of proof is 41. % 0.75/1.07 % Level of proof is 14. % 0.75/1.07 % Maximum clause weight is 12.000. % 0.75/1.07 % Given clauses 96. % 0.75/1.07 % 0.75/1.07 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 11 (all X bP(X) != pB) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.07 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.07 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.07 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.07 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.07 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.07 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.07 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.07 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.07 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.07 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.07 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.07 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.07 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.07 54 bP(A) != pB # label(axiom_012) # label(axiom) # answer(axiom_012). [clausify(11)]. % 0.75/1.07 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.07 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.07 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.07 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.07 74 linC(bP(A)) != linC(pB) # answer(axiom_012). [ur(59,b,54,a)]. % 0.75/1.07 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.07 93 linC(linC(bP(A))) != linC(linC(pB)) # answer(axiom_012). [ur(59,b,74,a)]. % 0.75/1.07 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.07 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.07 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.07 140 linC(linC(linC(bP(A)))) != linC(linC(linC(pB))) # answer(axiom_012). [ur(59,b,93,a)]. % 0.75/1.07 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.07 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.07 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.07 185 linC(linC(linC(linC(bP(A))))) != linC(linC(linC(linC(pB)))) # answer(axiom_012). [ur(59,b,140,a)]. % 0.75/1.07 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.07 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.07 297 A = B. [para(192(a,1),192(a,1))]. % 0.75/1.07 316 $F # answer(axiom_012). [resolve(297,a,185,a)]. % 0.75/1.07 % 0.75/1.07 % SZS output end Refutation % 0.75/1.07 ============================== end of proof ========================== % 0.75/1.07 % Redundant proof: 317 $F # answer(axiom_013). [resolve(297,a,184,a)]. % 0.75/1.07 % Redundant proof: 318 $F # answer(axiom_014). [resolve(297,a,182,a)]. % 0.75/1.07 % Redundant proof: 319 $F # answer(axiom_015). [resolve(297,a,173,a)]. % 0.75/1.07 % Redundant proof: 320 $F # answer(axiom_016). [resolve(297,a,172,a)]. % 0.75/1.07 % 0.75/1.07 ============================== PROOF ================================= % 0.75/1.07 % SZS status Theorem % 0.75/1.07 % SZS output start Refutation % 0.75/1.07 % 0.75/1.07 % Proof 12 at 0.04 (+ 0.00) seconds: axiom_007. % 0.75/1.07 % Length of proof is 40. % 0.75/1.07 % Level of proof is 14. % 0.75/1.07 % Maximum clause weight is 11.000. % 0.75/1.07 % Given clauses 96. % 0.75/1.07 % 0.75/1.07 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 6 (all X all X2 aP(X) != bP(X2)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 13 (all X all X2 proj1C(c2(X,X2)) = X) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 15 (all Y append(nil,Y) = Y) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 17 (all P linP(aP(P)) = append(cons(a,nil),append(linP(P),cons(a,nil)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 19 (all P all Q linC(c2(P,Q)) = append(linP(P),linP(Q))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.07 20 -(exists U exists V -(linC(U) = linC(V) -> U = V)) # label(goal_027) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.07 21 linP(pE) = nil # label(axiom_025) # label(axiom). [assumption]. % 0.75/1.07 22 nil = linP(pE). [copy(21),flip(a)]. % 0.75/1.07 25 append(nil,A) = A # label(axiom_019) # label(axiom). [clausify(15)]. % 0.75/1.07 26 append(linP(pE),A) = A. [copy(25),rewrite([22(1)])]. % 0.75/1.07 27 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.75/1.07 29 proj1C(c2(A,B)) = A # label(axiom_017) # label(axiom). [clausify(13)]. % 0.75/1.07 31 linP(pA) = cons(a,nil) # label(axiom_023) # label(axiom). [assumption]. % 0.75/1.07 32 cons(a,linP(pE)) = linP(pA). [copy(31),rewrite([22(4)]),flip(a)]. % 0.75/1.07 35 linC(c2(A,B)) = append(linP(A),linP(B)) # label(axiom_026) # label(axiom). [clausify(19)]. % 0.75/1.07 36 append(linP(A),linP(B)) = linC(c2(A,B)). [copy(35),flip(a)]. % 0.75/1.07 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_020) # label(axiom). [clausify(16)]. % 0.75/1.07 38 linP(aP(A)) = append(cons(a,nil),append(linP(A),cons(a,nil))) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.75/1.07 39 append(linP(pA),linC(c2(A,pA))) = linP(aP(A)). [copy(38),rewrite([22(4),32(6),22(7),32(9),36(8)]),flip(a)]. % 0.75/1.07 58 bP(A) != aP(B) # label(axiom_007) # label(axiom) # answer(axiom_007). [clausify(6)]. % 0.75/1.07 59 linC(A) != linC(B) | A = B # label(goal_027) # label(negated_conjecture). [clausify(20)]. % 0.75/1.07 64 linC(c2(pE,A)) = linP(A). [para(36(a,1),26(a,1))]. % 0.75/1.07 65 append(linP(pA),A) = cons(a,A). [para(32(a,1),37(a,1,1)),rewrite([26(7)])]. % 0.75/1.07 67 cons(a,linC(c2(A,pA))) = linP(aP(A)). [back_rewrite(39),rewrite([65(6)])]. % 0.75/1.07 71 linC(bP(A)) != linC(aP(B)) # answer(axiom_007). [ur(59,b,58,a)]. % 0.75/1.07 87 linC(A) != linP(B) | c2(pE,B) = A. [para(64(a,1),59(a,1)),flip(a)]. % 0.75/1.07 102 cons(a,linP(pA)) = linP(aP(pE)). [para(64(a,1),67(a,1,2))]. % 0.75/1.07 116 append(linP(aP(pE)),A) = cons(a,cons(a,A)). [para(102(a,1),37(a,1,1)),rewrite([65(8)])]. % 0.75/1.07 118 linC(linC(bP(A))) != linC(linC(aP(B))) # answer(axiom_007). [ur(59,b,71,a)]. % 0.75/1.07 135 linC(c2(aP(pE),pE)) = linP(aP(pE)). [para(32(a,1),116(a,2,2)),rewrite([36(6),102(9)])]. % 0.75/1.07 144 c2(aP(pE),pE) = c2(pE,aP(pE)). [hyper(87,a,135,a),flip(a)]. % 0.75/1.07 150 aP(pE) = pE. [para(144(a,1),29(a,1,1)),rewrite([29(5)]),flip(a)]. % 0.75/1.07 158 cons(a,cons(a,A)) = A. [back_rewrite(116),rewrite([150(2),26(3)]),flip(a)]. % 0.75/1.07 171 linC(linC(linC(bP(A)))) != linC(linC(linC(aP(B)))) # answer(axiom_007). [ur(59,b,118,a)]. % 0.75/1.07 186 head(A) = a. [para(158(a,1),27(a,1,1))]. % 0.75/1.07 192 a = A. [back_rewrite(27),rewrite([186(2)])]. % 0.75/1.07 297 A = B. [para(192(a,1),192(a,1))]. % 0.75/1.07 321 $F # answer(axiom_007). [resolve(297,a,171,a)]. % 0.75/1.07 % 0.75/1.07 % SZS output end Refutation % 0.75/1.07 ============================== end of proof ========================== % 0.75/1.07 % 0.75/1.07 ============================== STATISTICS ============================ % 0.75/1.07 % 0.75/1.07 Given=96. Generated=617. Kept=222. proofs=12. % 0.75/1.07 Usable=53. Sos=44. Demods=46. Limbo=37, Disabled=114. Hints=0. % 0.75/1.07 Megabytes=0.22. % 0.75/1.07 User_CPU=0.04, System_CPU=0.00, Wall_clock=0. % 0.75/1.07 % 0.75/1.07 ============================== end of statistics ===================== % 0.75/1.07 % 0.75/1.07 ============================== end of search ========================= % 0.75/1.07 % 0.75/1.07 THEOREM PROVED % 0.75/1.07 % SZS status Theorem % 0.75/1.07 % 0.75/1.07 Exiting with 12 proofs. % 0.75/1.07 % 0.75/1.07 Process 21384 exit (max_proofs) Wed Apr 29 00:59:49 2026 % 0.75/1.07 Prover9 interrupted %------------------------------------------------------------------------------