%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:21 PM UTC 2026
% Result : Unsatisfiable 122.20s 16.00s
% Output : CNFRefutation 42.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 20
% Syntax : Number of formulae : 283 ( 283 unt; 2 def)
% Number of atoms : 283 ( 282 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 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 : 201 ( 201 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : join(A,B) = join(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : composition(A,one) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : converse(converse(A)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : top = join(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : zero = meet(A,complement(A)),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B,C] : join(meet(composition(A,B),C),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
join(sk2,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
composition(sk1,sk2) != meet(sk1,sk2),
file('/export/starexec/sandbox/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(f34,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(f36,plain,
join(sk1,one) = one,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f37,plain,
join(sk2,one) = one,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f38,plain,
composition(sk1,sk2) != meet(sk1,sk2),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f39,definition,
sF0_fnc = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f40,definition,
sF1_fnc = meet(sk1,sk2),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f41,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f38,f40,f39]) ).
fof(f42,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f23,f22]) ).
fof(f57,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f27,f29]) ).
fof(f61,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(paramodulation,[status(thm)],[f27,f28]) ).
fof(f62,plain,
! [X0,X1] : join(converse(X0),converse(X1)) = converse(join(X1,X0)),
inference(paramodulation,[status(thm)],[f28,f20]) ).
fof(f68,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f25,f24]) ).
fof(f72,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f31,f23]) ).
fof(f73,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f20,f23]) ).
fof(f80,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f32,f72]) ).
fof(f85,plain,
! [X0,X1] : join(meet(X0,X1),meet(composition(X0,meet(one,composition(converse(X0),X1))),X1)) = meet(composition(X0,meet(one,composition(converse(X0),X1))),X1),
inference(paramodulation,[status(thm)],[f25,f34]) ).
fof(f158,plain,
! [X0,X1] : join(converse(X0),X1) = converse(join(converse(X1),X0)),
inference(paramodulation,[status(thm)],[f27,f62]) ).
fof(f229,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X1,X2),composition(X0,X2)),
inference(paramodulation,[status(thm)],[f20,f26]) ).
fof(f233,plain,
! [X0] : composition(join(sk1,X0),sk2) = join(sF0_fnc,composition(X0,sk2)),
inference(paramodulation,[status(thm)],[f39,f26]) ).
fof(f255,plain,
! [X0] : meet(complement(X0),X0) = complement(top),
inference(paramodulation,[status(thm)],[f31,f73]) ).
fof(f264,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f73,f23]) ).
fof(f270,plain,
! [X0] : meet(complement(X0),X0) = zero,
inference(forward_demodulation,[status(thm)],[f80,f255]) ).
fof(f336,plain,
! [X0] : join(meet(sF0_fnc,X0),composition(meet(sk1,composition(X0,converse(sk2))),meet(sk2,composition(converse(sk1),X0)))) = composition(meet(sk1,composition(X0,converse(sk2))),meet(sk2,composition(converse(sk1),X0))),
inference(paramodulation,[status(thm)],[f39,f33]) ).
fof(f338,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1))),
inference(paramodulation,[status(thm)],[f25,f33]) ).
fof(f352,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),composition(meet(X0,composition(one,converse(X1))),meet(X1,converse(X0)))) = composition(meet(X0,composition(one,converse(X1))),meet(X1,composition(converse(X0),one))),
inference(paramodulation,[status(thm)],[f25,f33]) ).
fof(f371,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),composition(meet(X0,composition(one,converse(X1))),meet(X1,converse(X0)))) = composition(meet(X0,composition(one,converse(X1))),meet(X1,converse(X0))),
inference(forward_demodulation,[status(thm)],[f25,f352]) ).
fof(f423,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f31,f21]) ).
fof(f439,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f25,f57]) ).
fof(f462,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f27,f439]) ).
fof(f486,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f68,f462]) ).
fof(f487,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f25,f462]) ).
fof(f502,plain,
! [X0] : join(composition(converse(converse(one)),complement(X0)),complement(X0)) = complement(X0),
inference(paramodulation,[status(thm)],[f462,f30]) ).
fof(f504,plain,
! [X0,X1] : join(meet(X0,X1),meet(composition(converse(one),meet(X0,composition(converse(converse(one)),X1))),X1)) = meet(composition(converse(one),meet(X0,composition(converse(converse(one)),X1))),X1),
inference(paramodulation,[status(thm)],[f462,f34]) ).
fof(f512,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),composition(meet(X0,composition(one,converse(X1))),meet(X1,converse(X0)))) = composition(meet(X0,converse(X1)),meet(X1,converse(X0))),
inference(backward_demodulation,[status(thm)],[f520,f371]) ).
fof(f520,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f462,f486]) ).
fof(f521,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,composition(converse(converse(one)),X1)),X1)) = meet(composition(converse(one),meet(X0,composition(converse(converse(one)),X1))),X1),
inference(forward_demodulation,[status(thm)],[f462,f504]) ).
fof(f522,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,composition(one,X1)),X1)) = meet(composition(converse(one),meet(X0,composition(converse(converse(one)),X1))),X1),
inference(forward_demodulation,[status(thm)],[f27,f521]) ).
fof(f523,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,X1),X1)) = meet(composition(converse(one),meet(X0,composition(converse(converse(one)),X1))),X1),
inference(forward_demodulation,[status(thm)],[f520,f522]) ).
fof(f524,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,X1),X1)) = meet(meet(X0,composition(converse(converse(one)),X1)),X1),
inference(forward_demodulation,[status(thm)],[f462,f523]) ).
fof(f525,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,X1),X1)) = meet(meet(X0,composition(one,X1)),X1),
inference(forward_demodulation,[status(thm)],[f27,f524]) ).
fof(f526,plain,
! [X0,X1] : join(meet(X0,X1),meet(meet(X0,X1),X1)) = meet(meet(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f520,f525]) ).
fof(f532,plain,
! [X0,X1] : join(meet(composition(X0,X1),one),composition(meet(X0,converse(X1)),meet(X1,converse(X0)))) = composition(meet(X0,converse(X1)),meet(X1,converse(X0))),
inference(forward_demodulation,[status(thm)],[f520,f512]) ).
fof(f539,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,composition(X1,converse(one))),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))),
inference(backward_demodulation,[status(thm)],[f487,f338]) ).
fof(f547,plain,
! [X0] : join(composition(one,complement(X0)),complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f27,f502]) ).
fof(f548,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f520,f547]) ).
fof(f567,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f487,f539]) ).
fof(f568,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,composition(X1,one)),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f25,f567]) ).
fof(f569,plain,
! [X0,X1] : join(meet(X0,X1),composition(meet(X0,X1),meet(one,composition(converse(X0),X1)))) = composition(meet(X0,X1),meet(one,composition(converse(X0),X1))),
inference(forward_demodulation,[status(thm)],[f25,f568]) ).
fof(f700,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f548,f73]) ).
fof(f702,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f548,f42]) ).
fof(f721,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f32,f702]) ).
fof(f828,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f700,f548]) ).
fof(f832,plain,
! [X0] : meet(meet(X0,X0),complement(X0)) = zero,
inference(paramodulation,[status(thm)],[f700,f270]) ).
fof(f839,plain,
! [X0] : top = join(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f700,f31]) ).
fof(f871,plain,
! [X0] : meet(X0,X0) = join(zero,complement(join(complement(meet(X0,X0)),complement(X0)))),
inference(paramodulation,[status(thm)],[f832,f42]) ).
fof(f877,plain,
! [X0] : meet(X0,X0) = join(zero,meet(X0,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f73,f871]) ).
fof(f900,plain,
! [X0] : X0 = join(meet(X0,meet(X0,X0)),complement(top)),
inference(paramodulation,[status(thm)],[f839,f42]) ).
fof(f901,plain,
! [X0,X1] : join(complement(X0),join(meet(X0,X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f839,f21]) ).
fof(f902,plain,
! [X0] : X0 = join(meet(X0,meet(X0,X0)),zero),
inference(forward_demodulation,[status(thm)],[f80,f900]) ).
fof(f905,plain,
! [X0] : X0 = join(zero,meet(X0,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f20,f902]) ).
fof(f912,plain,
! [X0] : meet(X0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f905,f877]) ).
fof(f915,plain,
! [X0] : X0 = join(meet(X0,X0),zero),
inference(backward_demodulation,[status(thm)],[f912,f902]) ).
fof(f937,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(backward_demodulation,[status(thm)],[f912,f905]) ).
fof(f939,plain,
! [X0,X1] : join(complement(X0),join(X0,X1)) = join(top,X1),
inference(backward_demodulation,[status(thm)],[f912,f901]) ).
fof(f942,plain,
! [X0] : join(X0,complement(complement(X0))) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f912,f828]) ).
fof(f974,plain,
! [X0] : X0 = join(X0,zero),
inference(forward_demodulation,[status(thm)],[f912,f915]) ).
fof(f976,plain,
! [X0] : X0 = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f999,f721]) ).
fof(f999,plain,
! [X0] : X0 = join(zero,X0),
inference(forward_demodulation,[status(thm)],[f912,f937]) ).
fof(f1082,plain,
! [X0] : join(X0,X0) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f976,f942]) ).
fof(f1086,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f976,f1082]) ).
fof(f1236,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f1086,f21]) ).
fof(f1734,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f42,f1236]) ).
fof(f1745,plain,
! [X0] : join(X0,top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f31,f1236]) ).
fof(f1747,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f20,f1236]) ).
fof(f1765,plain,
! [X0,X1] : join(meet(X0,X1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f42,f1734]) ).
fof(f1781,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f31,f1745]) ).
fof(f1809,plain,
! [X0] : top = join(top,X0),
inference(paramodulation,[status(thm)],[f1781,f20]) ).
fof(f1815,plain,
! [X0,X1] : join(complement(X0),join(X0,X1)) = top,
inference(backward_demodulation,[status(thm)],[f1809,f939]) ).
fof(f1816,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = top,
inference(backward_demodulation,[status(thm)],[f1809,f423]) ).
fof(f1934,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f20,f1765]) ).
fof(f1938,plain,
join(sF1_fnc,sk1) = sk1,
inference(paramodulation,[status(thm)],[f40,f1765]) ).
fof(f1943,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(paramodulation,[status(thm)],[f264,f1765]) ).
fof(f1947,plain,
! [X0,X1] : converse(converse(X0)) = join(converse(meet(converse(X0),X1)),X0),
inference(paramodulation,[status(thm)],[f1765,f61]) ).
fof(f1953,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f1934,f526]) ).
fof(f1956,plain,
! [X0,X1] : X0 = join(converse(meet(converse(X0),X1)),X0),
inference(forward_demodulation,[status(thm)],[f27,f1947]) ).
fof(f2249,plain,
join(sF1_fnc,sk2) = sk2,
inference(paramodulation,[status(thm)],[f40,f1943]) ).
fof(f2468,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(complement(X0)),X1)),complement(top)),
inference(paramodulation,[status(thm)],[f1816,f42]) ).
fof(f2479,plain,
! [X0,X1] : X0 = join(meet(X0,join(X0,X1)),complement(top)),
inference(forward_demodulation,[status(thm)],[f976,f2468]) ).
fof(f2480,plain,
! [X0,X1] : X0 = join(meet(X0,join(X0,X1)),zero),
inference(forward_demodulation,[status(thm)],[f80,f2479]) ).
fof(f2481,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f974,f2480]) ).
fof(f2485,plain,
sF1_fnc = meet(sF1_fnc,sk1),
inference(paramodulation,[status(thm)],[f1938,f2481]) ).
fof(f2508,plain,
sk2 = meet(sk2,one),
inference(paramodulation,[status(thm)],[f37,f2481]) ).
fof(f2510,plain,
sk1 = meet(sk1,one),
inference(paramodulation,[status(thm)],[f36,f2481]) ).
fof(f2539,plain,
sk2 = meet(one,sk2),
inference(paramodulation,[status(thm)],[f264,f2508]) ).
fof(f2645,plain,
sk1 = meet(one,sk1),
inference(paramodulation,[status(thm)],[f2510,f264]) ).
fof(f3061,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f264,f1953]) ).
fof(f3081,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X1,X0),X1),
inference(paramodulation,[status(thm)],[f264,f1953]) ).
fof(f3372,plain,
join(complement(sF1_fnc),sk2) = top,
inference(paramodulation,[status(thm)],[f2249,f1815]) ).
fof(f3452,plain,
! [X0] : join(complement(sF1_fnc),join(sk2,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f3372,f21]) ).
fof(f3458,plain,
! [X0] : join(complement(sF1_fnc),join(sk2,X0)) = top,
inference(forward_demodulation,[status(thm)],[f1809,f3452]) ).
fof(f3684,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),X0),
inference(paramodulation,[status(thm)],[f2481,f3061]) ).
fof(f3713,plain,
! [X0,X1] : X0 = meet(join(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f2481,f3684]) ).
fof(f3974,plain,
meet(sk2,sk1) = meet(sF1_fnc,sk1),
inference(paramodulation,[status(thm)],[f40,f3081]) ).
fof(f4031,plain,
meet(sk2,sk1) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f2485,f3974]) ).
fof(f5552,plain,
! [X0] : one = join(converse(meet(one,X0)),one),
inference(paramodulation,[status(thm)],[f487,f1956]) ).
fof(f7781,plain,
join(complement(sF1_fnc),one) = top,
inference(paramodulation,[status(thm)],[f37,f3458]) ).
fof(f7926,plain,
sF1_fnc = join(meet(sF1_fnc,one),complement(top)),
inference(paramodulation,[status(thm)],[f7781,f42]) ).
fof(f7946,plain,
sF1_fnc = join(meet(sF1_fnc,one),zero),
inference(forward_demodulation,[status(thm)],[f80,f7926]) ).
fof(f7947,plain,
sF1_fnc = meet(sF1_fnc,one),
inference(forward_demodulation,[status(thm)],[f974,f7946]) ).
fof(f7962,plain,
meet(sF1_fnc,one) = meet(one,sF1_fnc),
inference(paramodulation,[status(thm)],[f7947,f3061]) ).
fof(f7968,plain,
join(sF1_fnc,one) = one,
inference(paramodulation,[status(thm)],[f7947,f1943]) ).
fof(f7974,plain,
sF1_fnc = meet(one,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f7947,f7962]) ).
fof(f8376,plain,
! [X0,X1] : composition(join(X0,one),X1) = join(X1,composition(X0,X1)),
inference(paramodulation,[status(thm)],[f520,f229]) ).
fof(f8912,plain,
composition(join(sk1,one),sk2) = join(sF0_fnc,sk2),
inference(paramodulation,[status(thm)],[f520,f233]) ).
fof(f8926,plain,
composition(one,sk2) = join(sF0_fnc,sk2),
inference(forward_demodulation,[status(thm)],[f36,f8912]) ).
fof(f8927,plain,
sk2 = join(sF0_fnc,sk2),
inference(forward_demodulation,[status(thm)],[f520,f8926]) ).
fof(f8949,plain,
sF0_fnc = meet(sk2,sF0_fnc),
inference(paramodulation,[status(thm)],[f8927,f3713]) ).
fof(f8950,plain,
join(complement(sF0_fnc),sk2) = top,
inference(paramodulation,[status(thm)],[f8927,f1815]) ).
fof(f8952,plain,
sF0_fnc = meet(sF0_fnc,sk2),
inference(paramodulation,[status(thm)],[f8927,f2481]) ).
fof(f9219,plain,
! [X0] : join(complement(sF0_fnc),join(sk2,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f8950,f21]) ).
fof(f9223,plain,
! [X0] : join(complement(sF0_fnc),join(sk2,X0)) = top,
inference(forward_demodulation,[status(thm)],[f1809,f9219]) ).
fof(f10005,plain,
one = join(converse(sk1),one),
inference(paramodulation,[status(thm)],[f2645,f5552]) ).
fof(f10006,plain,
one = join(converse(sk2),one),
inference(paramodulation,[status(thm)],[f2539,f5552]) ).
fof(f10065,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(paramodulation,[status(thm)],[f10005,f3713]) ).
fof(f10068,plain,
converse(sk1) = meet(converse(sk1),one),
inference(paramodulation,[status(thm)],[f10005,f2481]) ).
fof(f10119,plain,
converse(sk2) = meet(one,converse(sk2)),
inference(paramodulation,[status(thm)],[f10006,f3713]) ).
fof(f10122,plain,
converse(sk2) = meet(converse(sk2),one),
inference(paramodulation,[status(thm)],[f10006,f2481]) ).
fof(f10634,plain,
join(converse(sk1),meet(composition(converse(sk1),meet(one,composition(converse(converse(sk1)),one))),one)) = meet(composition(converse(sk1),meet(one,composition(converse(converse(sk1)),one))),one),
inference(paramodulation,[status(thm)],[f10068,f85]) ).
fof(f10642,plain,
join(converse(sk1),meet(composition(converse(sk1),meet(one,converse(converse(sk1)))),one)) = meet(composition(converse(sk1),meet(one,composition(converse(converse(sk1)),one))),one),
inference(forward_demodulation,[status(thm)],[f25,f10634]) ).
fof(f10643,plain,
join(converse(sk1),meet(composition(converse(sk1),meet(one,sk1)),one)) = meet(composition(converse(sk1),meet(one,composition(converse(converse(sk1)),one))),one),
inference(forward_demodulation,[status(thm)],[f27,f10642]) ).
fof(f10644,plain,
join(converse(sk1),meet(composition(converse(sk1),sk1),one)) = meet(composition(converse(sk1),meet(one,composition(converse(converse(sk1)),one))),one),
inference(forward_demodulation,[status(thm)],[f2645,f10643]) ).
fof(f10645,plain,
join(converse(sk1),meet(composition(converse(sk1),sk1),one)) = meet(composition(converse(sk1),meet(one,converse(converse(sk1)))),one),
inference(forward_demodulation,[status(thm)],[f25,f10644]) ).
fof(f10646,plain,
join(converse(sk1),meet(composition(converse(sk1),sk1),one)) = meet(composition(converse(sk1),meet(one,sk1)),one),
inference(forward_demodulation,[status(thm)],[f27,f10645]) ).
fof(f10647,plain,
join(converse(sk1),meet(composition(converse(sk1),sk1),one)) = meet(composition(converse(sk1),sk1),one),
inference(forward_demodulation,[status(thm)],[f2645,f10646]) ).
fof(f11070,plain,
join(converse(sk2),meet(composition(converse(sk2),meet(one,composition(converse(converse(sk2)),one))),one)) = meet(composition(converse(sk2),meet(one,composition(converse(converse(sk2)),one))),one),
inference(paramodulation,[status(thm)],[f10122,f85]) ).
fof(f11082,plain,
join(converse(sk2),meet(composition(converse(sk2),meet(one,converse(converse(sk2)))),one)) = meet(composition(converse(sk2),meet(one,composition(converse(converse(sk2)),one))),one),
inference(forward_demodulation,[status(thm)],[f25,f11070]) ).
fof(f11083,plain,
join(converse(sk2),meet(composition(converse(sk2),meet(one,sk2)),one)) = meet(composition(converse(sk2),meet(one,composition(converse(converse(sk2)),one))),one),
inference(forward_demodulation,[status(thm)],[f27,f11082]) ).
fof(f11084,plain,
join(converse(sk2),meet(composition(converse(sk2),sk2),one)) = meet(composition(converse(sk2),meet(one,composition(converse(converse(sk2)),one))),one),
inference(forward_demodulation,[status(thm)],[f2539,f11083]) ).
fof(f11085,plain,
join(converse(sk2),meet(composition(converse(sk2),sk2),one)) = meet(composition(converse(sk2),meet(one,converse(converse(sk2)))),one),
inference(forward_demodulation,[status(thm)],[f25,f11084]) ).
fof(f11086,plain,
join(converse(sk2),meet(composition(converse(sk2),sk2),one)) = meet(composition(converse(sk2),meet(one,sk2)),one),
inference(forward_demodulation,[status(thm)],[f27,f11085]) ).
fof(f11087,plain,
join(converse(sk2),meet(composition(converse(sk2),sk2),one)) = meet(composition(converse(sk2),sk2),one),
inference(forward_demodulation,[status(thm)],[f2539,f11086]) ).
fof(f11948,plain,
join(sF0_fnc,composition(meet(sk1,composition(sk2,converse(sk2))),meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,composition(sk2,converse(sk2))),meet(sk2,composition(converse(sk1),sk2))),
inference(paramodulation,[status(thm)],[f8952,f336]) ).
fof(f11969,plain,
join(meet(sF0_fnc,one),composition(meet(sk1,composition(one,converse(sk2))),meet(sk2,converse(sk1)))) = composition(meet(sk1,composition(one,converse(sk2))),meet(sk2,composition(converse(sk1),one))),
inference(paramodulation,[status(thm)],[f25,f336]) ).
fof(f11991,plain,
join(meet(sF0_fnc,one),composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1)))) = composition(meet(sk1,composition(one,converse(sk2))),meet(sk2,composition(converse(sk1),one))),
inference(forward_demodulation,[status(thm)],[f520,f11969]) ).
fof(f11992,plain,
join(meet(sF0_fnc,one),composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1)))) = composition(meet(sk1,converse(sk2)),meet(sk2,composition(converse(sk1),one))),
inference(forward_demodulation,[status(thm)],[f520,f11991]) ).
fof(f11993,plain,
join(meet(sF0_fnc,one),composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1)))) = composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1))),
inference(forward_demodulation,[status(thm)],[f25,f11992]) ).
fof(f13981,plain,
join(complement(sF0_fnc),one) = top,
inference(paramodulation,[status(thm)],[f37,f9223]) ).
fof(f14600,plain,
sF0_fnc = join(meet(sF0_fnc,one),complement(top)),
inference(paramodulation,[status(thm)],[f13981,f42]) ).
fof(f14627,plain,
sF0_fnc = join(meet(sF0_fnc,one),zero),
inference(forward_demodulation,[status(thm)],[f80,f14600]) ).
fof(f14628,plain,
join(sF0_fnc,composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1)))) = composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1))),
inference(backward_demodulation,[status(thm)],[f14631,f11993]) ).
fof(f14631,plain,
sF0_fnc = meet(sF0_fnc,one),
inference(forward_demodulation,[status(thm)],[f974,f14627]) ).
fof(f14666,plain,
sF0_fnc = meet(one,sF0_fnc),
inference(paramodulation,[status(thm)],[f14631,f264]) ).
fof(f23556,plain,
join(meet(composition(one,sk2),one),composition(converse(sk2),meet(sk2,converse(one)))) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(paramodulation,[status(thm)],[f10119,f532]) ).
fof(f23558,plain,
join(meet(composition(one,sk1),one),composition(converse(sk1),meet(sk1,converse(one)))) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(paramodulation,[status(thm)],[f10065,f532]) ).
fof(f23586,plain,
join(meet(composition(sk2,one),one),composition(meet(sk2,converse(one)),converse(sk2))) = composition(meet(sk2,converse(one)),meet(one,converse(sk2))),
inference(paramodulation,[status(thm)],[f10119,f532]) ).
fof(f23725,plain,
join(meet(sk2,one),composition(converse(sk2),meet(sk2,converse(one)))) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f520,f23556]) ).
fof(f23726,plain,
join(sk2,composition(converse(sk2),meet(sk2,converse(one)))) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f2508,f23725]) ).
fof(f23727,plain,
join(sk2,composition(converse(sk2),meet(sk2,one))) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f487,f23726]) ).
fof(f23728,plain,
join(sk2,composition(converse(sk2),sk2)) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f2508,f23727]) ).
fof(f23729,plain,
composition(join(converse(sk2),one),sk2) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f8376,f23728]) ).
fof(f23730,plain,
composition(one,sk2) = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f10006,f23729]) ).
fof(f23731,plain,
sk2 = composition(meet(one,converse(sk2)),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f520,f23730]) ).
fof(f23732,plain,
sk2 = composition(converse(sk2),meet(sk2,converse(one))),
inference(forward_demodulation,[status(thm)],[f10119,f23731]) ).
fof(f23733,plain,
sk2 = composition(converse(sk2),meet(sk2,one)),
inference(forward_demodulation,[status(thm)],[f487,f23732]) ).
fof(f23734,plain,
join(converse(sk2),meet(composition(converse(sk2),sk2),one)) = meet(sk2,one),
inference(backward_demodulation,[status(thm)],[f23735,f11087]) ).
fof(f23735,plain,
sk2 = composition(converse(sk2),sk2),
inference(forward_demodulation,[status(thm)],[f2508,f23733]) ).
fof(f23736,plain,
join(converse(sk2),meet(sk2,one)) = meet(sk2,one),
inference(forward_demodulation,[status(thm)],[f23735,f23734]) ).
fof(f23737,plain,
join(converse(sk2),sk2) = meet(sk2,one),
inference(forward_demodulation,[status(thm)],[f2508,f23736]) ).
fof(f23738,plain,
join(converse(sk2),sk2) = sk2,
inference(forward_demodulation,[status(thm)],[f2508,f23737]) ).
fof(f23772,plain,
join(meet(sk2,one),composition(meet(sk2,converse(one)),converse(sk2))) = composition(meet(sk2,converse(one)),meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f25,f23586]) ).
fof(f23773,plain,
join(sk2,composition(meet(sk2,converse(one)),converse(sk2))) = composition(meet(sk2,converse(one)),meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f2508,f23772]) ).
fof(f23774,plain,
join(sk2,composition(meet(sk2,one),converse(sk2))) = composition(meet(sk2,converse(one)),meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f487,f23773]) ).
fof(f23775,plain,
join(sk2,composition(sk2,converse(sk2))) = composition(meet(sk2,converse(one)),meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f2508,f23774]) ).
fof(f23776,plain,
join(sk2,composition(sk2,converse(sk2))) = composition(meet(sk2,one),meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f487,f23775]) ).
fof(f23777,plain,
join(sk2,composition(sk2,converse(sk2))) = composition(sk2,meet(one,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f2508,f23776]) ).
fof(f23778,plain,
join(sk2,composition(sk2,converse(sk2))) = composition(sk2,converse(sk2)),
inference(forward_demodulation,[status(thm)],[f10119,f23777]) ).
fof(f23786,plain,
join(meet(sk1,one),composition(converse(sk1),meet(sk1,converse(one)))) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f520,f23558]) ).
fof(f23787,plain,
join(sk1,composition(converse(sk1),meet(sk1,converse(one)))) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f2510,f23786]) ).
fof(f23788,plain,
join(sk1,composition(converse(sk1),meet(sk1,one))) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f487,f23787]) ).
fof(f23789,plain,
join(sk1,composition(converse(sk1),sk1)) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f2510,f23788]) ).
fof(f23790,plain,
composition(join(converse(sk1),one),sk1) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f8376,f23789]) ).
fof(f23791,plain,
composition(one,sk1) = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f10005,f23790]) ).
fof(f23792,plain,
sk1 = composition(meet(one,converse(sk1)),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f520,f23791]) ).
fof(f23793,plain,
sk1 = composition(converse(sk1),meet(sk1,converse(one))),
inference(forward_demodulation,[status(thm)],[f10065,f23792]) ).
fof(f23794,plain,
sk1 = composition(converse(sk1),meet(sk1,one)),
inference(forward_demodulation,[status(thm)],[f487,f23793]) ).
fof(f23795,plain,
join(converse(sk1),meet(composition(converse(sk1),sk1),one)) = meet(sk1,one),
inference(backward_demodulation,[status(thm)],[f23796,f10647]) ).
fof(f23796,plain,
sk1 = composition(converse(sk1),sk1),
inference(forward_demodulation,[status(thm)],[f2510,f23794]) ).
fof(f23819,plain,
join(converse(sk1),meet(sk1,one)) = meet(sk1,one),
inference(forward_demodulation,[status(thm)],[f23796,f23795]) ).
fof(f23820,plain,
join(converse(sk1),sk1) = meet(sk1,one),
inference(forward_demodulation,[status(thm)],[f2510,f23819]) ).
fof(f23821,plain,
join(converse(sk1),sk1) = sk1,
inference(forward_demodulation,[status(thm)],[f2510,f23820]) ).
fof(f24146,plain,
join(converse(sk2),sk2) = converse(sk2),
inference(paramodulation,[status(thm)],[f23738,f158]) ).
fof(f24193,plain,
join(sk2,composition(sk2,converse(sk2))) = composition(sk2,sk2),
inference(backward_demodulation,[status(thm)],[f24274,f23778]) ).
fof(f24218,plain,
join(sF0_fnc,composition(meet(sk1,converse(sk2)),meet(sk2,converse(sk1)))) = composition(meet(sk1,sk2),meet(sk2,converse(sk1))),
inference(backward_demodulation,[status(thm)],[f24274,f14628]) ).
fof(f24224,plain,
join(sF0_fnc,composition(meet(sk1,composition(sk2,converse(sk2))),meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,composition(sk2,sk2)),meet(sk2,composition(converse(sk1),sk2))),
inference(backward_demodulation,[status(thm)],[f24274,f11948]) ).
fof(f24274,plain,
sk2 = converse(sk2),
inference(forward_demodulation,[status(thm)],[f23738,f24146]) ).
fof(f24283,plain,
join(sk2,composition(sk2,sk2)) = composition(sk2,sk2),
inference(forward_demodulation,[status(thm)],[f24274,f24193]) ).
fof(f24284,plain,
composition(join(sk2,one),sk2) = composition(sk2,sk2),
inference(forward_demodulation,[status(thm)],[f8376,f24283]) ).
fof(f24285,plain,
composition(one,sk2) = composition(sk2,sk2),
inference(forward_demodulation,[status(thm)],[f37,f24284]) ).
fof(f24286,plain,
sk2 = composition(sk2,sk2),
inference(forward_demodulation,[status(thm)],[f520,f24285]) ).
fof(f24300,plain,
join(sF0_fnc,composition(meet(sk1,sk2),meet(sk2,converse(sk1)))) = composition(meet(sk1,sk2),meet(sk2,converse(sk1))),
inference(forward_demodulation,[status(thm)],[f24274,f24218]) ).
fof(f24301,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,converse(sk1)))) = composition(meet(sk1,sk2),meet(sk2,converse(sk1))),
inference(forward_demodulation,[status(thm)],[f40,f24300]) ).
fof(f24302,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,converse(sk1)))) = composition(sF1_fnc,meet(sk2,converse(sk1))),
inference(forward_demodulation,[status(thm)],[f40,f24301]) ).
fof(f24308,plain,
join(sF0_fnc,composition(meet(sk1,composition(sk2,sk2)),meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,composition(sk2,sk2)),meet(sk2,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f24274,f24224]) ).
fof(f24309,plain,
join(sF0_fnc,composition(meet(sk1,sk2),meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,composition(sk2,sk2)),meet(sk2,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f24286,f24308]) ).
fof(f24310,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,composition(sk2,sk2)),meet(sk2,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f40,f24309]) ).
fof(f24311,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,composition(converse(sk1),sk2)))) = composition(meet(sk1,sk2),meet(sk2,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f24286,f24310]) ).
fof(f24312,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,composition(converse(sk1),sk2)))) = composition(sF1_fnc,meet(sk2,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f40,f24311]) ).
fof(f24437,plain,
join(sF1_fnc,composition(meet(sk1,sk2),meet(one,composition(converse(sk1),sk2)))) = composition(meet(sk1,sk2),meet(one,composition(converse(sk1),sk2))),
inference(paramodulation,[status(thm)],[f40,f569]) ).
fof(f24486,plain,
join(meet(one,sF1_fnc),composition(sF1_fnc,meet(one,composition(converse(one),sF1_fnc)))) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(paramodulation,[status(thm)],[f7974,f569]) ).
fof(f24745,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(converse(sk1),sk2)))) = composition(meet(sk1,sk2),meet(one,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f40,f24437]) ).
fof(f24746,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(converse(sk1),sk2)))) = composition(sF1_fnc,meet(one,composition(converse(sk1),sk2))),
inference(forward_demodulation,[status(thm)],[f40,f24745]) ).
fof(f24953,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(converse(one),sF1_fnc)))) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f7974,f24486]) ).
fof(f24954,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(one,sF1_fnc)))) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f487,f24953]) ).
fof(f24955,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,sF1_fnc))) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f520,f24954]) ).
fof(f24956,plain,
join(sF1_fnc,composition(sF1_fnc,sF1_fnc)) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f7974,f24955]) ).
fof(f24957,plain,
composition(join(sF1_fnc,one),sF1_fnc) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f8376,f24956]) ).
fof(f24958,plain,
composition(one,sF1_fnc) = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f7968,f24957]) ).
fof(f24959,plain,
sF1_fnc = composition(meet(one,sF1_fnc),meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f520,f24958]) ).
fof(f24960,plain,
sF1_fnc = composition(sF1_fnc,meet(one,composition(converse(one),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f7974,f24959]) ).
fof(f24961,plain,
sF1_fnc = composition(sF1_fnc,meet(one,composition(one,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f487,f24960]) ).
fof(f24962,plain,
sF1_fnc = composition(sF1_fnc,meet(one,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f520,f24961]) ).
fof(f24964,plain,
sF1_fnc = composition(sF1_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f7974,f24962]) ).
fof(f26091,plain,
join(converse(sk1),sk1) = converse(sk1),
inference(paramodulation,[status(thm)],[f23821,f158]) ).
fof(f26173,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(converse(sk1),sk2)))) = composition(sF1_fnc,meet(one,composition(sk1,sk2))),
inference(backward_demodulation,[status(thm)],[f26287,f24746]) ).
fof(f26198,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,composition(converse(sk1),sk2)))) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(backward_demodulation,[status(thm)],[f26287,f24312]) ).
fof(f26199,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,converse(sk1)))) = composition(sF1_fnc,meet(sk2,sk1)),
inference(backward_demodulation,[status(thm)],[f26287,f24302]) ).
fof(f26287,plain,
sk1 = converse(sk1),
inference(forward_demodulation,[status(thm)],[f23821,f26091]) ).
fof(f26356,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,sk1))) = composition(sF1_fnc,meet(sk2,sk1)),
inference(forward_demodulation,[status(thm)],[f26287,f26199]) ).
fof(f26357,plain,
join(sF0_fnc,composition(sF1_fnc,sF1_fnc)) = composition(sF1_fnc,meet(sk2,sk1)),
inference(forward_demodulation,[status(thm)],[f4031,f26356]) ).
fof(f26358,plain,
join(sF0_fnc,sF1_fnc) = composition(sF1_fnc,meet(sk2,sk1)),
inference(forward_demodulation,[status(thm)],[f24964,f26357]) ).
fof(f26359,plain,
join(sF0_fnc,sF1_fnc) = composition(sF1_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f4031,f26358]) ).
fof(f26360,plain,
join(sF0_fnc,sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f24964,f26359]) ).
fof(f26362,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,composition(sk1,sk2)))) = composition(sF1_fnc,meet(one,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f26287,f26173]) ).
fof(f26363,plain,
join(sF1_fnc,composition(sF1_fnc,meet(one,sF0_fnc))) = composition(sF1_fnc,meet(one,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f39,f26362]) ).
fof(f26364,plain,
join(sF1_fnc,composition(sF1_fnc,sF0_fnc)) = composition(sF1_fnc,meet(one,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f14666,f26363]) ).
fof(f26365,plain,
join(sF1_fnc,composition(sF1_fnc,sF0_fnc)) = composition(sF1_fnc,meet(one,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f39,f26364]) ).
fof(f26366,plain,
join(sF1_fnc,composition(sF1_fnc,sF0_fnc)) = composition(sF1_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f14666,f26365]) ).
fof(f26424,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,composition(sk1,sk2)))) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f26287,f26198]) ).
fof(f26425,plain,
join(sF0_fnc,composition(sF1_fnc,meet(sk2,sF0_fnc))) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f39,f26424]) ).
fof(f26426,plain,
join(sF0_fnc,composition(sF1_fnc,sF0_fnc)) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f8949,f26425]) ).
fof(f26427,plain,
composition(join(sF1_fnc,one),sF0_fnc) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f8376,f26426]) ).
fof(f26428,plain,
composition(one,sF0_fnc) = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f7968,f26427]) ).
fof(f26429,plain,
sF0_fnc = composition(sF1_fnc,meet(sk2,composition(sk1,sk2))),
inference(forward_demodulation,[status(thm)],[f520,f26428]) ).
fof(f26430,plain,
sF0_fnc = composition(sF1_fnc,meet(sk2,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f39,f26429]) ).
fof(f26431,plain,
join(sF1_fnc,composition(sF1_fnc,sF0_fnc)) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f26432,f26366]) ).
fof(f26432,plain,
sF0_fnc = composition(sF1_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f8949,f26430]) ).
fof(f26488,plain,
join(sF1_fnc,sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f26432,f26431]) ).
fof(f26505,plain,
join(sF1_fnc,sF1_fnc) = join(sF1_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f26360,f1747]) ).
fof(f26514,plain,
sF1_fnc = join(sF1_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1086,f26505]) ).
fof(f26515,plain,
sF1_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f26488,f26514]) ).
fof(f26516,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f26515,f41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n020.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 04:03:33 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.43 % Drodi V4.1.1
% 122.20/16.00 % Refutation found
% 122.20/16.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 122.20/16.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.48/16.32 % Elapsed time: 15.894281 seconds
% 6.48/16.32 % CPU time: 124.098345 seconds
% 6.48/16.32 % Total memory used: 717.099 MB
% 6.48/16.32 % Net memory used: 672.354 MB
%------------------------------------------------------------------------------