%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL044-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:45 PM UTC 2026
% Result : Unsatisfiable 32.17s 4.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL044-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n009.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 04:08:28 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 32.17/4.82 % Refutation found
% 32.17/4.82 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 32.17/4.82 % SZS output start CNFRefutation for theBenchmark
% 32.17/4.82 fof(f1,axiom,(
% 32.17/4.82 (![A,B]: (join(A,B) = join(B,A) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f2,axiom,(
% 32.17/4.82 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f3,axiom,(
% 32.17/4.82 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f4,axiom,(
% 32.17/4.82 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f5,axiom,(
% 32.17/4.82 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f6,axiom,(
% 32.17/4.82 (![A]: (composition(A,one) = A ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f7,axiom,(
% 32.17/4.82 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f8,axiom,(
% 32.17/4.82 (![A]: (converse(converse(A)) = A ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f9,axiom,(
% 32.17/4.82 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f10,axiom,(
% 32.17/4.82 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f11,axiom,(
% 32.17/4.82 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f12,axiom,(
% 32.17/4.82 (![A]: (top = join(A,complement(A)) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f13,axiom,(
% 32.17/4.82 (![A]: (zero = meet(A,complement(A)) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f14,axiom,(
% 32.17/4.82 (![A,B,C]: (join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f16,axiom,(
% 32.17/4.82 (![A,B,C]: (join(meet(composition(A,B),C),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C) ))),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f17,negated_conjecture,(
% 32.17/4.82 join(composition(complement(sk1),sk2),complement(sk3)) = complement(sk3) ),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f18,negated_conjecture,(
% 32.17/4.82 join(composition(sk3,converse(sk2)),sk1) != sk1 ),
% 32.17/4.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.17/4.82 fof(f19,plain,(
% 32.17/4.82 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f1])).
% 32.17/4.82 fof(f20,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f2])).
% 32.17/4.82 fof(f21,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f3])).
% 32.17/4.82 fof(f22,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f4])).
% 32.17/4.82 fof(f23,plain,(
% 32.17/4.82 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f5])).
% 32.17/4.82 fof(f24,plain,(
% 32.17/4.82 ![X0]: (composition(X0,one)=X0)),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f6])).
% 32.17/4.82 fof(f25,plain,(
% 32.17/4.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f7])).
% 32.17/4.82 fof(f26,plain,(
% 32.17/4.82 ![X0]: (converse(converse(X0))=X0)),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f8])).
% 32.17/4.82 fof(f27,plain,(
% 32.17/4.82 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f9])).
% 32.17/4.82 fof(f28,plain,(
% 32.17/4.82 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f10])).
% 32.17/4.82 fof(f29,plain,(
% 32.17/4.82 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f11])).
% 32.17/4.82 fof(f30,plain,(
% 32.17/4.82 ![X0]: (top=join(X0,complement(X0)))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f12])).
% 32.17/4.82 fof(f31,plain,(
% 32.17/4.82 ![X0]: (zero=meet(X0,complement(X0)))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f13])).
% 32.17/4.82 fof(f32,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f14])).
% 32.17/4.82 fof(f34,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f16])).
% 32.17/4.82 fof(f35,plain,(
% 32.17/4.82 join(composition(complement(sk1),sk2),complement(sk3))=complement(sk3)),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f17])).
% 32.17/4.82 fof(f36,plain,(
% 32.17/4.82 ~join(composition(sk3,converse(sk2)),sk1)=sk1),
% 32.17/4.82 inference(cnf_transformation,[status(thm)],[f18])).
% 32.17/4.82 fof(f37,definition,(
% 32.17/4.82 sF2_fnc=converse(sk2)),
% 32.17/4.82 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 32.17/4.82 fof(f38,definition,(
% 32.17/4.82 sF1_fnc=composition(sk3,sF2_fnc)),
% 32.17/4.82 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 32.17/4.82 fof(f39,definition,(
% 32.17/4.82 sF0_fnc=join(sF1_fnc,sk1)),
% 32.17/4.82 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 32.17/4.82 fof(f40,plain,(
% 32.17/4.82 ~sF0_fnc=sk1),
% 32.17/4.82 inference(definition_folding,[],[f36,f39,f38,f37])).
% 32.17/4.82 fof(f41,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 32.17/4.82 fof(f42,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f22,f41])).
% 32.17/4.82 fof(f43,plain,(
% 32.17/4.82 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 32.17/4.82 fof(f44,plain,(
% 32.17/4.82 join(complement(sk3),composition(complement(sk1),sk2))=complement(sk3)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f35])).
% 32.17/4.82 fof(f45,plain,(
% 32.17/4.82 sF0_fnc=join(sk1,sF1_fnc)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f39])).
% 32.17/4.82 fof(f46,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f42])).
% 32.17/4.82 fof(f48,plain,(
% 32.17/4.82 converse(sF2_fnc)=sk2),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f37,f26])).
% 32.17/4.82 fof(f54,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f20])).
% 32.17/4.82 fof(f59,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f20])).
% 32.17/4.82 fof(f65,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f22])).
% 32.17/4.82 fof(f76,plain,(
% 32.17/4.82 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f26,f27])).
% 32.17/4.82 fof(f79,plain,(
% 32.17/4.82 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f26,f27])).
% 32.17/4.82 fof(f87,plain,(
% 32.17/4.82 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f26,f28])).
% 32.17/4.82 fof(f90,plain,(
% 32.17/4.82 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f26,f28])).
% 32.17/4.82 fof(f96,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f54])).
% 32.17/4.82 fof(f104,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,X2)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f54])).
% 32.17/4.82 fof(f117,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f54])).
% 32.17/4.82 fof(f204,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f22,f65])).
% 32.17/4.82 fof(f214,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f204,f34])).
% 32.17/4.82 fof(f216,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f214])).
% 32.17/4.82 fof(f225,plain,(
% 32.17/4.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f25])).
% 32.17/4.82 fof(f228,plain,(
% 32.17/4.82 ![X0,X1,X2,X3]: (composition(join(composition(X0,X1),X2),X3)=join(composition(X0,composition(X1,X3)),composition(X2,X3)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f23,f25])).
% 32.17/4.82 fof(f273,plain,(
% 32.17/4.82 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f24,f23])).
% 32.17/4.82 fof(f284,plain,(
% 32.17/4.82 ![X0]: (meet(complement(X0),X0)=complement(top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f30,f65])).
% 32.17/4.82 fof(f286,plain,(
% 32.17/4.82 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f30,f59])).
% 32.17/4.82 fof(f289,plain,(
% 32.17/4.82 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f30,f20])).
% 32.17/4.82 fof(f292,plain,(
% 32.17/4.82 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f284])).
% 32.17/4.82 fof(f293,plain,(
% 32.17/4.82 zero=complement(top)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f31,f292])).
% 32.17/4.82 fof(f295,plain,(
% 32.17/4.82 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f54,f286])).
% 32.17/4.82 fof(f298,plain,(
% 32.17/4.82 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f293,f43])).
% 32.17/4.82 fof(f303,plain,(
% 32.17/4.82 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f298])).
% 32.17/4.82 fof(f465,plain,(
% 32.17/4.82 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f30,f76])).
% 32.17/4.82 fof(f808,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,composition(converse(X0),converse(X2)))))=composition(meet(X0,composition(converse(X2),converse(X1))),meet(X1,composition(converse(X0),converse(X2)))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f28,f32])).
% 32.17/4.82 fof(f859,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,composition(converse(X2),converse(X1))),meet(X1,composition(converse(X0),converse(X2)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f28,f808])).
% 32.17/4.82 fof(f860,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,converse(composition(X1,X2))),meet(X1,composition(converse(X0),converse(X2)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f28,f859])).
% 32.17/4.82 fof(f861,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),converse(X2)),composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))=composition(meet(X0,converse(composition(X1,X2))),meet(X1,converse(composition(X2,X0)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f28,f860])).
% 32.17/4.82 fof(f902,plain,(
% 32.17/4.82 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f31,f46])).
% 32.17/4.82 fof(f905,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f65,f46])).
% 32.17/4.82 fof(f906,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f22,f46])).
% 32.17/4.82 fof(f909,plain,(
% 32.17/4.82 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f30,f46])).
% 32.17/4.82 fof(f924,plain,(
% 32.17/4.82 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f65,f902])).
% 32.17/4.82 fof(f925,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f905])).
% 32.17/4.82 fof(f926,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f906])).
% 32.17/4.82 fof(f929,plain,(
% 32.17/4.82 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f909])).
% 32.17/4.82 fof(f930,plain,(
% 32.17/4.82 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f929])).
% 32.17/4.82 fof(f942,plain,(
% 32.17/4.82 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(meet(sk3,composition(X0,converse(sF2_fnc))),sF2_fnc)))=meet(X0,composition(meet(sk3,composition(X0,converse(sF2_fnc))),sF2_fnc)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f38,f216])).
% 32.17/4.82 fof(f968,plain,(
% 32.17/4.82 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f216,f20])).
% 32.17/4.82 fof(f975,plain,(
% 32.17/4.82 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(meet(sk3,composition(X0,sk2)),sF2_fnc)))=meet(X0,composition(meet(sk3,composition(X0,converse(sF2_fnc))),sF2_fnc)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f48,f942])).
% 32.17/4.82 fof(f976,plain,(
% 32.17/4.82 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(meet(sk3,composition(X0,sk2)),sF2_fnc)))=meet(X0,composition(meet(sk3,composition(X0,sk2)),sF2_fnc)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f48,f975])).
% 32.17/4.82 fof(f1231,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f925])).
% 32.17/4.82 fof(f1252,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f926])).
% 32.17/4.82 fof(f1268,plain,(
% 32.17/4.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(join(complement(X0),complement(X1)),complement(meet(X1,X0)))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f65,f930])).
% 32.17/4.82 fof(f1274,plain,(
% 32.17/4.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X1,X0)),join(complement(X0),complement(X1)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f1268])).
% 32.17/4.82 fof(f1283,plain,(
% 32.17/4.82 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f31,f1231])).
% 32.17/4.82 fof(f1296,plain,(
% 32.17/4.82 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f19,f1283])).
% 32.17/4.82 fof(f1303,plain,(
% 32.17/4.82 ![X0]: (complement(complement(X0))=X0)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f930,f1296])).
% 32.17/4.82 fof(f1309,plain,(
% 32.17/4.82 complement(zero)=top),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f293,f1303])).
% 32.17/4.82 fof(f1310,plain,(
% 32.17/4.82 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f65,f1303])).
% 32.17/4.82 fof(f1311,plain,(
% 32.17/4.82 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f22,f1303])).
% 32.17/4.82 fof(f1319,plain,(
% 32.17/4.82 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f65])).
% 32.17/4.82 fof(f1320,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f65])).
% 32.17/4.82 fof(f1321,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f22])).
% 32.17/4.82 fof(f1322,plain,(
% 32.17/4.82 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f22])).
% 32.17/4.82 fof(f1330,plain,(
% 32.17/4.82 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X1,X0)),complement(meet(X1,X0)))))),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f1310,f1274])).
% 32.17/4.82 fof(f1367,plain,(
% 32.17/4.82 ![X0,X1]: (complement(meet(X0,X1))=join(zero,meet(complement(meet(X1,X0)),complement(meet(X1,X0)))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1311,f1330])).
% 32.17/4.82 fof(f1368,plain,(
% 32.17/4.82 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f924,f1367])).
% 32.17/4.82 fof(f1407,plain,(
% 32.17/4.82 ![X0,X1]: (top=join(meet(X0,X1),complement(meet(X1,X0))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1368,f30])).
% 32.17/4.82 fof(f1878,plain,(
% 32.17/4.82 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f24,f90])).
% 32.17/4.82 fof(f1933,plain,(
% 32.17/4.82 ![X0]: (X0=composition(converse(one),X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f26,f1878])).
% 32.17/4.82 fof(f1989,plain,(
% 32.17/4.82 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f273,f1933])).
% 32.17/4.82 fof(f1990,plain,(
% 32.17/4.82 one=converse(one)),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f24,f1933])).
% 32.17/4.82 fof(f1991,plain,(
% 32.17/4.82 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1933,f43])).
% 32.17/4.82 fof(f2030,plain,(
% 32.17/4.82 ![X0]: (composition(one,X0)=X0)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1933,f1989])).
% 32.17/4.82 fof(f2040,plain,(
% 32.17/4.82 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1311,f1991])).
% 32.17/4.82 fof(f2041,plain,(
% 32.17/4.82 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f2030,f2040])).
% 32.17/4.82 fof(f2236,plain,(
% 32.17/4.82 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f2041,f1303])).
% 32.17/4.82 fof(f2245,plain,(
% 32.17/4.82 ![X0]: (X0=join(zero,X0))),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f2250,f924])).
% 32.17/4.82 fof(f2250,plain,(
% 32.17/4.82 ![X0]: (X0=meet(X0,X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1303,f2236])).
% 32.17/4.82 fof(f2272,plain,(
% 32.17/4.82 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f2245,f303])).
% 32.17/4.82 fof(f2303,plain,(
% 32.17/4.82 ![X0]: (X0=join(X0,meet(complement(X0),X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f2250,f1252])).
% 32.17/4.82 fof(f2371,plain,(
% 32.17/4.82 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f2303])).
% 32.17/4.82 fof(f2374,plain,(
% 32.17/4.82 ![X0]: (X0=join(X0,zero))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f31,f2371])).
% 32.17/4.82 fof(f2385,plain,(
% 32.17/4.82 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f2245,f79])).
% 32.17/4.82 fof(f2400,plain,(
% 32.17/4.82 ![X0]: (X0=join(converse(zero),X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f26,f2385])).
% 32.17/4.82 fof(f2444,plain,(
% 32.17/4.82 zero=converse(zero)),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f2374,f2400])).
% 32.17/4.82 fof(f5351,plain,(
% 32.17/4.82 ![X0]: (complement(meet(X0,top))=join(zero,complement(X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f293,f1310])).
% 32.17/4.82 fof(f5361,plain,(
% 32.17/4.82 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=join(top,complement(X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1310,f295])).
% 32.17/4.82 fof(f5382,plain,(
% 32.17/4.82 ![X0]: (complement(meet(X0,top))=complement(X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f2245,f5351])).
% 32.17/4.82 fof(f5679,plain,(
% 32.17/4.82 ![X0]: (complement(complement(X0))=meet(X0,top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f5382,f1303])).
% 32.17/4.82 fof(f5719,plain,(
% 32.17/4.82 ![X0]: (X0=meet(X0,top))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1303,f5679])).
% 32.17/4.82 fof(f5749,plain,(
% 32.17/4.82 ![X0]: (X0=meet(top,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f5719])).
% 32.17/4.82 fof(f6268,plain,(
% 32.17/4.82 ![X0]: (meet(complement(X0),zero)=complement(join(top,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1309,f1319])).
% 32.17/4.82 fof(f6269,plain,(
% 32.17/4.82 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f1319])).
% 32.17/4.82 fof(f6332,plain,(
% 32.17/4.82 ![X0]: (meet(zero,complement(X0))=complement(join(top,X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f6268])).
% 32.17/4.82 fof(f6549,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(join(complement(complement(X0)),X1)))=complement(join(top,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f289,f1321])).
% 32.17/4.82 fof(f6568,plain,(
% 32.17/4.82 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X0,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f1321])).
% 32.17/4.82 fof(f6611,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,meet(complement(X0),complement(X1)))=complement(join(top,X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1321,f6549])).
% 32.17/4.82 fof(f6612,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=complement(join(top,X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f6269,f6611])).
% 32.17/4.82 fof(f6613,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=meet(zero,complement(X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f6332,f6612])).
% 32.17/4.82 fof(f6799,plain,(
% 32.17/4.82 ![X0]: (top=join(X0,complement(meet(X0,X0))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f2250,f1407])).
% 32.17/4.82 fof(f6850,plain,(
% 32.17/4.82 ![X0]: (top=join(top,complement(X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f5361,f6799])).
% 32.17/4.82 fof(f6906,plain,(
% 32.17/4.82 ![X0]: (top=join(top,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1303,f6850])).
% 32.17/4.82 fof(f6911,plain,(
% 32.17/4.82 ![X0]: (meet(complement(top),X0)=complement(top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f6850,f1322])).
% 32.17/4.82 fof(f6912,plain,(
% 32.17/4.82 ![X0]: (meet(X0,complement(top))=complement(top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f6850,f1320])).
% 32.17/4.82 fof(f7033,plain,(
% 32.17/4.82 ![X0]: (meet(zero,X0)=complement(top))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f6911])).
% 32.17/4.82 fof(f7038,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,complement(join(X1,X0)))=zero)),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f7081,f6613])).
% 32.17/4.82 fof(f7081,plain,(
% 32.17/4.82 ![X0]: (meet(zero,X0)=zero)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f7033])).
% 32.17/4.82 fof(f7082,plain,(
% 32.17/4.82 ![X0]: (meet(X0,zero)=complement(top))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f6912])).
% 32.17/4.82 fof(f7091,plain,(
% 32.17/4.82 ![X0]: (meet(X0,zero)=zero)),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f293,f7082])).
% 32.17/4.82 fof(f7761,plain,(
% 32.17/4.82 top=converse(top)),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f465,f6906])).
% 32.17/4.82 fof(f7898,plain,(
% 32.17/4.82 ![X0]: (converse(composition(top,X0))=composition(converse(X0),top))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f7761,f90])).
% 32.17/4.82 fof(f7905,plain,(
% 32.17/4.82 ![X0]: (converse(composition(X0,top))=composition(top,converse(X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f7761,f87])).
% 32.17/4.82 fof(f8723,plain,(
% 32.17/4.82 meet(composition(complement(sk1),sk2),complement(complement(sk3)))=zero),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f44,f7038])).
% 32.17/4.82 fof(f8758,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(meet(X0,join(X1,X0)),zero))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f7038,f926])).
% 32.17/4.82 fof(f8789,plain,(
% 32.17/4.82 meet(complement(complement(sk3)),composition(complement(sk1),sk2))=zero),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f8723])).
% 32.17/4.82 fof(f8792,plain,(
% 32.17/4.82 meet(sk3,composition(complement(sk1),sk2))=zero),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1303,f8789])).
% 32.17/4.82 fof(f8829,plain,(
% 32.17/4.82 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f2374,f8758])).
% 32.17/4.82 fof(f8887,plain,(
% 32.17/4.82 ![X0,X1]: (complement(X0)=meet(complement(X0),complement(meet(X1,X0))))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1311,f8829])).
% 32.17/4.82 fof(f8912,plain,(
% 32.17/4.82 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f19,f8829])).
% 32.17/4.82 fof(f8940,plain,(
% 32.17/4.82 ![X0,X1]: (complement(X0)=complement(join(X0,meet(X1,X0))))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f6568,f8887])).
% 32.17/4.82 fof(f8976,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1252,f8912])).
% 32.17/4.82 fof(f8977,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f1231,f8912])).
% 32.17/4.82 fof(f9041,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f8976])).
% 32.17/4.82 fof(f9046,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f204,f8977])).
% 32.17/4.82 fof(f10075,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f9041])).
% 32.17/4.82 fof(f10084,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(meet(composition(X0,X1),X2),composition(meet(X0,composition(meet(composition(X0,X1),X2),converse(X1))),X1)))=meet(meet(composition(X0,X1),X2),composition(meet(X0,composition(meet(composition(X0,X1),X2),converse(X1))),X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f9041,f216])).
% 32.17/4.82 fof(f10163,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f9046])).
% 32.17/4.82 fof(f11926,plain,(
% 32.17/4.82 ![X0,X1]: (complement(complement(X0))=join(X0,meet(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f8940,f1303])).
% 32.17/4.82 fof(f12034,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f1303,f11926])).
% 32.17/4.82 fof(f12069,plain,(
% 32.17/4.82 ![X0]: (X0=join(X0,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f5749,f12034])).
% 32.17/4.82 fof(f12072,plain,(
% 32.17/4.82 ![X0,X1]: (meet(X0,X1)=join(meet(X0,X1),meet(X1,X0)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f10163,f12034])).
% 32.17/4.82 fof(f12086,plain,(
% 32.17/4.82 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f204,f12034])).
% 32.17/4.82 fof(f12117,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(meet(X0,X1),join(X1,X2))=join(X2,X1))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f12034,f117])).
% 32.17/4.82 fof(f12170,plain,(
% 32.17/4.82 ![X0,X1,X2]: (meet(composition(X0,X1),X2)=meet(meet(composition(X0,X1),X2),composition(meet(X0,composition(meet(composition(X0,X1),X2),converse(X1))),X1)))),
% 32.17/4.82 inference(backward_demodulation,[status(thm)],[f12086,f10084])).
% 32.17/4.82 fof(f12201,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),X2))=join(X2,X0))),
% 32.17/4.82 inference(forward_demodulation,[status(thm)],[f104,f12117])).
% 32.17/4.82 fof(f12306,plain,(
% 32.17/4.82 ![X0,X1]: (join(X0,join(X1,X0))=join(X1,X0))),
% 32.17/4.82 inference(paramodulation,[status(thm)],[f12069,f104])).
% 32.17/4.82 fof(f12448,plain,(
% 32.17/4.82 ![X0,X1,X2]: (join(X0,X1)=join(meet(X0,X2),join(X1,X0)))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f12086,f96])).
% 32.17/4.83 fof(f12479,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(X0,X2))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f117,f12448])).
% 32.17/4.83 fof(f19166,plain,(
% 32.17/4.83 composition(top,complement(composition(top,top)))=zero),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f7761,f2272])).
% 32.17/4.83 fof(f19200,plain,(
% 32.17/4.83 ![X0]: (converse(zero)=composition(converse(complement(composition(X0,top))),X0))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f2272,f90])).
% 32.17/4.83 fof(f19274,plain,(
% 32.17/4.83 ![X0]: (zero=composition(converse(complement(composition(X0,top))),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f2444,f19200])).
% 32.17/4.83 fof(f27737,plain,(
% 32.17/4.83 join(meet(sF1_fnc,complement(sk1)),meet(complement(sk1),composition(zero,sF2_fnc)))=meet(complement(sk1),composition(meet(sk3,composition(complement(sk1),sk2)),sF2_fnc))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f8792,f976])).
% 32.17/4.83 fof(f27783,plain,(
% 32.17/4.83 join(meet(sF1_fnc,complement(sk1)),meet(complement(sk1),composition(zero,sF2_fnc)))=meet(complement(sk1),composition(zero,sF2_fnc))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f8792,f27737])).
% 32.17/4.83 fof(f34858,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,X0),X2))=join(meet(X0,X1),X2))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f12072,f20])).
% 32.17/4.83 fof(f35471,plain,(
% 32.17/4.83 ![X0,X1]: (join(X0,X1)=join(meet(X1,complement(X0)),X0))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f926,f12201])).
% 32.17/4.83 fof(f35757,plain,(
% 32.17/4.83 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f19,f35471])).
% 32.17/4.83 fof(f38161,plain,(
% 32.17/4.83 ![X0,X1,X2,X3]: (join(meet(X0,composition(X1,X2)),join(meet(meet(composition(X1,X2),X0),composition(meet(X1,composition(meet(composition(X1,X2),X0),converse(X2))),X2)),X3))=join(meet(meet(composition(X1,X2),X0),composition(meet(X1,composition(meet(composition(X1,X2),X0),converse(X2))),X2)),X3))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f10163,f968])).
% 32.17/4.83 fof(f38193,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f24,f968])).
% 32.17/4.83 fof(f38364,plain,(
% 32.17/4.83 ![X0,X1,X2,X3]: (join(meet(X0,composition(X1,X2)),join(meet(composition(X1,X2),X0),X3))=join(meet(meet(composition(X1,X2),X0),composition(meet(X1,composition(meet(composition(X1,X2),X0),converse(X2))),X2)),X3))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f12170,f38161])).
% 32.17/4.83 fof(f38365,plain,(
% 32.17/4.83 ![X0,X1,X2,X3]: (join(meet(X0,composition(X1,X2)),X3)=join(meet(meet(composition(X1,X2),X0),composition(meet(X1,composition(meet(composition(X1,X2),X0),converse(X2))),X2)),X3))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f34858,f38364])).
% 32.17/4.83 fof(f38366,plain,(
% 32.17/4.83 ![X0,X1,X2,X3]: (join(meet(X0,composition(X1,X2)),X3)=join(meet(composition(X1,X2),X0),X3))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f12170,f38365])).
% 32.17/4.83 fof(f38391,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f24,f38193])).
% 32.17/4.83 fof(f38392,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,one))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f1990,f38391])).
% 32.17/4.83 fof(f38393,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f24,f38392])).
% 32.17/4.83 fof(f38394,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,composition(meet(X1,composition(X2,converse(one))),one)),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f12201,f38393])).
% 32.17/4.83 fof(f38395,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,meet(X1,composition(X2,converse(one)))),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f24,f38394])).
% 32.17/4.83 fof(f38396,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,meet(X1,composition(X2,one))),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f1990,f38395])).
% 32.17/4.83 fof(f38397,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,meet(X1,X2)),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f24,f38396])).
% 32.17/4.83 fof(f38406,plain,(
% 32.17/4.83 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,X1),X0))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f10075,f38397])).
% 32.17/4.83 fof(f39931,plain,(
% 32.17/4.83 ![X0,X1]: (join(meet(X0,complement(X1)),join(X1,X0))=join(X1,meet(X0,complement(X1))))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f35757,f12306])).
% 32.17/4.83 fof(f40068,plain,(
% 32.17/4.83 ![X0,X1]: (join(X0,join(X1,meet(X0,complement(X1))))=join(X1,meet(X0,complement(X1))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f117,f39931])).
% 32.17/4.83 fof(f40069,plain,(
% 32.17/4.83 ![X0,X1]: (join(X0,X1)=join(X1,meet(X0,complement(X1))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f12479,f40068])).
% 32.17/4.83 fof(f49124,plain,(
% 32.17/4.83 ![X0]: (join(meet(composition(complement(composition(top,top)),X0),converse(top)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f19166,f861])).
% 32.17/4.83 fof(f49143,plain,(
% 32.17/4.83 ![X0,X1]: (composition(join(composition(X0,top),X1),complement(composition(top,top)))=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f19166,f228])).
% 32.17/4.83 fof(f49145,plain,(
% 32.17/4.83 ![X0]: (composition(join(top,X0),complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f19166,f225])).
% 32.17/4.83 fof(f49153,plain,(
% 32.17/4.83 ![X0]: (composition(top,composition(complement(composition(top,top)),X0))=composition(zero,X0))),
% 32.17/4.83 inference(paramodulation,[status(thm)],[f19166,f23])).
% 32.17/4.83 fof(f49216,plain,(
% 32.17/4.83 ![X0]: (join(meet(converse(top),composition(complement(composition(top,top)),X0)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f38366,f49124])).
% 32.17/4.83 fof(f49217,plain,(
% 32.17/4.83 ![X0]: (join(meet(top,composition(complement(composition(top,top)),X0)),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7761,f49216])).
% 32.17/4.83 fof(f49218,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f5749,f49217])).
% 32.17/4.83 fof(f49219,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),meet(X0,converse(zero))))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7905,f49218])).
% 32.17/4.83 fof(f49220,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),meet(X0,zero)))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f2444,f49219])).
% 32.17/4.83 fof(f49221,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=composition(meet(complement(composition(top,top)),converse(composition(X0,top))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7091,f49220])).
% 32.17/4.83 fof(f49222,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=composition(meet(complement(composition(top,top)),composition(top,converse(X0))),meet(X0,converse(composition(top,complement(composition(top,top)))))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7905,f49221])).
% 32.17/4.83 fof(f49223,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=composition(meet(complement(composition(top,top)),composition(top,converse(X0))),meet(X0,composition(converse(complement(composition(top,top))),top))))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7898,f49222])).
% 32.17/4.83 fof(f49224,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=composition(meet(complement(composition(top,top)),composition(top,converse(X0))),meet(X0,zero)))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f19274,f49223])).
% 32.17/4.83 fof(f49225,plain,(
% 32.17/4.83 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f7091,f49224])).
% 32.17/4.83 fof(f49319,plain,(
% 32.17/4.83 ![X0]: (composition(top,complement(composition(top,top)))=join(composition(X0,complement(composition(top,top))),zero))),
% 32.17/4.83 inference(forward_demodulation,[status(thm)],[f6906,f49145])).
% 32.17/4.83 fof(f49320,plain,(
% 32.17/4.83 ![X0]: (zero=join(composition(X0,complement(composition(top,top))),zero))),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f19166,f49319])).
% 32.17/4.90 fof(f49322,plain,(
% 32.17/4.90 ![X0,X1]: (zero=join(composition(X0,zero),composition(X1,complement(composition(top,top)))))),
% 32.17/4.90 inference(backward_demodulation,[status(thm)],[f49327,f49143])).
% 32.17/4.90 fof(f49327,plain,(
% 32.17/4.90 ![X0]: (zero=composition(X0,complement(composition(top,top))))),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f2374,f49320])).
% 32.17/4.90 fof(f49346,plain,(
% 32.17/4.90 ![X0]: (zero=join(composition(X0,zero),zero))),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f49327,f49322])).
% 32.17/4.90 fof(f49359,plain,(
% 32.17/4.90 ![X0]: (join(composition(complement(composition(top,top)),X0),composition(meet(complement(composition(top,top)),composition(top,converse(X0))),zero))=zero)),
% 32.17/4.90 inference(backward_demodulation,[status(thm)],[f49468,f49225])).
% 32.17/4.90 fof(f49468,plain,(
% 32.17/4.90 ![X0]: (zero=composition(X0,zero))),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f2374,f49346])).
% 32.17/4.90 fof(f49497,plain,(
% 32.17/4.90 ![X0]: (join(composition(complement(composition(top,top)),X0),zero)=zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f49468,f49359])).
% 32.17/4.90 fof(f49499,plain,(
% 32.17/4.90 ![X0]: (composition(top,zero)=composition(zero,X0))),
% 32.17/4.90 inference(backward_demodulation,[status(thm)],[f49501,f49153])).
% 32.17/4.90 fof(f49501,plain,(
% 32.17/4.90 ![X0]: (composition(complement(composition(top,top)),X0)=zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f2374,f49497])).
% 32.17/4.90 fof(f49991,plain,(
% 32.17/4.90 join(meet(sF1_fnc,complement(sk1)),meet(complement(sk1),composition(zero,sF2_fnc)))=meet(complement(sk1),zero)),
% 32.17/4.90 inference(backward_demodulation,[status(thm)],[f50052,f27783])).
% 32.17/4.90 fof(f50052,plain,(
% 32.17/4.90 ![X0]: (zero=composition(zero,X0))),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f49468,f49499])).
% 32.17/4.90 fof(f50074,plain,(
% 32.17/4.90 join(meet(sF1_fnc,complement(sk1)),meet(complement(sk1),zero))=meet(complement(sk1),zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f50052,f49991])).
% 32.17/4.90 fof(f50075,plain,(
% 32.17/4.90 join(meet(zero,complement(sk1)),meet(sF1_fnc,complement(sk1)))=meet(complement(sk1),zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f38406,f50074])).
% 32.17/4.90 fof(f50076,plain,(
% 32.17/4.90 join(zero,meet(sF1_fnc,complement(sk1)))=meet(complement(sk1),zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f7081,f50075])).
% 32.17/4.90 fof(f50077,plain,(
% 32.17/4.90 meet(sF1_fnc,complement(sk1))=meet(complement(sk1),zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f2245,f50076])).
% 32.17/4.90 fof(f50078,plain,(
% 32.17/4.90 meet(sF1_fnc,complement(sk1))=zero),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f7091,f50077])).
% 32.17/4.90 fof(f51022,plain,(
% 32.17/4.90 join(sF1_fnc,sk1)=join(sk1,zero)),
% 32.17/4.90 inference(paramodulation,[status(thm)],[f50078,f40069])).
% 32.17/4.90 fof(f51077,plain,(
% 32.17/4.90 join(sk1,sF1_fnc)=join(sk1,zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f19,f51022])).
% 32.17/4.90 fof(f51078,plain,(
% 32.17/4.90 sF0_fnc=join(sk1,zero)),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f45,f51077])).
% 32.17/4.90 fof(f51079,plain,(
% 32.17/4.90 sF0_fnc=sk1),
% 32.17/4.90 inference(forward_demodulation,[status(thm)],[f2374,f51078])).
% 32.17/4.90 fof(f51080,plain,(
% 32.17/4.90 $false),
% 32.17/4.90 inference(forward_subsumption_resolution,[status(thm)],[f51079,f40])).
% 32.17/4.90 % SZS output end CNFRefutation for theBenchmark.p
% 2.00/4.97 % Elapsed time: 4.539703 seconds
% 2.00/4.97 % CPU time: 35.288230 seconds
% 2.00/4.97 % Total memory used: 340.563 MB
% 2.00/4.97 % Net memory used: 333.811 MB
%------------------------------------------------------------------------------