%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT007-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 : n006.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:03 PM UTC 2026
% Result : Unsatisfiable 8.48s 1.49s
% Output : CNFRefutation 7.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 7
% Syntax : Number of formulae : 136 ( 136 unt; 4 def)
% Number of atoms : 136 ( 135 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 91 ( 91 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : meet(X,join(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] : meet(X,join(Y,Z)) = join(meet(Z,X),meet(Y,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
join(join(a,b),c) != join(a,join(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1,X2] : meet(X0,join(X1,X2)) = join(meet(X2,X0),meet(X1,X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
join(join(a,b),c) != join(a,join(b,c)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f7,definition,
sF1_fnc = join(a,b),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f8,definition,
sF0_fnc = join(sF1_fnc,c),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f9,definition,
sF3_fnc = join(b,c),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f10,definition,
sF2_fnc = join(a,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f11,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
meet(b,sF3_fnc) = b,
inference(paramodulation,[status(thm)],[f9,f4]) ).
fof(f13,plain,
meet(sF1_fnc,sF0_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f8,f4]) ).
fof(f14,plain,
meet(a,sF2_fnc) = a,
inference(paramodulation,[status(thm)],[f10,f4]) ).
fof(f15,plain,
meet(a,sF1_fnc) = a,
inference(paramodulation,[status(thm)],[f7,f4]) ).
fof(f16,plain,
! [X0] : meet(sF1_fnc,join(X0,a)) = join(a,meet(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f15,f5]) ).
fof(f17,plain,
! [X0] : meet(sF2_fnc,join(X0,a)) = join(a,meet(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f14,f5]) ).
fof(f18,plain,
! [X0] : meet(sF0_fnc,join(X0,sF1_fnc)) = join(sF1_fnc,meet(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f13,f5]) ).
fof(f20,plain,
! [X0,X1,X2] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(X2,join(X0,X1))),
inference(paramodulation,[status(thm)],[f4,f5]) ).
fof(f21,plain,
! [X0] : meet(sF1_fnc,join(a,X0)) = join(meet(X0,sF1_fnc),a),
inference(paramodulation,[status(thm)],[f15,f5]) ).
fof(f22,plain,
! [X0] : meet(sF2_fnc,join(a,X0)) = join(meet(X0,sF2_fnc),a),
inference(paramodulation,[status(thm)],[f14,f5]) ).
fof(f23,plain,
! [X0] : meet(sF0_fnc,join(sF1_fnc,X0)) = join(meet(X0,sF0_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f13,f5]) ).
fof(f24,plain,
! [X0] : meet(sF3_fnc,join(b,X0)) = join(meet(X0,sF3_fnc),b),
inference(paramodulation,[status(thm)],[f12,f5]) ).
fof(f25,plain,
! [X0,X1,X2] : meet(join(X0,X1),join(X0,X2)) = join(meet(X2,join(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f4,f5]) ).
fof(f26,plain,
! [X0,X1,X2] : meet(meet(X0,X1),meet(X1,join(X2,X0))) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f27,plain,
sF1_fnc = join(a,meet(sF1_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f4,f16]) ).
fof(f32,plain,
sF2_fnc = join(a,meet(sF2_fnc,sF2_fnc)),
inference(paramodulation,[status(thm)],[f4,f17]) ).
fof(f37,plain,
sF0_fnc = join(sF1_fnc,meet(sF0_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f4,f18]) ).
fof(f66,plain,
! [X0,X1] : meet(meet(X0,X1),X1) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f4,f26]) ).
fof(f116,plain,
! [X0,X1,X2] : meet(X0,join(meet(X1,X0),X2)) = join(meet(X2,X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f66,f5]) ).
fof(f117,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = join(meet(X2,X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f66,f5]) ).
fof(f123,plain,
! [X0,X1,X2] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[status(thm)],[f5,f116]) ).
fof(f124,plain,
! [X0,X1,X2] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[status(thm)],[f5,f117]) ).
fof(f198,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),join(X0,X1))),
inference(paramodulation,[status(thm)],[f4,f20]) ).
fof(f212,plain,
! [X0] : meet(join(c,X0),sF3_fnc) = join(c,meet(b,join(c,X0))),
inference(paramodulation,[status(thm)],[f9,f20]) ).
fof(f214,plain,
! [X0] : meet(join(c,X0),sF0_fnc) = join(c,meet(sF1_fnc,join(c,X0))),
inference(paramodulation,[status(thm)],[f8,f20]) ).
fof(f217,plain,
! [X0] : meet(join(sF3_fnc,X0),sF2_fnc) = join(sF3_fnc,meet(a,join(sF3_fnc,X0))),
inference(paramodulation,[status(thm)],[f10,f20]) ).
fof(f218,plain,
! [X0] : meet(join(b,X0),sF1_fnc) = join(b,meet(a,join(b,X0))),
inference(paramodulation,[status(thm)],[f7,f20]) ).
fof(f260,plain,
! [X0] : meet(join(a,X0),sF1_fnc) = join(meet(b,join(a,X0)),a),
inference(paramodulation,[status(thm)],[f7,f25]) ).
fof(f283,plain,
meet(sF1_fnc,sF1_fnc) = join(meet(meet(sF1_fnc,sF1_fnc),sF1_fnc),a),
inference(paramodulation,[status(thm)],[f27,f21]) ).
fof(f293,plain,
meet(sF1_fnc,sF1_fnc) = join(meet(sF1_fnc,sF1_fnc),a),
inference(forward_demodulation,[status(thm)],[f66,f283]) ).
fof(f350,plain,
meet(sF2_fnc,sF2_fnc) = join(meet(meet(sF2_fnc,sF2_fnc),sF2_fnc),a),
inference(paramodulation,[status(thm)],[f32,f22]) ).
fof(f361,plain,
meet(sF2_fnc,sF2_fnc) = join(meet(sF2_fnc,sF2_fnc),a),
inference(forward_demodulation,[status(thm)],[f66,f350]) ).
fof(f455,plain,
meet(sF0_fnc,sF0_fnc) = join(meet(meet(sF0_fnc,sF0_fnc),sF0_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f37,f23]) ).
fof(f464,plain,
meet(sF0_fnc,sF0_fnc) = join(meet(sF0_fnc,sF0_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f66,f455]) ).
fof(f689,plain,
! [X0,X1,X2] : meet(X0,meet(X0,join(X1,X2))) = meet(X0,join(meet(X2,X0),X1)),
inference(paramodulation,[status(thm)],[f5,f124]) ).
fof(f757,plain,
! [X0,X1,X2] : meet(X0,meet(X0,join(X1,X2))) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f123,f689]) ).
fof(f782,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(meet(X1,join(X0,X1)),X0)),
inference(forward_demodulation,[status(thm)],[f25,f198]) ).
fof(f786,plain,
join(a,sF2_fnc) = join(a,join(join(meet(sF2_fnc,sF2_fnc),a),a)),
inference(paramodulation,[status(thm)],[f22,f782]) ).
fof(f839,plain,
join(a,sF2_fnc) = join(a,join(meet(sF2_fnc,sF2_fnc),a)),
inference(forward_demodulation,[status(thm)],[f361,f786]) ).
fof(f840,plain,
join(a,sF2_fnc) = join(a,meet(sF2_fnc,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f361,f839]) ).
fof(f841,plain,
join(a,sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f32,f840]) ).
fof(f928,plain,
meet(sF1_fnc,sF2_fnc) = join(meet(sF2_fnc,sF1_fnc),a),
inference(paramodulation,[status(thm)],[f841,f21]) ).
fof(f2204,plain,
! [X0,X1] : meet(X0,X0) = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f4,f757]) ).
fof(f2332,plain,
! [X0] : meet(X0,X0) = X0,
inference(paramodulation,[status(thm)],[f4,f2204]) ).
fof(f2452,plain,
meet(sF0_fnc,sF0_fnc) = join(sF0_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f2332,f464]) ).
fof(f2460,plain,
meet(sF1_fnc,sF1_fnc) = join(sF1_fnc,a),
inference(backward_demodulation,[status(thm)],[f2332,f293]) ).
fof(f2462,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(backward_demodulation,[status(thm)],[f2332,f2204]) ).
fof(f2506,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(meet(X1,X0),X0),
inference(paramodulation,[status(thm)],[f2332,f5]) ).
fof(f2509,plain,
sF0_fnc = join(sF0_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f2332,f2452]) ).
fof(f2511,plain,
sF1_fnc = join(sF1_fnc,a),
inference(forward_demodulation,[status(thm)],[f2332,f2460]) ).
fof(f2533,plain,
! [X0,X1] : X0 = join(meet(X1,X0),X0),
inference(forward_demodulation,[status(thm)],[f4,f2506]) ).
fof(f2648,plain,
c = meet(c,sF3_fnc),
inference(paramodulation,[status(thm)],[f9,f2462]) ).
fof(f2653,plain,
c = meet(c,sF0_fnc),
inference(paramodulation,[status(thm)],[f8,f2462]) ).
fof(f2658,plain,
sF3_fnc = meet(sF3_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f10,f2462]) ).
fof(f2659,plain,
b = meet(b,sF1_fnc),
inference(paramodulation,[status(thm)],[f7,f2462]) ).
fof(f2780,plain,
! [X0] : X0 = join(X0,X0),
inference(paramodulation,[status(thm)],[f2332,f2533]) ).
fof(f2810,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,X0)),
inference(paramodulation,[status(thm)],[f5,f2780]) ).
fof(f2824,plain,
meet(sF3_fnc,b) = join(meet(b,sF3_fnc),b),
inference(paramodulation,[status(thm)],[f2780,f24]) ).
fof(f2829,plain,
meet(sF1_fnc,a) = join(meet(a,sF1_fnc),a),
inference(paramodulation,[status(thm)],[f2780,f21]) ).
fof(f2841,plain,
! [X0,X1] : meet(join(X0,X1),X0) = join(meet(X0,join(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f2780,f25]) ).
fof(f2844,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(X0,meet(X1,join(X0,X0))),
inference(paramodulation,[status(thm)],[f2780,f20]) ).
fof(f2849,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f2780,f2810]) ).
fof(f2863,plain,
meet(sF3_fnc,b) = join(b,b),
inference(forward_demodulation,[status(thm)],[f12,f2824]) ).
fof(f2864,plain,
meet(sF3_fnc,b) = b,
inference(forward_demodulation,[status(thm)],[f2780,f2863]) ).
fof(f2870,plain,
meet(sF1_fnc,a) = join(a,a),
inference(forward_demodulation,[status(thm)],[f15,f2829]) ).
fof(f2871,plain,
meet(sF1_fnc,a) = a,
inference(forward_demodulation,[status(thm)],[f2780,f2870]) ).
fof(f2884,plain,
! [X0,X1] : meet(join(X0,X1),X0) = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f4,f2841]) ).
fof(f2885,plain,
! [X0,X1] : meet(join(X0,X1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f2780,f2884]) ).
fof(f2890,plain,
! [X0,X1] : X0 = join(X0,meet(X1,join(X0,X0))),
inference(forward_demodulation,[status(thm)],[f2462,f2844]) ).
fof(f2891,plain,
! [X0,X1] : X0 = join(X0,meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2780,f2890]) ).
fof(f3567,plain,
sF3_fnc = join(c,sF3_fnc),
inference(paramodulation,[status(thm)],[f2648,f2533]) ).
fof(f3594,plain,
sF0_fnc = join(c,sF0_fnc),
inference(paramodulation,[status(thm)],[f2653,f2533]) ).
fof(f3621,plain,
sF2_fnc = join(sF3_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f2658,f2533]) ).
fof(f3647,plain,
sF1_fnc = join(b,sF1_fnc),
inference(paramodulation,[status(thm)],[f2659,f2533]) ).
fof(f3673,plain,
! [X0] : meet(b,join(X0,b)) = meet(b,join(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f2864,f124]) ).
fof(f3690,plain,
! [X0] : b = meet(b,join(X0,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f2462,f3673]) ).
fof(f3770,plain,
! [X0] : meet(a,join(X0,a)) = meet(a,join(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f2871,f124]) ).
fof(f3786,plain,
! [X0] : a = meet(a,join(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f2462,f3770]) ).
fof(f3793,plain,
meet(join(c,sF3_fnc),sF3_fnc) = join(c,meet(b,sF3_fnc)),
inference(paramodulation,[status(thm)],[f3567,f212]) ).
fof(f3808,plain,
meet(sF3_fnc,sF3_fnc) = join(c,meet(b,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f3567,f3793]) ).
fof(f3809,plain,
sF3_fnc = join(c,meet(b,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f2332,f3808]) ).
fof(f3810,plain,
sF3_fnc = join(c,b),
inference(forward_demodulation,[status(thm)],[f12,f3809]) ).
fof(f3816,plain,
meet(join(c,sF0_fnc),sF0_fnc) = join(c,meet(sF1_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f3594,f214]) ).
fof(f3831,plain,
meet(sF0_fnc,sF0_fnc) = join(c,meet(sF1_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f3594,f3816]) ).
fof(f3832,plain,
sF0_fnc = join(c,meet(sF1_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f2332,f3831]) ).
fof(f3833,plain,
sF0_fnc = join(c,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f13,f3832]) ).
fof(f3840,plain,
meet(join(sF3_fnc,sF2_fnc),sF2_fnc) = join(sF3_fnc,meet(a,sF2_fnc)),
inference(paramodulation,[status(thm)],[f3621,f217]) ).
fof(f3854,plain,
meet(sF2_fnc,sF2_fnc) = join(sF3_fnc,meet(a,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3621,f3840]) ).
fof(f3855,plain,
sF2_fnc = join(sF3_fnc,meet(a,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f2332,f3854]) ).
fof(f3856,plain,
sF2_fnc = join(sF3_fnc,a),
inference(forward_demodulation,[status(thm)],[f14,f3855]) ).
fof(f3959,plain,
! [X0,X1] : X0 = join(meet(X0,X1),X0),
inference(paramodulation,[status(thm)],[f2849,f2533]) ).
fof(f4068,plain,
meet(sF3_fnc,c) = c,
inference(paramodulation,[status(thm)],[f3567,f2885]) ).
fof(f4167,plain,
sF2_fnc = join(sF2_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f2658,f2891]) ).
fof(f4253,plain,
meet(join(b,sF1_fnc),sF1_fnc) = join(b,meet(a,sF1_fnc)),
inference(paramodulation,[status(thm)],[f3647,f218]) ).
fof(f4257,plain,
meet(sF1_fnc,b) = b,
inference(paramodulation,[status(thm)],[f3647,f2885]) ).
fof(f4269,plain,
meet(sF1_fnc,sF1_fnc) = join(b,meet(a,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f3647,f4253]) ).
fof(f4270,plain,
sF1_fnc = join(b,meet(a,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f2332,f4269]) ).
fof(f4271,plain,
sF1_fnc = join(b,a),
inference(forward_demodulation,[status(thm)],[f15,f4270]) ).
fof(f5500,plain,
! [X0] : meet(c,join(X0,c)) = meet(c,join(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f4068,f124]) ).
fof(f5517,plain,
! [X0] : c = meet(c,join(X0,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f2462,f5500]) ).
fof(f5817,plain,
! [X0] : meet(b,join(X0,b)) = meet(b,join(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f4257,f124]) ).
fof(f5833,plain,
! [X0] : b = meet(b,join(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f2462,f5817]) ).
fof(f7774,plain,
meet(join(a,sF3_fnc),sF1_fnc) = join(b,a),
inference(paramodulation,[status(thm)],[f3690,f260]) ).
fof(f7809,plain,
meet(sF2_fnc,sF1_fnc) = join(b,a),
inference(forward_demodulation,[status(thm)],[f10,f7774]) ).
fof(f7810,plain,
meet(sF2_fnc,sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f4271,f7809]) ).
fof(f7872,plain,
meet(sF1_fnc,sF2_fnc) = join(sF1_fnc,a),
inference(backward_demodulation,[status(thm)],[f7810,f928]) ).
fof(f7900,plain,
meet(sF1_fnc,sF2_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f2511,f7872]) ).
fof(f10864,plain,
a = meet(a,sF0_fnc),
inference(paramodulation,[status(thm)],[f2509,f3786]) ).
fof(f12861,plain,
c = meet(c,sF2_fnc),
inference(paramodulation,[status(thm)],[f4167,f5517]) ).
fof(f12956,plain,
sF2_fnc = join(c,sF2_fnc),
inference(paramodulation,[status(thm)],[f12861,f2533]) ).
fof(f13056,plain,
meet(join(c,sF2_fnc),sF0_fnc) = join(c,meet(sF1_fnc,sF2_fnc)),
inference(paramodulation,[status(thm)],[f12956,f214]) ).
fof(f13091,plain,
meet(sF2_fnc,sF0_fnc) = join(c,meet(sF1_fnc,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f12956,f13056]) ).
fof(f13092,plain,
meet(sF2_fnc,sF0_fnc) = join(c,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f7900,f13091]) ).
fof(f13093,plain,
meet(sF2_fnc,sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f3833,f13092]) ).
fof(f13456,plain,
meet(sF0_fnc,sF2_fnc) = sF0_fnc,
inference(paramodulation,[status(thm)],[f2849,f13093]) ).
fof(f14408,plain,
meet(join(c,sF1_fnc),sF3_fnc) = join(c,b),
inference(paramodulation,[status(thm)],[f5833,f212]) ).
fof(f14450,plain,
meet(sF0_fnc,sF3_fnc) = join(c,b),
inference(forward_demodulation,[status(thm)],[f3833,f14408]) ).
fof(f14451,plain,
meet(sF0_fnc,sF3_fnc) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f3810,f14450]) ).
fof(f14686,plain,
sF0_fnc = join(sF3_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f14451,f3959]) ).
fof(f15016,plain,
meet(join(sF3_fnc,sF0_fnc),sF2_fnc) = join(sF3_fnc,meet(a,sF0_fnc)),
inference(paramodulation,[status(thm)],[f14686,f217]) ).
fof(f15052,plain,
meet(sF0_fnc,sF2_fnc) = join(sF3_fnc,meet(a,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f14686,f15016]) ).
fof(f15053,plain,
sF0_fnc = join(sF3_fnc,meet(a,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f13456,f15052]) ).
fof(f15054,plain,
sF0_fnc = join(sF3_fnc,a),
inference(forward_demodulation,[status(thm)],[f10864,f15053]) ).
fof(f15055,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f3856,f15054]) ).
fof(f15056,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15055,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT007-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 23:04:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 8.48/1.49 % Refutation found
% 8.48/1.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 8.48/1.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.24/2.70 % Elapsed time: 2.112584 seconds
% 11.24/2.70 % CPU time: 7.368288 seconds
% 11.24/2.70 % Total memory used: 114.426 MB
% 11.24/2.70 % Net memory used: 109.709 MB
%------------------------------------------------------------------------------