%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT089-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:11 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.53s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 6
% Syntax : Number of formulae : 108 ( 108 unt; 0 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 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 200 ( 200 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : join(meet(A,B),meet(A,join(A,B))) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : join(meet(A,A),meet(B,join(A,A))) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : join(meet(A,B),meet(B,join(A,B))) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B,C] : meet(meet(join(A,B),join(C,A)),A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : join(join(meet(A,B),meet(C,A)),A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
meet(b,a) != meet(a,b),
file('/export/starexec/sandbox2/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,
meet(b,a) != meet(a,b),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f16,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X0,join(X0,X1))),meet(meet(X0,X1),X0)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f7,f7]) ).
fof(f20,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(f23,plain,
! [X0,X1,X2] : join(meet(join(meet(X0,X1),meet(X2,X0)),X0),meet(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f11,f9]) ).
fof(f30,plain,
! [X0,X1,X2,X3] : meet(meet(X0,join(X1,join(meet(X0,X2),meet(X3,X0)))),join(meet(X0,X2),meet(X3,X0))) = join(meet(X0,X2),meet(X3,X0)),
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f34,plain,
! [X0,X1] : meet(meet(join(X0,X1),X0),X0) = X0,
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f40,plain,
! [X0,X1] : join(join(meet(X0,X1),X0),X0) = X0,
inference(paramodulation,[status(thm)],[f10,f11]) ).
fof(f67,plain,
! [X0,X1] : join(meet(join(meet(X0,X1),X0),X0),meet(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f40,f9]) ).
fof(f68,plain,
! [X0,X1] : join(meet(join(meet(X0,X1),X0),X0),meet(join(meet(X0,X1),X0),X0)) = join(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f40,f7]) ).
fof(f70,plain,
! [X0,X1] : meet(meet(X0,join(meet(X0,X1),X0)),join(meet(X0,X1),X0)) = join(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f40,f34]) ).
fof(f73,plain,
! [X0,X1] : meet(meet(X0,meet(X1,X0)),meet(X1,X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f9,f34]) ).
fof(f77,plain,
! [X0,X1] : join(join(X0,meet(join(X0,X1),X0)),meet(join(X0,X1),X0)) = meet(join(X0,X1),X0),
inference(paramodulation,[status(thm)],[f34,f40]) ).
fof(f98,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,f73]) ).
fof(f105,plain,
! [X0,X1] : join(join(meet(X0,X1),meet(X1,meet(X0,X1))),meet(X1,meet(X0,X1))) = meet(X1,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f73,f40]) ).
fof(f112,plain,
! [X0,X1,X2] : meet(meet(X0,X0),X0) = meet(meet(join(X0,X1),join(X2,X0)),X0),
inference(forward_demodulation,[status(thm)],[f10,f98]) ).
fof(f117,plain,
! [X0,X1] : join(meet(meet(X0,X0),meet(X1,join(X0,X0))),X0) = meet(X0,X0),
inference(backward_demodulation,[status(thm)],[f118,f20]) ).
fof(f118,plain,
! [X0] : meet(meet(X0,X0),X0) = X0,
inference(forward_demodulation,[status(thm)],[f10,f112]) ).
fof(f141,plain,
! [X0] : join(X0,meet(X0,join(meet(X0,X0),X0))) = X0,
inference(paramodulation,[status(thm)],[f118,f9]) ).
fof(f152,plain,
! [X0,X1] : meet(meet(X0,join(X1,X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f141,f10]) ).
fof(f153,plain,
! [X0] : join(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)) = meet(X0,join(meet(X0,X0),X0)),
inference(paramodulation,[status(thm)],[f141,f9]) ).
fof(f154,plain,
! [X0] : join(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f141,f7]) ).
fof(f156,plain,
! [X0] : join(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0) = meet(X0,join(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f152,f153]) ).
fof(f159,plain,
! [X0] : meet(meet(meet(X0,X0),X0),meet(X0,X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f67,f152]) ).
fof(f162,plain,
! [X0,X1] : meet(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(X1,X0))) = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f9,f152]) ).
fof(f174,plain,
! [X0,X1] : join(X0,meet(X0,join(meet(X0,join(X1,X0)),X0))) = X0,
inference(paramodulation,[status(thm)],[f152,f9]) ).
fof(f177,plain,
! [X0,X1] : join(X0,meet(meet(X0,join(X1,X0)),join(meet(X0,join(X1,X0)),X0))) = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f152,f7]) ).
fof(f179,plain,
! [X0] : meet(X0,meet(X0,X0)) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f118,f159]) ).
fof(f180,plain,
! [X0] : join(meet(X0,join(meet(X0,X0),X0)),meet(X0,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f183,f154]) ).
fof(f181,plain,
! [X0] : join(meet(X0,join(meet(X0,X0),X0)),X0) = meet(X0,join(meet(X0,X0),X0)),
inference(backward_demodulation,[status(thm)],[f183,f156]) ).
fof(f183,plain,
! [X0,X1] : meet(X0,meet(X0,join(X1,X0))) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f152,f162]) ).
fof(f196,plain,
! [X0] : meet(meet(X0,X0),meet(X0,X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f179,f73]) ).
fof(f230,plain,
! [X0] : join(meet(meet(meet(X0,X0),meet(X0,X0)),meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0)))),meet(meet(X0,X0),meet(X0,X0))) = meet(meet(X0,X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f196,f16]) ).
fof(f233,plain,
! [X0,X1] : join(meet(X0,X0),meet(X1,join(meet(X0,X0),meet(X0,X0)))) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f196,f8]) ).
fof(f241,plain,
! [X0] : join(meet(meet(X0,X0),meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0)))),meet(meet(X0,X0),meet(X0,X0))) = meet(meet(X0,X0),meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f196,f230]) ).
fof(f242,plain,
! [X0] : join(meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0))),meet(meet(X0,X0),meet(X0,X0))) = meet(meet(X0,X0),meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f183,f241]) ).
fof(f243,plain,
! [X0] : join(meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0))),meet(X0,X0)) = meet(meet(X0,X0),meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f196,f242]) ).
fof(f244,plain,
! [X0] : join(meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0))),meet(X0,X0)) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f196,f243]) ).
fof(f489,plain,
! [X0] : join(meet(meet(X0,X0),join(meet(meet(X0,X0),meet(X0,X0)),meet(X0,X0))),meet(X0,X0)) = meet(X0,X0),
inference(paramodulation,[status(thm)],[f196,f180]) ).
fof(f490,plain,
! [X0] : join(meet(X0,X0),meet(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f180,f23]) ).
fof(f493,plain,
! [X0] : join(X0,X0) = X0,
inference(paramodulation,[status(thm)],[f180,f11]) ).
fof(f503,plain,
! [X0] : meet(meet(X0,X0),join(meet(meet(X0,X0),meet(X0,X0)),meet(X0,X0))) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f181,f489]) ).
fof(f504,plain,
! [X0] : join(meet(X0,X0),meet(X0,X0)) = meet(X0,X0),
inference(backward_demodulation,[status(thm)],[f505,f244]) ).
fof(f505,plain,
! [X0] : meet(meet(X0,X0),join(meet(X0,X0),meet(X0,X0))) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f196,f503]) ).
fof(f507,plain,
! [X0,X1] : join(meet(X0,X0),meet(X1,X0)) = meet(X0,X0),
inference(backward_demodulation,[status(thm)],[f490,f233]) ).
fof(f522,plain,
! [X0,X1] : meet(join(meet(X0,X1),X0),X0) = join(meet(X0,X1),X0),
inference(backward_demodulation,[status(thm)],[f493,f68]) ).
fof(f541,plain,
! [X0,X1] : join(meet(meet(X0,X0),meet(X1,X0)),X0) = meet(X0,X0),
inference(backward_demodulation,[status(thm)],[f493,f117]) ).
fof(f613,plain,
! [X0] : X0 = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f490,f504]) ).
fof(f615,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f613,f507]) ).
fof(f616,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,meet(X0,X1))) = meet(X1,meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f618,f105]) ).
fof(f617,plain,
! [X0,X1] : join(X0,meet(join(X0,X1),X0)) = meet(join(X0,X1),X0),
inference(backward_demodulation,[status(thm)],[f618,f77]) ).
fof(f618,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f613,f615]) ).
fof(f671,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),X0) = meet(X0,X0),
inference(forward_demodulation,[status(thm)],[f613,f541]) ).
fof(f672,plain,
! [X0,X1] : join(meet(X0,meet(X1,X0)),X0) = X0,
inference(forward_demodulation,[status(thm)],[f613,f671]) ).
fof(f772,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(backward_demodulation,[status(thm)],[f777,f672]) ).
fof(f777,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f618,f616]) ).
fof(f783,plain,
! [X0,X1] : X0 = meet(join(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f618,f617]) ).
fof(f843,plain,
! [X0,X1] : join(meet(meet(X0,meet(X1,X0)),meet(X0,X0)),meet(meet(X0,meet(X1,X0)),X0)) = meet(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f618,f16]) ).
fof(f848,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,X1)),meet(meet(X1,meet(X0,X1)),X1)) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f777,f843]) ).
fof(f849,plain,
! [X0,X1] : join(meet(meet(X0,X1),X1),meet(meet(X1,meet(X0,X1)),X1)) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f613,f848]) ).
fof(f850,plain,
! [X0,X1] : join(meet(meet(X0,X1),X1),meet(meet(X0,X1),X1)) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f777,f849]) ).
fof(f851,plain,
! [X0,X1] : meet(meet(X0,X1),X1) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f493,f850]) ).
fof(f854,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),X0)) = join(meet(X0,X1),X0),
inference(backward_demodulation,[status(thm)],[f858,f70]) ).
fof(f858,plain,
! [X0,X1] : meet(meet(X0,X1),X1) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f777,f851]) ).
fof(f864,plain,
! [X0,X1] : join(X0,join(meet(X0,join(X1,X0)),X0)) = X0,
inference(backward_demodulation,[status(thm)],[f854,f174]) ).
fof(f896,plain,
! [X0,X1] : join(meet(meet(join(X0,X1),X0),meet(join(X0,X1),join(join(X0,X1),X0))),meet(X0,join(X0,X1))) = meet(join(X0,X1),X0),
inference(paramodulation,[status(thm)],[f783,f16]) ).
fof(f901,plain,
! [X0,X1] : join(X0,meet(join(X0,X1),join(join(X0,X1),X0))) = join(X0,X1),
inference(paramodulation,[status(thm)],[f783,f7]) ).
fof(f902,plain,
! [X0,X1] : join(meet(X0,meet(join(X0,X1),join(join(X0,X1),X0))),meet(X0,join(X0,X1))) = meet(join(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f783,f896]) ).
fof(f903,plain,
! [X0,X1] : join(meet(X0,meet(join(X0,X1),join(join(X0,X1),X0))),meet(X0,join(X0,X1))) = X0,
inference(forward_demodulation,[status(thm)],[f783,f902]) ).
fof(f1015,plain,
! [X0,X1] : join(meet(meet(X0,join(meet(X0,join(X1,X0)),X0)),meet(X0,X0)),meet(meet(X0,join(meet(X0,join(X1,X0)),X0)),X0)) = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(paramodulation,[status(thm)],[f864,f16]) ).
fof(f1030,plain,
! [X0,X1] : join(meet(join(meet(X0,join(X1,X0)),X0),meet(X0,X0)),meet(meet(X0,join(meet(X0,join(X1,X0)),X0)),X0)) = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(forward_demodulation,[status(thm)],[f854,f1015]) ).
fof(f1031,plain,
! [X0,X1] : join(meet(join(meet(X0,join(X1,X0)),X0),X0),meet(meet(X0,join(meet(X0,join(X1,X0)),X0)),X0)) = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(forward_demodulation,[status(thm)],[f613,f1030]) ).
fof(f1032,plain,
! [X0,X1] : join(join(meet(X0,join(X1,X0)),X0),meet(meet(X0,join(meet(X0,join(X1,X0)),X0)),X0)) = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(forward_demodulation,[status(thm)],[f522,f1031]) ).
fof(f1033,plain,
! [X0,X1] : join(join(meet(X0,join(X1,X0)),X0),X0) = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(forward_demodulation,[status(thm)],[f152,f1032]) ).
fof(f1034,plain,
! [X0,X1] : X0 = meet(X0,join(meet(X0,join(X1,X0)),X0)),
inference(forward_demodulation,[status(thm)],[f40,f1033]) ).
fof(f1036,plain,
! [X0,X1] : join(X0,meet(meet(X0,join(X1,X0)),X0)) = meet(X0,join(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1038,f177]) ).
fof(f1038,plain,
! [X0,X1] : X0 = join(meet(X0,join(X1,X0)),X0),
inference(forward_demodulation,[status(thm)],[f854,f1034]) ).
fof(f1051,plain,
! [X0,X1] : X0 = join(meet(X0,X1),X0),
inference(backward_demodulation,[status(thm)],[f1062,f854]) ).
fof(f1062,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f618,f1036]) ).
fof(f1083,plain,
! [X0,X1,X2] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X0,X1),join(X2,X0))),
inference(paramodulation,[status(thm)],[f10,f1051]) ).
fof(f1093,plain,
! [X0,X1] : join(meet(meet(X0,X1),X0),meet(meet(X0,X1),X0)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f1051,f7]) ).
fof(f1095,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),X0)) = join(X0,X1),
inference(backward_demodulation,[status(thm)],[f1083,f901]) ).
fof(f1109,plain,
! [X0,X1] : meet(meet(X0,X1),X0) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f493,f1093]) ).
fof(f1110,plain,
! [X0,X1] : join(meet(X0,join(X0,X1)),meet(X0,join(X0,X1))) = X0,
inference(backward_demodulation,[status(thm)],[f1095,f903]) ).
fof(f1118,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f493,f1110]) ).
fof(f1130,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X1,X0),
inference(paramodulation,[status(thm)],[f1062,f772]) ).
fof(f1150,plain,
! [X0,X1] : join(join(X0,X1),X0) = join(X0,X1),
inference(paramodulation,[status(thm)],[f1118,f618]) ).
fof(f1650,plain,
! [X0,X1,X2] : join(X0,join(meet(X0,X1),meet(X2,X0))) = join(join(meet(X0,X1),meet(X2,X0)),X0),
inference(paramodulation,[status(thm)],[f11,f1150]) ).
fof(f1672,plain,
! [X0,X1,X2] : join(X0,join(meet(X0,X1),meet(X2,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f11,f1650]) ).
fof(f1801,plain,
! [X0,X1,X2] : join(X0,join(meet(X1,X0),meet(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f777,f1672]) ).
fof(f2271,plain,
! [X0,X1,X2] : join(X0,join(meet(X1,X0),meet(X0,X2))) = X0,
inference(paramodulation,[status(thm)],[f1109,f1801]) ).
fof(f2525,plain,
! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),meet(X1,X0))) = join(meet(X0,X1),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f2271,f30]) ).
fof(f2554,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1118,f2525]) ).
fof(f2614,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = join(meet(X1,X0),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f2554,f1130]) ).
fof(f2668,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(forward_demodulation,[status(thm)],[f2554,f2614]) ).
fof(f2677,plain,
meet(b,a) != meet(b,a),
inference(backward_demodulation,[status(thm)],[f2716,f12]) ).
fof(f2716,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f2554,f2668]) ).
fof(f2722,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f2677]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT089-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 23:10:06 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.53 % Refutation found
% 0.12/0.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.56 % Elapsed time: 0.188832 seconds
% 0.12/0.56 % CPU time: 1.337533 seconds
% 0.12/0.56 % Total memory used: 60.402 MB
% 0.12/0.56 % Net memory used: 58.010 MB
%------------------------------------------------------------------------------