/* Property (C') of the binary modal operator F for S5 ================================================================== Let F(p,q) == - p \/ (q /\ <>(p /\ - q)) \/ - <>(p /\ q) The binary modal operator F is for S5 what "nand" or "nor" is for classical propositional logic, i.e. any other logical connective can be described solely in terms of F, and that as follows: A) - p <=> F(p,p) B) <>p <=> (F(F(F(p,p),p),p) => p) C) (p => q) <=> F(p,F(p,q)) (from Dubikajtis, Moraes: One single operator for Lewis S5 modal logic, Reports on Mathematical Logic, 11:57-61, 1981) Any modal formula P is an S5-theorem iff <>[]P is an S4-theorem (from Matsumoto: Reduction Theorem in Lewis' sentential calculi, Mathematica Japonicae, 3:133-135,1955). Thus the following are S4-theorems: A') <>[](- p <=> F(p,p)) B') <>[](<>p <=> (F(F(F(p,p),p),p) => p)) C') <>[]((p => q) <=> F(p,F(p,q))) We attempt to prove those theorems using the Kripke semantics of the logic. More precisely we employ a semi-functional translation which is defined by {<>P,u} = exists x {P,u:x} {[]P,u} = all v r(u,v) ==> {P,v} initial call for formula P is: {P,init} provided the formula to be translated is in negation normal form. The translation (of the respective negations) into first-order predicate logic results in the clause sets given below. Remark_1: the colon in the problems below denotes a binary function symbol written in infix notation Remark_2: each of the examples is followed by the S4-theory axioms all u r(u,u). all u x r(u,u:x). all u v w -r(u,v)| -r(v,w) | r(u,w). These can be replaced (if desired) by: all u r(u,u). all u v x (-r(u,v)|r(u,v:x)). Remark_3: I took advantage of the fact that {[]P,init} is equivalent to "all u {P,u}". This follows from the translation definition from above plus the connectedness assumption for modal logics which states that, given an initial world "init", any world is accessible from "init" under the reflexive, transitive closure of the relation "r" (thus r(init,u) for any u). ---------------------------------------------------------- ---------------------------- A' -------------------------- ---------------------------------------------------------- all x1 exists x2 ((-p(x1:x2)| -p(x1:x2)|p(x1:x2)& (exists x3 (p(x1:x2:x3)& -p(x1:x2:x3)))| (all x4 (-r(x1:x2,x4)| -p(x4)| -p(x4))))& (p(x1:x2)|p(x1:x2)& (-p(x1:x2)| (all x5 (-r(x1:x2,x5)| -p(x5)|p(x5))))& (exists x6 (p(x1:x2:x6)&p(x1:x2:x6))))). all u r(u,u). all u x r(u,u:x). all u v w -r(u,v)| -r(v,w) | r(u,w). Clause form (after some basic simplification steps): -p(x1:$f3(x1))| -r(x1:$f3(x1),x4)| -p(x4). p(x1:$f3(x1)). r(u,u). r(u,u:x). -r(u,v)| -r(v,w) | r(u,w). ---------------------------------------------------------- ---------------------------- B' -------------------------- ---------------------------------------------------------- Clause form: p(x1:$f28(x1):$f1(x1))|p(x1:$f28(x1))| -r(x1:$f28(x1),x9)|p(x9:$f5(x1,x9))| -p(x9). p(x1:$f28(x1):$f1(x1))|p(x1:$f28(x1):$f14(x1):$f10(x1))| -p(x1:$f28(x1):$f14(x1):$f12(x1))| -r(x1:$f28(x1):$f14(x1),x27)|p(x27:$f13(x1,x27))| -p(x27)|p(x1:$f28(x1)). p(x1:$f28(x1):$f1(x1))|p(x1:$f28(x1):$f14(x1))|p(x1:$f28(x1)). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1):$f18(x1))| -r(x1:$f28(x1):$f18(x1),x38)| -p(x38)| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1))| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))|p(x1:$f28(x1):$f23(x1):$f19(x1))| -p(x1:$f28(x1):$f23(x1):$f21(x1))| -r(x1:$f28(x1):$f23(x1),x45)|p(x45:$f22(x1,x45))| -p(x45)| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x50)| -p(x50). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48)| -r(x48,x51)|p(x51). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)| -p(x48:$f27(x1,x48))| -r(x48:$f27(x1,x48),x56)| -p(x56)| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)|p(x1:$f28(x1):$f18(x1))| -p(x1:$f28(x1):$f23(x1))| -r(x1:$f28(x1),x48)|p(x48:$f27(x1,x48))| -p(x48). -r(x1:$f28(x1),x30)| -p(x30)| -p(x1:$f28(x1)). r(u,u). r(u,u:x). -r(u,v)| -r(v,w) | r(u,w). ---------------------------------------------------------- ---------------------------- C' -------------------------- ---------------------------------------------------------- all x1 exists x2 ((-p(x1:x2)|q(x1:x2)| -p(x1:x2)| (-p(x1:x2)|q(x1:x2)& (exists x3 (p(x1:x2:x3)& -q(x1:x2:x3)))| (all x4 (-r(x1:x2,x4)| -p(x4)| -q(x4))))& (exists x5 (p(x1:x2:x5)&p(x1:x2:x5)& (-q(x1:x2:x5)| (all x6 (-r(x1:x2:x5,x6)| -p(x6)|q(x6))))& (exists x7 (p(x1:x2:x5:x7)&q(x1:x2:x5:x7)))))| (all x8 (-r(x1:x2,x8)| -p(x8)|p(x8)& (-q(x8)| (all x9 (-r(x8,x9)| -p(x9)|q(x9))))& (exists x10 (p(x8:x10)&q(x8:x10))))))& (p(x1:x2)& -q(x1:x2)|p(x1:x2)& (p(x1:x2)& (-q(x1:x2)| (all x11 (-r(x1:x2,x11)| -p(x11)|q(x11))))& (exists x12 (p(x1:x2:x12)&q(x1:x2:x12)))| (all x13 (-r(x1:x2,x13)| -p(x13)| -p(x13)|q(x13)& (exists x14 (p(x13:x14)& -q(x13:x14)))| (all x15 (-r(x13,x15)| -p(x15)| -q(x15))))))& (exists x16 (p(x1:x2:x16)& (-p(x1:x2:x16)|q(x1:x2:x16)& (exists x17 (p(x1:x2:x16:x17)& -q(x1:x2:x16:x17)))| (all x18 (-r(x1:x2:x16,x18)| -p(x18)| -q(x18)))))))). r(u,u). r(u,u:x). -r(u,v)| -r(v,w) | r(u,w). The clausal form of this problem is this example. */ predicates([p,q,r]). p(X1:f9(X1)),r(X1:f9(X1),X4),p(X4),q(X4),r(X1:f9(X1),X8),p(X8),q(X8),r(X8,X9),p(X9) -> q(X1:f9(X1)),q(X9). p(X1:f9(X1)),r(X1:f9(X1),X4),p(X4),q(X4),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),p(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X4),p(X4),q(X4),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),q(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8),q(X8),r(X8,X9),p(X9) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1)),q(X9). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1)),p(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1)),q(X8:f4(X1,X8)). p(X1:f9(X1)),q(X1:f9(X1):f3(X1)),r(X1:f9(X1):f3(X1),X6),p(X6),r(X1:f9(X1),X8),p(X8),q(X8),r(X8,X9),p(X9) -> q(X1:f9(X1)),q(X6),q(X9). p(X1:f9(X1)),q(X1:f9(X1):f3(X1)),r(X1:f9(X1):f3(X1),X6),p(X6),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),q(X6),p(X8:f4(X1,X8)). p(X1:f9(X1)),q(X1:f9(X1):f3(X1)),r(X1:f9(X1):f3(X1),X6),p(X6),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),q(X6),q(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8),q(X8),r(X8,X9),p(X9) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1):f2(X1)),q(X9). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1):f2(X1)),p(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),p(X1:f9(X1):f3(X1):f2(X1)),q(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8),q(X8),r(X8,X9),p(X9) -> q(X1:f9(X1)),q(X1:f9(X1):f3(X1):f2(X1)),q(X9). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),q(X1:f9(X1):f3(X1):f2(X1)),p(X8:f4(X1,X8)). p(X1:f9(X1)),r(X1:f9(X1),X8),p(X8) -> q(X1:f9(X1)),q(X1:f9(X1):f3(X1):f2(X1)),q(X8:f4(X1,X8)). p(X1:f9(X1)). q(X1:f9(X1)),r(X1:f9(X1),X11),p(X11),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> q(X11),q(X13). q(X1:f9(X1)),r(X1:f9(X1),X11),p(X11),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> q(X11),p(X13:f6(X1,X13)). q(X1:f9(X1)),r(X1:f9(X1),X11),p(X11),r(X1:f9(X1),X13),p(X13),q(X13:f6(X1,X13)),r(X13,X15),p(X15),q(X15) -> q(X11). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> p(X1:f9(X1):f5(X1)),q(X13). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> p(X1:f9(X1):f5(X1)),p(X13:f6(X1,X13)). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),q(X13:f6(X1,X13)),r(X13,X15),p(X15),q(X15) -> p(X1:f9(X1):f5(X1)). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> q(X1:f9(X1):f5(X1)),q(X13). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),r(X13,X15),p(X15),q(X15) -> q(X1:f9(X1):f5(X1)),p(X13:f6(X1,X13)). q(X1:f9(X1)),r(X1:f9(X1),X13),p(X13),q(X13:f6(X1,X13)),r(X13,X15),p(X15),q(X15) -> q(X1:f9(X1):f5(X1)). q(X1:f9(X1)) -> p(X1:f9(X1):f8(X1)). q(X1:f9(X1)),p(X1:f9(X1):f8(X1)),r(X1:f9(X1):f8(X1),X18),p(X18),q(X18) -> q(X1:f9(X1):f8(X1)). q(X1:f9(X1)),p(X1:f9(X1):f8(X1)),r(X1:f9(X1):f8(X1),X18),p(X18),q(X18) -> p(X1:f9(X1):f8(X1):f7(X1)). q(X1:f9(X1)),p(X1:f9(X1):f8(X1)),q(X1:f9(X1):f8(X1):f7(X1)),r(X1:f9(X1):f8(X1),X18),p(X18),q(X18) -> []. r(U,U). r(U,U:X). % 1 r(U,V),r(V,W) -> r(U,W). % 1' %r(U,V) -> r(U,V:X). % 2 precedence([':',f1,f2,f3,f4,f5,f6,f7,f8,f9,p,q,r]). :-sama([1]). :-saci([1]). :-option(var_depth(4)). /* For this example it is essential to make predicates smaller than functions. Choosing an ordered strategy with selection of maximal literals (sama([1]) helps. With a positive strategy it takes 10 times longer. Variant 2 (leaving out clauses 1 and 1') also takes 10 times longer. In that case we apply ordered resolution to 2. The respective restrictions are weaker than those for ordered chaining with 1. Saturation terminated. Current Set of Rules : 414 : -> Total time: 357740 milliseconds of which: 84780 milliseconds of inference computation 110020 milliseconds of clause simplification 17600 milliseconds of rule simplification 40420 milliseconds of constraint solving 104920 milliseconds for the rest Number of computed inferences: 347 Number of rules computed: 225 Proof: ====== initial axiom 1 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2),q(x2),r(x1:f9(x1),x3),p(x3),q(x3),r(x3,x4),p(x4) -> q(x1:f9(x1)),q(x4) initial axiom 11 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1)),p(x1:f9(x1):f3(x1):f2(x1)),p(x2:f4(x1,x2)) initial axiom 12 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1)),p(x1:f9(x1):f3(x1):f2(x1)),q(x2:f4(x1,x2)) initial axiom 14 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1)),q(x1:f9(x1):f3(x1):f2(x1)),p(x2:f4(x1,x2)) initial axiom 15 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1)),q(x1:f9(x1):f3(x1):f2(x1)),q(x2:f4(x1,x2)) initial axiom 16 : -> p(x1:f9(x1)) initial axiom 17 : q(x1:f9(x1)),r(x1:f9(x1),x2),p(x2),r(x1:f9(x1),x3),p(x3),r(x3,x4),p(x4),q(x4) -> q(x2),q(x3) initial axiom 26 : q(x1:f9(x1)) -> p(x1:f9(x1):f8(x1)) initial axiom 27 : q(x1:f9(x1)),p(x1:f9(x1):f8(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> q(x1:f9(x1):f8(x1)) initial axiom 28 : q(x1:f9(x1)),p(x1:f9(x1):f8(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> p(x1:f9(x1):f8(x1):f7(x1)) initial axiom 29 : q(x1:f9(x1)),p(x1:f9(x1):f8(x1)),q(x1:f9(x1):f8(x1):f7(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> initial axiom 31 : -> r(x1,x1:x2) condensement of 1 33 : p(x1:f9(x1)),r(x1:f9(x1),x2),p(x2),q(x2),r(x2,x3),p(x3) -> q(x1:f9(x1)),q(x3) condensement of 17 34 : q(x1:f9(x1)),r(x1:f9(x1),x2),p(x2),r(x2,x3),p(x3),q(x3) -> q(x2) reduction of 27 by [26] 35 : q(x1:f9(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> q(x1:f9(x1):f8(x1)) reduction of 28 by [26] 36 : q(x1:f9(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> p(x1:f9(x1):f8(x1):f7(x1)) reduction of 29 by [26] 37 : q(x1:f9(x1)),q(x1:f9(x1):f8(x1):f7(x1)),r(x1:f9(x1):f8(x1),x2),p(x2),q(x2) -> reduction of 33 by [16] 38 : r(x1:f9(x1),x2),p(x2),r(x2,x3),p(x3),q(x2) -> q(x1:f9(x1)),q(x3) reduction of 11 by [16] 45 : r(x1:f9(x1),x2),p(x2) -> p(x1:f9(x1):f3(x1):f2(x1)),p(x2:f4(x1,x2)),q(x1:f9(x1)) reduction of 12 by [16] 46 : r(x1:f9(x1),x2),p(x2) -> p(x1:f9(x1):f3(x1):f2(x1)),q(x2:f4(x1,x2)),q(x1:f9(x1)) reduction of 14 by [16] 47 : r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1):f3(x1):f2(x1)),p(x2:f4(x1,x2)),q(x1:f9(x1)) reduction of 15 by [16] 48 : r(x1:f9(x1),x2),p(x2) -> q(x1:f9(x1):f3(x1):f2(x1)),q(x2:f4(x1,x2)),q(x1:f9(x1)) negative chaining of 31 from 38 49 : x1:f9(x1)=x2,p(x2:x3),r(x2:x3,x4),p(x4),q(x2:x3) -> q(x1:f9(x1)),q(x4) reflexivity resolution on 49 51 : p((x1:f9(x1)):x2),r((x1:f9(x1)):x2,x3),p(x3),q((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(x3) negative chaining of 31 from 34 53 : x1:f9(x1)=x2,q(x1:f9(x1)),p(x2:x3),r(x2:x3,x4),p(x4),q(x4) -> q(x2:x3) reflexivity resolution on 53 66 : q(x1:f9(x1)),p((x1:f9(x1)):x2),r((x1:f9(x1)):x2,x3),p(x3),q(x3) -> q((x1:f9(x1)):x2) negative chaining of 31 from 35 69 : r(x1:f9(x1):f8(x1),x2),p(x2:x3),q(x1:f9(x1)),q(x2:x3) -> q(x1:f9(x1):f8(x1)) negative chaining of 31 from 69 90 : x1:f9(x1):f8(x1)=x2,p((x2:x3):x4),q(x1:f9(x1)),q((x2:x3):x4) -> q(x1:f9(x1):f8(x1)) reflexivity resolution on 36 92 : p(x1:f9(x1):f8(x1)),q(x1:f9(x1)),q(x1:f9(x1):f8(x1)) -> p(x1:f9(x1):f8(x1):f7(x1)) reduction of 92 by [26] 93 : q(x1:f9(x1)),q(x1:f9(x1):f8(x1)) -> p(x1:f9(x1):f8(x1):f7(x1)) reflexivity resolution on 90 94 : p(((x1:f9(x1):f8(x1)):x2):x3),q(x1:f9(x1)),q(((x1:f9(x1):f8(x1)):x2):x3) -> q(x1:f9(x1):f8(x1)) reflexivity resolution on 45 113 : p(x1:f9(x1)) -> p(x1:f9(x1):f3(x1):f2(x1)),p((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reduction of 113 by [16] 114 : -> p(x1:f9(x1):f3(x1):f2(x1)),p((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reflexivity resolution on 46 115 : p(x1:f9(x1)) -> p(x1:f9(x1):f3(x1):f2(x1)),q((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reduction of 115 by [16] 116 : -> p(x1:f9(x1):f3(x1):f2(x1)),q((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reflexivity resolution on 47 117 : p(x1:f9(x1)) -> q(x1:f9(x1):f3(x1):f2(x1)),p((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reduction of 117 by [16] 118 : -> q(x1:f9(x1):f3(x1):f2(x1)),p((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reflexivity resolution on 48 119 : p(x1:f9(x1)) -> q(x1:f9(x1):f3(x1):f2(x1)),q((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) reduction of 119 by [16] 120 : -> q(x1:f9(x1):f3(x1):f2(x1)),q((x1:f9(x1)):f4(x1,x1:f9(x1))),q(x1:f9(x1)) negative chaining of 31 from 51 144 : (x1:f9(x1)):x2=x3,p((x1:f9(x1)):x2),p(x3:x4),q((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(x3:x4) reflexivity resolution on 144 168 : p((x1:f9(x1)):x2),p(((x1:f9(x1)):x2):x3),q((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(((x1:f9(x1)):x2):x3) negative chaining of 31 from 66 171 : (x1:f9(x1)):x2=x3,p((x1:f9(x1)):x2),p(x3:x4),q(x1:f9(x1)),q(x3:x4) -> q((x1:f9(x1)):x2) reflexivity resolution on 37 186 : q(x1:f9(x1):f8(x1):f7(x1)),p(x1:f9(x1):f8(x1)),q(x1:f9(x1)),q(x1:f9(x1):f8(x1)) -> reduction of 186 by [26] 187 : q(x1:f9(x1):f8(x1):f7(x1)),q(x1:f9(x1)),q(x1:f9(x1):f8(x1)) -> reflexivity resolution on 171 196 : p((x1:f9(x1)):x2),p(((x1:f9(x1)):x2):x3),q(x1:f9(x1)),q(((x1:f9(x1)):x2):x3) -> q((x1:f9(x1)):x2) negative chaining of 31 from 37 205 : x1:f9(x1):f8(x1)=x2,q(x1:f9(x1):f8(x1):f7(x1)),p(x2:x3),q(x1:f9(x1)),q(x2:x3) -> reflexivity resolution on 205 231 : q(x1:f9(x1):f8(x1):f7(x1)),p((x1:f9(x1):f8(x1)):x2),q(x1:f9(x1)),q((x1:f9(x1):f8(x1)):x2) -> negative chaining of 16 from 231 285 : q(x1:f9(x1)),q(x1:f9(x1):f8(x1):f7(x1)),q((x1:f9(x1):f8(x1)):f9(x1:f9(x1):f8(x1))) -> negative chaining of 16 from 196 319 : q(x1:f9(x1)),p((x1:f9(x1)):x2),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2)) -> q((x1:f9(x1)):x2) negative chaining of 16 from 168 321 : q((x1:f9(x1)):x2),p((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2)) negative chaining of 26 from 168 324 : q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2)),q((x1:f9(x1)):x2),p((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2):f8((x1:f9(x1)):x2)) reduction of 324 by [321] 325 : q((x1:f9(x1)):x2),p((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2):f8((x1:f9(x1)):x2)) negative chaining of 16 from 94 326 : q(x1:f9(x1)),q(((x1:f9(x1):f8(x1)):x2):f9((x1:f9(x1):f8(x1)):x2)) -> q(x1:f9(x1):f8(x1)) negative chaining of 93 from 168 332 : q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2)),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2):f8((x1:f9(x1)):x2)),q((x1:f9(x1)):x2),p((x1:f9(x1)):x2) -> q(x1:f9(x1)),q(((x1:f9(x1)):x2):f9((x1:f9(x1)):x2):f8((x1:f9(x1)):x2):f7((x1:f9(x1)):x2)) reduction of 332 by [187,325,321] 333 : q((x1:f9(x1)):x2),p((x1:f9(x1)):x2) -> q(x1:f9(x1)) negative chaining of 16 from 333 334 : q((x1:f9(x1)):f9(x1:f9(x1))) -> q(x1:f9(x1)) negative chaining of 114 from 333 341 : q((x1:f9(x1)):f4(x1,x1:f9(x1))) -> q(x1:f9(x1)),p(x1:f9(x1):f3(x1):f2(x1)) negative chaining of 118 from 333 342 : q((x1:f9(x1)):f4(x1,x1:f9(x1))) -> q(x1:f9(x1)),q(x1:f9(x1):f3(x1):f2(x1)) reduction of 341 by [116] 344 : -> q(x1:f9(x1)),p(x1:f9(x1):f3(x1):f2(x1)) reduction of 342 by [120] 345 : -> q(x1:f9(x1)),q(x1:f9(x1):f3(x1):f2(x1)) negative chaining of 344 from 333 349 : q((x1:f9(x1)):f9(x1:f9(x1)):f3(x1:f9(x1)):f2(x1:f9(x1))) -> q((x1:f9(x1)):f9(x1:f9(x1))),q(x1:f9(x1)) reduction of 349 by [334] 350 : q((x1:f9(x1)):f9(x1:f9(x1)):f3(x1:f9(x1)):f2(x1:f9(x1))) -> q(x1:f9(x1)) negative chaining of 345 from 350 351 : -> q((x1:f9(x1)):f9(x1:f9(x1))),q(x1:f9(x1)) reduction of 351 by [334] 352 : -> q(x1:f9(x1)) reduction of 93 by [352] 358 : q(x1:f9(x1):f8(x1)) -> p(x1:f9(x1):f8(x1):f7(x1)) reduction of 285 by [352,352] 394 : q(x1:f9(x1):f8(x1):f7(x1)) -> reduction of 319 by [352,352] 401 : p((x1:f9(x1)):x2) -> q((x1:f9(x1)):x2) reduction of 326 by [352,352] 402 : -> q(x1:f9(x1):f8(x1)) reduction of 358 by [402] 403 : -> p(x1:f9(x1):f8(x1):f7(x1)) negative chaining of 403 from 401 413 : -> q((x1:f9(x1)):f9(x1:f9(x1)):f8(x1:f9(x1)):f7(x1:f9(x1))) reduction of 413 by [394] 414 : -> Length of proof: 71 */