%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT152-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 : 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:16 PM UTC 2026
% Result : Unsatisfiable 98.61s 12.91s
% Output : CNFRefutation 18.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 19
% Syntax : Number of formulae : 142 ( 142 unt; 9 def)
% Number of atoms : 142 ( 141 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 : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 113 ( 113 !; 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,join(X,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Z,join(X,Y)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
meet(a,join(b,meet(a,c))) != meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
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,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
meet(a,join(b,meet(a,c))) != meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
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,
sF6_fnc = join(b,sF2_fnc),
introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition]) ).
fof(f25,definition,
sF5_fnc = meet(a,sF6_fnc),
introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition]) ).
fof(f26,definition,
sF8_fnc = join(a,b),
introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition]) ).
fof(f27,definition,
sF7_fnc = meet(c,sF8_fnc),
introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition]) ).
fof(f28,definition,
sF4_fnc = join(sF5_fnc,sF7_fnc),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f29,definition,
sF3_fnc = meet(a,sF4_fnc),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f30,plain,
sF0_fnc != sF3_fnc,
inference(definition_folding,[],[f20,f29,f28,f27,f26,f25,f24,f23,f22,f21]) ).
fof(f31,plain,
sF6_fnc = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f22,f24]) ).
fof(f32,plain,
sF5_fnc = meet(a,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f31,f25]) ).
fof(f33,plain,
sF5_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f23,f32]) ).
fof(f34,plain,
sF4_fnc = join(sF0_fnc,sF7_fnc),
inference(forward_demodulation,[status(thm)],[f33,f28]) ).
fof(f36,plain,
meet(b,sF1_fnc) = b,
inference(paramodulation,[status(thm)],[f22,f13]) ).
fof(f37,plain,
meet(a,sF8_fnc) = a,
inference(paramodulation,[status(thm)],[f26,f13]) ).
fof(f41,plain,
join(a,sF0_fnc) = a,
inference(paramodulation,[status(thm)],[f23,f14]) ).
fof(f42,plain,
join(a,sF2_fnc) = a,
inference(paramodulation,[status(thm)],[f21,f14]) ).
fof(f46,plain,
meet(sF0_fnc,sF4_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f34,f13]) ).
fof(f56,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f15,f14]) ).
fof(f60,plain,
join(sF4_fnc,sF0_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f46,f56]) ).
fof(f61,plain,
join(sF1_fnc,b) = sF1_fnc,
inference(paramodulation,[status(thm)],[f36,f56]) ).
fof(f62,plain,
join(sF8_fnc,sF7_fnc) = sF8_fnc,
inference(paramodulation,[status(thm)],[f27,f56]) ).
fof(f63,plain,
join(sF8_fnc,a) = sF8_fnc,
inference(paramodulation,[status(thm)],[f37,f56]) ).
fof(f64,plain,
join(sF4_fnc,sF3_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f29,f56]) ).
fof(f65,plain,
join(sF1_fnc,sF0_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f23,f56]) ).
fof(f66,plain,
join(c,sF2_fnc) = c,
inference(paramodulation,[status(thm)],[f21,f56]) ).
fof(f78,plain,
sF8_fnc = join(a,sF8_fnc),
inference(paramodulation,[status(thm)],[f63,f16]) ).
fof(f79,plain,
sF8_fnc = join(sF7_fnc,sF8_fnc),
inference(paramodulation,[status(thm)],[f62,f16]) ).
fof(f80,plain,
sF1_fnc = join(b,sF1_fnc),
inference(paramodulation,[status(thm)],[f61,f16]) ).
fof(f81,plain,
sF4_fnc = join(sF0_fnc,sF4_fnc),
inference(paramodulation,[status(thm)],[f60,f16]) ).
fof(f94,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f16,f13]) ).
fof(f100,plain,
join(sF3_fnc,sF4_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f16,f64]) ).
fof(f112,plain,
meet(sF7_fnc,sF8_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f79,f13]) ).
fof(f114,plain,
! [X0,X1,X2] : meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))),
inference(paramodulation,[status(thm)],[f13,f17]) ).
fof(f115,plain,
! [X0,X1,X2] : meet(X0,meet(X1,X2)) = meet(X1,meet(X2,X0)),
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f121,plain,
! [X0] : meet(sF7_fnc,X0) = meet(c,meet(sF8_fnc,X0)),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f124,plain,
! [X0] : meet(sF0_fnc,X0) = meet(a,meet(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f129,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(paramodulation,[status(thm)],[f11,f17]) ).
fof(f131,plain,
! [X0,X1,X2] : join(X0,meet(X1,meet(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f17,f56]) ).
fof(f152,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X2,X0)),
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f168,plain,
! [X0] : join(sF4_fnc,X0) = join(sF0_fnc,join(sF7_fnc,X0)),
inference(paramodulation,[status(thm)],[f34,f18]) ).
fof(f175,plain,
! [X0] : join(sF1_fnc,X0) = join(b,join(sF2_fnc,X0)),
inference(paramodulation,[status(thm)],[f22,f18]) ).
fof(f180,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f12,f18]) ).
fof(f193,plain,
! [X0,X1,X2] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f18,f94]) ).
fof(f202,plain,
meet(sF2_fnc,c) = sF2_fnc,
inference(paramodulation,[status(thm)],[f66,f94]) ).
fof(f208,plain,
meet(sF2_fnc,a) = sF2_fnc,
inference(paramodulation,[status(thm)],[f42,f94]) ).
fof(f209,plain,
meet(sF0_fnc,a) = sF0_fnc,
inference(paramodulation,[status(thm)],[f41,f94]) ).
fof(f213,plain,
meet(sF2_fnc,sF1_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f22,f94]) ).
fof(f215,plain,
! [X0,X1] : meet(meet(X0,X1),X0) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f14,f94]) ).
fof(f221,plain,
! [X0,X1,X2] : meet(X0,X1) = meet(X0,meet(join(X2,X0),X1)),
inference(paramodulation,[status(thm)],[f94,f17]) ).
fof(f226,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f17,f215]) ).
fof(f228,plain,
meet(c,sF2_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f15,f202]) ).
fof(f249,plain,
meet(a,sF2_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f15,f208]) ).
fof(f256,plain,
meet(a,sF0_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f15,f209]) ).
fof(f275,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,join(X0,meet(X2,join(X0,X1)))))) = meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))),
inference(paramodulation,[status(thm)],[f12,f19]) ).
fof(f301,plain,
! [X0,X1] : meet(a,join(b,meet(X0,join(a,X1)))) = meet(a,join(b,meet(X0,join(X1,meet(X0,sF8_fnc))))),
inference(paramodulation,[status(thm)],[f26,f19]) ).
fof(f322,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,join(X0,X0)))) = meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f19,f275]) ).
fof(f323,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f12,f322]) ).
fof(f324,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f129,f323]) ).
fof(f349,plain,
meet(sF1_fnc,sF2_fnc) = sF2_fnc,
inference(paramodulation,[status(thm)],[f15,f213]) ).
fof(f548,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f11,f115]) ).
fof(f814,plain,
meet(sF4_fnc,sF3_fnc) = meet(sF4_fnc,a),
inference(paramodulation,[status(thm)],[f29,f226]) ).
fof(f816,plain,
meet(c,sF2_fnc) = meet(c,a),
inference(paramodulation,[status(thm)],[f21,f226]) ).
fof(f846,plain,
sF2_fnc = meet(c,a),
inference(forward_demodulation,[status(thm)],[f228,f816]) ).
fof(f986,plain,
! [X0,X1,X2,X3] : meet(X0,X1) = meet(X1,meet(join(X2,join(X3,X1)),X0)),
inference(paramodulation,[status(thm)],[f193,f115]) ).
fof(f987,plain,
! [X0,X1,X2,X3] : meet(X0,join(X1,join(X2,X0))) = meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))),
inference(paramodulation,[status(thm)],[f193,f114]) ).
fof(f1000,plain,
! [X0,X1,X2,X3] : X0 = meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))),
inference(forward_demodulation,[status(thm)],[f193,f987]) ).
fof(f1003,plain,
! [X0,X1] : X0 = meet(join(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f986,f1000]) ).
fof(f1011,plain,
sF3_fnc = meet(sF4_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f100,f1003]) ).
fof(f1025,plain,
sF0_fnc = meet(sF4_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f81,f1003]) ).
fof(f1027,plain,
a = meet(sF8_fnc,a),
inference(paramodulation,[status(thm)],[f78,f1003]) ).
fof(f1055,plain,
sF3_fnc = meet(sF4_fnc,a),
inference(backward_demodulation,[status(thm)],[f1011,f814]) ).
fof(f1195,plain,
meet(sF7_fnc,a) = meet(c,a),
inference(paramodulation,[status(thm)],[f1027,f121]) ).
fof(f1205,plain,
meet(sF7_fnc,a) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f846,f1195]) ).
fof(f1247,plain,
join(sF7_fnc,sF2_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f1205,f14]) ).
fof(f1258,plain,
meet(sF0_fnc,sF2_fnc) = meet(a,sF2_fnc),
inference(paramodulation,[status(thm)],[f349,f124]) ).
fof(f1286,plain,
meet(sF0_fnc,sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f249,f1258]) ).
fof(f1377,plain,
join(sF0_fnc,sF2_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f1286,f14]) ).
fof(f1662,plain,
join(sF2_fnc,sF7_fnc) = sF7_fnc,
inference(paramodulation,[status(thm)],[f16,f1247]) ).
fof(f3291,plain,
! [X0] : join(X0,sF1_fnc) = join(sF1_fnc,join(b,X0)),
inference(paramodulation,[status(thm)],[f61,f152]) ).
fof(f3321,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X1,X0)),
inference(paramodulation,[status(thm)],[f12,f152]) ).
fof(f3596,plain,
join(sF4_fnc,sF2_fnc) = join(sF0_fnc,sF7_fnc),
inference(paramodulation,[status(thm)],[f1247,f168]) ).
fof(f3631,plain,
join(sF4_fnc,sF2_fnc) = sF4_fnc,
inference(forward_demodulation,[status(thm)],[f34,f3596]) ).
fof(f3720,plain,
join(sF2_fnc,sF4_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f16,f3631]) ).
fof(f3972,plain,
join(sF1_fnc,sF7_fnc) = join(b,sF7_fnc),
inference(paramodulation,[status(thm)],[f1662,f175]) ).
fof(f4138,plain,
join(sF1_fnc,sF4_fnc) = join(b,sF4_fnc),
inference(paramodulation,[status(thm)],[f3720,f175]) ).
fof(f7340,plain,
join(sF2_fnc,sF0_fnc) = join(sF0_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f1377,f3321]) ).
fof(f7477,plain,
join(sF2_fnc,sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f12,f7340]) ).
fof(f7596,plain,
join(sF1_fnc,sF0_fnc) = join(b,sF0_fnc),
inference(paramodulation,[status(thm)],[f7477,f175]) ).
fof(f7620,plain,
sF1_fnc = join(b,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f65,f7596]) ).
fof(f8297,plain,
join(sF0_fnc,b) = join(b,sF1_fnc),
inference(paramodulation,[status(thm)],[f7620,f3321]) ).
fof(f8318,plain,
join(sF0_fnc,b) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f80,f8297]) ).
fof(f8338,plain,
! [X0] : join(X0,sF1_fnc) = join(sF0_fnc,join(b,X0)),
inference(paramodulation,[status(thm)],[f8318,f152]) ).
fof(f10946,plain,
! [X0] : meet(a,join(b,meet(X0,a))) = meet(a,join(b,meet(X0,sF8_fnc))),
inference(paramodulation,[status(thm)],[f26,f324]) ).
fof(f16258,plain,
! [X0] : meet(a,join(b,meet(sF7_fnc,join(a,X0)))) = meet(a,join(b,meet(sF7_fnc,join(X0,sF7_fnc)))),
inference(paramodulation,[status(thm)],[f112,f301]) ).
fof(f16343,plain,
! [X0] : meet(a,join(b,meet(sF7_fnc,join(a,X0)))) = meet(a,join(b,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f94,f16258]) ).
fof(f25174,plain,
! [X0] : join(sF8_fnc,meet(X0,sF7_fnc)) = sF8_fnc,
inference(paramodulation,[status(thm)],[f112,f131]) ).
fof(f27659,plain,
! [X0] : join(sF8_fnc,meet(sF7_fnc,X0)) = sF8_fnc,
inference(paramodulation,[status(thm)],[f15,f25174]) ).
fof(f32312,plain,
meet(a,join(b,meet(sF7_fnc,join(a,sF8_fnc)))) = meet(a,join(b,meet(sF7_fnc,sF8_fnc))),
inference(paramodulation,[status(thm)],[f27659,f301]) ).
fof(f32378,plain,
meet(a,join(b,sF7_fnc)) = meet(a,join(b,meet(sF7_fnc,sF8_fnc))),
inference(forward_demodulation,[status(thm)],[f16343,f32312]) ).
fof(f32379,plain,
meet(a,join(b,sF7_fnc)) = meet(a,join(b,meet(sF7_fnc,a))),
inference(forward_demodulation,[status(thm)],[f10946,f32378]) ).
fof(f32380,plain,
meet(a,join(b,sF7_fnc)) = meet(a,join(b,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f1205,f32379]) ).
fof(f32381,plain,
meet(a,join(b,sF7_fnc)) = meet(a,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f22,f32380]) ).
fof(f32383,plain,
meet(a,join(b,sF7_fnc)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f23,f32381]) ).
fof(f40775,plain,
join(sF1_fnc,sF7_fnc) = join(sF1_fnc,join(b,sF7_fnc)),
inference(paramodulation,[status(thm)],[f3972,f180]) ).
fof(f40788,plain,
join(b,sF7_fnc) = join(sF1_fnc,join(b,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f3972,f40775]) ).
fof(f40789,plain,
join(b,sF7_fnc) = join(sF7_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f3291,f40788]) ).
fof(f40892,plain,
join(sF1_fnc,sF4_fnc) = join(sF1_fnc,join(b,sF4_fnc)),
inference(paramodulation,[status(thm)],[f4138,f180]) ).
fof(f40905,plain,
join(b,sF4_fnc) = join(sF1_fnc,join(b,sF4_fnc)),
inference(forward_demodulation,[status(thm)],[f4138,f40892]) ).
fof(f40906,plain,
join(b,sF4_fnc) = join(sF4_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f3291,f40905]) ).
fof(f42808,plain,
meet(join(b,sF7_fnc),a) = meet(a,sF0_fnc),
inference(paramodulation,[status(thm)],[f32383,f548]) ).
fof(f42843,plain,
meet(join(b,sF7_fnc),a) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f256,f42808]) ).
fof(f48776,plain,
join(sF4_fnc,sF1_fnc) = join(sF0_fnc,join(b,sF7_fnc)),
inference(paramodulation,[status(thm)],[f40789,f168]) ).
fof(f48824,plain,
join(b,sF4_fnc) = join(sF0_fnc,join(b,sF7_fnc)),
inference(forward_demodulation,[status(thm)],[f40906,f48776]) ).
fof(f48825,plain,
join(b,sF7_fnc) = join(b,sF4_fnc),
inference(backward_demodulation,[status(thm)],[f48826,f40789]) ).
fof(f48826,plain,
join(b,sF4_fnc) = join(sF7_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f8338,f48824]) ).
fof(f48887,plain,
meet(join(b,sF4_fnc),a) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f48825,f42843]) ).
fof(f60074,plain,
meet(sF4_fnc,a) = meet(sF4_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f48887,f221]) ).
fof(f60119,plain,
sF3_fnc = meet(sF4_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1055,f60074]) ).
fof(f60120,plain,
sF3_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1025,f60119]) ).
fof(f60121,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f60120,f30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT152-1 : TPTP v9.3.1. Released v3.1.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:16:06 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 98.61/12.91 % Refutation found
% 98.61/12.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 98.61/12.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 18.96/13.06 % Elapsed time: 12.690712 seconds
% 18.96/13.06 % CPU time: 100.304970 seconds
% 18.96/13.06 % Total memory used: 549.413 MB
% 18.96/13.06 % Net memory used: 534.825 MB
%------------------------------------------------------------------------------