%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL018-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:17 PM UTC 2026
% Result : Unsatisfiable 9.84s 2.03s
% Output : CNFRefutation 12.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 15
% Syntax : Number of formulae : 179 ( 179 unt; 0 def)
% Number of atoms : 179 ( 178 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 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/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,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
composition(complement(sk1),top) != complement(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f19,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f20,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f21,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f22,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f23,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f24,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f25,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f26,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f27,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f28,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f29,plain,
composition(sk1,top) = sk1,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f30,plain,
composition(complement(sk1),top) != complement(sk1),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f16,f18]) ).
fof(f35,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f19,f34]) ).
fof(f36,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f16,f26]) ).
fof(f37,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f16,f35]) ).
fof(f39,plain,
! [X0] : composition(sk1,composition(top,X0)) = composition(sk1,X0),
inference(paramodulation,[status(thm)],[f29,f20]) ).
fof(f45,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)],[f20,f22]) ).
fof(f49,plain,
! [X0,X1] : composition(join(X0,sk1),composition(top,X1)) = join(composition(X0,composition(top,X1)),composition(sk1,X1)),
inference(paramodulation,[status(thm)],[f39,f22]) ).
fof(f52,plain,
! [X0,X1] : composition(join(X0,sk1),composition(top,X1)) = composition(join(composition(X0,top),sk1),X1),
inference(forward_demodulation,[status(thm)],[f45,f49]) ).
fof(f53,plain,
! [X0,X1] : composition(join(X0,sk1),composition(top,X1)) = composition(join(sk1,composition(X0,top)),X1),
inference(forward_demodulation,[status(thm)],[f16,f52]) ).
fof(f56,plain,
! [X0] : X0 = join(meet(X0,complement(complement(X0))),complement(top)),
inference(paramodulation,[status(thm)],[f27,f37]) ).
fof(f57,plain,
! [X0] : X0 = join(complement(top),meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f56]) ).
fof(f283,plain,
! [X0,X1] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(paramodulation,[status(thm)],[f21,f20]) ).
fof(f297,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f37]) ).
fof(f298,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f297]) ).
fof(f301,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X1,X2),composition(X0,X2)),
inference(paramodulation,[status(thm)],[f22,f16]) ).
fof(f331,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = composition(join(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f22,f301]) ).
fof(f384,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f393,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f402,plain,
! [X0] : converse(top) = join(X0,converse(complement(converse(X0)))),
inference(paramodulation,[status(thm)],[f27,f384]) ).
fof(f420,plain,
! [X0] : meet(X0,complement(X0)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f19]) ).
fof(f421,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f425,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f37]) ).
fof(f434,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(backward_demodulation,[status(thm)],[f435,f57]) ).
fof(f435,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f28,f420]) ).
fof(f436,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f421]) ).
fof(f438,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f425]) ).
fof(f473,plain,
top = join(zero,meet(top,complement(zero))),
inference(paramodulation,[status(thm)],[f435,f434]) ).
fof(f479,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f492,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f515,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = complement(top),
inference(paramodulation,[status(thm)],[f435,f36]) ).
fof(f526,plain,
join(complement(top),composition(converse(sk1),complement(sk1))) = complement(top),
inference(paramodulation,[status(thm)],[f29,f36]) ).
fof(f531,plain,
! [X0] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = zero,
inference(forward_demodulation,[status(thm)],[f435,f515]) ).
fof(f540,plain,
join(zero,composition(converse(sk1),complement(sk1))) = complement(top),
inference(forward_demodulation,[status(thm)],[f435,f526]) ).
fof(f541,plain,
join(zero,composition(converse(sk1),complement(sk1))) = zero,
inference(forward_demodulation,[status(thm)],[f435,f540]) ).
fof(f671,plain,
! [X0] : join(zero,join(composition(converse(sk1),complement(sk1)),X0)) = join(zero,X0),
inference(paramodulation,[status(thm)],[f541,f17]) ).
fof(f675,plain,
! [X0] : join(zero,join(X0,composition(converse(sk1),complement(sk1)))) = join(zero,X0),
inference(paramodulation,[status(thm)],[f16,f671]) ).
fof(f802,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f436,f438]) ).
fof(f805,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f436,f438]) ).
fof(f807,plain,
! [X0] : X0 = join(meet(X0,top),meet(X0,zero)),
inference(paramodulation,[status(thm)],[f435,f438]) ).
fof(f816,plain,
! [X0] : X0 = join(meet(X0,top),meet(zero,X0)),
inference(paramodulation,[status(thm)],[f436,f807]) ).
fof(f825,plain,
complement(zero) = join(meet(complement(zero),top),zero),
inference(paramodulation,[status(thm)],[f28,f816]) ).
fof(f834,plain,
complement(zero) = join(zero,meet(complement(zero),top)),
inference(forward_demodulation,[status(thm)],[f16,f825]) ).
fof(f835,plain,
complement(zero) = join(zero,meet(top,complement(zero))),
inference(forward_demodulation,[status(thm)],[f436,f834]) ).
fof(f838,plain,
complement(zero) = top,
inference(forward_demodulation,[status(thm)],[f473,f835]) ).
fof(f945,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f436,f802]) ).
fof(f961,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f805]) ).
fof(f972,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f961]) ).
fof(f973,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f436,f972]) ).
fof(f984,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f434,f973]) ).
fof(f1085,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(X1)),
inference(paramodulation,[status(thm)],[f19,f984]) ).
fof(f1150,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f393]) ).
fof(f1165,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f1150]) ).
fof(f1181,plain,
! [X0] : composition(one,X0) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f283,f1165]) ).
fof(f1182,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f1165]) ).
fof(f1183,plain,
! [X0] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f1165,f36]) ).
fof(f1199,plain,
! [X0,X1] : composition(join(converse(one),X0),X1) = join(X1,composition(X0,X1)),
inference(paramodulation,[status(thm)],[f1165,f22]) ).
fof(f1205,plain,
! [X0] : composition(one,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1165,f1181]) ).
fof(f1208,plain,
! [X0] : complement(meet(X0,composition(one,X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1085,f1183]) ).
fof(f1209,plain,
! [X0] : complement(meet(X0,X0)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1205,f1208]) ).
fof(f1235,plain,
! [X0,X1] : composition(join(one,X0),X1) = join(X1,composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1182,f1199]) ).
fof(f1289,plain,
! [X0] : complement(complement(X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f1209,f984]) ).
fof(f1298,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f1307,f298]) ).
fof(f1307,plain,
! [X0] : X0 = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f984,f1289]) ).
fof(f1327,plain,
! [X0] : join(X0,composition(converse(sk1),complement(sk1))) = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f1298,f675]) ).
fof(f1328,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(backward_demodulation,[status(thm)],[f1298,f541]) ).
fof(f1335,plain,
! [X0] : composition(converse(X0),complement(composition(X0,top))) = zero,
inference(backward_demodulation,[status(thm)],[f1298,f531]) ).
fof(f1347,plain,
! [X0] : join(X0,composition(converse(sk1),complement(sk1))) = X0,
inference(forward_demodulation,[status(thm)],[f1298,f1327]) ).
fof(f1348,plain,
! [X0] : join(X0,zero) = X0,
inference(backward_demodulation,[status(thm)],[f1328,f1347]) ).
fof(f1365,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(zero)),
inference(paramodulation,[status(thm)],[f1348,f384]) ).
fof(f1373,plain,
! [X0] : X0 = join(X0,converse(zero)),
inference(forward_demodulation,[status(thm)],[f23,f1365]) ).
fof(f1451,plain,
zero = converse(zero),
inference(paramodulation,[status(thm)],[f1298,f1373]) ).
fof(f1609,plain,
converse(zero) = composition(converse(complement(sk1)),sk1),
inference(paramodulation,[status(thm)],[f1328,f393]) ).
fof(f1611,plain,
join(complement(complement(sk1)),composition(converse(converse(sk1)),complement(zero))) = complement(complement(sk1)),
inference(paramodulation,[status(thm)],[f1328,f36]) ).
fof(f1619,plain,
zero = composition(converse(complement(sk1)),sk1),
inference(forward_demodulation,[status(thm)],[f1451,f1609]) ).
fof(f1625,plain,
join(sk1,composition(converse(converse(sk1)),complement(zero))) = complement(complement(sk1)),
inference(forward_demodulation,[status(thm)],[f984,f1611]) ).
fof(f1626,plain,
join(sk1,composition(sk1,complement(zero))) = complement(complement(sk1)),
inference(forward_demodulation,[status(thm)],[f23,f1625]) ).
fof(f1627,plain,
join(sk1,composition(sk1,top)) = complement(complement(sk1)),
inference(forward_demodulation,[status(thm)],[f838,f1626]) ).
fof(f1628,plain,
join(sk1,sk1) = complement(complement(sk1)),
inference(forward_demodulation,[status(thm)],[f29,f1627]) ).
fof(f1634,plain,
join(sk1,sk1) = sk1,
inference(forward_demodulation,[status(thm)],[f984,f1628]) ).
fof(f1863,plain,
! [X0] : join(sk1,join(sk1,X0)) = join(sk1,X0),
inference(paramodulation,[status(thm)],[f1634,f17]) ).
fof(f1882,plain,
join(complement(sk1),composition(converse(converse(complement(sk1))),complement(zero))) = complement(sk1),
inference(paramodulation,[status(thm)],[f1619,f36]) ).
fof(f1896,plain,
join(complement(sk1),composition(complement(sk1),complement(zero))) = complement(sk1),
inference(forward_demodulation,[status(thm)],[f23,f1882]) ).
fof(f1897,plain,
join(complement(sk1),composition(complement(sk1),top)) = complement(sk1),
inference(forward_demodulation,[status(thm)],[f838,f1896]) ).
fof(f1957,plain,
join(sk1,top) = join(sk1,complement(sk1)),
inference(paramodulation,[status(thm)],[f27,f1863]) ).
fof(f1969,plain,
join(sk1,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f1957]) ).
fof(f2085,plain,
! [X0] : join(sk1,join(top,X0)) = join(top,X0),
inference(paramodulation,[status(thm)],[f1969,f17]) ).
fof(f2141,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(paramodulation,[status(thm)],[f984,f1085]) ).
fof(f2145,plain,
! [X0] : complement(meet(X0,zero)) = join(complement(X0),top),
inference(paramodulation,[status(thm)],[f838,f1085]) ).
fof(f2146,plain,
! [X0] : complement(meet(X0,top)) = join(complement(X0),zero),
inference(paramodulation,[status(thm)],[f435,f1085]) ).
fof(f2160,plain,
! [X0] : complement(meet(X0,zero)) = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f16,f2145]) ).
fof(f2162,plain,
! [X0] : complement(meet(X0,top)) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1348,f2146]) ).
fof(f2184,plain,
! [X0] : complement(complement(X0)) = meet(X0,top),
inference(paramodulation,[status(thm)],[f2162,f984]) ).
fof(f2210,plain,
! [X0] : X0 = meet(X0,top),
inference(forward_demodulation,[status(thm)],[f984,f2184]) ).
fof(f2692,plain,
join(sk1,converse(top)) = join(sk1,converse(complement(converse(sk1)))),
inference(paramodulation,[status(thm)],[f402,f1863]) ).
fof(f2711,plain,
join(sk1,converse(top)) = converse(top),
inference(forward_demodulation,[status(thm)],[f402,f2692]) ).
fof(f4060,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(complement(X0))),
inference(paramodulation,[status(thm)],[f1307,f2141]) ).
fof(f4098,plain,
! [X0] : X0 = join(X0,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f984,f4060]) ).
fof(f4103,plain,
! [X0] : X0 = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f984,f4098]) ).
fof(f4165,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(paramodulation,[status(thm)],[f4103,f479]) ).
fof(f4237,plain,
! [X0] : join(sk1,join(X0,top)) = join(top,X0),
inference(paramodulation,[status(thm)],[f16,f2085]) ).
fof(f4371,plain,
! [X0] : zero = meet(meet(X0,zero),join(top,complement(X0))),
inference(paramodulation,[status(thm)],[f2160,f28]) ).
fof(f4898,plain,
! [X0] : join(X0,converse(top)) = join(top,converse(complement(converse(complement(X0))))),
inference(paramodulation,[status(thm)],[f402,f492]) ).
fof(f4905,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(paramodulation,[status(thm)],[f4103,f492]) ).
fof(f4965,plain,
! [X0] : zero = meet(meet(X0,zero),top),
inference(backward_demodulation,[status(thm)],[f4978,f4371]) ).
fof(f4978,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[status(thm)],[f27,f4905]) ).
fof(f5039,plain,
! [X0] : zero = meet(X0,zero),
inference(forward_demodulation,[status(thm)],[f2210,f4965]) ).
fof(f5199,plain,
! [X0] : complement(zero) = join(X0,complement(zero)),
inference(paramodulation,[status(thm)],[f5039,f2141]) ).
fof(f5215,plain,
! [X0] : top = join(X0,complement(zero)),
inference(forward_demodulation,[status(thm)],[f838,f5199]) ).
fof(f5221,plain,
! [X0] : join(sk1,top) = join(top,X0),
inference(backward_demodulation,[status(thm)],[f5232,f4237]) ).
fof(f5232,plain,
! [X0] : top = join(X0,top),
inference(forward_demodulation,[status(thm)],[f838,f5215]) ).
fof(f5257,plain,
! [X0] : join(X0,converse(top)) = top,
inference(backward_demodulation,[status(thm)],[f5287,f4898]) ).
fof(f5287,plain,
! [X0] : top = join(top,X0),
inference(forward_demodulation,[status(thm)],[f1969,f5221]) ).
fof(f5304,plain,
top = converse(top),
inference(backward_demodulation,[status(thm)],[f5257,f2711]) ).
fof(f5417,plain,
composition(top,complement(composition(top,top))) = zero,
inference(paramodulation,[status(thm)],[f5304,f1335]) ).
fof(f5425,plain,
! [X0] : converse(composition(top,X0)) = composition(converse(X0),top),
inference(paramodulation,[status(thm)],[f5304,f393]) ).
fof(f5427,plain,
! [X0] : join(complement(X0),composition(top,complement(composition(top,X0)))) = complement(X0),
inference(paramodulation,[status(thm)],[f5304,f36]) ).
fof(f5915,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X0),X1)) = join(meet(complement(X0),X1),X1),
inference(paramodulation,[status(thm)],[f945,f4165]) ).
fof(f5983,plain,
! [X0,X1] : X0 = join(meet(complement(X1),X0),X0),
inference(forward_demodulation,[status(thm)],[f945,f5915]) ).
fof(f5984,plain,
! [X0,X1] : X0 = join(X0,meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f5983]) ).
fof(f6078,plain,
! [X0,X1] : X0 = join(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f984,f5984]) ).
fof(f6959,plain,
! [X0] : composition(join(X0,top),complement(composition(top,top))) = join(composition(X0,complement(composition(top,top))),zero),
inference(paramodulation,[status(thm)],[f5417,f22]) ).
fof(f7002,plain,
! [X0] : composition(top,complement(composition(top,top))) = join(composition(X0,complement(composition(top,top))),zero),
inference(forward_demodulation,[status(thm)],[f5232,f6959]) ).
fof(f7003,plain,
! [X0] : zero = join(composition(X0,complement(composition(top,top))),zero),
inference(forward_demodulation,[status(thm)],[f5417,f7002]) ).
fof(f7010,plain,
! [X0] : zero = composition(X0,complement(composition(top,top))),
inference(forward_demodulation,[status(thm)],[f1348,f7003]) ).
fof(f7015,plain,
zero = complement(composition(top,top)),
inference(paramodulation,[status(thm)],[f1205,f7010]) ).
fof(f7116,plain,
complement(zero) = composition(top,top),
inference(paramodulation,[status(thm)],[f7015,f984]) ).
fof(f7164,plain,
top = composition(top,top),
inference(forward_demodulation,[status(thm)],[f838,f7116]) ).
fof(f7205,plain,
! [X0] : composition(join(top,sk1),composition(top,X0)) = composition(join(sk1,top),X0),
inference(paramodulation,[status(thm)],[f7164,f53]) ).
fof(f7227,plain,
! [X0] : composition(join(sk1,top),composition(top,X0)) = composition(join(sk1,top),X0),
inference(forward_demodulation,[status(thm)],[f331,f7205]) ).
fof(f7228,plain,
! [X0] : composition(top,composition(top,X0)) = composition(join(sk1,top),X0),
inference(forward_demodulation,[status(thm)],[f5232,f7227]) ).
fof(f7229,plain,
! [X0] : composition(top,composition(top,X0)) = composition(top,X0),
inference(forward_demodulation,[status(thm)],[f5232,f7228]) ).
fof(f11337,plain,
! [X0] : join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0)))) = complement(composition(top,X0)),
inference(paramodulation,[status(thm)],[f7229,f36]) ).
fof(f11420,plain,
! [X0] : composition(join(one,converse(top)),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f1235,f11337]) ).
fof(f11421,plain,
! [X0] : composition(join(one,top),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f5304,f11420]) ).
fof(f11422,plain,
! [X0] : composition(join(top,one),complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f331,f11421]) ).
fof(f11435,plain,
! [X0] : join(complement(X0),complement(composition(top,X0))) = complement(X0),
inference(backward_demodulation,[status(thm)],[f11436,f5427]) ).
fof(f11436,plain,
! [X0] : composition(top,complement(composition(top,X0))) = complement(composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f5287,f11422]) ).
fof(f11467,plain,
! [X0] : complement(meet(X0,composition(top,X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f1085,f11435]) ).
fof(f11501,plain,
! [X0] : complement(complement(X0)) = meet(X0,composition(top,X0)),
inference(paramodulation,[status(thm)],[f11467,f984]) ).
fof(f11555,plain,
! [X0] : X0 = meet(X0,composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f984,f11501]) ).
fof(f11598,plain,
! [X0] : composition(top,X0) = join(composition(top,X0),X0),
inference(paramodulation,[status(thm)],[f11555,f6078]) ).
fof(f11634,plain,
! [X0] : composition(top,X0) = join(X0,composition(top,X0)),
inference(forward_demodulation,[status(thm)],[f16,f11598]) ).
fof(f12135,plain,
! [X0] : converse(composition(top,converse(X0))) = join(X0,converse(composition(top,converse(X0)))),
inference(paramodulation,[status(thm)],[f11634,f384]) ).
fof(f12180,plain,
! [X0] : composition(converse(converse(X0)),top) = join(X0,converse(composition(top,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f5425,f12135]) ).
fof(f12181,plain,
! [X0] : composition(X0,top) = join(X0,converse(composition(top,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f12180]) ).
fof(f12182,plain,
! [X0] : composition(X0,top) = join(X0,composition(converse(converse(X0)),top)),
inference(forward_demodulation,[status(thm)],[f5425,f12181]) ).
fof(f12183,plain,
composition(complement(sk1),top) = complement(sk1),
inference(backward_demodulation,[status(thm)],[f12184,f1897]) ).
fof(f12184,plain,
! [X0] : composition(X0,top) = join(X0,composition(X0,top)),
inference(forward_demodulation,[status(thm)],[f23,f12182]) ).
fof(f12212,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f12183,f30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL018-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:00:26 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 9.84/2.03 % Refutation found
% 9.84/2.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.84/2.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.86/2.07 % Elapsed time: 1.717156 seconds
% 12.86/2.07 % CPU time: 13.369845 seconds
% 12.86/2.07 % Total memory used: 155.394 MB
% 12.86/2.07 % Net memory used: 148.652 MB
%------------------------------------------------------------------------------