%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT155-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 : 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:17 PM UTC 2026
% Result : Unsatisfiable 213.11s 27.43s
% Output : CNFRefutation 213.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 19
% Syntax : Number of formulae : 177 ( 177 unt; 10 def)
% Number of atoms : 177 ( 176 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 : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 130 ( 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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,join(X,U)))) = meet(X,join(Y,join(meet(X,Z),meet(Z,join(Y,U))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
meet(a,join(b,meet(a,c))) != meet(a,join(b,meet(c,join(meet(a,join(b,c)),meet(b,c))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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,join(X0,X3)))) = meet(X0,join(X1,join(meet(X0,X2),meet(X2,join(X1,X3))))),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
meet(a,join(b,meet(a,c))) != meet(a,join(b,meet(c,join(meet(a,join(b,c)),meet(b,c))))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f21,definition,
sF2_fnc = meet(a,c),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f22,definition,
sF1_fnc = join(b,sF2_fnc),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f23,definition,
sF0_fnc = meet(a,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f24,definition,
sF8_fnc = join(b,c),
introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition]) ).
fof(f25,definition,
sF7_fnc = meet(a,sF8_fnc),
introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition]) ).
fof(f26,definition,
sF9_fnc = meet(b,c),
introduced(definition,[new_symbols(definition,[sF9_fnc])],[function_definition]) ).
fof(f27,definition,
sF6_fnc = join(sF7_fnc,sF9_fnc),
introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition]) ).
fof(f28,definition,
sF5_fnc = meet(c,sF6_fnc),
introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition]) ).
fof(f29,definition,
sF4_fnc = join(b,sF5_fnc),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f30,definition,
sF3_fnc = meet(a,sF4_fnc),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f31,plain,
sF0_fnc != sF3_fnc,
inference(definition_folding,[],[f20,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21]) ).
fof(f38,plain,
! [X0,X1] : meet(X0,join(b,meet(X1,join(X0,sF2_fnc)))) = meet(X0,join(b,join(meet(X0,X1),meet(X1,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f22,f19]) ).
fof(f56,plain,
meet(sF7_fnc,sF6_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f27,f13]) ).
fof(f57,plain,
meet(b,sF1_fnc) = b,
inference(paramodulation,[status(thm)],[f22,f13]) ).
fof(f65,plain,
meet(b,sF8_fnc) = b,
inference(paramodulation,[status(thm)],[f24,f13]) ).
fof(f66,plain,
! [X0,X1] : meet(X0,join(b,meet(X1,join(X0,c)))) = meet(X0,join(b,join(meet(X0,X1),meet(X1,sF8_fnc)))),
inference(paramodulation,[status(thm)],[f24,f19]) ).
fof(f71,plain,
sF2_fnc = meet(c,a),
inference(paramodulation,[status(thm)],[f21,f15]) ).
fof(f73,plain,
meet(sF6_fnc,sF7_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f15,f56]) ).
fof(f83,plain,
! [X0] : join(sF6_fnc,X0) = join(sF7_fnc,join(sF9_fnc,X0)),
inference(paramodulation,[status(thm)],[f27,f18]) ).
fof(f84,plain,
! [X0] : join(sF8_fnc,X0) = join(b,join(c,X0)),
inference(paramodulation,[status(thm)],[f24,f18]) ).
fof(f85,plain,
! [X0] : join(sF4_fnc,X0) = join(b,join(sF5_fnc,X0)),
inference(paramodulation,[status(thm)],[f29,f18]) ).
fof(f86,plain,
! [X0] : join(sF1_fnc,X0) = join(b,join(sF2_fnc,X0)),
inference(paramodulation,[status(thm)],[f22,f18]) ).
fof(f107,plain,
join(b,sF9_fnc) = b,
inference(paramodulation,[status(thm)],[f26,f14]) ).
fof(f108,plain,
join(c,sF2_fnc) = c,
inference(paramodulation,[status(thm)],[f71,f14]) ).
fof(f109,plain,
join(c,sF5_fnc) = c,
inference(paramodulation,[status(thm)],[f28,f14]) ).
fof(f110,plain,
join(a,sF2_fnc) = a,
inference(paramodulation,[status(thm)],[f21,f14]) ).
fof(f117,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f15,f14]) ).
fof(f131,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(paramodulation,[status(thm)],[f18,f16]) ).
fof(f137,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f16,f13]) ).
fof(f140,plain,
! [X0,X1,X2,X3] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,join(meet(X2,join(X1,X3)),meet(X0,X2)))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f141,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f148,plain,
! [X0] : join(b,X0) = join(b,join(sF9_fnc,X0)),
inference(paramodulation,[status(thm)],[f107,f18]) ).
fof(f165,plain,
! [X0] : meet(sF5_fnc,X0) = meet(c,meet(sF6_fnc,X0)),
inference(paramodulation,[status(thm)],[f28,f17]) ).
fof(f167,plain,
! [X0] : meet(sF7_fnc,X0) = meet(a,meet(sF8_fnc,X0)),
inference(paramodulation,[status(thm)],[f25,f17]) ).
fof(f173,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f176,plain,
! [X0,X1,X2] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f17,f13]) ).
fof(f218,plain,
join(sF8_fnc,b) = sF8_fnc,
inference(paramodulation,[status(thm)],[f65,f117]) ).
fof(f220,plain,
join(sF1_fnc,b) = sF1_fnc,
inference(paramodulation,[status(thm)],[f57,f117]) ).
fof(f221,plain,
join(c,sF9_fnc) = c,
inference(paramodulation,[status(thm)],[f26,f117]) ).
fof(f225,plain,
join(sF8_fnc,sF7_fnc) = sF8_fnc,
inference(paramodulation,[status(thm)],[f25,f117]) ).
fof(f229,plain,
! [X0,X1] : join(join(X0,X1),X0) = join(X0,X1),
inference(paramodulation,[status(thm)],[f13,f117]) ).
fof(f240,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X0,X1),
inference(forward_demodulation,[status(thm)],[f18,f229]) ).
fof(f255,plain,
sF8_fnc = join(b,sF8_fnc),
inference(paramodulation,[status(thm)],[f218,f16]) ).
fof(f269,plain,
join(b,sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f16,f220]) ).
fof(f325,plain,
meet(sF2_fnc,a) = sF2_fnc,
inference(paramodulation,[status(thm)],[f110,f137]) ).
fof(f331,plain,
meet(sF2_fnc,c) = sF2_fnc,
inference(paramodulation,[status(thm)],[f108,f137]) ).
fof(f332,plain,
! [X0,X1,X2] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f18,f137]) ).
fof(f338,plain,
meet(c,sF8_fnc) = c,
inference(paramodulation,[status(thm)],[f24,f137]) ).
fof(f340,plain,
meet(sF2_fnc,sF1_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f22,f137]) ).
fof(f342,plain,
! [X0,X1] : meet(meet(X0,X1),X0) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f14,f137]) ).
fof(f348,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,join(X0,X2)))) = meet(X0,join(X1,join(meet(X0,X2),X2))),
inference(paramodulation,[status(thm)],[f137,f19]) ).
fof(f354,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f17,f342]) ).
fof(f358,plain,
! [X0,X1,X2] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(meet(X0,X2),X2))),
inference(forward_demodulation,[status(thm)],[f137,f348]) ).
fof(f368,plain,
join(sF1_fnc,sF2_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f340,f117]) ).
fof(f410,plain,
sF2_fnc = meet(c,sF2_fnc),
inference(paramodulation,[status(thm)],[f331,f15]) ).
fof(f1637,plain,
join(sF2_fnc,sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f368,f16]) ).
fof(f3114,plain,
join(sF8_fnc,sF9_fnc) = join(b,c),
inference(paramodulation,[status(thm)],[f221,f84]) ).
fof(f3115,plain,
join(sF8_fnc,sF5_fnc) = join(b,c),
inference(paramodulation,[status(thm)],[f109,f84]) ).
fof(f3116,plain,
join(sF8_fnc,sF2_fnc) = join(b,c),
inference(paramodulation,[status(thm)],[f108,f84]) ).
fof(f3138,plain,
join(sF8_fnc,sF2_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f24,f3116]) ).
fof(f3139,plain,
join(sF8_fnc,sF5_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f24,f3115]) ).
fof(f3146,plain,
join(sF8_fnc,sF9_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f24,f3114]) ).
fof(f3159,plain,
join(sF2_fnc,sF8_fnc) = sF8_fnc,
inference(paramodulation,[status(thm)],[f16,f3138]) ).
fof(f3211,plain,
meet(sF5_fnc,sF8_fnc) = sF5_fnc,
inference(paramodulation,[status(thm)],[f3139,f137]) ).
fof(f3271,plain,
meet(sF9_fnc,sF8_fnc) = sF9_fnc,
inference(paramodulation,[status(thm)],[f3146,f137]) ).
fof(f4350,plain,
meet(sF9_fnc,join(b,meet(sF8_fnc,join(sF9_fnc,sF2_fnc)))) = meet(sF9_fnc,join(b,join(sF9_fnc,meet(sF8_fnc,sF1_fnc)))),
inference(paramodulation,[status(thm)],[f3271,f38]) ).
fof(f4358,plain,
meet(sF9_fnc,join(b,meet(sF8_fnc,join(sF9_fnc,sF2_fnc)))) = meet(sF9_fnc,join(b,meet(sF8_fnc,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f148,f4350]) ).
fof(f4397,plain,
meet(sF2_fnc,join(b,meet(a,join(sF2_fnc,c)))) = meet(sF2_fnc,join(b,join(sF2_fnc,meet(a,sF8_fnc)))),
inference(paramodulation,[status(thm)],[f325,f66]) ).
fof(f4449,plain,
! [X0] : meet(X0,join(b,meet(sF5_fnc,join(X0,c)))) = meet(X0,join(b,join(meet(X0,sF5_fnc),sF5_fnc))),
inference(paramodulation,[status(thm)],[f3211,f66]) ).
fof(f4495,plain,
meet(sF2_fnc,join(b,meet(a,join(sF2_fnc,c)))) = meet(sF2_fnc,join(sF1_fnc,meet(a,sF8_fnc))),
inference(forward_demodulation,[status(thm)],[f86,f4397]) ).
fof(f4496,plain,
meet(sF2_fnc,join(b,meet(a,join(sF2_fnc,c)))) = meet(sF2_fnc,join(sF1_fnc,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f25,f4495]) ).
fof(f4644,plain,
! [X0] : meet(X0,join(b,meet(sF5_fnc,join(X0,c)))) = meet(X0,join(b,sF5_fnc)),
inference(forward_demodulation,[status(thm)],[f358,f4449]) ).
fof(f4645,plain,
! [X0] : meet(X0,join(b,meet(sF5_fnc,join(X0,c)))) = meet(X0,sF4_fnc),
inference(forward_demodulation,[status(thm)],[f29,f4644]) ).
fof(f6004,plain,
join(sF1_fnc,sF8_fnc) = join(b,sF8_fnc),
inference(paramodulation,[status(thm)],[f3159,f86]) ).
fof(f6055,plain,
join(sF1_fnc,sF8_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f255,f6004]) ).
fof(f6121,plain,
meet(sF1_fnc,sF8_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f6055,f13]) ).
fof(f6186,plain,
meet(sF8_fnc,sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f6121,f15]) ).
fof(f6189,plain,
meet(sF9_fnc,join(b,meet(sF8_fnc,join(sF9_fnc,sF2_fnc)))) = meet(sF9_fnc,join(b,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f6186,f4358]) ).
fof(f6194,plain,
meet(sF9_fnc,join(b,meet(sF8_fnc,join(sF9_fnc,sF2_fnc)))) = meet(sF9_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f269,f6189]) ).
fof(f8926,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(join(X1,X0),join(X0,X2)),
inference(paramodulation,[status(thm)],[f240,f141]) ).
fof(f9003,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),join(X1,X2)),
inference(forward_demodulation,[status(thm)],[f141,f8926]) ).
fof(f9004,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,join(X1,X2))),
inference(forward_demodulation,[status(thm)],[f141,f9003]) ).
fof(f9459,plain,
! [X0,X1] : meet(sF2_fnc,join(X0,meet(a,join(sF2_fnc,X1)))) = meet(sF2_fnc,join(X0,join(meet(a,join(X0,X1)),sF2_fnc))),
inference(paramodulation,[status(thm)],[f325,f140]) ).
fof(f9462,plain,
! [X0,X1] : meet(sF9_fnc,join(X0,meet(sF8_fnc,join(sF9_fnc,X1)))) = meet(sF9_fnc,join(X0,join(meet(sF8_fnc,join(X0,X1)),sF9_fnc))),
inference(paramodulation,[status(thm)],[f3271,f140]) ).
fof(f9594,plain,
sF9_fnc = meet(sF9_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f9599,f6194]) ).
fof(f9599,plain,
! [X0,X1] : meet(sF9_fnc,join(X0,meet(sF8_fnc,join(sF9_fnc,X1)))) = sF9_fnc,
inference(forward_demodulation,[status(thm)],[f332,f9462]) ).
fof(f9941,plain,
sF2_fnc = meet(sF2_fnc,join(sF1_fnc,sF7_fnc)),
inference(backward_demodulation,[status(thm)],[f9947,f4496]) ).
fof(f9947,plain,
! [X0,X1] : meet(sF2_fnc,join(X0,meet(a,join(sF2_fnc,X1)))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f332,f9459]) ).
fof(f10035,plain,
join(sF1_fnc,sF9_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f9594,f117]) ).
fof(f10497,plain,
! [X0] : join(X0,sF1_fnc) = join(sF2_fnc,join(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f1637,f131]) ).
fof(f10715,plain,
! [X0,X1] : join(X0,join(X1,join(X0,X1))) = join(X0,X1),
inference(paramodulation,[status(thm)],[f131,f12]) ).
fof(f10774,plain,
! [X0,X1] : join(X0,join(X1,X0)) = join(X1,X0),
inference(forward_demodulation,[status(thm)],[f9004,f10715]) ).
fof(f11215,plain,
join(sF9_fnc,sF1_fnc) = join(sF1_fnc,sF9_fnc),
inference(paramodulation,[status(thm)],[f10035,f10774]) ).
fof(f11228,plain,
join(sF9_fnc,sF8_fnc) = join(sF8_fnc,sF9_fnc),
inference(paramodulation,[status(thm)],[f3146,f10774]) ).
fof(f11232,plain,
join(sF7_fnc,sF8_fnc) = join(sF8_fnc,sF7_fnc),
inference(paramodulation,[status(thm)],[f225,f10774]) ).
fof(f11255,plain,
join(sF5_fnc,c) = join(c,sF5_fnc),
inference(paramodulation,[status(thm)],[f109,f10774]) ).
fof(f11279,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(X1,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f117,f10774]) ).
fof(f11338,plain,
join(sF9_fnc,sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f10035,f11215]) ).
fof(f11342,plain,
join(sF5_fnc,c) = c,
inference(forward_demodulation,[status(thm)],[f109,f11255]) ).
fof(f11458,plain,
! [X0,X1] : join(meet(X0,X1),X1) = X1,
inference(forward_demodulation,[status(thm)],[f117,f11279]) ).
fof(f11504,plain,
join(sF9_fnc,sF8_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f3146,f11228]) ).
fof(f11527,plain,
join(sF7_fnc,sF8_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f225,f11232]) ).
fof(f11587,plain,
join(sF4_fnc,c) = join(b,c),
inference(paramodulation,[status(thm)],[f11342,f85]) ).
fof(f11640,plain,
join(sF4_fnc,c) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f24,f11587]) ).
fof(f12429,plain,
! [X0,X1,X2] : meet(meet(X0,X1),X2) = meet(meet(X1,X0),meet(X0,X2)),
inference(paramodulation,[status(thm)],[f354,f173]) ).
fof(f12649,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),meet(X1,X2)),
inference(forward_demodulation,[status(thm)],[f173,f12429]) ).
fof(f12650,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[status(thm)],[f173,f12649]) ).
fof(f13204,plain,
join(sF6_fnc,sF1_fnc) = join(sF7_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f11338,f83]) ).
fof(f14127,plain,
join(sF6_fnc,sF8_fnc) = join(sF7_fnc,sF8_fnc),
inference(paramodulation,[status(thm)],[f11504,f83]) ).
fof(f14189,plain,
join(sF6_fnc,sF8_fnc) = sF8_fnc,
inference(forward_demodulation,[status(thm)],[f11527,f14127]) ).
fof(f14224,plain,
meet(sF4_fnc,sF8_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f11640,f13]) ).
fof(f14717,plain,
meet(sF6_fnc,sF8_fnc) = sF6_fnc,
inference(paramodulation,[status(thm)],[f14189,f13]) ).
fof(f14965,plain,
! [X0,X1] : meet(X0,meet(X1,meet(X0,X1))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f12,f176]) ).
fof(f15161,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f12650,f14965]) ).
fof(f16150,plain,
join(sF2_fnc,join(sF1_fnc,sF7_fnc)) = join(sF1_fnc,sF7_fnc),
inference(paramodulation,[status(thm)],[f9941,f11458]) ).
fof(f16350,plain,
join(sF7_fnc,sF1_fnc) = join(sF1_fnc,sF7_fnc),
inference(forward_demodulation,[status(thm)],[f10497,f16150]) ).
fof(f16365,plain,
join(sF6_fnc,sF1_fnc) = join(sF1_fnc,sF7_fnc),
inference(forward_demodulation,[status(thm)],[f13204,f16350]) ).
fof(f18110,plain,
meet(sF5_fnc,sF7_fnc) = meet(c,sF7_fnc),
inference(paramodulation,[status(thm)],[f73,f165]) ).
fof(f18129,plain,
! [X0] : meet(sF5_fnc,join(sF6_fnc,X0)) = meet(c,sF6_fnc),
inference(paramodulation,[status(thm)],[f13,f165]) ).
fof(f18242,plain,
! [X0] : meet(sF5_fnc,join(sF6_fnc,X0)) = sF5_fnc,
inference(forward_demodulation,[status(thm)],[f28,f18129]) ).
fof(f19490,plain,
meet(sF8_fnc,sF4_fnc) = meet(sF4_fnc,sF8_fnc),
inference(paramodulation,[status(thm)],[f14224,f15161]) ).
fof(f19524,plain,
meet(sF8_fnc,sF6_fnc) = meet(sF6_fnc,sF8_fnc),
inference(paramodulation,[status(thm)],[f14717,f15161]) ).
fof(f19552,plain,
meet(sF8_fnc,c) = meet(c,sF8_fnc),
inference(paramodulation,[status(thm)],[f338,f15161]) ).
fof(f19705,plain,
meet(sF8_fnc,c) = c,
inference(forward_demodulation,[status(thm)],[f338,f19552]) ).
fof(f19715,plain,
meet(sF8_fnc,sF6_fnc) = sF6_fnc,
inference(forward_demodulation,[status(thm)],[f14717,f19524]) ).
fof(f19837,plain,
meet(sF8_fnc,sF4_fnc) = sF4_fnc,
inference(forward_demodulation,[status(thm)],[f14224,f19490]) ).
fof(f25227,plain,
meet(sF7_fnc,c) = meet(a,c),
inference(paramodulation,[status(thm)],[f19705,f167]) ).
fof(f25228,plain,
meet(sF7_fnc,sF4_fnc) = meet(a,sF4_fnc),
inference(paramodulation,[status(thm)],[f19837,f167]) ).
fof(f25230,plain,
meet(sF7_fnc,sF6_fnc) = meet(a,sF6_fnc),
inference(paramodulation,[status(thm)],[f19715,f167]) ).
fof(f25233,plain,
meet(sF7_fnc,sF1_fnc) = meet(a,sF1_fnc),
inference(paramodulation,[status(thm)],[f6186,f167]) ).
fof(f25329,plain,
meet(sF7_fnc,c) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f21,f25227]) ).
fof(f25332,plain,
meet(sF7_fnc,sF1_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f23,f25233]) ).
fof(f25363,plain,
sF7_fnc = meet(a,sF6_fnc),
inference(forward_demodulation,[status(thm)],[f56,f25230]) ).
fof(f25405,plain,
meet(sF7_fnc,sF4_fnc) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f30,f25228]) ).
fof(f25577,plain,
meet(sF6_fnc,sF7_fnc) = meet(sF6_fnc,a),
inference(paramodulation,[status(thm)],[f25363,f354]) ).
fof(f25599,plain,
sF7_fnc = meet(sF6_fnc,a),
inference(forward_demodulation,[status(thm)],[f73,f25577]) ).
fof(f26077,plain,
meet(c,sF2_fnc) = meet(c,sF7_fnc),
inference(paramodulation,[status(thm)],[f25329,f354]) ).
fof(f26094,plain,
meet(sF5_fnc,sF7_fnc) = sF2_fnc,
inference(backward_demodulation,[status(thm)],[f26095,f18110]) ).
fof(f26095,plain,
sF2_fnc = meet(c,sF7_fnc),
inference(forward_demodulation,[status(thm)],[f410,f26077]) ).
fof(f26277,plain,
meet(sF5_fnc,a) = meet(c,sF7_fnc),
inference(paramodulation,[status(thm)],[f25599,f165]) ).
fof(f26325,plain,
meet(sF5_fnc,a) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f26095,f26277]) ).
fof(f27835,plain,
sF2_fnc = meet(sF7_fnc,sF5_fnc),
inference(paramodulation,[status(thm)],[f26094,f15]) ).
fof(f28773,plain,
meet(sF5_fnc,join(b,meet(a,join(sF5_fnc,c)))) = meet(sF5_fnc,join(b,join(sF2_fnc,meet(a,sF8_fnc)))),
inference(paramodulation,[status(thm)],[f26325,f66]) ).
fof(f28802,plain,
meet(sF5_fnc,join(b,meet(a,c))) = meet(sF5_fnc,join(b,join(sF2_fnc,meet(a,sF8_fnc)))),
inference(forward_demodulation,[status(thm)],[f11342,f28773]) ).
fof(f28803,plain,
meet(sF5_fnc,join(b,sF2_fnc)) = meet(sF5_fnc,join(b,join(sF2_fnc,meet(a,sF8_fnc)))),
inference(forward_demodulation,[status(thm)],[f21,f28802]) ).
fof(f28804,plain,
meet(sF5_fnc,sF1_fnc) = meet(sF5_fnc,join(b,join(sF2_fnc,meet(a,sF8_fnc)))),
inference(forward_demodulation,[status(thm)],[f22,f28803]) ).
fof(f28805,plain,
meet(sF5_fnc,sF1_fnc) = meet(sF5_fnc,join(sF1_fnc,meet(a,sF8_fnc))),
inference(forward_demodulation,[status(thm)],[f86,f28804]) ).
fof(f28806,plain,
meet(sF5_fnc,sF1_fnc) = meet(sF5_fnc,join(sF1_fnc,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f25,f28805]) ).
fof(f28807,plain,
meet(sF5_fnc,sF1_fnc) = meet(sF5_fnc,join(sF6_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f16365,f28806]) ).
fof(f28808,plain,
meet(sF5_fnc,sF1_fnc) = sF5_fnc,
inference(forward_demodulation,[status(thm)],[f18242,f28807]) ).
fof(f28993,plain,
meet(sF7_fnc,join(b,meet(sF5_fnc,join(sF7_fnc,c)))) = meet(sF7_fnc,join(b,join(sF2_fnc,meet(sF5_fnc,sF8_fnc)))),
inference(paramodulation,[status(thm)],[f27835,f66]) ).
fof(f29019,plain,
meet(sF7_fnc,sF4_fnc) = meet(sF7_fnc,join(b,join(sF2_fnc,meet(sF5_fnc,sF8_fnc)))),
inference(forward_demodulation,[status(thm)],[f4645,f28993]) ).
fof(f29020,plain,
sF3_fnc = meet(sF7_fnc,join(b,join(sF2_fnc,meet(sF5_fnc,sF8_fnc)))),
inference(forward_demodulation,[status(thm)],[f25405,f29019]) ).
fof(f29021,plain,
sF3_fnc = meet(sF7_fnc,join(sF1_fnc,meet(sF5_fnc,sF8_fnc))),
inference(forward_demodulation,[status(thm)],[f86,f29020]) ).
fof(f29022,plain,
sF3_fnc = meet(sF7_fnc,join(sF1_fnc,sF5_fnc)),
inference(forward_demodulation,[status(thm)],[f3211,f29021]) ).
fof(f29916,plain,
join(sF1_fnc,sF5_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f28808,f117]) ).
fof(f29933,plain,
sF3_fnc = meet(sF7_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f29916,f29022]) ).
fof(f29955,plain,
sF3_fnc = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f29933,f25332]) ).
fof(f29957,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f29955,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT155-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.33 % Computer : n014.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Sun Sep 20 23:16:19 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 % Drodi V4.1.1
% 213.11/27.43 % Refutation found
% 213.11/27.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 213.11/27.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.14/27.66 % Elapsed time: 27.308424 seconds
% 19.14/27.66 % CPU time: 215.249985 seconds
% 19.14/27.66 % Total memory used: 812.705 MB
% 19.14/27.66 % Net memory used: 785.949 MB
%------------------------------------------------------------------------------