%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL019-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:17 PM UTC 2026
% Result : Unsatisfiable 204.96s 26.11s
% Output : CNFRefutation 147.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 19
% Syntax : Number of formulae : 359 ( 359 unt; 2 def)
% Number of atoms : 359 ( 358 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 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 : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 453 ( 453 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : join(A,B) = join(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : composition(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : converse(converse(A)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : top = join(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [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))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
composition(sk2,top) = sk2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
composition(meet(sk1,sk2),top) != meet(sk1,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f23,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f25,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f26,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f27,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f28,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f29,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f32,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),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(f36,plain,
composition(sk1,top) = sk1,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f37,plain,
composition(sk2,top) = sk2,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f38,plain,
composition(meet(sk1,sk2),top) != meet(sk1,sk2),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f39,definition,
sF1_fnc = meet(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f40,definition,
sF0_fnc = composition(sF1_fnc,top),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f41,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f38,f40,f39]) ).
fof(f42,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f20,f22]) ).
fof(f43,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f23,f42]) ).
fof(f44,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f20,f30]) ).
fof(f45,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f20,f43]) ).
fof(f52,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f20,f21]) ).
fof(f55,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f31,f21]) ).
fof(f56,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X1,X0),X2),
inference(paramodulation,[status(thm)],[f20,f21]) ).
fof(f63,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(forward_demodulation,[status(thm)],[f21,f56]) ).
fof(f65,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f31,f23]) ).
fof(f66,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f20,f23]) ).
fof(f71,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f23,f31]) ).
fof(f72,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f32,f65]) ).
fof(f73,plain,
sF1_fnc = meet(sk2,sk1),
inference(backward_demodulation,[status(thm)],[f76,f39]) ).
fof(f76,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f23,f66]) ).
fof(f79,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f21,f71]) ).
fof(f82,plain,
! [X0] : meet(X0,top) = complement(join(complement(X0),zero)),
inference(paramodulation,[status(thm)],[f72,f23]) ).
fof(f85,plain,
top = join(top,zero),
inference(paramodulation,[status(thm)],[f72,f31]) ).
fof(f86,plain,
! [X0] : meet(X0,top) = complement(join(zero,complement(X0))),
inference(forward_demodulation,[status(thm)],[f20,f82]) ).
fof(f89,plain,
top = join(zero,top),
inference(forward_demodulation,[status(thm)],[f20,f85]) ).
fof(f95,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f25,f24]) ).
fof(f115,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f27,f28]) ).
fof(f116,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(paramodulation,[status(thm)],[f27,f28]) ).
fof(f124,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X1,X2),composition(X0,X2)),
inference(paramodulation,[status(thm)],[f20,f26]) ).
fof(f126,plain,
! [X0,X1,X2,X3] : composition(join(composition(X0,X1),X2),X3) = join(composition(X0,composition(X1,X3)),composition(X2,X3)),
inference(paramodulation,[status(thm)],[f24,f26]) ).
fof(f127,plain,
! [X0] : composition(join(sF1_fnc,X0),top) = join(sF0_fnc,composition(X0,top)),
inference(paramodulation,[status(thm)],[f40,f26]) ).
fof(f129,plain,
! [X0] : composition(join(sk1,X0),top) = join(sk1,composition(X0,top)),
inference(paramodulation,[status(thm)],[f36,f26]) ).
fof(f141,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = composition(join(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f26,f124]) ).
fof(f197,plain,
! [X0,X1] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(paramodulation,[status(thm)],[f27,f29]) ).
fof(f200,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f27,f29]) ).
fof(f237,plain,
! [X0,X1,X2,X3] : join(X0,composition(join(X1,X2),X3)) = join(composition(X2,X3),join(X0,composition(X1,X3))),
inference(paramodulation,[status(thm)],[f26,f52]) ).
fof(f261,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X1,X0)),
inference(paramodulation,[status(thm)],[f20,f52]) ).
fof(f320,plain,
! [X0] : join(X0,top) = join(top,complement(complement(X0))),
inference(paramodulation,[status(thm)],[f31,f55]) ).
fof(f323,plain,
! [X0] : join(top,join(zero,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f72,f55]) ).
fof(f334,plain,
! [X0] : join(zero,join(X0,top)) = join(top,X0),
inference(forward_demodulation,[status(thm)],[f52,f323]) ).
fof(f351,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(paramodulation,[status(thm)],[f52,f63]) ).
fof(f457,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = complement(top),
inference(paramodulation,[status(thm)],[f72,f44]) ).
fof(f461,plain,
! [X0,X1] : join(complement(X0),composition(X1,complement(composition(converse(X1),X0)))) = complement(X0),
inference(paramodulation,[status(thm)],[f27,f44]) ).
fof(f463,plain,
! [X0,X1,X2] : join(complement(X0),composition(converse(composition(X1,X2)),complement(composition(X1,composition(X2,X0))))) = complement(X0),
inference(paramodulation,[status(thm)],[f24,f44]) ).
fof(f465,plain,
join(complement(top),composition(converse(sk2),complement(sk2))) = complement(top),
inference(paramodulation,[status(thm)],[f37,f44]) ).
fof(f468,plain,
! [X0] : join(complement(one),composition(converse(X0),complement(X0))) = complement(one),
inference(paramodulation,[status(thm)],[f25,f44]) ).
fof(f476,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f72,f457]) ).
fof(f481,plain,
join(zero,composition(converse(sk2),complement(sk2))) = complement(top),
inference(forward_demodulation,[status(thm)],[f72,f465]) ).
fof(f482,plain,
join(zero,composition(converse(sk2),complement(sk2))) = zero,
inference(forward_demodulation,[status(thm)],[f72,f481]) ).
fof(f491,plain,
meet(top,top) = complement(join(zero,zero)),
inference(paramodulation,[status(thm)],[f72,f86]) ).
fof(f667,plain,
! [X0,X1,X2] : join(meet(composition(X0,converse(X1)),X2),composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(converse(X1)))),meet(converse(X1),composition(converse(X0),X2))),
inference(paramodulation,[status(thm)],[f27,f33]) ).
fof(f692,plain,
! [X0,X1,X2] : join(meet(composition(X0,converse(X1)),X2),composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,X1)),meet(converse(X1),composition(converse(X0),X2))),
inference(forward_demodulation,[status(thm)],[f27,f667]) ).
fof(f874,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f25,f200]) ).
fof(f897,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f27,f874]) ).
fof(f916,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f95,f897]) ).
fof(f917,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f25,f897]) ).
fof(f918,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f897,f44]) ).
fof(f928,plain,
! [X0,X1] : composition(join(X0,converse(one)),X1) = join(composition(X0,X1),X1),
inference(paramodulation,[status(thm)],[f897,f26]) ).
fof(f937,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f897,f916]) ).
fof(f940,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f937,f918]) ).
fof(f961,plain,
! [X0,X1] : composition(join(X0,one),X1) = join(composition(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f917,f928]) ).
fof(f963,plain,
! [X0,X1] : composition(join(X0,one),X1) = join(X1,composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f20,f961]) ).
fof(f1001,plain,
sk2 = join(sF1_fnc,complement(join(complement(sk2),sk1))),
inference(paramodulation,[status(thm)],[f73,f45]) ).
fof(f1002,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),complement(X0)))),
inference(paramodulation,[status(thm)],[f32,f45]) ).
fof(f1005,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f23,f45]) ).
fof(f1007,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))),
inference(paramodulation,[status(thm)],[f55,f45]) ).
fof(f1014,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(X1,complement(X0)))),
inference(paramodulation,[status(thm)],[f20,f45]) ).
fof(f1026,plain,
sk2 = join(sF1_fnc,complement(join(sk1,complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f20,f1001]) ).
fof(f1027,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f23,f1002]) ).
fof(f1028,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f20,f1005]) ).
fof(f1030,plain,
! [X0,X1] : X0 = join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f20,f1007]) ).
fof(f1043,plain,
! [X0] : converse(join(X0,one)) = join(converse(X0),one),
inference(paramodulation,[status(thm)],[f917,f116]) ).
fof(f1055,plain,
! [X0] : converse(join(X0,one)) = join(one,converse(X0)),
inference(forward_demodulation,[status(thm)],[f20,f1043]) ).
fof(f1083,plain,
join(zero,complement(top)) = complement(top),
inference(paramodulation,[status(thm)],[f72,f940]) ).
fof(f1085,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),complement(X1)))) = complement(join(complement(X0),complement(X1))),
inference(paramodulation,[status(thm)],[f23,f940]) ).
fof(f1089,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f940,f23]) ).
fof(f1090,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f940,f45]) ).
fof(f1091,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(paramodulation,[status(thm)],[f940,f55]) ).
fof(f1098,plain,
join(zero,zero) = complement(top),
inference(forward_demodulation,[status(thm)],[f72,f1083]) ).
fof(f1099,plain,
meet(top,top) = complement(zero),
inference(backward_demodulation,[status(thm)],[f1100,f491]) ).
fof(f1100,plain,
join(zero,zero) = zero,
inference(forward_demodulation,[status(thm)],[f72,f1098]) ).
fof(f1103,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,X1)) = complement(join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f23,f1085]) ).
fof(f1105,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,X1)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f23,f1103]) ).
fof(f1115,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f20,f1090]) ).
fof(f1116,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f32,f1115]) ).
fof(f1117,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f20,f1116]) ).
fof(f1119,plain,
! [X0] : join(X0,top) = top,
inference(backward_demodulation,[status(thm)],[f1120,f320]) ).
fof(f1120,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f31,f1091]) ).
fof(f1128,plain,
! [X0] : join(zero,top) = join(top,X0),
inference(backward_demodulation,[status(thm)],[f1119,f334]) ).
fof(f1142,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(complement(X0)),X1))),
inference(backward_demodulation,[status(thm)],[f1148,f1030]) ).
fof(f1148,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[status(thm)],[f89,f1128]) ).
fof(f1159,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(complement(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f72,f1142]) ).
fof(f1168,plain,
! [X0] : converse(top) = join(X0,converse(top)),
inference(paramodulation,[status(thm)],[f1119,f115]) ).
fof(f1169,plain,
! [X0] : X0 = join(meet(X0,top),complement(top)),
inference(paramodulation,[status(thm)],[f1119,f45]) ).
fof(f1184,plain,
! [X0] : X0 = join(complement(top),meet(X0,top)),
inference(forward_demodulation,[status(thm)],[f20,f1169]) ).
fof(f1186,plain,
! [X0] : X0 = join(zero,meet(X0,top)),
inference(forward_demodulation,[status(thm)],[f72,f1184]) ).
fof(f1242,plain,
! [X0] : join(zero,join(X0,zero)) = join(X0,zero),
inference(paramodulation,[status(thm)],[f1100,f63]) ).
fof(f1312,plain,
! [X0] : meet(complement(X0),top) = complement(join(zero,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f1089,f86]) ).
fof(f1336,plain,
! [X0] : meet(top,complement(X0)) = complement(join(zero,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f76,f1312]) ).
fof(f1337,plain,
! [X0] : meet(top,complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1027,f1336]) ).
fof(f1345,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f23,f1117]) ).
fof(f1349,plain,
! [X0,X1] : join(zero,join(complement(complement(X0)),X1)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f1117,f52]) ).
fof(f1373,plain,
! [X0] : X0 = join(zero,meet(top,X0)),
inference(paramodulation,[status(thm)],[f76,f1186]) ).
fof(f1410,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(paramodulation,[status(thm)],[f1337,f1373]) ).
fof(f1423,plain,
! [X0] : X0 = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1410,f1117]) ).
fof(f1424,plain,
! [X0] : meet(X0,top) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f1410,f86]) ).
fof(f1425,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1410,f1345]) ).
fof(f1441,plain,
! [X0,X1] : join(zero,join(X0,X1)) = join(X1,X0),
inference(backward_demodulation,[status(thm)],[f1423,f1349]) ).
fof(f1446,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(X0,X1))),
inference(backward_demodulation,[status(thm)],[f1423,f1159]) ).
fof(f1449,plain,
top = complement(zero),
inference(backward_demodulation,[status(thm)],[f1454,f1099]) ).
fof(f1451,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f1454,f1186]) ).
fof(f1454,plain,
! [X0] : meet(X0,top) = X0,
inference(forward_demodulation,[status(thm)],[f1423,f1424]) ).
fof(f1493,plain,
! [X0] : join(zero,X0) = join(X0,zero),
inference(backward_demodulation,[status(thm)],[f1441,f1242]) ).
fof(f1500,plain,
! [X0] : X0 = meet(top,X0),
inference(backward_demodulation,[status(thm)],[f1451,f1373]) ).
fof(f1502,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1451,f1446]) ).
fof(f1505,plain,
composition(converse(sk2),complement(sk2)) = zero,
inference(backward_demodulation,[status(thm)],[f1451,f482]) ).
fof(f1507,plain,
! [X0] : composition(converse(X0),complement(composition(X0,top))) = zero,
inference(backward_demodulation,[status(thm)],[f1451,f476]) ).
fof(f1532,plain,
! [X0] : X0 = join(X0,zero),
inference(forward_demodulation,[status(thm)],[f1451,f1493]) ).
fof(f1555,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)),
inference(paramodulation,[status(thm)],[f79,f45]) ).
fof(f1578,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f20,f1555]) ).
fof(f1579,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f72,f1578]) ).
fof(f1580,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1451,f1579]) ).
fof(f1668,plain,
! [X0] : converse(converse(X0)) = join(converse(zero),X0),
inference(paramodulation,[status(thm)],[f1451,f116]) ).
fof(f1690,plain,
! [X0] : X0 = join(converse(zero),X0),
inference(forward_demodulation,[status(thm)],[f27,f1668]) ).
fof(f1932,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f45,f1502]) ).
fof(f1942,plain,
! [X0,X1,X2] : X0 = meet(X0,join(X1,join(X0,X2))),
inference(paramodulation,[status(thm)],[f63,f1502]) ).
fof(f1947,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f20,f1502]) ).
fof(f1954,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f76,f1932]) ).
fof(f1961,plain,
zero = converse(zero),
inference(paramodulation,[status(thm)],[f1532,f1690]) ).
fof(f2155,plain,
! [X0,X1] : converse(X0) = meet(converse(X0),converse(join(X1,X0))),
inference(paramodulation,[status(thm)],[f28,f1947]) ).
fof(f2181,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1148,f1168]) ).
fof(f2277,plain,
! [X0] : converse(composition(top,X0)) = composition(converse(X0),top),
inference(paramodulation,[status(thm)],[f2181,f200]) ).
fof(f2320,plain,
meet(sk2,sk1) = meet(sk2,sF1_fnc),
inference(paramodulation,[status(thm)],[f73,f1954]) ).
fof(f2328,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f76,f1954]) ).
fof(f2336,plain,
sF1_fnc = meet(sk2,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f73,f2320]) ).
fof(f2337,plain,
sF1_fnc = meet(sF1_fnc,sk2),
inference(forward_demodulation,[status(thm)],[f76,f2336]) ).
fof(f2414,plain,
composition(join(sF1_fnc,sk2),top) = join(sF0_fnc,sk2),
inference(paramodulation,[status(thm)],[f37,f127]) ).
fof(f2497,plain,
meet(sk1,sk2) = meet(sk1,sF1_fnc),
inference(paramodulation,[status(thm)],[f73,f2328]) ).
fof(f2519,plain,
meet(sk2,sk1) = meet(sk1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f76,f2497]) ).
fof(f2520,plain,
sF1_fnc = meet(sk1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f73,f2519]) ).
fof(f2521,plain,
sF1_fnc = meet(sF1_fnc,sk1),
inference(forward_demodulation,[status(thm)],[f76,f2520]) ).
fof(f2566,plain,
converse(zero) = composition(converse(complement(sk2)),sk2),
inference(paramodulation,[status(thm)],[f1505,f200]) ).
fof(f2575,plain,
zero = composition(converse(complement(sk2)),sk2),
inference(forward_demodulation,[status(thm)],[f1961,f2566]) ).
fof(f2762,plain,
join(complement(sk2),composition(converse(converse(complement(sk2))),complement(zero))) = complement(sk2),
inference(paramodulation,[status(thm)],[f2575,f44]) ).
fof(f2774,plain,
join(complement(sk2),composition(complement(sk2),complement(zero))) = complement(sk2),
inference(forward_demodulation,[status(thm)],[f27,f2762]) ).
fof(f2775,plain,
join(complement(sk2),composition(complement(sk2),top)) = complement(sk2),
inference(forward_demodulation,[status(thm)],[f1449,f2774]) ).
fof(f2948,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f76,f1028]) ).
fof(f2954,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f76,f1028]) ).
fof(f3003,plain,
! [X0,X1] : X0 = meet(X0,join(X1,meet(X0,complement(X1)))),
inference(paramodulation,[status(thm)],[f1423,f1580]) ).
fof(f3397,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f76,f2948]) ).
fof(f3571,plain,
! [X0,X1] : X0 = meet(X0,join(X1,meet(complement(X1),X0))),
inference(paramodulation,[status(thm)],[f76,f3003]) ).
fof(f4321,plain,
! [X0,X1] : join(X0,top) = join(complement(X1),join(X1,X0)),
inference(paramodulation,[status(thm)],[f31,f261]) ).
fof(f4490,plain,
! [X0,X1] : top = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1119,f4321]) ).
fof(f4492,plain,
! [X0,X1] : top = join(X0,join(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f63,f4490]) ).
fof(f5595,plain,
! [X0] : join(X0,meet(top,X0)) = meet(top,X0),
inference(paramodulation,[status(thm)],[f1500,f1105]) ).
fof(f5666,plain,
! [X0] : join(X0,X0) = meet(top,X0),
inference(forward_demodulation,[status(thm)],[f1500,f5595]) ).
fof(f5673,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1500,f5666]) ).
fof(f5803,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f5673,f261]) ).
fof(f5812,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f5673,f63]) ).
fof(f5894,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(complement(X0),X1),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f3397,f5803]) ).
fof(f5895,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(complement(X1),X0),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f2954,f5803]) ).
fof(f6000,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(complement(X1),X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f20,f5894]) ).
fof(f6001,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f20,f6000]) ).
fof(f6008,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f3397,f6001]) ).
fof(f6009,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(complement(X1),X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f20,f5895]) ).
fof(f6010,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f20,f6009]) ).
fof(f6040,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2954,f6010]) ).
fof(f6165,plain,
join(sk1,sF1_fnc) = sk1,
inference(paramodulation,[status(thm)],[f2521,f6008]) ).
fof(f6166,plain,
join(sk2,sF1_fnc) = sk2,
inference(paramodulation,[status(thm)],[f2337,f6008]) ).
fof(f6174,plain,
! [X0,X1] : join(join(X0,meet(complement(X0),X1)),X1) = join(X0,meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f3571,f6008]) ).
fof(f6175,plain,
! [X0,X1] : join(join(X0,meet(X1,complement(X0))),X1) = join(X0,meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f3003,f6008]) ).
fof(f6219,plain,
join(sF1_fnc,sk1) = sk1,
inference(forward_demodulation,[status(thm)],[f20,f6165]) ).
fof(f6220,plain,
composition(sk2,top) = join(sF0_fnc,sk2),
inference(backward_demodulation,[status(thm)],[f6221,f2414]) ).
fof(f6221,plain,
join(sF1_fnc,sk2) = sk2,
inference(forward_demodulation,[status(thm)],[f20,f6166]) ).
fof(f6251,plain,
! [X0,X1] : join(X0,join(meet(complement(X0),X1),X1)) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f21,f6174]) ).
fof(f6252,plain,
! [X0,X1] : join(X0,join(X1,meet(complement(X0),X1))) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f351,f6251]) ).
fof(f6265,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[status(thm)],[f6008,f6252]) ).
fof(f6266,plain,
! [X0,X1] : join(X0,join(meet(X1,complement(X0)),X1)) = join(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[status(thm)],[f21,f6175]) ).
fof(f6267,plain,
! [X0,X1] : join(X0,join(X1,meet(X1,complement(X0)))) = join(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[status(thm)],[f351,f6266]) ).
fof(f6274,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[status(thm)],[f6040,f6267]) ).
fof(f6300,plain,
sk2 = join(sF0_fnc,sk2),
inference(forward_demodulation,[status(thm)],[f37,f6220]) ).
fof(f6528,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(converse(X0),X1))),
inference(paramodulation,[status(thm)],[f6040,f115]) ).
fof(f6566,plain,
! [X0,X1] : X0 = join(X0,converse(meet(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f27,f6528]) ).
fof(f6587,plain,
! [X0] : sF1_fnc = meet(sF1_fnc,join(X0,sk1)),
inference(paramodulation,[status(thm)],[f6219,f1942]) ).
fof(f6655,plain,
sF0_fnc = meet(sF0_fnc,sk2),
inference(paramodulation,[status(thm)],[f6300,f1502]) ).
fof(f6903,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),X0) = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f45,f5812]) ).
fof(f7007,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f20,f6903]) ).
fof(f7008,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f45,f7007]) ).
fof(f7137,plain,
! [X0] : sF1_fnc = meet(sF1_fnc,join(sk1,X0)),
inference(paramodulation,[status(thm)],[f20,f6587]) ).
fof(f8540,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(paramodulation,[status(thm)],[f1423,f1425]) ).
fof(f8543,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f1423,f1425]) ).
fof(f8546,plain,
! [X0,X1] : top = join(X0,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f1425,f4492]) ).
fof(f8631,plain,
! [X0,X1] : top = complement(meet(X0,meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f1425,f8546]) ).
fof(f10145,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = complement(top),
inference(paramodulation,[status(thm)],[f8631,f1423]) ).
fof(f10197,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = zero,
inference(forward_demodulation,[status(thm)],[f72,f10145]) ).
fof(f10222,plain,
! [X0,X1] : meet(X0,meet(X1,complement(X0))) = zero,
inference(paramodulation,[status(thm)],[f76,f10197]) ).
fof(f10227,plain,
! [X0,X1] : meet(complement(X0),meet(X0,X1)) = zero,
inference(paramodulation,[status(thm)],[f1423,f10197]) ).
fof(f10296,plain,
! [X0,X1] : meet(complement(X0),meet(X1,X0)) = zero,
inference(paramodulation,[status(thm)],[f1423,f10222]) ).
fof(f10380,plain,
meet(complement(sk2),sF1_fnc) = zero,
inference(paramodulation,[status(thm)],[f73,f10227]) ).
fof(f10429,plain,
meet(sF1_fnc,complement(sk2)) = zero,
inference(forward_demodulation,[status(thm)],[f76,f10380]) ).
fof(f10467,plain,
complement(sk2) = join(zero,meet(complement(sF1_fnc),complement(sk2))),
inference(paramodulation,[status(thm)],[f10429,f3397]) ).
fof(f10482,plain,
complement(sk2) = meet(complement(sF1_fnc),complement(sk2)),
inference(forward_demodulation,[status(thm)],[f1451,f10467]) ).
fof(f10510,plain,
meet(complement(sk2),sF0_fnc) = zero,
inference(paramodulation,[status(thm)],[f6655,f10296]) ).
fof(f10530,plain,
! [X0,X1] : meet(complement(join(X0,X1)),X1) = zero,
inference(paramodulation,[status(thm)],[f1947,f10296]) ).
fof(f10563,plain,
meet(sF0_fnc,complement(sk2)) = zero,
inference(forward_demodulation,[status(thm)],[f76,f10510]) ).
fof(f10579,plain,
! [X0,X1] : meet(X0,complement(join(X1,X0))) = zero,
inference(forward_demodulation,[status(thm)],[f76,f10530]) ).
fof(f11179,plain,
complement(sk2) = join(zero,meet(complement(sF0_fnc),complement(sk2))),
inference(paramodulation,[status(thm)],[f10563,f3397]) ).
fof(f11194,plain,
complement(sk2) = meet(complement(sF0_fnc),complement(sk2)),
inference(forward_demodulation,[status(thm)],[f1451,f11179]) ).
fof(f11312,plain,
! [X0] : meet(composition(converse(X0),complement(X0)),complement(complement(one))) = zero,
inference(paramodulation,[status(thm)],[f468,f10579]) ).
fof(f11393,plain,
! [X0] : meet(complement(complement(one)),composition(converse(X0),complement(X0))) = zero,
inference(forward_demodulation,[status(thm)],[f76,f11312]) ).
fof(f11394,plain,
! [X0] : meet(one,composition(converse(X0),complement(X0))) = zero,
inference(forward_demodulation,[status(thm)],[f1423,f11393]) ).
fof(f14089,plain,
join(sk1,complement(sk2)) = join(meet(join(sk1,complement(sk2)),sF1_fnc),complement(sk2)),
inference(paramodulation,[status(thm)],[f1026,f1014]) ).
fof(f14218,plain,
join(sk1,complement(sk2)) = join(complement(sk2),meet(join(sk1,complement(sk2)),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f20,f14089]) ).
fof(f14219,plain,
join(sk1,complement(sk2)) = join(complement(sk2),meet(sF1_fnc,join(sk1,complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f76,f14218]) ).
fof(f14220,plain,
join(sk1,complement(sk2)) = join(complement(sk2),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f7137,f14219]) ).
fof(f14225,plain,
join(sk1,complement(sk2)) = join(sF1_fnc,complement(sk2)),
inference(forward_demodulation,[status(thm)],[f20,f14220]) ).
fof(f14758,plain,
composition(top,complement(composition(top,top))) = zero,
inference(paramodulation,[status(thm)],[f2181,f1507]) ).
fof(f39051,plain,
! [X0,X1,X2] : join(complement(X0),meet(complement(X1),X2)) = complement(meet(X0,join(X1,complement(X2)))),
inference(paramodulation,[status(thm)],[f8540,f8543]) ).
fof(f39067,plain,
! [X0,X1,X2] : join(meet(X0,complement(X1)),complement(X2)) = complement(meet(join(complement(X0),X1),X2)),
inference(paramodulation,[status(thm)],[f8543,f8540]) ).
fof(f39078,plain,
! [X0,X1,X2] : join(meet(X0,complement(X1)),complement(join(join(complement(X0),X1),X2))) = meet(X0,complement(X1)),
inference(paramodulation,[status(thm)],[f8543,f7008]) ).
fof(f39155,plain,
! [X0,X1,X2] : complement(meet(join(complement(X0),X1),join(join(complement(X0),X1),X2))) = meet(X0,complement(X1)),
inference(forward_demodulation,[status(thm)],[f39067,f39078]) ).
fof(f39186,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(X1)),
inference(forward_demodulation,[status(thm)],[f1502,f39155]) ).
fof(f47417,plain,
complement(sF1_fnc) = join(meet(complement(sF1_fnc),sk2),complement(sk2)),
inference(paramodulation,[status(thm)],[f10482,f1028]) ).
fof(f47466,plain,
complement(sF1_fnc) = join(complement(sk2),meet(complement(sF1_fnc),sk2)),
inference(forward_demodulation,[status(thm)],[f20,f47417]) ).
fof(f47467,plain,
complement(sF1_fnc) = complement(meet(sk2,join(sF1_fnc,complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f39051,f47466]) ).
fof(f48519,plain,
complement(sF0_fnc) = join(meet(complement(sF0_fnc),sk2),complement(sk2)),
inference(paramodulation,[status(thm)],[f11194,f1028]) ).
fof(f48568,plain,
complement(sF0_fnc) = join(complement(sk2),meet(complement(sF0_fnc),sk2)),
inference(forward_demodulation,[status(thm)],[f20,f48519]) ).
fof(f48569,plain,
complement(sF0_fnc) = complement(meet(sk2,join(sF0_fnc,complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f39051,f48568]) ).
fof(f49949,plain,
! [X0] : join(meet(composition(one,converse(complement(X0))),converse(X0)),composition(zero,meet(converse(complement(X0)),composition(converse(one),converse(X0))))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(paramodulation,[status(thm)],[f11394,f692]) ).
fof(f50031,plain,
! [X0] : join(meet(converse(X0),composition(one,converse(complement(X0)))),composition(zero,meet(converse(complement(X0)),composition(converse(one),converse(X0))))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f76,f49949]) ).
fof(f50032,plain,
! [X0] : join(meet(converse(X0),converse(complement(X0))),composition(zero,meet(converse(complement(X0)),composition(converse(one),converse(X0))))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f937,f50031]) ).
fof(f50033,plain,
! [X0] : join(meet(converse(X0),converse(complement(X0))),composition(zero,meet(converse(complement(X0)),converse(composition(X0,one))))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f29,f50032]) ).
fof(f50034,plain,
! [X0] : join(meet(converse(X0),converse(complement(X0))),composition(zero,meet(converse(complement(X0)),converse(X0)))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f25,f50033]) ).
fof(f50035,plain,
! [X0] : join(meet(converse(X0),converse(complement(X0))),composition(zero,meet(converse(X0),converse(complement(X0))))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f76,f50034]) ).
fof(f50036,plain,
! [X0] : composition(join(zero,one),meet(converse(X0),converse(complement(X0)))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f963,f50035]) ).
fof(f50037,plain,
! [X0] : composition(one,meet(converse(X0),converse(complement(X0)))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f1451,f50036]) ).
fof(f50038,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = composition(meet(one,composition(converse(X0),complement(X0))),meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f937,f50037]) ).
fof(f50039,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = composition(zero,meet(converse(complement(X0)),composition(converse(one),converse(X0)))),
inference(forward_demodulation,[status(thm)],[f11394,f50038]) ).
fof(f50040,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = composition(zero,meet(converse(complement(X0)),converse(composition(X0,one)))),
inference(forward_demodulation,[status(thm)],[f29,f50039]) ).
fof(f50041,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = composition(zero,meet(converse(complement(X0)),converse(X0))),
inference(forward_demodulation,[status(thm)],[f25,f50040]) ).
fof(f50042,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = composition(zero,meet(converse(X0),converse(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f76,f50041]) ).
fof(f53943,plain,
! [X0,X1] : join(X0,composition(join(top,X1),complement(composition(top,top)))) = join(composition(X1,complement(composition(top,top))),join(X0,zero)),
inference(paramodulation,[status(thm)],[f14758,f237]) ).
fof(f53967,plain,
! [X0,X1] : composition(join(composition(X0,top),X1),complement(composition(top,top))) = join(composition(X0,zero),composition(X1,complement(composition(top,top)))),
inference(paramodulation,[status(thm)],[f14758,f126]) ).
fof(f53970,plain,
! [X0] : composition(join(X0,top),complement(composition(top,top))) = join(composition(X0,complement(composition(top,top))),zero),
inference(paramodulation,[status(thm)],[f14758,f26]) ).
fof(f53975,plain,
! [X0,X1] : join(X0,composition(top,complement(composition(top,top)))) = join(composition(X1,complement(composition(top,top))),join(X0,zero)),
inference(forward_demodulation,[status(thm)],[f1148,f53943]) ).
fof(f53976,plain,
! [X0,X1] : join(X0,zero) = join(composition(X1,complement(composition(top,top))),join(X0,zero)),
inference(forward_demodulation,[status(thm)],[f14758,f53975]) ).
fof(f53977,plain,
! [X0,X1] : X0 = join(composition(X1,complement(composition(top,top))),join(X0,zero)),
inference(forward_demodulation,[status(thm)],[f1532,f53976]) ).
fof(f53978,plain,
! [X0,X1] : X0 = join(zero,join(X0,composition(X1,complement(composition(top,top))))),
inference(forward_demodulation,[status(thm)],[f261,f53977]) ).
fof(f53979,plain,
! [X0,X1] : X0 = join(X0,composition(X1,complement(composition(top,top)))),
inference(forward_demodulation,[status(thm)],[f1451,f53978]) ).
fof(f54090,plain,
! [X0,X1] : composition(join(composition(X0,top),X1),complement(composition(top,top))) = composition(X0,zero),
inference(forward_demodulation,[status(thm)],[f53979,f53967]) ).
fof(f54098,plain,
! [X0] : composition(top,complement(composition(top,top))) = join(composition(X0,complement(composition(top,top))),zero),
inference(forward_demodulation,[status(thm)],[f1119,f53970]) ).
fof(f54099,plain,
! [X0] : zero = join(composition(X0,complement(composition(top,top))),zero),
inference(forward_demodulation,[status(thm)],[f14758,f54098]) ).
fof(f54104,plain,
! [X0] : zero = composition(X0,zero),
inference(backward_demodulation,[status(thm)],[f54109,f54090]) ).
fof(f54109,plain,
! [X0] : zero = composition(X0,complement(composition(top,top))),
inference(forward_demodulation,[status(thm)],[f1532,f54099]) ).
fof(f54465,plain,
! [X0] : join(complement(zero),composition(X0,complement(zero))) = complement(zero),
inference(paramodulation,[status(thm)],[f54104,f461]) ).
fof(f54467,plain,
! [X0] : converse(zero) = composition(converse(zero),X0),
inference(paramodulation,[status(thm)],[f54104,f200]) ).
fof(f54496,plain,
! [X0] : join(complement(zero),composition(converse(X0),complement(zero))) = complement(zero),
inference(paramodulation,[status(thm)],[f54104,f44]) ).
fof(f54521,plain,
! [X0] : composition(join(X0,one),complement(zero)) = complement(zero),
inference(forward_demodulation,[status(thm)],[f963,f54465]) ).
fof(f54522,plain,
! [X0] : composition(join(X0,one),top) = complement(zero),
inference(forward_demodulation,[status(thm)],[f1449,f54521]) ).
fof(f54526,plain,
! [X0] : composition(join(X0,one),top) = top,
inference(forward_demodulation,[status(thm)],[f1449,f54522]) ).
fof(f54528,plain,
! [X0] : zero = composition(converse(zero),X0),
inference(forward_demodulation,[status(thm)],[f1961,f54467]) ).
fof(f54560,plain,
! [X0] : meet(converse(X0),converse(complement(X0))) = zero,
inference(backward_demodulation,[status(thm)],[f54576,f50042]) ).
fof(f54576,plain,
! [X0] : zero = composition(zero,X0),
inference(forward_demodulation,[status(thm)],[f1961,f54528]) ).
fof(f54704,plain,
! [X0] : composition(join(converse(X0),one),complement(zero)) = complement(zero),
inference(forward_demodulation,[status(thm)],[f963,f54496]) ).
fof(f54705,plain,
! [X0] : composition(join(one,converse(X0)),complement(zero)) = complement(zero),
inference(forward_demodulation,[status(thm)],[f141,f54704]) ).
fof(f54706,plain,
! [X0] : composition(converse(join(X0,one)),complement(zero)) = complement(zero),
inference(forward_demodulation,[status(thm)],[f1055,f54705]) ).
fof(f54707,plain,
! [X0] : composition(converse(join(X0,one)),top) = complement(zero),
inference(forward_demodulation,[status(thm)],[f1449,f54706]) ).
fof(f54708,plain,
! [X0] : converse(composition(top,join(X0,one))) = complement(zero),
inference(forward_demodulation,[status(thm)],[f2277,f54707]) ).
fof(f54709,plain,
! [X0] : converse(composition(top,join(X0,one))) = top,
inference(forward_demodulation,[status(thm)],[f1449,f54708]) ).
fof(f54979,plain,
composition(top,top) = top,
inference(paramodulation,[status(thm)],[f1148,f54526]) ).
fof(f55267,plain,
! [X0] : composition(top,composition(top,X0)) = composition(top,X0),
inference(paramodulation,[status(thm)],[f54979,f24]) ).
fof(f56576,plain,
! [X0] : meet(X0,converse(complement(converse(X0)))) = zero,
inference(paramodulation,[status(thm)],[f27,f54560]) ).
fof(f56620,plain,
! [X0] : converse(X0) = join(zero,meet(complement(converse(complement(X0))),converse(X0))),
inference(paramodulation,[status(thm)],[f54560,f2954]) ).
fof(f56677,plain,
! [X0] : converse(X0) = meet(complement(converse(complement(X0))),converse(X0)),
inference(forward_demodulation,[status(thm)],[f1451,f56620]) ).
fof(f56678,plain,
! [X0] : converse(X0) = meet(converse(X0),complement(converse(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f76,f56677]) ).
fof(f57005,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = join(X0,zero),
inference(paramodulation,[status(thm)],[f56576,f6265]) ).
fof(f57070,plain,
! [X0] : join(X0,converse(complement(converse(complement(X0))))) = X0,
inference(forward_demodulation,[status(thm)],[f1532,f57005]) ).
fof(f59370,plain,
! [X0,X1] : composition(top,join(X0,one)) = join(composition(top,join(X0,one)),converse(meet(top,X1))),
inference(paramodulation,[status(thm)],[f54709,f6566]) ).
fof(f59385,plain,
! [X0,X1] : converse(join(top,X0)) = join(composition(top,join(X1,one)),converse(X0)),
inference(paramodulation,[status(thm)],[f54709,f115]) ).
fof(f59492,plain,
! [X0,X1] : composition(top,join(X0,one)) = join(composition(top,join(X0,one)),converse(X1)),
inference(forward_demodulation,[status(thm)],[f1500,f59370]) ).
fof(f59516,plain,
! [X0,X1] : converse(top) = join(composition(top,join(X0,one)),converse(X1)),
inference(forward_demodulation,[status(thm)],[f1148,f59385]) ).
fof(f59517,plain,
! [X0,X1] : top = join(composition(top,join(X0,one)),converse(X1)),
inference(forward_demodulation,[status(thm)],[f2181,f59516]) ).
fof(f59537,plain,
! [X0] : top = composition(top,join(X0,one)),
inference(forward_demodulation,[status(thm)],[f59492,f59517]) ).
fof(f59575,plain,
! [X0,X1] : top = composition(top,join(X0,join(X1,one))),
inference(paramodulation,[status(thm)],[f21,f59537]) ).
fof(f63255,plain,
! [X0] : converse(converse(complement(converse(complement(X0))))) = meet(converse(converse(complement(converse(complement(X0))))),converse(X0)),
inference(paramodulation,[status(thm)],[f57070,f2155]) ).
fof(f63344,plain,
! [X0] : complement(converse(complement(X0))) = meet(converse(converse(complement(converse(complement(X0))))),converse(X0)),
inference(forward_demodulation,[status(thm)],[f27,f63255]) ).
fof(f63345,plain,
! [X0] : complement(converse(complement(X0))) = meet(converse(X0),converse(converse(complement(converse(complement(X0)))))),
inference(forward_demodulation,[status(thm)],[f76,f63344]) ).
fof(f63346,plain,
! [X0] : complement(converse(complement(X0))) = meet(converse(X0),complement(converse(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f27,f63345]) ).
fof(f63375,plain,
! [X0] : complement(converse(complement(X0))) = converse(X0),
inference(forward_demodulation,[status(thm)],[f56678,f63346]) ).
fof(f63464,plain,
! [X0] : complement(converse(X0)) = converse(complement(X0)),
inference(paramodulation,[status(thm)],[f1423,f63375]) ).
fof(f104751,plain,
! [X0] : join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0)))) = complement(composition(top,X0)),
inference(paramodulation,[status(thm)],[f55267,f44]) ).
fof(f104979,plain,
! [X0] : composition(join(converse(top),one),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f963,f104751]) ).
fof(f104980,plain,
! [X0] : composition(join(one,converse(top)),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f141,f104979]) ).
fof(f104981,plain,
! [X0] : composition(converse(join(top,one)),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f1055,f104980]) ).
fof(f104982,plain,
! [X0] : composition(converse(top),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f1148,f104981]) ).
fof(f104987,plain,
! [X0] : composition(top,complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f2181,f104982]) ).
fof(f105251,plain,
! [X0,X1,X2] : join(complement(X0),composition(converse(top),complement(composition(top,composition(join(X1,join(X2,one)),X0))))) = complement(X0),
inference(paramodulation,[status(thm)],[f59575,f463]) ).
fof(f105262,plain,
! [X0,X1,X2] : composition(top,composition(join(X0,join(X1,one)),X2)) = composition(top,X2),
inference(paramodulation,[status(thm)],[f59575,f24]) ).
fof(f105494,plain,
! [X0,X1,X2] : join(complement(X0),composition(top,complement(composition(top,composition(join(X1,join(X2,one)),X0))))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f2181,f105251]) ).
fof(f105495,plain,
! [X0,X1,X2] : join(complement(X0),complement(composition(top,composition(join(X1,join(X2,one)),X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f104987,f105494]) ).
fof(f105496,plain,
! [X0,X1,X2] : complement(meet(X0,composition(top,composition(join(X1,join(X2,one)),X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1425,f105495]) ).
fof(f105525,plain,
! [X0] : complement(meet(X0,composition(top,X0))) = complement(X0),
inference(backward_demodulation,[status(thm)],[f105262,f105496]) ).
fof(f110768,plain,
! [X0] : meet(X0,composition(top,X0)) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f105525,f1423]) ).
fof(f110833,plain,
! [X0] : meet(X0,composition(top,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1423,f110768]) ).
fof(f110909,plain,
! [X0] : join(X0,composition(top,complement(X0))) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f110833,f6265]) ).
fof(f111053,plain,
! [X0] : join(X0,composition(top,complement(X0))) = top,
inference(forward_demodulation,[status(thm)],[f31,f110909]) ).
fof(f111567,plain,
! [X0] : converse(top) = join(X0,converse(composition(top,complement(converse(X0))))),
inference(paramodulation,[status(thm)],[f111053,f115]) ).
fof(f111712,plain,
! [X0] : top = join(X0,converse(composition(top,complement(converse(X0))))),
inference(forward_demodulation,[status(thm)],[f2181,f111567]) ).
fof(f111713,plain,
! [X0] : top = join(X0,converse(composition(top,converse(complement(X0))))),
inference(forward_demodulation,[status(thm)],[f63464,f111712]) ).
fof(f111714,plain,
! [X0] : top = join(X0,composition(complement(X0),converse(top))),
inference(forward_demodulation,[status(thm)],[f197,f111713]) ).
fof(f111718,plain,
! [X0] : top = join(X0,composition(complement(X0),top)),
inference(forward_demodulation,[status(thm)],[f2181,f111714]) ).
fof(f113907,plain,
! [X0] : complement(top) = meet(X0,complement(composition(complement(complement(X0)),top))),
inference(paramodulation,[status(thm)],[f111718,f39186]) ).
fof(f114068,plain,
! [X0] : zero = meet(X0,complement(composition(complement(complement(X0)),top))),
inference(forward_demodulation,[status(thm)],[f72,f113907]) ).
fof(f114069,plain,
! [X0] : zero = meet(X0,complement(composition(X0,top))),
inference(forward_demodulation,[status(thm)],[f1423,f114068]) ).
fof(f114611,plain,
! [X0] : join(composition(X0,top),X0) = join(composition(X0,top),zero),
inference(paramodulation,[status(thm)],[f114069,f6274]) ).
fof(f114754,plain,
! [X0] : join(X0,composition(X0,top)) = join(composition(X0,top),zero),
inference(forward_demodulation,[status(thm)],[f20,f114611]) ).
fof(f114756,plain,
composition(complement(sk2),top) = complement(sk2),
inference(backward_demodulation,[status(thm)],[f114758,f2775]) ).
fof(f114758,plain,
! [X0] : join(X0,composition(X0,top)) = composition(X0,top),
inference(forward_demodulation,[status(thm)],[f1532,f114754]) ).
fof(f117308,plain,
composition(join(sk1,complement(sk2)),top) = join(sk1,complement(sk2)),
inference(paramodulation,[status(thm)],[f114756,f129]) ).
fof(f117310,plain,
composition(join(sF1_fnc,complement(sk2)),top) = join(sF0_fnc,complement(sk2)),
inference(paramodulation,[status(thm)],[f114756,f127]) ).
fof(f117349,plain,
composition(join(sF1_fnc,complement(sk2)),top) = join(sk1,complement(sk2)),
inference(forward_demodulation,[status(thm)],[f14225,f117308]) ).
fof(f117350,plain,
composition(join(sF1_fnc,complement(sk2)),top) = join(sF1_fnc,complement(sk2)),
inference(forward_demodulation,[status(thm)],[f14225,f117349]) ).
fof(f117353,plain,
complement(sF0_fnc) = complement(meet(sk2,join(sF1_fnc,complement(sk2)))),
inference(backward_demodulation,[status(thm)],[f117354,f48569]) ).
fof(f117354,plain,
join(sF1_fnc,complement(sk2)) = join(sF0_fnc,complement(sk2)),
inference(forward_demodulation,[status(thm)],[f117350,f117310]) ).
fof(f117569,plain,
complement(sF0_fnc) = complement(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f47467,f117353]) ).
fof(f117686,plain,
sF0_fnc = complement(complement(sF1_fnc)),
inference(paramodulation,[status(thm)],[f117569,f1423]) ).
fof(f117759,plain,
sF0_fnc = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f1423,f117686]) ).
fof(f117760,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f117759,f41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : REL019-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Mon Sep 21 04:00:36 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 204.96/26.11 % Refutation found
% 204.96/26.11 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 204.96/26.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.05/27.47 % Elapsed time: 27.163972 seconds
% 15.05/27.47 % CPU time: 209.965446 seconds
% 15.05/27.47 % Total memory used: 1.775 GB
% 15.05/27.47 % Net memory used: 1.639 GB
%------------------------------------------------------------------------------