% we want definitions to be expanded %precedence([';',image,par,union,intersection,product,id,',',eq_elem]). top_predicates_precedence([eq,func,pfunc,injective,total,rel,unique,dom,contains]). option(full_cnf(yes)). /* Saturate Version 2.99-o (linux-sicstus3) of 9 March 2004 at 14:19:11. full_cnf(yes) Proof: ====== 1 : eq_elem(A,B)==(A=B) [input] 2 : eq(A,B)==!C,D.(contains(A,(D,C))<=>contains(B,(D,C))) [input] 4 : contains((A;B),(C,D))==?E.(contains(A,(C,E))and contains(B,(E,D))) [input] 7 : rel(A,B,C)==!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) [input] 11 : total(A,B)==!C.(contains(B,C)=>?D.(contains(A,(C,D)))) [input] 12 : unique(A)==!B,C,D.(contains(A,(D,C))and contains(A,(D,B))=>eq_elem(C,B)) [input] 13 : pfunc(A,B,C)==(rel(A,B,C)and unique(A)) [input] 14 : injective(A)==!B,C,D.(contains(A,(D,B))and contains(A,(C,B))=>eq_elem(D,C)) [input] 15 : func(A,B,C)==(pfunc(A,B,C)and total(A,B)) [input] 16 + rel(p,s,t)and rel(q,s,t)and func(f,t,b)and injective(f)=>eq((p;f),(q;f))=>eq(p,q) -> [input] 18 : unique(A)==!B,C,D.(contains(A,(D,C))and contains(A,(D,B))=>C=B) [reduction of 12 by [1]] 19 : pfunc(A,B,C)==(!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) and!F,G,H.(contains(A,(H,G))and contains(A,(H,F))=>G=F)) [reduction of 13 by [18,7]] 20 : injective(A)==!B,C,D.(contains(A,(D,B))and contains(A,(C,B))=>D=C) [reduction of 14 by [1]] 21 : func(A,B,C)==(!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) and!F,G,H.(contains(A,(H,G))and contains(A,(H,F))=>G=F) and!I.(contains(B,I)=>?J.(contains(A,(I,J))))) [reduction of 15 by [11,19]] 22 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K)))))and!L,M,N.(contains(f,(N,L))and contains(f,(M,L))=>N=M)=>!O,P.(?Q.(contains(p,(P,Q))and contains(f,(Q,O)))<=>?R.(contains(q,(P,R))and contains(f,(R,O))))=>!S,T.(contains(p,(T,S))<=>contains(q,(T,S))) -> [reduction of 16 by [2,2,4,4,20,21,7,7]] 23 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K)))))and!L,M,N.(contains(f,(N,L))and contains(f,(M,L))=>N=M) [expansion from 22] 24 + !A,B.(?C.(contains(p,(B,C))and contains(f,(C,A)))<=>?D.(contains(q,(B,D))and contains(f,(D,A))))=>!E,F.(contains(p,(F,E))<=>contains(q,(F,E))) -> [expansion from 22] 25 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K))))) [expansion from 23] 26 + contains(f,(A,B)),contains(f,(C,B)) -> A=C [expansion from 23] 27 + ?C.(contains(p,(A,C))and contains(f,(C,B)))==?D.(contains(q,(A,D))and contains(f,(D,B))) [expansion from 24] 28 + !A,B.(contains(p,(B,A))<=>contains(q,(B,A))) -> [expansion from 24] 29 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) [expansion from 25] 30 + !A,B.(contains(f,(B,A))=>contains(t,B)and contains(b,A)) and!C,D,E.(contains(f,(E,D))and contains(f,(E,C))=>D=C) and!F.(contains(t,F)=>?G.(contains(f,(F,G)))) [expansion from 25] 31 + contains(q,(A,B)),contains(f,(B,C)) -> ?D.(contains(p,(A,D))and contains(f,(D,C))) [expansion from 27] 32 + contains(p,(A,B)),contains(f,(B,C)) -> ?D.(contains(q,(A,D))and contains(f,(D,C))) [expansion from 27] 33 + !A.(contains(p,(A,s$16))<=>contains(q,(A,s$16))) -> [expansion from 28] 35 + contains(p,(A,B)) -> contains(s,A)and contains(t,B) [expansion from 29] 36 + contains(q,(A,B)) -> contains(s,A)and contains(t,B) [expansion from 29] 38 + contains(t,A) -> ?B.(contains(f,(A,B))) [expansion from 30] 39 + contains(q,(A,B)),contains(f,(B,C)) -> contains(p,(A,s$3(p,f,A,C)))and contains(f,(s$3(p,f,A,C),C)) [expansion from 31] 40 + contains(f,(A,B)),contains(p,(C,A)) -> contains(q,(C,s$3(q,f,C,B)))and contains(f,(s$3(q,f,C,B),B)) [expansion from 32] 41 + contains(p,(s$17,s$16))==contains(q,(s$17,s$16)) -> [expansion from 33] 44 + contains(p,(A,B)) -> contains(t,B) [expansion from 35] 46 + contains(q,(A,B)) -> contains(t,B) [expansion from 36] 49 + contains(t,A) -> contains(f,(A,s$9(f,A))) [expansion from 38] 50 + contains(q,(A,B)),contains(f,(B,C)) -> contains(p,(A,s$3(p,f,A,C))) [expansion from 39] 51 + contains(q,(A,B)),contains(f,(B,C)) -> contains(f,(s$3(p,f,A,C),C)) [expansion from 39] 52 + contains(f,(A,B)),contains(p,(C,A)) -> contains(q,(C,s$3(q,f,C,B))) [expansion from 40] 53 + contains(f,(A,B)),contains(p,(C,A)) -> contains(f,(s$3(q,f,C,B),B)) [expansion from 40] 54 + contains(q,(s$17,s$16))=>contains(p,(s$17,s$16)),contains(p,(s$17,s$16))=>contains(q,(s$17,s$16)) -> [expansion from 41] 57 + contains(p,(s$17,s$16))=>contains(q,(s$17,s$16)) -> contains(q,(s$17,s$16)) [expansion from 54] 58 + contains(p,(s$17,s$16))=>contains(q,(s$17,s$16)),contains(p,(s$17,s$16)) -> [expansion from 54] 59 + contains(p,(A,B)) -> contains(f,(B,s$9(f,B))) [negative chaining of 44 from 49] 60 + contains(q,(A,B)) -> contains(f,(B,s$9(f,B))) [negative chaining of 46 from 49] 63 + contains(q,(s$17,s$16)),contains(p,(s$17,s$16)) [expansion from 57] 64 + contains(p,(s$17,s$16)),contains(q,(s$17,s$16)) -> [expansion from 58] 67 + contains(f,(s$16,A)) -> contains(p,(s$17,s$16)),contains(p,(s$17,s$3(p,f,s$17,A))) [negative chaining of 63 from 50] 68 + contains(f,(s$16,A)) -> contains(p,(s$17,s$16)),contains(f,(s$3(p,f,s$17,A),A)) [negative chaining of 63 from 51] 69 + contains(p,(s$17,s$16)),contains(f,(s$16,s$9(f,s$16))) [negative chaining of 63 from 60] 70 + contains(f,(s$16,s$9(f,s$16))) [reduction of 69 by [59,L]] 71 + contains(f,(A,s$9(f,s$16))) -> A=s$16 [negative chaining of 70 from 26] 78 + contains(f,(s$16,A)),contains(f,(s$16,B)) -> contains(f,(s$3(p,f,s$17,A),A)),contains(f,(s$3(q,f,s$17,B),B)) [negative chaining of 68 from 53] 98 + contains(f,(s$16,A)),contains(f,(s$16,s$9(f,s$16))) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(q,f,s$17,s$9(f,s$16))=s$16 [negative chaining of 78 from 71] 101 + contains(f,(s$16,A)) -> s$3(q,f,s$17,s$9(f,s$16))=s$16,contains(f,(s$3(p,f,s$17,A),A)) [reduction of 98 by [70]] 105 + contains(f,(s$16,s$9(f,s$16))) -> s$3(q,f,s$17,s$9(f,s$16))=s$16,s$3(p,f,s$17,s$9(f,s$16))=s$16 [negative chaining of 101 from 71] 107 + s$3(p,f,s$17,s$9(f,s$16))=s$16,s$3(q,f,s$17,s$9(f,s$16))=s$16 [reduction of 105 by [70]] 108 + contains(f,(A,s$9(f,s$16))),contains(p,(s$17,A)) -> contains(q,(s$17,s$16)),s$3(p,f,s$17,s$9(f,s$16))=s$16 [chaining of 107 from 52] 114 + contains(f,(A,s$9(f,s$16))),contains(p,(s$17,A)),contains(f,(s$16,B)) -> s$3(p,f,s$17,s$9(f,s$16))=s$16,contains(f,(s$3(p,f,s$17,B),B)) [negative chaining of 108 from 51] 219 + contains(f,(s$16,A)),contains(f,(s$16,s$9(f,s$16))),contains(f,(s$16,B)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(p,f,s$17,s$9(f,s$16))=s$16,contains(f,(s$3(p,f,s$17,B),B)) [negative chaining of 68 from 114] 225 + contains(f,(s$16,s$9(f,s$16))),contains(f,(s$16,A)) -> s$3(p,f,s$17,s$9(f,s$16))=s$16,contains(f,(s$3(p,f,s$17,A),A)) [condensement of 219] 226 + contains(f,(s$16,A)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(p,f,s$17,s$9(f,s$16))=s$16 [reduction of 225 by [70]] 231 + contains(f,(s$16,s$9(f,s$16))) -> s$3(p,f,s$17,s$9(f,s$16))=s$16,s$3(p,f,s$17,s$9(f,s$16))=s$16 [negative chaining of 226 from 71] 239 + contains(f,(s$16,s$9(f,s$16))) -> s$3(p,f,s$17,s$9(f,s$16))=s$16 [condensement of 231] 240 + s$3(p,f,s$17,s$9(f,s$16))=s$16 [reduction of 239 by [70]] 246 + contains(f,(s$16,s$9(f,s$16))) -> contains(p,(s$17,s$16)),contains(p,(s$17,s$16)) [chaining of 240 from 67] 252 + contains(f,(s$16,s$9(f,s$16))) -> contains(p,(s$17,s$16)) [condensement of 246] 253 + contains(p,(s$17,s$16)) [reduction of 252 by [70]] 254 + contains(q,(s$17,s$16)) -> [reduction of 64 by [253]] 255 + contains(f,(s$16,A)) -> contains(f,(s$3(q,f,s$17,A),A)) [negative chaining of 253 from 53] 263 + contains(f,(s$16,s$9(f,s$16))) -> s$3(q,f,s$17,s$9(f,s$16))=s$16 [negative chaining of 255 from 71] 268 + s$3(q,f,s$17,s$9(f,s$16))=s$16 [reduction of 263 by [70]] 271 + contains(f,(A,s$9(f,s$16))),contains(p,(s$17,A)) -> contains(q,(s$17,s$16)) [chaining of 268 from 52] 275 + contains(f,(A,s$9(f,s$16))),contains(p,(s$17,A)) -> [reduction of 271 by [254,L]] 276 + contains(f,(s$16,s$9(f,s$16))) -> [negative chaining of 253 from 275] 290 + false [reduction of 276 by [70]] Length = 75, Depth = 37, Search Depth = 14 Total time: 7660 milliseconds Number of forward inferences: 180 Number of tableau inferences: 38 Number of generated clauses: 290 Number of kept clauses: 136 ============================================================================ full_cnf(no) Proof: ====== 1 : eq_elem(A,B)==(A=B) [input] 2 : eq(A,B)==!C,D.(contains(A,(D,C))<=>contains(B,(D,C))) [input] 4 : contains((A;B),(C,D))==?E.(contains(A,(C,E))and contains(B,(E,D))) [input] 7 : rel(A,B,C)==!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) [input] 11 : total(A,B)==!C.(contains(B,C)=>?D.(contains(A,(C,D)))) [input] 12 : unique(A)==!B,C,D.(contains(A,(D,C))and contains(A,(D,B))=>eq_elem(C,B)) [input] 13 : pfunc(A,B,C)==(rel(A,B,C)and unique(A)) [input] 14 : injective(A)==!B,C,D.(contains(A,(D,B))and contains(A,(C,B))=>eq_elem(D,C)) [input] 15 : func(A,B,C)==(pfunc(A,B,C)and total(A,B)) [input] 16 + rel(p,s,t)and rel(q,s,t)and func(f,t,b)and injective(f)=>eq((p;f),(q;f))=>eq(p,q) -> [input] 18 : unique(A)==!B,C,D.(contains(A,(D,C))and contains(A,(D,B))=>C=B) [reduction of 12 by [1]] 19 : pfunc(A,B,C)==(!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) and!F,G,H.(contains(A,(H,G))and contains(A,(H,F))=>G=F)) [reduction of 13 by [18,7]] 20 : injective(A)==!B,C,D.(contains(A,(D,B))and contains(A,(C,B))=>D=C) [reduction of 14 by [1]] 21 : func(A,B,C)==(!D,E.(contains(A,(E,D))=>contains(B,E)and contains(C,D)) and!F,G,H.(contains(A,(H,G))and contains(A,(H,F))=>G=F) and!I.(contains(B,I)=>?J.(contains(A,(I,J))))) [reduction of 15 by [11,19]] 22 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K)))))and!L,M,N.(contains(f,(N,L))and contains(f,(M,L))=>N=M)=>!O,P.(?Q.(contains(p,(P,Q))and contains(f,(Q,O)))<=>?R.(contains(q,(P,R))and contains(f,(R,O))))=>!S,T.(contains(p,(T,S))<=>contains(q,(T,S))) -> [reduction of 16 by [2,2,4,4,20,21,7,7]] 23 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K)))))and!L,M,N.(contains(f,(N,L))and contains(f,(M,L))=>N=M) [expansion from 22] 24 + !A,B.(?C.(contains(p,(B,C))and contains(f,(C,A)))<=>?D.(contains(q,(B,D))and contains(f,(D,A))))=>!E,F.(contains(p,(F,E))<=>contains(q,(F,E))) -> [expansion from 22] 25 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) and(!E,F.(contains(f,(F,E))=>contains(t,F)and contains(b,E)) and!G,H,I.(contains(f,(I,H))and contains(f,(I,G))=>H=G) and!J.(contains(t,J)=>?K.(contains(f,(J,K))))) [expansion from 23] 26 + contains(f,(A,B)),contains(f,(C,B)) -> A=C [expansion from 23] 27 + ?C.(contains(p,(A,C))and contains(f,(C,B)))==?D.(contains(q,(A,D))and contains(f,(D,B))) [expansion from 24] 28 + !A,B.(contains(p,(B,A))<=>contains(q,(B,A))) -> [expansion from 24] 29 + !A,B.(contains(p,(B,A))=>contains(s,B)and contains(t,A)) and!C,D.(contains(q,(D,C))=>contains(s,D)and contains(t,C)) [expansion from 25] 30 + !A,B.(contains(f,(B,A))=>contains(t,B)and contains(b,A)) and!C,D,E.(contains(f,(E,D))and contains(f,(E,C))=>D=C) and!F.(contains(t,F)=>?G.(contains(f,(F,G)))) [expansion from 25] 31 + contains(q,(A,B)),contains(f,(B,C)) -> ?D.(contains(p,(A,D))and contains(f,(D,C))) [expansion from 27] 32 + contains(p,(A,B)),contains(f,(B,C)) -> ?D.(contains(q,(A,D))and contains(f,(D,C))) [expansion from 27] 33 + !A.(contains(p,(A,s$16))<=>contains(q,(A,s$16))) -> [expansion from 28] 35 + contains(p,(A,B)) -> contains(s,A)and contains(t,B) [expansion from 29] 36 + contains(q,(A,B)) -> contains(s,A)and contains(t,B) [expansion from 29] 38 + contains(t,A) -> ?B.(contains(f,(A,B))) [expansion from 30] 39 + contains(f,(A,B)),contains(p,(C,A)) -> contains(q,(C,s$3(q,f,C,B)))and contains(f,(s$3(q,f,C,B),B)) [expansion from 32] 40 + contains(p,(s$17,s$16))==contains(q,(s$17,s$16)) -> [expansion from 33] 43 + contains(p,(A,B)) -> contains(t,B) [expansion from 35] 45 + contains(q,(A,B)) -> contains(t,B) [expansion from 36] 48 + contains(f,(A,B)),contains(p,(C,A)) -> contains(q,(C,s$3(q,f,C,B))) [expansion from 39] 49 + contains(f,(A,B)),contains(p,(C,A)) -> contains(f,(s$3(q,f,C,B),B)) [expansion from 39] 50 + contains(q,(s$17,s$16))== ~contains(p,(s$17,s$16)) [expansion from 40] 53 + contains(p,(A,B)) -> ?C.(contains(f,(B,C))) [negative chaining of 43 from 38] 54 + contains(q,(A,B)) -> ?C.(contains(f,(B,C))) [negative chaining of 45 from 38] 55 + ~contains(p,(s$17,s$16)),contains(f,(s$16,A)) -> ?B.(contains(p,(s$17,B))and contains(f,(B,A))) [negative chaining of 50 from 31] 57 + contains(f,(s$16,A)) -> ?B.(contains(p,(s$17,B))and contains(f,(B,A))),contains(p,(s$17,s$16)) [reduction of 55 by [L]] 58 + contains(f,(s$16,A)) -> contains(p,(s$17,s$16)),contains(p,(s$17,s$3(p,f,s$17,A)))and contains(f,(s$3(p,f,s$17,A),A)) [expansion from 57] 60 + ~contains(p,(s$17,s$16)) -> ?A.(contains(f,(s$16,A))) [negative chaining of 50 from 54] 62 + ?A.(contains(f,(s$16,A))) [reduction of 60 by [53,L]] 63 + contains(f,(s$16,A)) -> contains(p,(s$17,s$16)),contains(p,(s$17,s$3(p,f,s$17,A))) [expansion from 58] 64 + contains(f,(s$16,A)) -> contains(p,(s$17,s$16)),contains(f,(s$3(p,f,s$17,A),A)) [expansion from 58] 65 + contains(f,(s$16,s$18)) [expansion from 62] 67 + contains(f,(A,s$18)) -> A=s$16 [negative chaining of 65 from 26] 73 + contains(f,(s$16,A)),contains(f,(s$16,B)) -> contains(f,(s$3(p,f,s$17,A),A)),contains(f,(s$3(q,f,s$17,B),B)) [negative chaining of 64 from 49] 105 + contains(f,(s$16,A)),contains(f,(s$16,s$18)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(q,f,s$17,s$18)=s$16 [negative chaining of 73 from 67] 108 + contains(f,(s$16,A)) -> s$3(q,f,s$17,s$18)=s$16,contains(f,(s$3(p,f,s$17,A),A)) [reduction of 105 by [65]] 115 + contains(f,(s$16,s$18)) -> s$3(q,f,s$17,s$18)=s$16,s$3(p,f,s$17,s$18)=s$16 [negative chaining of 108 from 67] 117 + s$3(p,f,s$17,s$18)=s$16,s$3(q,f,s$17,s$18)=s$16 [reduction of 115 by [65]] 119 + contains(f,(A,s$18)),contains(p,(s$17,A)) -> contains(q,(s$17,s$16)),s$3(p,f,s$17,s$18)=s$16 [chaining of 117 from 48] 122 + contains(f,(A,s$18)),contains(p,(s$17,A)),contains(p,(s$17,s$16)) -> s$3(p,f,s$17,s$18)=s$16 [reduction of 119 by [50,L]] 123 + contains(f,(s$16,A)),contains(f,(B,s$18)),contains(p,(s$17,B)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(p,f,s$17,s$18)=s$16 [negative chaining of 64 from 122] 247 + contains(f,(s$16,A)),contains(f,(s$16,B)),contains(f,(s$16,s$18)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(p,f,s$17,s$18)=s$16,contains(f,(s$3(p,f,s$17,B),B)) [negative chaining of 64 from 123] 251 + contains(f,(s$16,A)),contains(f,(s$16,s$18)) -> s$3(p,f,s$17,s$18)=s$16,contains(f,(s$3(p,f,s$17,A),A)) [condensement of 247] 252 + contains(f,(s$16,A)) -> contains(f,(s$3(p,f,s$17,A),A)),s$3(p,f,s$17,s$18)=s$16 [reduction of 251 by [65]] 256 + contains(f,(s$16,s$18)) -> s$3(p,f,s$17,s$18)=s$16,s$3(p,f,s$17,s$18)=s$16 [negative chaining of 252 from 67] 266 + contains(f,(s$16,s$18)) -> s$3(p,f,s$17,s$18)=s$16 [condensement of 256] 267 + s$3(p,f,s$17,s$18)=s$16 [reduction of 266 by [65]] 273 + contains(f,(s$16,s$18)) -> contains(p,(s$17,s$16)),contains(p,(s$17,s$16)) [chaining of 267 from 63] 282 + contains(f,(s$16,s$18)) -> contains(p,(s$17,s$16)) [condensement of 273] 283 + contains(p,(s$17,s$16)) [reduction of 282 by [65]] 285 + contains(q,(s$17,s$16)) -> [reduction of 50 by [283,L,L]] 287 + contains(f,(s$16,A)) -> contains(f,(s$3(q,f,s$17,A),A)) [negative chaining of 283 from 49] 297 + contains(f,(s$16,s$18)) -> s$3(q,f,s$17,s$18)=s$16 [negative chaining of 287 from 67] 301 + s$3(q,f,s$17,s$18)=s$16 [reduction of 297 by [65]] 304 + contains(f,(A,s$18)),contains(p,(s$17,A)) -> contains(q,(s$17,s$16)) [chaining of 301 from 48] 307 + contains(f,(A,s$18)),contains(p,(s$17,A)) -> [reduction of 304 by [285,L]] 308 + contains(f,(s$16,s$18)) -> [negative chaining of 283 from 307] 319 + false [reduction of 308 by [65]] Length = 72, Depth = 38, Search Depth = 14 Total time: 8330 milliseconds Number of forward inferences: 181 Number of tableau inferences: 59 Number of generated clauses: 319 Number of kept clauses: 163 */