%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL050+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:29 PM UTC 2026
% Result : Theorem 16.34s 2.48s
% Output : CNFRefutation 16.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 19
% Syntax : Number of formulae : 251 ( 251 unt; 4 def)
% Number of atoms : 251 ( 250 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 275 ( 274 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [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))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f21,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f22,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f24,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f29,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f30,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f31,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f32,plain,
! [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))),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f35,plain,
? [X0] : complement(composition(X0,top)) != composition(complement(composition(X0,top)),top),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f36,plain,
complement(composition(sK0_skl,top)) != composition(complement(composition(sK0_skl,top)),top),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f35]) ).
fof(f37,plain,
complement(composition(sK0_skl,top)) != composition(complement(composition(sK0_skl,top)),top),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,definition,
sF1_fnc = composition(sK0_skl,top),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f39,definition,
sF0_fnc = complement(sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f40,definition,
sF3_fnc = complement(sF1_fnc),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f41,definition,
sF2_fnc = composition(sF3_fnc,top),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f42,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f37,f41,f40,f39,f38]) ).
fof(f43,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f19,f21]) ).
fof(f44,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f22,f43]) ).
fof(f45,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f19,f29]) ).
fof(f46,plain,
sF3_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f39,f40]) ).
fof(f47,plain,
sF2_fnc = composition(sF0_fnc,top),
inference(forward_demodulation,[status(thm)],[f46,f41]) ).
fof(f48,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f19,f44]) ).
fof(f55,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f22,f30]) ).
fof(f57,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f30,f22]) ).
fof(f58,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f20,f55]) ).
fof(f60,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f31,f57]) ).
fof(f73,plain,
! [X0] : composition(sF0_fnc,composition(top,X0)) = composition(sF2_fnc,X0),
inference(paramodulation,[status(thm)],[f47,f23]) ).
fof(f98,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = complement(top),
inference(paramodulation,[status(thm)],[f60,f45]) ).
fof(f104,plain,
join(complement(top),composition(converse(sF0_fnc),complement(sF2_fnc))) = complement(top),
inference(paramodulation,[status(thm)],[f47,f45]) ).
fof(f106,plain,
join(complement(top),composition(converse(sK0_skl),complement(sF1_fnc))) = complement(top),
inference(paramodulation,[status(thm)],[f38,f45]) ).
fof(f107,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f60,f98]) ).
fof(f111,plain,
join(zero,composition(converse(sF0_fnc),complement(sF2_fnc))) = complement(top),
inference(forward_demodulation,[status(thm)],[f60,f104]) ).
fof(f112,plain,
join(zero,composition(converse(sF0_fnc),complement(sF2_fnc))) = zero,
inference(forward_demodulation,[status(thm)],[f60,f111]) ).
fof(f113,plain,
join(zero,composition(converse(sK0_skl),complement(sF1_fnc))) = complement(top),
inference(forward_demodulation,[status(thm)],[f60,f106]) ).
fof(f114,plain,
join(zero,composition(converse(sK0_skl),sF0_fnc)) = complement(top),
inference(forward_demodulation,[status(thm)],[f39,f113]) ).
fof(f115,plain,
join(zero,composition(converse(sK0_skl),sF0_fnc)) = zero,
inference(forward_demodulation,[status(thm)],[f60,f114]) ).
fof(f120,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f22,f48]) ).
fof(f122,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f30,f48]) ).
fof(f131,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f120]) ).
fof(f133,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f122]) ).
fof(f134,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f60,f133]) ).
fof(f143,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f24,f23]) ).
fof(f152,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),complement(X0)))),
inference(paramodulation,[status(thm)],[f31,f48]) ).
fof(f154,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f22,f152]) ).
fof(f162,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f19,f22]) ).
fof(f170,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f22,f162]) ).
fof(f194,plain,
top = join(zero,meet(top,complement(zero))),
inference(paramodulation,[status(thm)],[f60,f134]) ).
fof(f197,plain,
sF1_fnc = join(zero,meet(sF1_fnc,complement(sF0_fnc))),
inference(paramodulation,[status(thm)],[f39,f134]) ).
fof(f199,plain,
! [X0,X1] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f200,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f201,plain,
! [X0,X1] : join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))) = complement(converse(X0)),
inference(paramodulation,[status(thm)],[f28,f45]) ).
fof(f203,plain,
! [X0,X1] : join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))) = complement(converse(X0)),
inference(forward_demodulation,[status(thm)],[f26,f201]) ).
fof(f207,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f170,f131]) ).
fof(f210,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f170,f131]) ).
fof(f212,plain,
! [X0] : X0 = join(meet(X0,top),meet(X0,zero)),
inference(paramodulation,[status(thm)],[f60,f131]) ).
fof(f215,plain,
! [X0] : X0 = join(meet(X0,sF1_fnc),meet(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f39,f131]) ).
fof(f220,plain,
! [X0] : X0 = join(meet(X0,sF0_fnc),meet(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f19,f215]) ).
fof(f224,plain,
! [X0] : X0 = join(meet(X0,top),meet(zero,X0)),
inference(paramodulation,[status(thm)],[f170,f212]) ).
fof(f227,plain,
! [X0] : X0 = join(meet(sF0_fnc,X0),meet(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f170,f220]) ).
fof(f230,plain,
! [X0] : X0 = join(meet(X0,sF0_fnc),meet(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f170,f220]) ).
fof(f238,plain,
complement(zero) = join(meet(complement(zero),top),zero),
inference(paramodulation,[status(thm)],[f31,f224]) ).
fof(f244,plain,
complement(zero) = join(zero,meet(complement(zero),top)),
inference(forward_demodulation,[status(thm)],[f19,f238]) ).
fof(f245,plain,
complement(zero) = join(zero,meet(top,complement(zero))),
inference(forward_demodulation,[status(thm)],[f170,f244]) ).
fof(f247,plain,
complement(zero) = top,
inference(forward_demodulation,[status(thm)],[f194,f245]) ).
fof(f249,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f262,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f30,f20]) ).
fof(f263,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X1,X0),X2),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f270,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(forward_demodulation,[status(thm)],[f20,f263]) ).
fof(f279,plain,
! [X0] : composition(join(sK0_skl,X0),top) = join(sF1_fnc,composition(X0,top)),
inference(paramodulation,[status(thm)],[f38,f25]) ).
fof(f313,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f26,f27]) ).
fof(f325,plain,
! [X0] : X0 = join(meet(sF0_fnc,X0),meet(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f170,f230]) ).
fof(f359,plain,
complement(sF0_fnc) = join(zero,meet(complement(sF0_fnc),sF1_fnc)),
inference(paramodulation,[status(thm)],[f31,f227]) ).
fof(f369,plain,
complement(sF0_fnc) = join(zero,meet(sF1_fnc,complement(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f359]) ).
fof(f372,plain,
complement(sF0_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f197,f369]) ).
fof(f418,plain,
! [X0] : zero = join(meet(zero,X0),complement(join(top,X0))),
inference(paramodulation,[status(thm)],[f247,f48]) ).
fof(f552,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f31,f210]) ).
fof(f568,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f19,f552]) ).
fof(f569,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f170,f568]) ).
fof(f573,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f134,f569]) ).
fof(f581,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(X1)),
inference(paramodulation,[status(thm)],[f22,f573]) ).
fof(f591,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f573,f22]) ).
fof(f592,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f573,f22]) ).
fof(f800,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f24,f200]) ).
fof(f817,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f26,f800]) ).
fof(f832,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f143,f817]) ).
fof(f833,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f24,f817]) ).
fof(f836,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f817,f45]) ).
fof(f846,plain,
! [X0,X1] : composition(join(converse(one),X0),X1) = join(X1,composition(X0,X1)),
inference(paramodulation,[status(thm)],[f817,f25]) ).
fof(f853,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f817,f832]) ).
fof(f857,plain,
! [X0] : complement(meet(X0,composition(one,X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f581,f836]) ).
fof(f858,plain,
! [X0] : complement(meet(X0,X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f853,f857]) ).
fof(f874,plain,
! [X0,X1] : composition(join(one,X0),X1) = join(X1,composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f833,f846]) ).
fof(f883,plain,
! [X0] : converse(join(one,X0)) = join(one,converse(X0)),
inference(paramodulation,[status(thm)],[f833,f27]) ).
fof(f926,plain,
! [X0] : complement(complement(X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f858,f573]) ).
fof(f937,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f944,f154]) ).
fof(f944,plain,
! [X0] : X0 = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f573,f926]) ).
fof(f963,plain,
composition(converse(sK0_skl),sF0_fnc) = zero,
inference(backward_demodulation,[status(thm)],[f937,f115]) ).
fof(f982,plain,
composition(converse(sF0_fnc),complement(sF2_fnc)) = zero,
inference(backward_demodulation,[status(thm)],[f937,f112]) ).
fof(f983,plain,
! [X0] : composition(converse(X0),complement(composition(X0,top))) = zero,
inference(backward_demodulation,[status(thm)],[f937,f107]) ).
fof(f1007,plain,
! [X0] : X0 = join(X0,zero),
inference(paramodulation,[status(thm)],[f19,f937]) ).
fof(f1055,plain,
! [X0] : top = join(complement(X0),join(complement(X0),X0)),
inference(paramodulation,[status(thm)],[f944,f58]) ).
fof(f1115,plain,
! [X0] : top = join(complement(X0),join(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f249,f1055]) ).
fof(f1116,plain,
! [X0] : top = join(X0,join(complement(X0),complement(X0))),
inference(forward_demodulation,[status(thm)],[f270,f1115]) ).
fof(f1117,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f262,f1116]) ).
fof(f1127,plain,
! [X0,X1,X2] : join(meet(converse(composition(X0,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X0)))),meet(converse(X0),composition(converse(converse(X1)),X2)))) = composition(meet(converse(X1),composition(X2,converse(converse(X0)))),meet(converse(X0),composition(converse(converse(X1)),X2))),
inference(paramodulation,[status(thm)],[f28,f32]) ).
fof(f1133,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))),
inference(paramodulation,[status(thm)],[f24,f32]) ).
fof(f1138,plain,
! [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)))),
inference(paramodulation,[status(thm)],[f28,f32]) ).
fof(f1161,plain,
! [X0,X1,X2] : join(meet(converse(composition(X0,X1)),X2),composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(converse(converse(X1)),X2)))) = composition(meet(converse(X1),composition(X2,converse(converse(X0)))),meet(converse(X0),composition(converse(converse(X1)),X2))),
inference(forward_demodulation,[status(thm)],[f26,f1127]) ).
fof(f1162,plain,
! [X0,X1,X2] : join(meet(converse(composition(X0,X1)),X2),composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(X1,X2)))) = composition(meet(converse(X1),composition(X2,converse(converse(X0)))),meet(converse(X0),composition(converse(converse(X1)),X2))),
inference(forward_demodulation,[status(thm)],[f26,f1161]) ).
fof(f1163,plain,
! [X0,X1,X2] : join(meet(converse(composition(X0,X1)),X2),composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(X1,X2)))) = composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(converse(converse(X1)),X2))),
inference(forward_demodulation,[status(thm)],[f26,f1162]) ).
fof(f1164,plain,
! [X0,X1,X2] : join(meet(converse(composition(X0,X1)),X2),composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(X1,X2)))) = composition(meet(converse(X1),composition(X2,X0)),meet(converse(X0),composition(X1,X2))),
inference(forward_demodulation,[status(thm)],[f26,f1163]) ).
fof(f1165,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f833,f1133]) ).
fof(f1166,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f24,f1165]) ).
fof(f1167,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f833,f1166]) ).
fof(f1168,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,X1),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f24,f1167]) ).
fof(f1182,plain,
! [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)))),
inference(forward_demodulation,[status(thm)],[f28,f1138]) ).
fof(f1183,plain,
! [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)))),
inference(forward_demodulation,[status(thm)],[f28,f1182]) ).
fof(f1184,plain,
! [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)))),
inference(forward_demodulation,[status(thm)],[f28,f1183]) ).
fof(f1362,plain,
! [X0] : top = join(top,X0),
inference(paramodulation,[status(thm)],[f573,f1117]) ).
fof(f1383,plain,
! [X0] : zero = join(meet(zero,X0),complement(top)),
inference(backward_demodulation,[status(thm)],[f1362,f418]) ).
fof(f1393,plain,
! [X0] : zero = join(complement(top),meet(zero,X0)),
inference(forward_demodulation,[status(thm)],[f19,f1383]) ).
fof(f1394,plain,
! [X0] : zero = join(zero,meet(zero,X0)),
inference(forward_demodulation,[status(thm)],[f60,f1393]) ).
fof(f1403,plain,
! [X0] : zero = meet(zero,X0),
inference(forward_demodulation,[status(thm)],[f937,f1394]) ).
fof(f1438,plain,
! [X0] : top = join(X0,top),
inference(paramodulation,[status(thm)],[f19,f1362]) ).
fof(f1566,plain,
! [X0] : zero = meet(X0,zero),
inference(paramodulation,[status(thm)],[f170,f1403]) ).
fof(f1701,plain,
join(complement(converse(converse(sF0_fnc))),composition(complement(sF2_fnc),complement(converse(zero)))) = complement(converse(converse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f982,f203]) ).
fof(f1702,plain,
join(complement(converse(converse(sK0_skl))),composition(sF0_fnc,complement(converse(zero)))) = complement(converse(converse(sK0_skl))),
inference(paramodulation,[status(thm)],[f963,f203]) ).
fof(f1727,plain,
join(complement(sF0_fnc),composition(complement(sF2_fnc),complement(converse(zero)))) = complement(converse(converse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f26,f1701]) ).
fof(f1728,plain,
join(sF1_fnc,composition(complement(sF2_fnc),complement(converse(zero)))) = complement(converse(converse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f372,f1727]) ).
fof(f1729,plain,
join(sF1_fnc,composition(complement(sF2_fnc),complement(converse(zero)))) = complement(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f26,f1728]) ).
fof(f1730,plain,
join(sF1_fnc,composition(complement(sF2_fnc),complement(converse(zero)))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f372,f1729]) ).
fof(f1731,plain,
join(complement(sK0_skl),composition(sF0_fnc,complement(converse(zero)))) = complement(converse(converse(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f26,f1702]) ).
fof(f1732,plain,
join(complement(sK0_skl),composition(sF0_fnc,complement(converse(zero)))) = complement(sK0_skl),
inference(forward_demodulation,[status(thm)],[f26,f1731]) ).
fof(f1946,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(zero)),
inference(paramodulation,[status(thm)],[f1007,f313]) ).
fof(f1972,plain,
! [X0] : X0 = join(X0,converse(zero)),
inference(forward_demodulation,[status(thm)],[f26,f1946]) ).
fof(f1987,plain,
zero = converse(zero),
inference(paramodulation,[status(thm)],[f937,f1972]) ).
fof(f2010,plain,
join(complement(sK0_skl),composition(sF0_fnc,complement(zero))) = complement(sK0_skl),
inference(backward_demodulation,[status(thm)],[f1987,f1732]) ).
fof(f2011,plain,
join(sF1_fnc,composition(complement(sF2_fnc),complement(zero))) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f1987,f1730]) ).
fof(f2033,plain,
join(complement(sK0_skl),composition(sF0_fnc,top)) = complement(sK0_skl),
inference(forward_demodulation,[status(thm)],[f247,f2010]) ).
fof(f2034,plain,
join(complement(sK0_skl),sF2_fnc) = complement(sK0_skl),
inference(forward_demodulation,[status(thm)],[f47,f2033]) ).
fof(f2035,plain,
join(sF2_fnc,complement(sK0_skl)) = complement(sK0_skl),
inference(forward_demodulation,[status(thm)],[f19,f2034]) ).
fof(f2036,plain,
join(sF1_fnc,composition(complement(sF2_fnc),top)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f247,f2011]) ).
fof(f2278,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(complement(X0),X1),
inference(paramodulation,[status(thm)],[f573,f581]) ).
fof(f2430,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = complement(join(X0,X1)),
inference(paramodulation,[status(thm)],[f573,f591]) ).
fof(f2483,plain,
meet(complement(sF2_fnc),sK0_skl) = complement(complement(sK0_skl)),
inference(paramodulation,[status(thm)],[f2035,f592]) ).
fof(f2522,plain,
meet(sK0_skl,complement(sF2_fnc)) = complement(complement(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f170,f2483]) ).
fof(f2523,plain,
meet(sK0_skl,complement(sF2_fnc)) = sK0_skl,
inference(forward_demodulation,[status(thm)],[f573,f2522]) ).
fof(f2950,plain,
! [X0,X1] : join(X0,top) = join(X1,join(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f30,f270]) ).
fof(f3053,plain,
! [X0,X1] : top = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[status(thm)],[f1438,f2950]) ).
fof(f3876,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(paramodulation,[status(thm)],[f581,f3053]) ).
fof(f3991,plain,
! [X0,X1] : meet(X0,complement(complement(meet(X1,complement(X0))))) = complement(top),
inference(paramodulation,[status(thm)],[f3876,f591]) ).
fof(f4021,plain,
! [X0,X1] : meet(X0,meet(X1,complement(X0))) = complement(top),
inference(forward_demodulation,[status(thm)],[f573,f3991]) ).
fof(f4023,plain,
! [X0,X1] : meet(X0,meet(X1,complement(X0))) = zero,
inference(forward_demodulation,[status(thm)],[f60,f4021]) ).
fof(f4168,plain,
! [X0,X1] : X0 = join(zero,meet(complement(meet(X1,complement(X0))),X0)),
inference(paramodulation,[status(thm)],[f4023,f210]) ).
fof(f4210,plain,
! [X0,X1] : X0 = meet(complement(meet(X1,complement(X0))),X0),
inference(forward_demodulation,[status(thm)],[f937,f4168]) ).
fof(f4211,plain,
! [X0,X1] : X0 = meet(X0,complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[status(thm)],[f170,f4210]) ).
fof(f4212,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f2278,f4211]) ).
fof(f4223,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X1,X0))),
inference(paramodulation,[status(thm)],[f581,f4212]) ).
fof(f4273,plain,
! [X0,X1] : complement(X0) = complement(join(X0,meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2430,f4223]) ).
fof(f6297,plain,
! [X0,X1] : complement(complement(X0)) = join(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f4273,f573]) ).
fof(f6377,plain,
! [X0,X1] : X0 = join(X0,meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f573,f6297]) ).
fof(f6404,plain,
complement(sF2_fnc) = join(complement(sF2_fnc),sK0_skl),
inference(paramodulation,[status(thm)],[f2523,f6377]) ).
fof(f6446,plain,
complement(sF2_fnc) = join(sK0_skl,complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f19,f6404]) ).
fof(f7783,plain,
composition(complement(sF2_fnc),top) = join(sF1_fnc,composition(complement(sF2_fnc),top)),
inference(paramodulation,[status(thm)],[f6446,f279]) ).
fof(f7803,plain,
composition(complement(sF2_fnc),top) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f2036,f7783]) ).
fof(f7837,plain,
join(complement(top),composition(converse(complement(sF2_fnc)),complement(sF1_fnc))) = complement(top),
inference(paramodulation,[status(thm)],[f7803,f45]) ).
fof(f7873,plain,
join(zero,composition(converse(complement(sF2_fnc)),complement(sF1_fnc))) = complement(top),
inference(forward_demodulation,[status(thm)],[f60,f7837]) ).
fof(f7874,plain,
composition(converse(complement(sF2_fnc)),complement(sF1_fnc)) = complement(top),
inference(forward_demodulation,[status(thm)],[f937,f7873]) ).
fof(f7875,plain,
composition(converse(complement(sF2_fnc)),sF0_fnc) = complement(top),
inference(forward_demodulation,[status(thm)],[f39,f7874]) ).
fof(f7877,plain,
composition(converse(complement(sF2_fnc)),sF0_fnc) = zero,
inference(forward_demodulation,[status(thm)],[f60,f7875]) ).
fof(f8437,plain,
! [X0] : composition(join(one,converse(X0)),complement(composition(join(one,X0),top))) = zero,
inference(paramodulation,[status(thm)],[f883,f983]) ).
fof(f8481,plain,
! [X0] : composition(join(one,converse(X0)),complement(join(top,composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f874,f8437]) ).
fof(f8482,plain,
! [X0] : composition(join(one,converse(X0)),complement(top)) = zero,
inference(forward_demodulation,[status(thm)],[f1362,f8481]) ).
fof(f8483,plain,
! [X0] : composition(join(one,converse(X0)),zero) = zero,
inference(forward_demodulation,[status(thm)],[f60,f8482]) ).
fof(f8484,plain,
! [X0] : join(zero,composition(converse(X0),zero)) = zero,
inference(forward_demodulation,[status(thm)],[f874,f8483]) ).
fof(f8489,plain,
! [X0] : composition(converse(X0),zero) = zero,
inference(forward_demodulation,[status(thm)],[f937,f8484]) ).
fof(f9693,plain,
! [X0,X1] : composition(composition(X0,converse(X1)),zero) = zero,
inference(paramodulation,[status(thm)],[f199,f8489]) ).
fof(f9699,plain,
! [X0] : converse(zero) = composition(converse(zero),X0),
inference(paramodulation,[status(thm)],[f8489,f200]) ).
fof(f9726,plain,
! [X0,X1] : composition(X0,composition(converse(X1),zero)) = zero,
inference(forward_demodulation,[status(thm)],[f23,f9693]) ).
fof(f9757,plain,
! [X0] : composition(X0,zero) = zero,
inference(forward_demodulation,[status(thm)],[f8489,f9726]) ).
fof(f9775,plain,
! [X0] : zero = composition(converse(zero),X0),
inference(forward_demodulation,[status(thm)],[f1987,f9699]) ).
fof(f9804,plain,
! [X0] : zero = composition(zero,X0),
inference(forward_demodulation,[status(thm)],[f1987,f9775]) ).
fof(f13729,plain,
! [X0] : join(meet(converse(composition(X0,converse(sK0_skl))),sF0_fnc),composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),zero))) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(paramodulation,[status(thm)],[f963,f1164]) ).
fof(f14160,plain,
! [X0] : join(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),zero))) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f13729]) ).
fof(f14161,plain,
! [X0] : join(meet(sF0_fnc,composition(sK0_skl,converse(X0))),composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),zero))) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f199,f14160]) ).
fof(f14162,plain,
! [X0] : join(meet(sF0_fnc,composition(sK0_skl,converse(X0))),composition(meet(sK0_skl,composition(sF0_fnc,X0)),meet(converse(X0),zero))) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f26,f14161]) ).
fof(f14163,plain,
! [X0] : join(meet(sF0_fnc,composition(sK0_skl,converse(X0))),composition(meet(sK0_skl,composition(sF0_fnc,X0)),zero)) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f1566,f14162]) ).
fof(f14164,plain,
! [X0] : join(meet(sF0_fnc,composition(sK0_skl,converse(X0))),zero) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f9757,f14163]) ).
fof(f14165,plain,
! [X0] : meet(sF0_fnc,composition(sK0_skl,converse(X0))) = composition(meet(converse(converse(sK0_skl)),composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f1007,f14164]) ).
fof(f14166,plain,
! [X0] : meet(sF0_fnc,composition(sK0_skl,converse(X0))) = composition(meet(sK0_skl,composition(sF0_fnc,X0)),meet(converse(X0),composition(converse(sK0_skl),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f26,f14165]) ).
fof(f14167,plain,
! [X0] : meet(sF0_fnc,composition(sK0_skl,converse(X0))) = composition(meet(sK0_skl,composition(sF0_fnc,X0)),meet(converse(X0),zero)),
inference(forward_demodulation,[status(thm)],[f963,f14166]) ).
fof(f14168,plain,
! [X0] : meet(sF0_fnc,composition(sK0_skl,converse(X0))) = composition(meet(sK0_skl,composition(sF0_fnc,X0)),zero),
inference(forward_demodulation,[status(thm)],[f1566,f14167]) ).
fof(f14169,plain,
! [X0] : meet(sF0_fnc,composition(sK0_skl,converse(X0))) = zero,
inference(forward_demodulation,[status(thm)],[f9757,f14168]) ).
fof(f14305,plain,
join(meet(complement(sF2_fnc),sF0_fnc),composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,zero))) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(paramodulation,[status(thm)],[f7877,f1168]) ).
fof(f14490,plain,
join(meet(sF0_fnc,complement(sF2_fnc)),composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,zero))) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f14305]) ).
fof(f14491,plain,
join(meet(sF0_fnc,complement(sF2_fnc)),composition(meet(sF0_fnc,complement(sF2_fnc)),meet(one,zero))) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f14490]) ).
fof(f14492,plain,
join(meet(sF0_fnc,complement(sF2_fnc)),composition(meet(sF0_fnc,complement(sF2_fnc)),zero)) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f1566,f14491]) ).
fof(f14493,plain,
join(meet(sF0_fnc,complement(sF2_fnc)),zero) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f9757,f14492]) ).
fof(f14494,plain,
meet(sF0_fnc,complement(sF2_fnc)) = composition(meet(complement(sF2_fnc),sF0_fnc),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f1007,f14493]) ).
fof(f14495,plain,
meet(sF0_fnc,complement(sF2_fnc)) = composition(meet(sF0_fnc,complement(sF2_fnc)),meet(one,composition(converse(complement(sF2_fnc)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f14494]) ).
fof(f14496,plain,
meet(sF0_fnc,complement(sF2_fnc)) = composition(meet(sF0_fnc,complement(sF2_fnc)),meet(one,zero)),
inference(forward_demodulation,[status(thm)],[f7877,f14495]) ).
fof(f14497,plain,
meet(sF0_fnc,complement(sF2_fnc)) = composition(meet(sF0_fnc,complement(sF2_fnc)),zero),
inference(forward_demodulation,[status(thm)],[f1566,f14496]) ).
fof(f14498,plain,
meet(sF0_fnc,complement(sF2_fnc)) = zero,
inference(forward_demodulation,[status(thm)],[f9757,f14497]) ).
fof(f14671,plain,
! [X0] : join(meet(composition(sF0_fnc,X0),converse(converse(sK0_skl))),composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(zero)))) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(paramodulation,[status(thm)],[f963,f1184]) ).
fof(f15113,plain,
! [X0] : join(meet(composition(sF0_fnc,X0),sK0_skl),composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(zero)))) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f26,f14671]) ).
fof(f15114,plain,
! [X0] : join(meet(sK0_skl,composition(sF0_fnc,X0)),composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(zero)))) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f170,f15113]) ).
fof(f15115,plain,
! [X0] : join(meet(sK0_skl,composition(sF0_fnc,X0)),composition(meet(sF0_fnc,composition(sK0_skl,converse(X0))),meet(X0,converse(zero)))) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f199,f15114]) ).
fof(f15116,plain,
! [X0] : join(meet(sK0_skl,composition(sF0_fnc,X0)),composition(zero,meet(X0,converse(zero)))) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f14169,f15115]) ).
fof(f15117,plain,
! [X0] : join(meet(sK0_skl,composition(sF0_fnc,X0)),zero) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f9804,f15116]) ).
fof(f15118,plain,
! [X0] : meet(sK0_skl,composition(sF0_fnc,X0)) = composition(meet(sF0_fnc,converse(composition(X0,converse(sK0_skl)))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f1007,f15117]) ).
fof(f15119,plain,
! [X0] : meet(sK0_skl,composition(sF0_fnc,X0)) = composition(meet(sF0_fnc,composition(sK0_skl,converse(X0))),meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f199,f15118]) ).
fof(f15120,plain,
! [X0] : meet(sK0_skl,composition(sF0_fnc,X0)) = composition(zero,meet(X0,converse(composition(converse(sK0_skl),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f14169,f15119]) ).
fof(f15121,plain,
! [X0] : meet(sK0_skl,composition(sF0_fnc,X0)) = zero,
inference(forward_demodulation,[status(thm)],[f9804,f15120]) ).
fof(f15370,plain,
sF0_fnc = join(meet(sF2_fnc,sF0_fnc),zero),
inference(paramodulation,[status(thm)],[f14498,f207]) ).
fof(f15401,plain,
sF0_fnc = meet(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1007,f15370]) ).
fof(f15402,plain,
sF0_fnc = meet(sF0_fnc,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f170,f15401]) ).
fof(f15536,plain,
sF2_fnc = join(sF0_fnc,meet(sF1_fnc,sF2_fnc)),
inference(paramodulation,[status(thm)],[f15402,f325]) ).
fof(f15716,plain,
! [X0] : meet(sK0_skl,composition(sF2_fnc,X0)) = zero,
inference(paramodulation,[status(thm)],[f73,f15121]) ).
fof(f15784,plain,
! [X0] : join(meet(composition(sK0_skl,X0),sF2_fnc),composition(zero,meet(X0,composition(converse(sK0_skl),sF2_fnc)))) = composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),meet(X0,composition(converse(sK0_skl),sF2_fnc))),
inference(paramodulation,[status(thm)],[f15716,f32]) ).
fof(f15808,plain,
! [X0] : join(meet(sF2_fnc,composition(sK0_skl,X0)),composition(zero,meet(X0,composition(converse(sK0_skl),sF2_fnc)))) = composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),meet(X0,composition(converse(sK0_skl),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f170,f15784]) ).
fof(f15809,plain,
! [X0] : join(meet(sF2_fnc,composition(sK0_skl,X0)),zero) = composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),meet(X0,composition(converse(sK0_skl),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f9804,f15808]) ).
fof(f15810,plain,
! [X0] : meet(sF2_fnc,composition(sK0_skl,X0)) = composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),meet(X0,composition(converse(sK0_skl),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f1007,f15809]) ).
fof(f15811,plain,
! [X0] : meet(sF2_fnc,composition(sK0_skl,X0)) = composition(zero,meet(X0,composition(converse(sK0_skl),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f15716,f15810]) ).
fof(f15812,plain,
! [X0] : meet(sF2_fnc,composition(sK0_skl,X0)) = zero,
inference(forward_demodulation,[status(thm)],[f9804,f15811]) ).
fof(f15890,plain,
meet(sF2_fnc,sF1_fnc) = zero,
inference(paramodulation,[status(thm)],[f38,f15812]) ).
fof(f15915,plain,
sF2_fnc = join(sF0_fnc,zero),
inference(backward_demodulation,[status(thm)],[f15916,f15536]) ).
fof(f15916,plain,
meet(sF1_fnc,sF2_fnc) = zero,
inference(forward_demodulation,[status(thm)],[f170,f15890]) ).
fof(f15951,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1007,f15915]) ).
fof(f15952,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15951,f42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n005.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 04:08:48 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 16.34/2.48 % Refutation found
% 16.34/2.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.34/2.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.30/2.57 % Elapsed time: 2.206240 seconds
% 3.30/2.57 % CPU time: 17.262802 seconds
% 3.30/2.57 % Total memory used: 289.412 MB
% 3.30/2.57 % Net memory used: 284.100 MB
%------------------------------------------------------------------------------