%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL026+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:20 PM UTC 2026
% Result : Theorem 230.29s 29.73s
% Output : CNFRefutation 85.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 19
% Syntax : Number of formulae : 262 ( 257 unt; 3 def)
% Number of atoms : 267 ( 266 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 11 ( 6 ~; 0 |; 3 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 8 ( 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 : 374 ( 370 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [X0,X1] :
( join(X0,one) = one
=> meet(composition(X0,top),X1) = composition(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( join(X0,one) = one
=> meet(composition(X0,top),X1) = composition(X0,X1) ),
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(f33,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f35,plain,
? [X0,X1] :
( meet(composition(X0,top),X1) != composition(X0,X1)
& join(X0,one) = one ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f36,plain,
? [X0] :
( ? [X1] : meet(composition(X0,top),X1) != composition(X0,X1)
& join(X0,one) = one ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f37,plain,
( meet(composition(sK0_skl,top),sK1_skl) != composition(sK0_skl,sK1_skl)
& join(sK0_skl,one) = one ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f36]) ).
fof(f38,plain,
join(sK0_skl,one) = one,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
meet(composition(sK0_skl,top),sK1_skl) != composition(sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f40,definition,
sF1_fnc = composition(sK0_skl,top),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f41,definition,
sF0_fnc = meet(sF1_fnc,sK1_skl),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f42,definition,
sF2_fnc = composition(sK0_skl,sK1_skl),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f43,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f39,f42,f41,f40]) ).
fof(f44,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f19,f21]) ).
fof(f45,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f22,f44]) ).
fof(f46,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f19,f29]) ).
fof(f47,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f19,f45]) ).
fof(f55,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f24,f23]) ).
fof(f69,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f30,f47]) ).
fof(f70,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(X1,complement(X0)))),
inference(paramodulation,[status(thm)],[f19,f47]) ).
fof(f73,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f69]) ).
fof(f74,plain,
! [X0,X1] : join(X0,join(X1,complement(join(X0,X1)))) = top,
inference(paramodulation,[status(thm)],[f30,f20]) ).
fof(f75,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f78,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2)) = join(X0,X2),
inference(paramodulation,[status(thm)],[f47,f20]) ).
fof(f80,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f30,f20]) ).
fof(f91,plain,
! [X0] : composition(join(sK0_skl,X0),top) = join(sF1_fnc,composition(X0,top)),
inference(paramodulation,[status(thm)],[f40,f25]) ).
fof(f112,plain,
! [X0,X1] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f113,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f117,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f30,f22]) ).
fof(f118,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f19,f22]) ).
fof(f122,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f22,f47]) ).
fof(f126,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(backward_demodulation,[status(thm)],[f127,f73]) ).
fof(f127,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f31,f117]) ).
fof(f128,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f122]) ).
fof(f134,plain,
! [X0] : meet(X0,top) = complement(join(complement(X0),zero)),
inference(paramodulation,[status(thm)],[f127,f22]) ).
fof(f135,plain,
! [X0] : meet(top,X0) = complement(join(zero,complement(X0))),
inference(paramodulation,[status(thm)],[f127,f22]) ).
fof(f139,plain,
! [X0] : meet(X0,top) = complement(join(zero,complement(X0))),
inference(forward_demodulation,[status(thm)],[f19,f134]) ).
fof(f140,plain,
top = join(zero,meet(top,complement(zero))),
inference(paramodulation,[status(thm)],[f127,f126]) ).
fof(f144,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X1),converse(X0)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f228,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0)) = meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0),
inference(paramodulation,[status(thm)],[f40,f33]) ).
fof(f232,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2))) = meet(composition(X0,meet(X1,composition(converse(X0),converse(X2)))),converse(X2)),
inference(paramodulation,[status(thm)],[f28,f33]) ).
fof(f234,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one)) = meet(composition(X0,meet(X1,composition(converse(X0),one))),one),
inference(paramodulation,[status(thm)],[f24,f33]) ).
fof(f244,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2))) = meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2)),
inference(forward_demodulation,[status(thm)],[f28,f232]) ).
fof(f246,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one)) = meet(composition(X0,meet(X1,converse(X0))),one),
inference(forward_demodulation,[status(thm)],[f24,f234]) ).
fof(f331,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(paramodulation,[status(thm)],[f30,f80]) ).
fof(f338,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))),
inference(paramodulation,[status(thm)],[f80,f47]) ).
fof(f344,plain,
! [X0,X1] : X0 = join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f19,f338]) ).
fof(f353,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(converse(X1),X0),
inference(paramodulation,[status(thm)],[f26,f144]) ).
fof(f358,plain,
! [X0] : meet(top,X0) = meet(X0,top),
inference(paramodulation,[status(thm)],[f139,f135]) ).
fof(f370,plain,
! [X0,X1] : meet(X0,join(zero,complement(X1))) = complement(join(complement(X0),meet(top,X1))),
inference(paramodulation,[status(thm)],[f135,f22]) ).
fof(f410,plain,
! [X0] : X0 = join(meet(top,X0),complement(join(complement(X0),top))),
inference(paramodulation,[status(thm)],[f358,f47]) ).
fof(f417,plain,
! [X0] : X0 = join(meet(top,X0),complement(join(top,complement(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f410]) ).
fof(f443,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f24,f113]) ).
fof(f463,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f26,f443]) ).
fof(f486,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f55,f463]) ).
fof(f487,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f24,f463]) ).
fof(f488,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f463,f46]) ).
fof(f501,plain,
! [X0,X1] : composition(join(X0,converse(one)),X1) = join(composition(X0,X1),X1),
inference(paramodulation,[status(thm)],[f463,f25]) ).
fof(f513,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f463,f486]) ).
fof(f516,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f513,f488]) ).
fof(f553,plain,
! [X0,X1] : composition(join(X0,one),X1) = join(composition(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f487,f501]) ).
fof(f555,plain,
! [X0,X1] : composition(join(X0,one),X1) = join(X1,composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f553]) ).
fof(f648,plain,
! [X0] : join(meet(X0,top),complement(join(zero,complement(X0)))) = complement(join(zero,complement(X0))),
inference(paramodulation,[status(thm)],[f139,f516]) ).
fof(f655,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(paramodulation,[status(thm)],[f516,f80]) ).
fof(f656,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f516,f47]) ).
fof(f663,plain,
! [X0] : join(meet(X0,top),meet(top,X0)) = complement(join(zero,complement(X0))),
inference(forward_demodulation,[status(thm)],[f135,f648]) ).
fof(f664,plain,
! [X0] : join(meet(X0,top),meet(top,X0)) = meet(top,X0),
inference(forward_demodulation,[status(thm)],[f135,f663]) ).
fof(f682,plain,
! [X0] : join(X0,top) = top,
inference(backward_demodulation,[status(thm)],[f684,f331]) ).
fof(f683,plain,
! [X0] : X0 = join(meet(top,X0),complement(top)),
inference(backward_demodulation,[status(thm)],[f684,f417]) ).
fof(f684,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f30,f655]) ).
fof(f685,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f19,f656]) ).
fof(f686,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f31,f685]) ).
fof(f687,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f19,f686]) ).
fof(f689,plain,
! [X0] : X0 = join(complement(top),meet(top,X0)),
inference(forward_demodulation,[status(thm)],[f19,f683]) ).
fof(f690,plain,
top = complement(zero),
inference(backward_demodulation,[status(thm)],[f692,f140]) ).
fof(f692,plain,
! [X0] : X0 = join(zero,meet(top,X0)),
inference(forward_demodulation,[status(thm)],[f127,f689]) ).
fof(f714,plain,
! [X0,X1,X2,X3] : join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3)) = join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3),
inference(paramodulation,[status(thm)],[f34,f20]) ).
fof(f752,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f22,f70]) ).
fof(f775,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f752]) ).
fof(f930,plain,
! [X0] : meet(X0,zero) = complement(join(complement(X0),top)),
inference(paramodulation,[status(thm)],[f690,f22]) ).
fof(f952,plain,
! [X0] : meet(X0,zero) = complement(join(top,complement(X0))),
inference(forward_demodulation,[status(thm)],[f19,f930]) ).
fof(f953,plain,
! [X0] : meet(X0,zero) = complement(top),
inference(forward_demodulation,[status(thm)],[f684,f952]) ).
fof(f961,plain,
! [X0] : meet(X0,zero) = zero,
inference(forward_demodulation,[status(thm)],[f127,f953]) ).
fof(f1050,plain,
! [X0,X1] : join(top,X0) = join(X0,join(X1,complement(X1))),
inference(paramodulation,[status(thm)],[f80,f75]) ).
fof(f1148,plain,
! [X0] : join(top,X0) = join(X0,top),
inference(forward_demodulation,[status(thm)],[f30,f1050]) ).
fof(f1165,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(complement(X0)),X1))),
inference(backward_demodulation,[status(thm)],[f1170,f344]) ).
fof(f1170,plain,
! [X0] : join(top,X0) = top,
inference(forward_demodulation,[status(thm)],[f682,f1148]) ).
fof(f1241,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f127,f1165]) ).
fof(f1250,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),X1))) = join(X0,complement(join(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f516,f78]) ).
fof(f1294,plain,
! [X0,X1] : X0 = join(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f47,f1250]) ).
fof(f1334,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f22,f687]) ).
fof(f1337,plain,
! [X0] : complement(X0) = join(meet(complement(X0),zero),complement(X0)),
inference(paramodulation,[status(thm)],[f687,f70]) ).
fof(f1346,plain,
! [X0] : complement(X0) = join(complement(X0),meet(complement(X0),zero)),
inference(forward_demodulation,[status(thm)],[f19,f1337]) ).
fof(f1347,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(forward_demodulation,[status(thm)],[f961,f1346]) ).
fof(f1348,plain,
! [X0] : X0 = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1373,f687]) ).
fof(f1349,plain,
! [X0] : meet(top,X0) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1373,f135]) ).
fof(f1350,plain,
! [X0] : meet(X0,top) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1373,f139]) ).
fof(f1351,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1373,f1334]) ).
fof(f1362,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),meet(top,X1))),
inference(backward_demodulation,[status(thm)],[f1373,f370]) ).
fof(f1373,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[status(thm)],[f19,f1347]) ).
fof(f1387,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(X0,X1))),
inference(backward_demodulation,[status(thm)],[f1348,f1241]) ).
fof(f1400,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0)) = meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0),
inference(backward_demodulation,[status(thm)],[f1412,f228]) ).
fof(f1409,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f1412,f692]) ).
fof(f1410,plain,
! [X0] : join(meet(X0,top),meet(top,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f1412,f664]) ).
fof(f1412,plain,
! [X0] : meet(top,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1348,f1349]) ).
fof(f1421,plain,
! [X0] : meet(X0,top) = X0,
inference(forward_demodulation,[status(thm)],[f1348,f1350]) ).
fof(f1429,plain,
! [X0,X1] : meet(X0,X1) = complement(complement(meet(X1,X0))),
inference(backward_demodulation,[status(thm)],[f1351,f118]) ).
fof(f1468,plain,
! [X0,X1] : X0 = join(X0,meet(X0,complement(X1))),
inference(backward_demodulation,[status(thm)],[f1471,f1294]) ).
fof(f1471,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f1412,f1362]) ).
fof(f1519,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0)) = meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0),
inference(forward_demodulation,[status(thm)],[f1412,f1400]) ).
fof(f1535,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1409,f1387]) ).
fof(f1540,plain,
! [X0] : join(X0,meet(top,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1421,f1410]) ).
fof(f1543,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1412,f1540]) ).
fof(f1555,plain,
sF0_fnc = meet(sK1_skl,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f1595,f41]) ).
fof(f1573,plain,
! [X0,X1,X2,X3] : join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3)) = join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3),
inference(backward_demodulation,[status(thm)],[f1595,f714]) ).
fof(f1580,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0)) = meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))),
inference(backward_demodulation,[status(thm)],[f1595,f1519]) ).
fof(f1588,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),converse(X2)),meet(composition(X0,meet(X1,converse(composition(X2,X0)))),converse(X2))) = meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0))))),
inference(backward_demodulation,[status(thm)],[f1595,f244]) ).
fof(f1589,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one)) = meet(one,composition(X0,meet(X1,converse(X0)))),
inference(backward_demodulation,[status(thm)],[f1595,f246]) ).
fof(f1595,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f1348,f1429]) ).
fof(f1643,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f1595,f1573]) ).
fof(f1650,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0)))) = meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))),
inference(forward_demodulation,[status(thm)],[f1595,f1580]) ).
fof(f1658,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),converse(X2)),meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0)))))) = meet(converse(X2),composition(X0,meet(X1,converse(composition(X2,X0))))),
inference(forward_demodulation,[status(thm)],[f1595,f1588]) ).
fof(f1659,plain,
! [X0,X1] : join(meet(one,composition(X0,X1)),meet(composition(X0,meet(X1,converse(X0))),one)) = meet(one,composition(X0,meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f1595,f1589]) ).
fof(f1660,plain,
! [X0,X1] : join(meet(one,composition(X0,X1)),meet(one,composition(X0,meet(X1,converse(X0))))) = meet(one,composition(X0,meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f1595,f1659]) ).
fof(f1783,plain,
! [X0,X1] : X0 = join(X0,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f1348,f1468]) ).
fof(f1817,plain,
! [X0,X1,X2] : join(X0,join(meet(X0,X1),X2)) = join(X2,X0),
inference(paramodulation,[status(thm)],[f1783,f75]) ).
fof(f1820,plain,
! [X0,X1,X2] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(paramodulation,[status(thm)],[f1783,f20]) ).
fof(f2121,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f1543,f75]) ).
fof(f2142,plain,
! [X0,X1] : converse(X0) = meet(converse(X0),converse(join(X0,X1))),
inference(paramodulation,[status(thm)],[f27,f1535]) ).
fof(f2149,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f128,f1535]) ).
fof(f2159,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f19,f1535]) ).
fof(f2170,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1595,f2149]) ).
fof(f2701,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X1,complement(X0)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f775,f2121]) ).
fof(f2703,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X1),
inference(paramodulation,[status(thm)],[f775,f1535]) ).
fof(f2731,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X0,complement(X1)),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f19,f2701]) ).
fof(f2732,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f19,f2731]) ).
fof(f2734,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f775,f2732]) ).
fof(f2736,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1595,f2703]) ).
fof(f2833,plain,
! [X0,X1,X2] : join(X0,join(meet(X1,X0),X2)) = join(X0,X2),
inference(paramodulation,[status(thm)],[f2734,f20]) ).
fof(f6122,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1595,f2736]) ).
fof(f6124,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1595,f2170]) ).
fof(f7067,plain,
! [X0,X1,X2] : join(X0,meet(X0,X1)) = join(meet(X2,meet(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f2734,f1817]) ).
fof(f7156,plain,
! [X0,X1,X2] : X0 = join(meet(X1,meet(X0,X2)),X0),
inference(forward_demodulation,[status(thm)],[f1783,f7067]) ).
fof(f7157,plain,
! [X0,X1,X2] : X0 = join(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[status(thm)],[f19,f7156]) ).
fof(f7260,plain,
! [X0,X1,X2] : X0 = join(X0,meet(X1,meet(X2,X0))),
inference(paramodulation,[status(thm)],[f6122,f7157]) ).
fof(f7342,plain,
! [X0,X1,X2] : X0 = join(X0,meet(meet(X1,X0),X2)),
inference(paramodulation,[status(thm)],[f1595,f7260]) ).
fof(f9158,plain,
! [X0,X1,X2] : meet(X0,X1) = join(meet(X0,X1),meet(meet(X1,X0),X2)),
inference(paramodulation,[status(thm)],[f6124,f7342]) ).
fof(f9679,plain,
converse(sK0_skl) = meet(converse(sK0_skl),converse(one)),
inference(paramodulation,[status(thm)],[f38,f2142]) ).
fof(f9695,plain,
! [X0] : converse(X0) = meet(converse(X0),converse(top)),
inference(paramodulation,[status(thm)],[f74,f2142]) ).
fof(f9770,plain,
converse(sK0_skl) = meet(converse(sK0_skl),one),
inference(forward_demodulation,[status(thm)],[f487,f9679]) ).
fof(f9771,plain,
converse(sK0_skl) = meet(one,converse(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1595,f9770]) ).
fof(f10723,plain,
! [X0] : converse(converse(X0)) = meet(X0,converse(top)),
inference(paramodulation,[status(thm)],[f26,f9695]) ).
fof(f10765,plain,
! [X0] : X0 = meet(X0,converse(top)),
inference(forward_demodulation,[status(thm)],[f26,f10723]) ).
fof(f10844,plain,
top = converse(top),
inference(paramodulation,[status(thm)],[f1412,f10765]) ).
fof(f11088,plain,
! [X0] : converse(composition(top,X0)) = composition(converse(X0),top),
inference(paramodulation,[status(thm)],[f10844,f113]) ).
fof(f18765,plain,
! [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),
inference(paramodulation,[status(thm)],[f24,f1643]) ).
fof(f18914,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f24,f18765]) ).
fof(f18915,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f487,f18914]) ).
fof(f18916,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f24,f18915]) ).
fof(f18917,plain,
! [X0,X1,X2] : join(meet(X0,X1),X2) = join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2),
inference(forward_demodulation,[status(thm)],[f2833,f18916]) ).
fof(f18918,plain,
! [X0,X1,X2] : join(meet(X0,X1),X2) = join(meet(X1,meet(X0,composition(X1,converse(one)))),X2),
inference(forward_demodulation,[status(thm)],[f24,f18917]) ).
fof(f18919,plain,
! [X0,X1,X2] : join(meet(X0,X1),X2) = join(meet(X1,meet(X0,composition(X1,one))),X2),
inference(forward_demodulation,[status(thm)],[f487,f18918]) ).
fof(f18920,plain,
! [X0,X1,X2] : join(meet(X0,X1),X2) = join(meet(X1,meet(X0,X1)),X2),
inference(forward_demodulation,[status(thm)],[f24,f18919]) ).
fof(f18921,plain,
! [X0,X1,X2] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f6124,f18920]) ).
fof(f19464,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc))))) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f6124,f1650]) ).
fof(f19466,plain,
! [X0] : join(meet(X0,sF1_fnc),meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc))))) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f2736,f1650]) ).
fof(f19472,plain,
join(sF1_fnc,meet(top,composition(sK0_skl,composition(converse(sK0_skl),top)))) = meet(top,composition(sK0_skl,composition(converse(sK0_skl),top))),
inference(paramodulation,[status(thm)],[f1421,f1650]) ).
fof(f19514,plain,
! [X0] : meet(sF1_fnc,X0) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f9158,f19464]) ).
fof(f19516,plain,
! [X0] : meet(X0,sF1_fnc) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f1783,f19466]) ).
fof(f19518,plain,
join(sF1_fnc,composition(sK0_skl,composition(converse(sK0_skl),top))) = meet(top,composition(sK0_skl,composition(converse(sK0_skl),top))),
inference(forward_demodulation,[status(thm)],[f1412,f19472]) ).
fof(f19519,plain,
join(sF1_fnc,composition(sK0_skl,converse(composition(top,sK0_skl)))) = meet(top,composition(sK0_skl,composition(converse(sK0_skl),top))),
inference(forward_demodulation,[status(thm)],[f11088,f19518]) ).
fof(f19520,plain,
join(sF1_fnc,composition(sK0_skl,converse(composition(top,sK0_skl)))) = composition(sK0_skl,composition(converse(sK0_skl),top)),
inference(forward_demodulation,[status(thm)],[f1412,f19519]) ).
fof(f19521,plain,
join(sF1_fnc,composition(sK0_skl,converse(composition(top,sK0_skl)))) = composition(sK0_skl,converse(composition(top,sK0_skl))),
inference(forward_demodulation,[status(thm)],[f11088,f19520]) ).
fof(f37706,plain,
! [X0] : composition(one,X0) = join(X0,composition(sK0_skl,X0)),
inference(paramodulation,[status(thm)],[f38,f555]) ).
fof(f37864,plain,
! [X0] : X0 = join(X0,composition(sK0_skl,X0)),
inference(forward_demodulation,[status(thm)],[f513,f37706]) ).
fof(f38976,plain,
! [X0] : converse(converse(X0)) = join(converse(composition(sK0_skl,converse(X0))),X0),
inference(paramodulation,[status(thm)],[f37864,f353]) ).
fof(f38993,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(X0,composition(sK0_skl,meet(X0,X1))),
inference(paramodulation,[status(thm)],[f37864,f1820]) ).
fof(f39031,plain,
! [X0] : composition(sK0_skl,X0) = meet(composition(sK0_skl,X0),X0),
inference(paramodulation,[status(thm)],[f37864,f2159]) ).
fof(f39065,plain,
! [X0] : X0 = join(converse(composition(sK0_skl,converse(X0))),X0),
inference(forward_demodulation,[status(thm)],[f26,f38976]) ).
fof(f39066,plain,
! [X0] : X0 = join(X0,converse(composition(sK0_skl,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f19,f39065]) ).
fof(f39067,plain,
! [X0] : X0 = join(X0,composition(X0,converse(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f112,f39066]) ).
fof(f39105,plain,
! [X0,X1] : X0 = join(X0,composition(sK0_skl,meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1783,f38993]) ).
fof(f39139,plain,
! [X0] : composition(sK0_skl,X0) = meet(X0,composition(sK0_skl,X0)),
inference(forward_demodulation,[status(thm)],[f1595,f39031]) ).
fof(f39699,plain,
composition(sK0_skl,top) = join(sF1_fnc,composition(composition(sK0_skl,converse(sK0_skl)),top)),
inference(paramodulation,[status(thm)],[f39067,f91]) ).
fof(f39806,plain,
sF1_fnc = join(sF1_fnc,composition(composition(sK0_skl,converse(sK0_skl)),top)),
inference(forward_demodulation,[status(thm)],[f40,f39699]) ).
fof(f39807,plain,
sF1_fnc = join(sF1_fnc,composition(sK0_skl,composition(converse(sK0_skl),top))),
inference(forward_demodulation,[status(thm)],[f23,f39806]) ).
fof(f39808,plain,
sF1_fnc = composition(sK0_skl,converse(composition(top,sK0_skl))),
inference(backward_demodulation,[status(thm)],[f39809,f19521]) ).
fof(f39809,plain,
sF1_fnc = join(sF1_fnc,composition(sK0_skl,converse(composition(top,sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f11088,f39807]) ).
fof(f41164,plain,
converse(sF1_fnc) = composition(composition(top,sK0_skl),converse(sK0_skl)),
inference(paramodulation,[status(thm)],[f39808,f112]) ).
fof(f41252,plain,
converse(sF1_fnc) = composition(top,composition(sK0_skl,converse(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f23,f41164]) ).
fof(f42612,plain,
! [X0,X1] : composition(sK0_skl,meet(X0,X1)) = meet(composition(sK0_skl,meet(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f39105,f2159]) ).
fof(f42714,plain,
! [X0,X1] : composition(sK0_skl,meet(X0,X1)) = meet(X0,composition(sK0_skl,meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1595,f42612]) ).
fof(f42727,plain,
join(composition(sK0_skl,one),meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))) = meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))),
inference(paramodulation,[status(thm)],[f39139,f1660]) ).
fof(f42855,plain,
join(sK0_skl,meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))) = meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f24,f42727]) ).
fof(f42856,plain,
join(sK0_skl,composition(sK0_skl,meet(one,converse(sK0_skl)))) = meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f42714,f42855]) ).
fof(f42857,plain,
join(sK0_skl,composition(sK0_skl,converse(sK0_skl))) = meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f9771,f42856]) ).
fof(f42858,plain,
sK0_skl = meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f39067,f42857]) ).
fof(f42859,plain,
sK0_skl = composition(sK0_skl,meet(one,converse(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f42714,f42858]) ).
fof(f42861,plain,
converse(sF1_fnc) = composition(top,sK0_skl),
inference(backward_demodulation,[status(thm)],[f42866,f41252]) ).
fof(f42866,plain,
sK0_skl = composition(sK0_skl,converse(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f9771,f42859]) ).
fof(f43339,plain,
! [X0] : join(meet(composition(sK0_skl,X0),converse(top)),meet(converse(top),composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(paramodulation,[status(thm)],[f42861,f1658]) ).
fof(f43402,plain,
! [X0] : join(meet(converse(top),composition(sK0_skl,X0)),meet(converse(top),composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f18921,f43339]) ).
fof(f43403,plain,
! [X0] : join(meet(top,composition(sK0_skl,X0)),meet(converse(top),composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f10844,f43402]) ).
fof(f43404,plain,
! [X0] : join(composition(sK0_skl,X0),meet(converse(top),composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f1412,f43403]) ).
fof(f43405,plain,
! [X0] : join(composition(sK0_skl,X0),meet(top,composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f10844,f43404]) ).
fof(f43406,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,converse(converse(sF1_fnc))))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f1412,f43405]) ).
fof(f43407,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = meet(converse(top),composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f26,f43406]) ).
fof(f43408,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = meet(top,composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl))))),
inference(forward_demodulation,[status(thm)],[f10844,f43407]) ).
fof(f43409,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = composition(sK0_skl,meet(X0,converse(composition(top,sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f1412,f43408]) ).
fof(f43410,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = composition(sK0_skl,meet(X0,converse(converse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f42861,f43409]) ).
fof(f43411,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = composition(sK0_skl,meet(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f26,f43410]) ).
fof(f44493,plain,
converse(sK0_skl) = composition(sK0_skl,converse(sK0_skl)),
inference(paramodulation,[status(thm)],[f42866,f112]) ).
fof(f44548,plain,
! [X0] : composition(sK0_skl,composition(converse(sK0_skl),X0)) = composition(sK0_skl,X0),
inference(paramodulation,[status(thm)],[f42866,f23]) ).
fof(f44600,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0)))) = meet(X0,composition(sK0_skl,composition(sK0_skl,X0))),
inference(backward_demodulation,[status(thm)],[f44939,f1650]) ).
fof(f44877,plain,
! [X0] : meet(X0,sF1_fnc) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(sK0_skl,meet(X0,sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f44939,f19516]) ).
fof(f44879,plain,
! [X0] : meet(sF1_fnc,X0) = meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(sK0_skl,meet(X0,sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f44939,f19514]) ).
fof(f44939,plain,
converse(sK0_skl) = sK0_skl,
inference(forward_demodulation,[status(thm)],[f42866,f44493]) ).
fof(f45246,plain,
! [X0] : composition(sK0_skl,composition(sK0_skl,X0)) = composition(sK0_skl,X0),
inference(forward_demodulation,[status(thm)],[f44939,f44548]) ).
fof(f45265,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(sK0_skl,X0)))) = meet(X0,composition(sK0_skl,composition(sK0_skl,X0))),
inference(forward_demodulation,[status(thm)],[f44939,f44600]) ).
fof(f45266,plain,
! [X0] : join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,X0))) = meet(X0,composition(sK0_skl,composition(sK0_skl,X0))),
inference(forward_demodulation,[status(thm)],[f45246,f45265]) ).
fof(f45267,plain,
! [X0] : join(meet(sF1_fnc,X0),composition(sK0_skl,X0)) = meet(X0,composition(sK0_skl,composition(sK0_skl,X0))),
inference(forward_demodulation,[status(thm)],[f39139,f45266]) ).
fof(f45268,plain,
! [X0] : join(meet(sF1_fnc,X0),composition(sK0_skl,X0)) = meet(X0,composition(sK0_skl,X0)),
inference(forward_demodulation,[status(thm)],[f45246,f45267]) ).
fof(f45269,plain,
! [X0] : join(meet(sF1_fnc,X0),composition(sK0_skl,X0)) = composition(sK0_skl,X0),
inference(forward_demodulation,[status(thm)],[f39139,f45268]) ).
fof(f45712,plain,
! [X0] : meet(X0,sF1_fnc) = meet(meet(X0,sF1_fnc),composition(sK0_skl,meet(X0,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f45246,f44877]) ).
fof(f45714,plain,
! [X0] : join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc))) = meet(X0,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f45715,f43411]) ).
fof(f45715,plain,
! [X0] : meet(X0,sF1_fnc) = composition(sK0_skl,meet(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f39139,f45712]) ).
fof(f45718,plain,
! [X0] : meet(sF1_fnc,X0) = meet(meet(X0,sF1_fnc),composition(sK0_skl,meet(X0,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f45246,f44879]) ).
fof(f45719,plain,
! [X0] : meet(sF1_fnc,X0) = composition(sK0_skl,meet(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f39139,f45718]) ).
fof(f45838,plain,
! [X0] : join(composition(sK0_skl,X0),meet(sF1_fnc,X0)) = meet(X0,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f45719,f45714]) ).
fof(f45839,plain,
! [X0] : meet(X0,sF1_fnc) = composition(sK0_skl,X0),
inference(backward_demodulation,[status(thm)],[f45840,f45269]) ).
fof(f45840,plain,
! [X0] : join(meet(sF1_fnc,X0),composition(sK0_skl,X0)) = meet(X0,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f19,f45838]) ).
fof(f45846,plain,
sF2_fnc = meet(sK1_skl,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f45839,f42]) ).
fof(f46229,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1555,f45846]) ).
fof(f46230,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f46229,f43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL026+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.55 % Computer : n010.cluster.edu
% 0.08/0.55 % Model : x86_64 x86_64
% 0.08/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.55 % Memory : 8046.5625MB
% 0.08/0.55 % OS : Linux 6.8.0-71-generic
% 0.08/0.55 % CPULimit : 300
% 0.08/0.55 % WCLimit : 300
% 0.08/0.55 % DateTime : Mon Sep 21 04:02:25 UTC 2026
% 0.08/0.55 % CPUTime :
% 0.13/0.56 % Drodi V4.1.1
% 230.29/29.73 % Refutation found
% 230.29/29.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 230.29/29.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 38.34/30.09 % Elapsed time: 29.499189 seconds
% 38.34/30.09 % CPU time: 233.018001 seconds
% 38.34/30.09 % Total memory used: 1.147 GB
% 38.34/30.09 % Net memory used: 1.110 GB
%------------------------------------------------------------------------------