%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT029-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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 01:02:06 PM UTC 2026
% Result : Unsatisfiable 0.24s 10.60s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 10
% Syntax : Number of formulae : 102 ( 85 unt; 4 def)
% Number of atoms : 125 ( 98 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 41 ( 18 ~; 19 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 167 ( 167 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : join(meet(X,Y),meet(X,join(X,Y))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : join(meet(X,X),meet(Y,join(X,X))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : join(meet(X,Y),meet(Y,join(X,Y))) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Z] : meet(meet(join(X,Y),join(Z,X)),X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : join(join(meet(X,Y),meet(Z,X)),X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,join(X0,X1))) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f8,plain,
! [X0,X1] : join(meet(X0,X0),meet(X1,join(X0,X0))) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f9,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,join(X0,X1))) = X1,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f10,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,X0)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f11,plain,
! [X0,X1,X2] : join(join(meet(X0,X1),meet(X2,X0)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f12,plain,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f13,definition,
( sQ0_spl
<=> meet(a,a) = a ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f15,plain,
( sQ0_spl
| meet(a,a) != a ),
inference(component_clause,[status(thm)],[f13]) ).
fof(f16,definition,
( sQ1_spl
<=> meet(b,a) = meet(a,b) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f18,plain,
( sQ1_spl
| meet(b,a) != meet(a,b) ),
inference(component_clause,[status(thm)],[f16]) ).
fof(f19,definition,
( sQ2_spl
<=> join(a,a) = a ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21,plain,
( sQ2_spl
| join(a,a) != a ),
inference(component_clause,[status(thm)],[f19]) ).
fof(f22,definition,
( sQ3_spl
<=> join(b,a) = join(a,b) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f24,plain,
( sQ3_spl
| join(b,a) != join(a,b) ),
inference(component_clause,[status(thm)],[f22]) ).
fof(f25,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f12,f13,f16,f19,f22]) ).
fof(f29,plain,
! [X0,X1] : join(meet(meet(X0,X0),meet(X1,join(X0,X0))),meet(meet(X0,X0),X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f8,f7]) ).
fof(f32,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,join(X0,X1))),meet(meet(X1,join(X0,X1)),X1)) = meet(X1,join(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f9]) ).
fof(f33,plain,
! [X0,X1] : join(meet(meet(X0,X0),meet(X1,join(X0,X0))),meet(meet(X1,join(X0,X0)),X0)) = meet(X1,join(X0,X0)),
inference(paramodulation,[status(thm)],[f8,f9]) ).
fof(f37,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,join(X0,X1))),meet(meet(X0,X1),X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f9,f7]) ).
fof(f38,plain,
! [X0,X1,X2] : meet(meet(X0,join(X1,meet(X2,X0))),meet(X2,X0)) = meet(X2,X0),
inference(paramodulation,[status(thm)],[f9,f10]) ).
fof(f44,plain,
! [X0] : join(meet(X0,X0),join(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f10,f8]) ).
fof(f51,plain,
! [X0,X1,X2,X3] : join(join(X0,meet(X1,meet(join(X0,X2),join(X3,X0)))),meet(join(X0,X2),join(X3,X0))) = meet(join(X0,X2),join(X3,X0)),
inference(paramodulation,[status(thm)],[f10,f11]) ).
fof(f52,plain,
! [X0,X1] : join(join(meet(X0,X1),X0),X0) = X0,
inference(paramodulation,[status(thm)],[f10,f11]) ).
fof(f53,plain,
! [X0,X1] : meet(meet(join(X0,X1),X0),X0) = X0,
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f65,plain,
! [X0,X1] : meet(meet(X0,meet(X1,X0)),meet(X1,X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f9,f53]) ).
fof(f67,plain,
! [X0,X1] : meet(meet(X0,meet(X0,X1)),meet(X0,X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f7,f53]) ).
fof(f88,plain,
! [X0,X1,X2] : meet(meet(X0,X0),meet(meet(join(X0,X1),join(X2,X0)),X0)) = meet(meet(join(X0,X1),join(X2,X0)),X0),
inference(paramodulation,[status(thm)],[f10,f65]) ).
fof(f100,plain,
! [X0,X1,X2] : meet(meet(X0,X0),X0) = meet(meet(join(X0,X1),join(X2,X0)),X0),
inference(forward_demodulation,[status(thm)],[f10,f88]) ).
fof(f101,plain,
! [X0] : meet(meet(X0,X0),X0) = X0,
inference(forward_demodulation,[status(thm)],[f10,f100]) ).
fof(f153,plain,
! [X0] : join(X0,meet(X0,join(meet(X0,X0),X0))) = X0,
inference(paramodulation,[status(thm)],[f101,f9]) ).
fof(f162,plain,
! [X0,X1] : meet(meet(X0,join(X1,X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f153,f10]) ).
fof(f197,plain,
! [X0,X1] : join(meet(meet(X0,X0),meet(X1,join(X0,X0))),X0) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f101,f29]) ).
fof(f205,plain,
! [X0,X1] : meet(meet(join(X0,X1),meet(X0,X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f197,f10]) ).
fof(f294,plain,
! [X0,X1] : meet(meet(meet(join(X0,X1),meet(X0,X0)),X0),meet(meet(join(X0,X1),meet(X0,X0)),X0)) = meet(meet(join(X0,X1),meet(X0,X0)),X0),
inference(paramodulation,[status(thm)],[f205,f67]) ).
fof(f323,plain,
! [X0,X1] : meet(X0,meet(meet(join(X0,X1),meet(X0,X0)),X0)) = meet(meet(join(X0,X1),meet(X0,X0)),X0),
inference(forward_demodulation,[status(thm)],[f205,f294]) ).
fof(f324,plain,
! [X0,X1] : meet(X0,X0) = meet(meet(join(X0,X1),meet(X0,X0)),X0),
inference(forward_demodulation,[status(thm)],[f205,f323]) ).
fof(f325,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f205,f324]) ).
fof(f380,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,join(X0,X1))),X1) = meet(X1,join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f162,f32]) ).
fof(f437,plain,
! [X0] : join(X0,join(X0,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f325,f44]) ).
fof(f438,plain,
! [X0,X1] : join(X0,meet(X1,join(X0,X0))) = X0,
inference(backward_demodulation,[status(thm)],[f325,f8]) ).
fof(f439,plain,
! [X0] : meet(join(X0,X0),X0) = X0,
inference(paramodulation,[status(thm)],[f325,f10]) ).
fof(f501,plain,
! [X0] : join(join(X0,join(X0,X0)),join(X0,X0)) = join(X0,X0),
inference(paramodulation,[status(thm)],[f439,f52]) ).
fof(f518,plain,
! [X0] : join(X0,join(X0,X0)) = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f437,f501]) ).
fof(f519,plain,
! [X0] : X0 = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f437,f518]) ).
fof(f522,plain,
! [X0,X1] : join(meet(X0,meet(X1,join(X0,X0))),meet(meet(X1,join(X0,X0)),X0)) = meet(X1,join(X0,X0)),
inference(forward_demodulation,[status(thm)],[f325,f33]) ).
fof(f535,plain,
! [X0,X1] : join(meet(X0,join(X1,X1)),X1) = X1,
inference(paramodulation,[status(thm)],[f522,f11]) ).
fof(f577,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f519,f438]) ).
fof(f723,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(forward_demodulation,[status(thm)],[f519,f535]) ).
fof(f741,plain,
! [X0,X1] : join(meet(meet(X0,X1),X1),meet(meet(X0,X1),X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f723,f7]) ).
fof(f752,plain,
! [X0,X1] : meet(meet(X0,X1),X1) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f519,f741]) ).
fof(f781,plain,
! [X0,X1] : meet(join(X0,X1),X0) = X0,
inference(backward_demodulation,[status(thm)],[f752,f53]) ).
fof(f829,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,join(X0,X1))),meet(X0,X1)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f752,f37]) ).
fof(f847,plain,
! [X0,X1] : join(meet(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(meet(X0,join(X1,X0)),X0))),X0) = meet(meet(X0,join(X1,X0)),X0),
inference(paramodulation,[status(thm)],[f162,f829]) ).
fof(f882,plain,
! [X0,X1] : meet(X0,join(meet(X0,join(X1,X0)),X0)) = meet(meet(X0,join(X1,X0)),X0),
inference(forward_demodulation,[status(thm)],[f380,f847]) ).
fof(f883,plain,
! [X0,X1] : meet(X0,join(meet(X0,join(X1,X0)),X0)) = X0,
inference(forward_demodulation,[status(thm)],[f162,f882]) ).
fof(f1724,plain,
! [X0,X1] : join(join(meet(X0,join(X1,X0)),X0),X0) = join(meet(X0,join(X1,X0)),X0),
inference(paramodulation,[status(thm)],[f883,f577]) ).
fof(f1769,plain,
! [X0,X1] : X0 = join(meet(X0,join(X1,X0)),X0),
inference(forward_demodulation,[status(thm)],[f52,f1724]) ).
fof(f1812,plain,
! [X0,X1] : join(meet(meet(X0,join(X1,X0)),X0),meet(meet(X0,join(X1,X0)),X0)) = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f1769,f7]) ).
fof(f1851,plain,
! [X0,X1] : meet(meet(X0,join(X1,X0)),X0) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f519,f1812]) ).
fof(f1852,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f162,f1851]) ).
fof(f1876,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,meet(X1,join(X0,X1)))),X1) = meet(X1,join(X0,X1)),
inference(paramodulation,[status(thm)],[f1852,f38]) ).
fof(f1883,plain,
! [X0,X1] : join(join(X0,X1),X1) = join(X0,X1),
inference(paramodulation,[status(thm)],[f1852,f577]) ).
fof(f1911,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,X1)),X1) = meet(X1,join(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1852,f1876]) ).
fof(f1912,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,X1)),X1) = X1,
inference(forward_demodulation,[status(thm)],[f1852,f1911]) ).
fof(f2146,plain,
! [X0,X1] : join(meet(X0,X1),X0) = X0,
inference(backward_demodulation,[status(thm)],[f1883,f52]) ).
fof(f2210,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f781,f2146]) ).
fof(f2238,plain,
! [X0,X1] : join(meet(meet(X0,X1),X0),meet(meet(X0,X1),X0)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f2146,f7]) ).
fof(f2254,plain,
! [X0,X1] : meet(meet(X0,X1),X0) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f519,f2238]) ).
fof(f2349,plain,
! [X0,X1] : join(meet(X0,join(X0,X1)),meet(X0,join(X0,X1))) = X0,
inference(paramodulation,[status(thm)],[f2210,f7]) ).
fof(f2368,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f519,f2349]) ).
fof(f2398,plain,
! [X0,X1] : join(join(X0,X1),X0) = join(X0,X1),
inference(paramodulation,[status(thm)],[f2368,f577]) ).
fof(f2449,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f2254,f577]) ).
fof(f2496,plain,
! [X0,X1] : meet(meet(X0,X1),meet(X1,X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f2449,f38]) ).
fof(f2987,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X1,X2)),X1) = X1,
inference(paramodulation,[status(thm)],[f2398,f1912]) ).
fof(f3734,plain,
! [X0,X1] : meet(meet(meet(X0,X1),meet(X1,X0)),meet(X0,X1)) = meet(meet(X1,X0),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f2496,f2496]) ).
fof(f3787,plain,
! [X0,X1] : meet(meet(X0,X1),meet(X1,X0)) = meet(meet(X1,X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f2254,f3734]) ).
fof(f3788,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2496,f3787]) ).
fof(f4397,plain,
! [X0,X1,X2] : meet(meet(X0,meet(join(X1,X0),join(X0,X2))),X0) = meet(meet(join(X1,X0),join(X0,X2)),X0),
inference(paramodulation,[status(thm)],[f2987,f2496]) ).
fof(f4449,plain,
! [X0,X1,X2] : meet(X0,meet(join(X1,X0),join(X0,X2))) = meet(meet(join(X1,X0),join(X0,X2)),X0),
inference(forward_demodulation,[status(thm)],[f2254,f4397]) ).
fof(f4450,plain,
! [X0,X1,X2] : meet(X0,meet(join(X1,X0),join(X0,X2))) = X0,
inference(forward_demodulation,[status(thm)],[f2987,f4449]) ).
fof(f4883,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f2496,f3788]) ).
fof(f6388,plain,
! [X0,X1] : join(join(X0,X1),meet(join(X0,X1),join(X1,X0))) = meet(join(X0,X1),join(X1,X0)),
inference(paramodulation,[status(thm)],[f4450,f51]) ).
fof(f6459,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2449,f6388]) ).
fof(f6527,plain,
! [X0,X1] : join(X0,X1) = meet(join(X1,X0),join(X0,X1)),
inference(paramodulation,[status(thm)],[f4883,f6459]) ).
fof(f6738,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(paramodulation,[status(thm)],[f6459,f6527]) ).
fof(f6953,plain,
( sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f24,f6738]) ).
fof(f7100,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f6953]) ).
fof(f7105,plain,
( sQ2_spl
| a != a ),
inference(forward_demodulation,[status(thm)],[f519,f21]) ).
fof(f7106,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7105]) ).
fof(f7107,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f7106]) ).
fof(f7108,plain,
( sQ0_spl
| a != a ),
inference(forward_demodulation,[status(thm)],[f325,f15]) ).
fof(f7109,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7108]) ).
fof(f7110,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f7109]) ).
fof(f7111,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18,f4883]) ).
fof(f7112,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f7111]) ).
fof(f7113,plain,
$false,
inference(sat_refutation,[status(thm)],[f25,f7100,f7107,f7110,f7112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT029-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/10.46 % Computer : n010.cluster.edu
% 0.19/10.46 % Model : x86_64 x86_64
% 0.19/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/10.46 % Memory : 8046.5625MB
% 0.19/10.46 % OS : Linux 6.8.0-71-generic
% 0.19/10.46 % CPULimit : 300
% 0.19/10.46 % WCLimit : 300
% 0.19/10.46 % DateTime : Sun Sep 20 23:07:53 UTC 2026
% 0.19/10.47 % CPUTime :
% 0.19/10.48 % Drodi V4.1.1
% 0.24/10.60 % Refutation found
% 0.24/10.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/10.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.24/10.66 % Elapsed time: 0.174115 seconds
% 0.24/10.66 % CPU time: 0.912405 seconds
% 0.24/10.66 % Total memory used: 78.770 MB
% 0.24/10.66 % Net memory used: 78.073 MB
%------------------------------------------------------------------------------