%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT147-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:16 PM UTC 2026
% Result : Unsatisfiable 228.60s 34.16s
% Output : CNFRefutation 122.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 20
% Syntax : Number of formulae : 108 ( 108 unt; 10 def)
% Number of atoms : 108 ( 107 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 : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 14 con; 0-2 aty)
% Number of variables : 87 ( 87 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : meet(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : join(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] : join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] : meet(meet(X,Y),Z) = meet(X,meet(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y,Z] : join(join(X,Y),Z) = join(X,join(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z,U] : meet(X,join(Y,meet(Z,U))) = meet(X,join(Y,meet(Z,join(Y,meet(U,join(Y,Z)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
meet(a,meet(b,join(c,meet(a,d)))) != meet(a,meet(b,join(c,meet(d,join(a,meet(b,c)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,plain,
! [X0] : meet(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f12,plain,
! [X0] : join(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f13,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f14,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f15,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f17,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f18,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f19,plain,
! [X0,X1,X2,X3] : meet(X0,join(X1,meet(X2,X3))) = meet(X0,join(X1,meet(X2,join(X1,meet(X3,join(X1,X2)))))),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
meet(a,meet(b,join(c,meet(a,d)))) != meet(a,meet(b,join(c,meet(d,join(a,meet(b,c)))))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f21,definition,
sF3_fnc = meet(a,d),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f22,definition,
sF2_fnc = join(c,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f23,definition,
sF1_fnc = meet(b,sF2_fnc),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f24,definition,
sF0_fnc = meet(a,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f25,definition,
sF9_fnc = meet(b,c),
introduced(definition,[new_symbols(definition,[sF9_fnc])],[function_definition]) ).
fof(f26,definition,
sF8_fnc = join(a,sF9_fnc),
introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition]) ).
fof(f27,definition,
sF7_fnc = meet(d,sF8_fnc),
introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition]) ).
fof(f28,definition,
sF6_fnc = join(c,sF7_fnc),
introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition]) ).
fof(f29,definition,
sF5_fnc = meet(b,sF6_fnc),
introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition]) ).
fof(f30,definition,
sF4_fnc = meet(a,sF5_fnc),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f31,plain,
sF0_fnc != sF4_fnc,
inference(definition_folding,[],[f20,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21]) ).
fof(f32,plain,
meet(a,sF8_fnc) = a,
inference(paramodulation,[status(thm)],[f26,f13]) ).
fof(f37,plain,
join(a,sF0_fnc) = a,
inference(paramodulation,[status(thm)],[f24,f14]) ).
fof(f49,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f15,f14]) ).
fof(f56,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f16,f13]) ).
fof(f58,plain,
join(d,sF7_fnc) = d,
inference(paramodulation,[status(thm)],[f27,f14]) ).
fof(f61,plain,
join(a,sF4_fnc) = a,
inference(paramodulation,[status(thm)],[f30,f14]) ).
fof(f64,plain,
! [X0,X1,X2] : meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))),
inference(paramodulation,[status(thm)],[f13,f17]) ).
fof(f65,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)),
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f67,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,meet(X0,X1))),
inference(paramodulation,[status(thm)],[f11,f17]) ).
fof(f70,plain,
! [X0] : meet(sF7_fnc,X0) = meet(d,meet(sF8_fnc,X0)),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f71,plain,
! [X0] : meet(sF5_fnc,X0) = meet(b,meet(sF6_fnc,X0)),
inference(paramodulation,[status(thm)],[f29,f17]) ).
fof(f73,plain,
! [X0] : meet(sF1_fnc,X0) = meet(b,meet(sF2_fnc,X0)),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f74,plain,
! [X0] : meet(a,X0) = meet(a,meet(sF8_fnc,X0)),
inference(paramodulation,[status(thm)],[f32,f17]) ).
fof(f75,plain,
! [X0] : meet(sF4_fnc,X0) = meet(a,meet(sF5_fnc,X0)),
inference(paramodulation,[status(thm)],[f30,f17]) ).
fof(f76,plain,
! [X0] : meet(sF0_fnc,X0) = meet(a,meet(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f24,f17]) ).
fof(f94,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,join(X0,X1))),
inference(paramodulation,[status(thm)],[f12,f18]) ).
fof(f96,plain,
! [X0] : join(sF8_fnc,X0) = join(a,join(sF9_fnc,X0)),
inference(paramodulation,[status(thm)],[f26,f18]) ).
fof(f98,plain,
! [X0] : join(sF2_fnc,X0) = join(c,join(sF3_fnc,X0)),
inference(paramodulation,[status(thm)],[f22,f18]) ).
fof(f129,plain,
join(c,sF9_fnc) = c,
inference(paramodulation,[status(thm)],[f25,f49]) ).
fof(f131,plain,
join(sF8_fnc,a) = sF8_fnc,
inference(paramodulation,[status(thm)],[f32,f49]) ).
fof(f132,plain,
join(sF5_fnc,sF4_fnc) = sF5_fnc,
inference(paramodulation,[status(thm)],[f30,f49]) ).
fof(f133,plain,
join(sF1_fnc,sF0_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f24,f49]) ).
fof(f150,plain,
meet(sF0_fnc,a) = sF0_fnc,
inference(paramodulation,[status(thm)],[f37,f56]) ).
fof(f151,plain,
meet(sF9_fnc,sF8_fnc) = sF9_fnc,
inference(paramodulation,[status(thm)],[f26,f56]) ).
fof(f167,plain,
meet(sF7_fnc,d) = sF7_fnc,
inference(paramodulation,[status(thm)],[f58,f56]) ).
fof(f176,plain,
meet(sF4_fnc,a) = sF4_fnc,
inference(paramodulation,[status(thm)],[f61,f56]) ).
fof(f190,plain,
! [X0,X1,X2] : meet(meet(X0,join(X1,meet(X2,join(X1,X0)))),join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X1,X0)))),
inference(paramodulation,[status(thm)],[f56,f19]) ).
fof(f237,plain,
! [X0,X1,X2] : meet(X0,meet(join(X1,meet(X2,join(X1,X0))),join(X1,meet(X0,X2)))) = meet(X0,join(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[status(thm)],[f17,f190]) ).
fof(f346,plain,
! [X0,X1,X2] : meet(X0,X1) = meet(X1,meet(join(meet(X0,X1),X2),X0)),
inference(paramodulation,[status(thm)],[f64,f65]) ).
fof(f395,plain,
! [X0,X1,X2] : meet(join(X0,X1),meet(X2,X1)) = meet(X2,X1),
inference(paramodulation,[status(thm)],[f56,f65]) ).
fof(f462,plain,
! [X0] : join(c,X0) = join(c,join(sF9_fnc,X0)),
inference(paramodulation,[status(thm)],[f129,f18]) ).
fof(f489,plain,
meet(sF4_fnc,sF5_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f132,f56]) ).
fof(f502,plain,
! [X0] : meet(sF7_fnc,join(X0,sF8_fnc)) = meet(d,sF8_fnc),
inference(paramodulation,[status(thm)],[f56,f70]) ).
fof(f520,plain,
! [X0] : meet(sF7_fnc,join(X0,sF8_fnc)) = sF7_fnc,
inference(forward_demodulation,[status(thm)],[f27,f502]) ).
fof(f537,plain,
meet(sF0_fnc,sF1_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f133,f56]) ).
fof(f593,plain,
join(sF8_fnc,sF9_fnc) = sF8_fnc,
inference(paramodulation,[status(thm)],[f151,f49]) ).
fof(f657,plain,
meet(sF8_fnc,d) = meet(sF8_fnc,meet(sF7_fnc,d)),
inference(paramodulation,[status(thm)],[f70,f67]) ).
fof(f708,plain,
meet(sF8_fnc,d) = meet(sF8_fnc,sF7_fnc),
inference(forward_demodulation,[status(thm)],[f167,f657]) ).
fof(f850,plain,
! [X0] : meet(sF5_fnc,X0) = meet(b,meet(X0,sF6_fnc)),
inference(paramodulation,[status(thm)],[f15,f71]) ).
fof(f958,plain,
! [X0] : meet(sF1_fnc,X0) = meet(b,meet(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f15,f73]) ).
fof(f1030,plain,
meet(sF5_fnc,a) = meet(sF5_fnc,meet(sF4_fnc,a)),
inference(paramodulation,[status(thm)],[f75,f67]) ).
fof(f1056,plain,
meet(sF5_fnc,a) = meet(sF5_fnc,sF4_fnc),
inference(forward_demodulation,[status(thm)],[f176,f1030]) ).
fof(f1112,plain,
meet(sF1_fnc,a) = meet(sF1_fnc,meet(sF0_fnc,a)),
inference(paramodulation,[status(thm)],[f76,f67]) ).
fof(f1138,plain,
meet(sF1_fnc,a) = meet(sF1_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f150,f1112]) ).
fof(f2703,plain,
join(sF9_fnc,a) = join(sF9_fnc,join(sF8_fnc,a)),
inference(paramodulation,[status(thm)],[f96,f94]) ).
fof(f2777,plain,
join(sF9_fnc,a) = join(sF9_fnc,sF8_fnc),
inference(forward_demodulation,[status(thm)],[f131,f2703]) ).
fof(f27813,plain,
meet(a,sF7_fnc) = meet(a,meet(sF8_fnc,d)),
inference(paramodulation,[status(thm)],[f708,f74]) ).
fof(f27845,plain,
meet(a,sF7_fnc) = meet(a,d),
inference(forward_demodulation,[status(thm)],[f74,f27813]) ).
fof(f27846,plain,
meet(a,sF7_fnc) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f21,f27845]) ).
fof(f27928,plain,
join(sF7_fnc,sF3_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f27846,f49]) ).
fof(f29618,plain,
join(sF3_fnc,sF7_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f16,f27928]) ).
fof(f29764,plain,
join(sF2_fnc,sF7_fnc) = join(c,sF7_fnc),
inference(paramodulation,[status(thm)],[f29618,f98]) ).
fof(f29791,plain,
join(sF2_fnc,sF7_fnc) = sF6_fnc,
inference(forward_demodulation,[status(thm)],[f28,f29764]) ).
fof(f39048,plain,
meet(sF5_fnc,a) = meet(sF4_fnc,sF5_fnc),
inference(paramodulation,[status(thm)],[f15,f1056]) ).
fof(f39092,plain,
meet(sF5_fnc,a) = sF4_fnc,
inference(forward_demodulation,[status(thm)],[f489,f39048]) ).
fof(f41268,plain,
meet(sF1_fnc,a) = meet(sF0_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f15,f1138]) ).
fof(f41316,plain,
meet(sF1_fnc,a) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f537,f41268]) ).
fof(f43071,plain,
join(sF9_fnc,a) = join(sF8_fnc,sF9_fnc),
inference(paramodulation,[status(thm)],[f16,f2777]) ).
fof(f43109,plain,
join(sF9_fnc,a) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f593,f43071]) ).
fof(f53983,plain,
! [X0,X1,X2] : meet(X0,join(X1,X0)) = meet(join(meet(X0,join(X1,X0)),X2),X0),
inference(paramodulation,[status(thm)],[f346,f395]) ).
fof(f54546,plain,
! [X0,X1,X2] : X0 = meet(join(meet(X0,join(X1,X0)),X2),X0),
inference(forward_demodulation,[status(thm)],[f56,f53983]) ).
fof(f54547,plain,
! [X0,X1] : X0 = meet(join(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f56,f54546]) ).
fof(f56970,plain,
sF2_fnc = meet(sF6_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f29791,f54547]) ).
fof(f132467,plain,
join(c,a) = join(c,sF8_fnc),
inference(paramodulation,[status(thm)],[f43109,f462]) ).
fof(f132634,plain,
meet(sF7_fnc,join(c,a)) = sF7_fnc,
inference(paramodulation,[status(thm)],[f132467,f520]) ).
fof(f133493,plain,
meet(a,meet(join(c,sF7_fnc),join(c,meet(a,sF7_fnc)))) = meet(a,join(c,meet(sF7_fnc,join(c,a)))),
inference(paramodulation,[status(thm)],[f132634,f237]) ).
fof(f133560,plain,
meet(a,meet(sF6_fnc,join(c,meet(a,sF7_fnc)))) = meet(a,join(c,meet(sF7_fnc,join(c,a)))),
inference(forward_demodulation,[status(thm)],[f28,f133493]) ).
fof(f133561,plain,
meet(a,meet(sF6_fnc,join(c,sF3_fnc))) = meet(a,join(c,meet(sF7_fnc,join(c,a)))),
inference(forward_demodulation,[status(thm)],[f27846,f133560]) ).
fof(f133562,plain,
meet(a,meet(sF6_fnc,sF2_fnc)) = meet(a,join(c,meet(sF7_fnc,join(c,a)))),
inference(forward_demodulation,[status(thm)],[f22,f133561]) ).
fof(f133563,plain,
meet(a,sF2_fnc) = meet(a,join(c,meet(sF7_fnc,join(c,a)))),
inference(forward_demodulation,[status(thm)],[f56970,f133562]) ).
fof(f133564,plain,
meet(a,sF2_fnc) = meet(a,join(c,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f132634,f133563]) ).
fof(f133565,plain,
meet(a,sF2_fnc) = meet(a,sF6_fnc),
inference(forward_demodulation,[status(thm)],[f28,f133564]) ).
fof(f136130,plain,
meet(sF5_fnc,a) = meet(b,meet(a,sF2_fnc)),
inference(paramodulation,[status(thm)],[f133565,f850]) ).
fof(f136193,plain,
sF4_fnc = meet(b,meet(a,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f39092,f136130]) ).
fof(f136194,plain,
sF4_fnc = meet(sF1_fnc,a),
inference(forward_demodulation,[status(thm)],[f958,f136193]) ).
fof(f136195,plain,
sF4_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f41316,f136194]) ).
fof(f136196,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f136195,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT147-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.50 % Computer : n019.cluster.edu
% 0.19/0.50 % Model : x86_64 x86_64
% 0.19/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.50 % Memory : 8046.5625MB
% 0.19/0.50 % OS : Linux 6.8.0-71-generic
% 0.19/0.50 % CPULimit : 300
% 0.19/0.50 % WCLimit : 300
% 0.19/0.50 % DateTime : Sun Sep 20 23:15:51 UTC 2026
% 0.19/0.50 % CPUTime :
% 0.19/0.51 % Drodi V4.1.1
% 228.60/34.16 % Refutation found
% 228.60/34.16 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 228.60/34.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 122.74/34.28 % Elapsed time: 33.765139 seconds
% 122.74/34.28 % CPU time: 266.538109 seconds
% 122.74/34.28 % Total memory used: 588.341 MB
% 122.74/34.28 % Net memory used: 566.896 MB
%------------------------------------------------------------------------------