%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT043-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 01:02:08 PM UTC 2026
% Result : Unsatisfiable 9.78s 1.89s
% Output : CNFRefutation 9.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 115 ( 115 unt; 5 def)
% Number of atoms : 115 ( 114 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 : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 97 ( 97 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : meet(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] : join(X,Y) = join(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(X,Y),meet(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] : join(complement(X),X) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] : meet(complement(X),X) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : complement(complement(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
complement(join(c,d)) != meet(complement(c),complement(d)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,plain,
! [X0] : meet(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f17,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f18,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f19,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f20,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f21,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f22,plain,
! [X0,X1,X2] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f23,plain,
! [X0] : join(complement(X0),X0) = n1,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f24,plain,
! [X0] : meet(complement(X0),X0) = n0,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f25,plain,
! [X0] : complement(complement(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f26,plain,
complement(join(c,d)) != meet(complement(c),complement(d)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f27,definition,
sF1_fnc = join(c,d),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f28,definition,
sF0_fnc = complement(sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f29,definition,
sF3_fnc = complement(c),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f30,definition,
sF4_fnc = complement(d),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f31,definition,
sF2_fnc = meet(sF3_fnc,sF4_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f32,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f26,f31,f30,f29,f28,f27]) ).
fof(f34,plain,
complement(sF0_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f28,f25]) ).
fof(f35,plain,
complement(sF3_fnc) = c,
inference(paramodulation,[status(thm)],[f29,f25]) ).
fof(f37,plain,
complement(sF4_fnc) = d,
inference(paramodulation,[status(thm)],[f30,f25]) ).
fof(f44,plain,
meet(c,sF1_fnc) = c,
inference(paramodulation,[status(thm)],[f27,f16]) ).
fof(f49,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f18,f17]) ).
fof(f51,plain,
join(sF3_fnc,sF2_fnc) = sF3_fnc,
inference(paramodulation,[status(thm)],[f31,f17]) ).
fof(f54,plain,
join(d,sF4_fnc) = n1,
inference(paramodulation,[status(thm)],[f37,f23]) ).
fof(f60,plain,
! [X0] : join(X0,complement(X0)) = n1,
inference(paramodulation,[status(thm)],[f25,f23]) ).
fof(f65,plain,
sF3_fnc = join(sF2_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f51,f19]) ).
fof(f74,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f19,f16]) ).
fof(f105,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)),
inference(paramodulation,[status(thm)],[f18,f20]) ).
fof(f112,plain,
! [X0] : meet(sF2_fnc,X0) = meet(sF3_fnc,meet(sF4_fnc,X0)),
inference(paramodulation,[status(thm)],[f31,f20]) ).
fof(f154,plain,
! [X0,X1,X2] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(paramodulation,[status(thm)],[f17,f21]) ).
fof(f168,plain,
! [X0] : join(sF1_fnc,X0) = join(c,join(d,X0)),
inference(paramodulation,[status(thm)],[f27,f21]) ).
fof(f234,plain,
! [X0,X1,X2] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(paramodulation,[status(thm)],[f18,f22]) ).
fof(f236,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f14,f22]) ).
fof(f270,plain,
! [X0,X1] : X0 = join(meet(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f74,f236]) ).
fof(f298,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = join(meet(complement(X0),X1),n0),
inference(paramodulation,[status(thm)],[f24,f22]) ).
fof(f314,plain,
! [X0] : meet(X0,n1) = X0,
inference(paramodulation,[status(thm)],[f60,f16]) ).
fof(f324,plain,
! [X0] : meet(n1,X0) = X0,
inference(paramodulation,[status(thm)],[f18,f314]) ).
fof(f401,plain,
! [X0] : n1 = join(n1,X0),
inference(paramodulation,[status(thm)],[f16,f324]) ).
fof(f448,plain,
! [X0] : n1 = join(X0,n1),
inference(paramodulation,[status(thm)],[f19,f401]) ).
fof(f466,plain,
! [X0] : join(X0,n0) = X0,
inference(paramodulation,[status(thm)],[f24,f49]) ).
fof(f469,plain,
join(sF1_fnc,c) = sF1_fnc,
inference(paramodulation,[status(thm)],[f44,f49]) ).
fof(f470,plain,
join(sF4_fnc,sF2_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f31,f49]) ).
fof(f472,plain,
! [X0,X1] : join(join(X0,X1),X0) = join(X0,X1),
inference(paramodulation,[status(thm)],[f16,f49]) ).
fof(f483,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(complement(X0),X1),
inference(backward_demodulation,[status(thm)],[f466,f298]) ).
fof(f485,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X0,X1),
inference(forward_demodulation,[status(thm)],[f21,f472]) ).
fof(f594,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f20,f74]) ).
fof(f667,plain,
join(c,sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f19,f469]) ).
fof(f674,plain,
join(sF2_fnc,sF4_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f19,f470]) ).
fof(f1057,plain,
! [X0,X1] : X0 = join(meet(X1,X0),X0),
inference(paramodulation,[status(thm)],[f18,f270]) ).
fof(f2391,plain,
! [X0,X1] : join(complement(X0),X0) = join(complement(X0),join(X0,meet(n1,X1))),
inference(paramodulation,[status(thm)],[f23,f154]) ).
fof(f2466,plain,
! [X0,X1] : n1 = join(complement(X0),join(X0,meet(n1,X1))),
inference(forward_demodulation,[status(thm)],[f23,f2391]) ).
fof(f2467,plain,
! [X0,X1] : n1 = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f324,f2466]) ).
fof(f3308,plain,
join(sF1_fnc,sF4_fnc) = join(c,n1),
inference(paramodulation,[status(thm)],[f54,f168]) ).
fof(f3340,plain,
join(sF1_fnc,sF4_fnc) = n1,
inference(forward_demodulation,[status(thm)],[f448,f3308]) ).
fof(f3377,plain,
join(sF4_fnc,n1) = join(sF4_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f3340,f485]) ).
fof(f3385,plain,
n1 = join(sF4_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f448,f3377]) ).
fof(f6222,plain,
! [X0,X1] : n1 = join(complement(meet(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f270,f2467]) ).
fof(f6224,plain,
n1 = join(complement(sF2_fnc),sF4_fnc),
inference(paramodulation,[status(thm)],[f674,f2467]) ).
fof(f6225,plain,
n1 = join(complement(sF2_fnc),sF3_fnc),
inference(paramodulation,[status(thm)],[f65,f2467]) ).
fof(f6247,plain,
n1 = join(complement(c),sF1_fnc),
inference(paramodulation,[status(thm)],[f667,f2467]) ).
fof(f6298,plain,
n1 = join(sF3_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f29,f6247]) ).
fof(f9373,plain,
meet(complement(sF1_fnc),n1) = meet(complement(sF1_fnc),sF4_fnc),
inference(paramodulation,[status(thm)],[f3385,f483]) ).
fof(f9388,plain,
meet(complement(sF3_fnc),n1) = meet(complement(sF3_fnc),complement(sF2_fnc)),
inference(paramodulation,[status(thm)],[f6225,f483]) ).
fof(f9389,plain,
meet(complement(sF4_fnc),n1) = meet(complement(sF4_fnc),complement(sF2_fnc)),
inference(paramodulation,[status(thm)],[f6224,f483]) ).
fof(f9394,plain,
meet(complement(sF1_fnc),n1) = meet(complement(sF1_fnc),sF3_fnc),
inference(paramodulation,[status(thm)],[f6298,f483]) ).
fof(f9479,plain,
complement(sF1_fnc) = meet(complement(sF1_fnc),sF4_fnc),
inference(forward_demodulation,[status(thm)],[f314,f9373]) ).
fof(f9480,plain,
sF0_fnc = meet(complement(sF1_fnc),sF4_fnc),
inference(forward_demodulation,[status(thm)],[f28,f9479]) ).
fof(f9481,plain,
sF0_fnc = meet(sF0_fnc,sF4_fnc),
inference(forward_demodulation,[status(thm)],[f28,f9480]) ).
fof(f9505,plain,
complement(sF3_fnc) = meet(complement(sF3_fnc),complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f314,f9388]) ).
fof(f9506,plain,
c = meet(complement(sF3_fnc),complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f35,f9505]) ).
fof(f9507,plain,
c = meet(c,complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f35,f9506]) ).
fof(f9508,plain,
complement(sF4_fnc) = meet(complement(sF4_fnc),complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f314,f9389]) ).
fof(f9509,plain,
d = meet(complement(sF4_fnc),complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f37,f9508]) ).
fof(f9510,plain,
d = meet(d,complement(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f37,f9509]) ).
fof(f9517,plain,
complement(sF1_fnc) = meet(complement(sF1_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f314,f9394]) ).
fof(f9518,plain,
sF0_fnc = meet(complement(sF1_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f28,f9517]) ).
fof(f9519,plain,
sF0_fnc = meet(sF0_fnc,sF3_fnc),
inference(forward_demodulation,[status(thm)],[f28,f9518]) ).
fof(f9587,plain,
join(sF4_fnc,sF0_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f9481,f49]) ).
fof(f9666,plain,
! [X0] : meet(sF0_fnc,join(sF3_fnc,X0)) = join(sF0_fnc,meet(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f9519,f234]) ).
fof(f9680,plain,
join(sF3_fnc,sF0_fnc) = sF3_fnc,
inference(paramodulation,[status(thm)],[f9519,f49]) ).
fof(f9688,plain,
! [X0] : meet(sF0_fnc,join(sF3_fnc,X0)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f49,f9666]) ).
fof(f10022,plain,
complement(sF2_fnc) = join(c,complement(sF2_fnc)),
inference(paramodulation,[status(thm)],[f9507,f1057]) ).
fof(f10059,plain,
complement(sF2_fnc) = join(d,complement(sF2_fnc)),
inference(paramodulation,[status(thm)],[f9510,f1057]) ).
fof(f14679,plain,
! [X0,X1] : meet(X0,sF0_fnc) = meet(sF0_fnc,meet(join(sF3_fnc,X1),X0)),
inference(paramodulation,[status(thm)],[f9688,f105]) ).
fof(f16160,plain,
! [X0,X1] : meet(sF0_fnc,meet(join(sF3_fnc,X0),join(X1,sF0_fnc))) = meet(sF0_fnc,join(sF3_fnc,X0)),
inference(paramodulation,[status(thm)],[f9688,f594]) ).
fof(f16383,plain,
! [X0,X1] : meet(join(X0,sF0_fnc),sF0_fnc) = meet(sF0_fnc,join(sF3_fnc,X1)),
inference(forward_demodulation,[status(thm)],[f14679,f16160]) ).
fof(f16384,plain,
! [X0] : meet(join(X0,sF0_fnc),sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f9688,f16383]) ).
fof(f17010,plain,
meet(sF4_fnc,sF0_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f9587,f16384]) ).
fof(f17015,plain,
meet(sF3_fnc,sF0_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f9680,f16384]) ).
fof(f17651,plain,
meet(sF2_fnc,sF0_fnc) = meet(sF3_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f17010,f112]) ).
fof(f17689,plain,
meet(sF2_fnc,sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f17015,f17651]) ).
fof(f17716,plain,
n1 = join(complement(sF0_fnc),sF2_fnc),
inference(paramodulation,[status(thm)],[f17689,f6222]) ).
fof(f17744,plain,
n1 = join(sF1_fnc,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f34,f17716]) ).
fof(f17840,plain,
meet(complement(sF2_fnc),n1) = meet(complement(sF2_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f17744,f483]) ).
fof(f17865,plain,
complement(sF2_fnc) = meet(complement(sF2_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f314,f17840]) ).
fof(f22338,plain,
join(sF1_fnc,complement(sF2_fnc)) = join(c,complement(sF2_fnc)),
inference(paramodulation,[status(thm)],[f10059,f168]) ).
fof(f22366,plain,
join(sF1_fnc,complement(sF2_fnc)) = complement(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f10022,f22338]) ).
fof(f23394,plain,
join(sF1_fnc,complement(sF2_fnc)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f17865,f49]) ).
fof(f23490,plain,
complement(sF2_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f22366,f23394]) ).
fof(f23562,plain,
complement(sF1_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f23490,f25]) ).
fof(f23565,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f28,f23562]) ).
fof(f23566,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f23565,f32]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT043-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.45 % Computer : n014.cluster.edu
% 0.15/0.45 % Model : x86_64 x86_64
% 0.15/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.45 % Memory : 8046.5625MB
% 0.15/0.45 % OS : Linux 6.8.0-71-generic
% 0.15/0.45 % CPULimit : 300
% 0.15/0.45 % WCLimit : 300
% 0.15/0.45 % DateTime : Sun Sep 20 23:07:49 UTC 2026
% 0.15/0.45 % CPUTime :
% 0.15/0.47 % Drodi V4.1.1
% 9.78/1.89 % Refutation found
% 9.78/1.89 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.78/1.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.31/3.14 % Elapsed time: 2.466366 seconds
% 12.31/3.14 % CPU time: 9.311669 seconds
% 12.31/3.14 % Total memory used: 71.530 MB
% 12.31/3.14 % Net memory used: 68.691 MB
%------------------------------------------------------------------------------