%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:05 PM UTC 2026
% Result : Unsatisfiable 97.62s 12.82s
% Output : CNFRefutation 84.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 7
% Syntax : Number of formulae : 96 ( 96 unt; 0 def)
% Number of atoms : 96 ( 95 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 259 ( 259 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X] : join(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] : meet(X,Y) = meet(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : join(X,Y) = join(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : meet(meet(join(X,Y),join(Z,Y)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : join(join(meet(X,Y),meet(Z,Y)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
! [X,Y,Z] : meet(X,join(Y,join(X,Z))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
meet(meet(a,b),c) != meet(a,meet(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,plain,
! [X0] : join(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f11,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f12,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f13,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,X1)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f14,plain,
! [X0,X1,X2] : join(join(meet(X0,X1),meet(X2,X1)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f15,plain,
! [X0,X1,X2] : meet(X0,join(X1,join(X0,X2))) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f16,plain,
meet(meet(a,b),c) != meet(a,meet(b,c)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f22,plain,
! [X0,X1,X2] : meet(X0,meet(join(X1,X0),join(X2,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f11,f13]) ).
fof(f23,plain,
! [X0,X1,X2] : join(X0,join(meet(X1,X0),meet(X2,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f12,f14]) ).
fof(f24,plain,
meet(c,meet(a,b)) != meet(a,meet(b,c)),
inference(forward_demodulation,[status(thm)],[f11,f16]) ).
fof(f44,plain,
! [X0,X1,X2] : meet(X0,meet(join(X0,X1),join(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f12,f22]) ).
fof(f109,plain,
! [X0,X1,X2] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f12,f15]) ).
fof(f129,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f10,f23]) ).
fof(f149,plain,
! [X0,X1,X2] : join(X0,join(meet(X1,X0),meet(X0,X2))) = X0,
inference(paramodulation,[status(thm)],[f11,f23]) ).
fof(f153,plain,
! [X0,X1] : meet(meet(X0,X1),X1) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f23,f15]) ).
fof(f177,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f11,f153]) ).
fof(f344,plain,
! [X0,X1] : meet(X0,meet(X0,X1)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f11,f177]) ).
fof(f364,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f11,f129]) ).
fof(f382,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(join(X2,meet(X0,X1)),X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f129,f22]) ).
fof(f416,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X1,join(X2,meet(X0,X1)))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f11,f382]) ).
fof(f433,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f344,f129]) ).
fof(f434,plain,
! [X0,X1] : meet(meet(X0,X1),meet(X1,X0)) = meet(X0,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f344,f177]) ).
fof(f459,plain,
! [X0,X1] : meet(meet(X0,X1),meet(X1,X0)) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f344,f434]) ).
fof(f793,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(join(meet(X0,X1),X2),meet(X1,X0))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f433,f44]) ).
fof(f880,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X1,X0),join(meet(X0,X1),X2))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f11,f793]) ).
fof(f901,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,join(X2,meet(X1,X0)))) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f11,f416]) ).
fof(f924,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f11,f416]) ).
fof(f1430,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X0,X1),join(X2,meet(meet(X0,X1),meet(X1,X0))))) = meet(meet(X1,X0),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f459,f924]) ).
fof(f1501,plain,
! [X0,X1,X2] : meet(join(X0,meet(meet(X1,X2),meet(X2,X1))),meet(X1,X2)) = meet(meet(X2,X1),meet(X1,X2)),
inference(forward_demodulation,[status(thm)],[f344,f1430]) ).
fof(f1502,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),meet(X1,X0)))) = meet(meet(X1,X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f11,f1501]) ).
fof(f1503,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(X2,meet(X1,X0))) = meet(meet(X1,X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f459,f1502]) ).
fof(f1506,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(X2,meet(X1,X0))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f459,f1503]) ).
fof(f1683,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(X2,X0)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f364,f109]) ).
fof(f1684,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(X2,X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f129,f109]) ).
fof(f2064,plain,
! [X0,X1,X2] : meet(join(X0,X1),meet(X1,X2)) = meet(X1,X2),
inference(paramodulation,[status(thm)],[f11,f1683]) ).
fof(f2088,plain,
! [X0,X1,X2] : meet(meet(meet(X0,X1),X2),meet(X1,X0)) = meet(meet(X0,X1),X2),
inference(paramodulation,[status(thm)],[f433,f1683]) ).
fof(f2104,plain,
! [X0,X1,X2,X3] : meet(meet(X0,X1),meet(join(X2,X0),join(X3,meet(join(X2,X0),meet(X0,X1))))) = meet(meet(X0,X1),join(X2,X0)),
inference(paramodulation,[status(thm)],[f1683,f924]) ).
fof(f2145,plain,
! [X0,X1,X2] : meet(meet(X0,X1),join(meet(X1,X0),X2)) = meet(X1,X0),
inference(backward_demodulation,[status(thm)],[f2146,f880]) ).
fof(f2146,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X1,X0),X2)) = meet(meet(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f11,f2088]) ).
fof(f2162,plain,
! [X0,X1,X2,X3] : meet(meet(X0,X1),meet(join(X2,X0),join(X3,meet(X0,X1)))) = meet(meet(X0,X1),join(X2,X0)),
inference(forward_demodulation,[status(thm)],[f2064,f2104]) ).
fof(f2163,plain,
! [X0,X1,X2,X3] : meet(meet(X0,X1),meet(join(X2,X0),join(X3,meet(X0,X1)))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f1683,f2162]) ).
fof(f2566,plain,
! [X0,X1,X2] : join(join(X0,meet(X1,X2)),meet(X2,X1)) = join(X0,meet(X1,X2)),
inference(paramodulation,[status(thm)],[f1506,f129]) ).
fof(f2687,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(X2,meet(X1,X0))) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f12,f2566]) ).
fof(f2724,plain,
! [X0,X1,X2] : join(meet(X0,X1),join(meet(X2,meet(X0,X1)),meet(X1,X0))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f901,f149]) ).
fof(f2786,plain,
! [X0,X1,X2] : join(meet(X0,meet(X1,X2)),meet(X2,X1)) = meet(X1,X2),
inference(forward_demodulation,[status(thm)],[f2687,f2724]) ).
fof(f2788,plain,
! [X0,X1,X2] : join(meet(X0,X1),meet(X2,meet(X1,X0))) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f12,f2786]) ).
fof(f2890,plain,
! [X0,X1,X2] : join(meet(X0,X1),meet(meet(X1,X0),X2)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f11,f2788]) ).
fof(f3840,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X0,X1),X2)) = meet(meet(X1,X0),X2),
inference(paramodulation,[status(thm)],[f11,f2146]) ).
fof(f4008,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(forward_demodulation,[status(thm)],[f344,f3840]) ).
fof(f6560,plain,
! [X0,X1,X2] : meet(meet(X0,meet(X1,X2)),X2) = meet(X0,meet(X1,X2)),
inference(paramodulation,[status(thm)],[f129,f1684]) ).
fof(f6670,plain,
! [X0,X1,X2] : meet(X0,meet(X1,meet(X2,X0))) = meet(X1,meet(X2,X0)),
inference(forward_demodulation,[status(thm)],[f11,f6560]) ).
fof(f9545,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(join(X2,X0),X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f129,f2163]) ).
fof(f9985,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(join(X2,X1),X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f11,f9545]) ).
fof(f10006,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X1,join(X2,X0))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f11,f9545]) ).
fof(f10014,plain,
! [X0,X1,X2] : meet(meet(meet(X0,X1),X2),meet(meet(X1,X0),X2)) = meet(meet(X0,X1),X2),
inference(paramodulation,[status(thm)],[f433,f9545]) ).
fof(f10015,plain,
! [X0,X1,X2] : meet(meet(meet(X0,X1),X2),meet(X0,X2)) = meet(meet(X0,X1),X2),
inference(paramodulation,[status(thm)],[f364,f9545]) ).
fof(f10145,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X0,X2),X1)) = meet(meet(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f11,f10015]) ).
fof(f10348,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,join(X2,X1))) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f11,f9985]) ).
fof(f13623,plain,
! [X0,X1,X2] : meet(meet(X0,meet(X1,X2)),meet(X0,X1)) = meet(meet(X1,X2),X0),
inference(paramodulation,[status(thm)],[f364,f10348]) ).
fof(f13893,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,meet(X1,X2))) = meet(meet(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f11,f13623]) ).
fof(f15838,plain,
! [X0,X1,X2] : meet(meet(X0,meet(X1,join(X2,meet(X1,X0)))),meet(X0,X1)) = meet(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(paramodulation,[status(thm)],[f924,f10145]) ).
fof(f15845,plain,
! [X0,X1,X2] : meet(meet(X0,meet(X1,join(X2,X0))),meet(X0,X1)) = meet(meet(X0,X1),meet(X1,join(X2,X0))),
inference(paramodulation,[status(thm)],[f10006,f10145]) ).
fof(f15870,plain,
! [X0,X1,X2,X3] : meet(meet(meet(X0,X1),X2),meet(meet(X1,X0),X2)) = meet(meet(meet(X0,X1),join(meet(X1,X0),X3)),X2),
inference(paramodulation,[status(thm)],[f2145,f10145]) ).
fof(f15920,plain,
! [X0,X1,X2] : join(meet(X0,X1),meet(meet(X1,X2),X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f10145,f2890]) ).
fof(f16117,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,meet(X1,join(X2,meet(X1,X0))))) = meet(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[status(thm)],[f11,f15838]) ).
fof(f16118,plain,
! [X0,X1,X2] : meet(meet(X0,join(X1,meet(X0,X2))),X2) = meet(meet(X2,X0),meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f13893,f16117]) ).
fof(f16119,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(X2,meet(X1,X0)))) = meet(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[status(thm)],[f11,f16118]) ).
fof(f16120,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(X2,meet(X1,X0)))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f924,f16119]) ).
fof(f16189,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,meet(X1,join(X2,X0)))) = meet(meet(X0,X1),meet(X1,join(X2,X0))),
inference(forward_demodulation,[status(thm)],[f11,f15845]) ).
fof(f16190,plain,
! [X0,X1,X2] : meet(meet(X0,join(X1,X2)),X2) = meet(meet(X2,X0),meet(X0,join(X1,X2))),
inference(forward_demodulation,[status(thm)],[f13893,f16189]) ).
fof(f16191,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(X2,X0))) = meet(meet(X0,X1),meet(X1,join(X2,X0))),
inference(forward_demodulation,[status(thm)],[f11,f16190]) ).
fof(f16278,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(X2,X0))) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f10006,f16191]) ).
fof(f16329,plain,
! [X0,X1,X2,X3] : meet(meet(X0,X1),X2) = meet(meet(meet(X0,X1),join(meet(X1,X0),X3)),X2),
inference(forward_demodulation,[status(thm)],[f10014,f15870]) ).
fof(f16330,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(meet(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f2145,f16329]) ).
fof(f16944,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X2,X1)) = meet(meet(X0,X1),X2),
inference(paramodulation,[status(thm)],[f129,f16278]) ).
fof(f17062,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,X2)) = meet(meet(X0,X2),X1),
inference(backward_demodulation,[status(thm)],[f16944,f10145]) ).
fof(f22446,plain,
! [X0,X1,X2] : meet(X0,meet(meet(X1,X2),meet(X1,X0))) = meet(X0,meet(X1,X2)),
inference(paramodulation,[status(thm)],[f15920,f16120]) ).
fof(f22447,plain,
! [X0,X1,X2] : meet(meet(X0,meet(X1,X2)),meet(X1,X0)) = meet(X0,meet(X1,X2)),
inference(paramodulation,[status(thm)],[f15920,f1506]) ).
fof(f22659,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,X2)) = meet(X2,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f6670,f22446]) ).
fof(f23044,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(backward_demodulation,[status(thm)],[f23053,f16330]) ).
fof(f23053,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(forward_demodulation,[status(thm)],[f17062,f22659]) ).
fof(f23054,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(meet(X0,X2),X1)) = meet(X1,meet(X0,X2)),
inference(forward_demodulation,[status(thm)],[f4008,f22447]) ).
fof(f23055,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X0,X2)) = meet(X1,meet(X0,X2)),
inference(forward_demodulation,[status(thm)],[f16944,f23054]) ).
fof(f23056,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X2,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f17062,f23055]) ).
fof(f23057,plain,
meet(b,meet(a,c)) != meet(a,meet(b,c)),
inference(backward_demodulation,[status(thm)],[f23075,f24]) ).
fof(f23075,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f23053,f23056]) ).
fof(f24229,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,X2)),
inference(forward_demodulation,[status(thm)],[f23053,f23044]) ).
fof(f24235,plain,
meet(a,meet(b,c)) != meet(a,meet(b,c)),
inference(forward_demodulation,[status(thm)],[f24229,f23057]) ).
fof(f24236,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f24235]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 23:05:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 97.62/12.82 % Refutation found
% 97.62/12.82 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 97.62/12.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.81/12.95 % Elapsed time: 12.563620 seconds
% 19.81/12.95 % CPU time: 99.196216 seconds
% 19.81/12.95 % Total memory used: 702.492 MB
% 19.81/12.95 % Net memory used: 679.319 MB
%------------------------------------------------------------------------------