%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT005-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n013.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 : Fri Sep 25 01:58:04 PM UTC 2026
% Result : Unsatisfiable 148.32s 23.99s
% Output : CNFRefutation 148.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 20
% Syntax : Number of formulae : 182 ( 164 unt; 5 def)
% Number of atoms : 464 ( 206 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 66 ( 35 ~; 31 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 114 ( 0 sgn 114 !; 0 ?; 92 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_join) ).
fof(f9,axiom,
! [X0] : meet(X0,n0) = n0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-1.ax',x_meet_0) ).
fof(f10,plain,
! [X0] : n0 = meet(X0,n0),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : join(X0,n0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-1.ax',x_join_0) ).
fof(f15,axiom,
! [X2,X0,X1] :
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-1.ax',modular) ).
fof(f16,axiom,
! [X0,X1] :
( meet(X0,X1) = n0
| ~ complement(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-2.ax',complement_meet) ).
fof(f19,axiom,
complement(r1,join(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_of_a_join_b) ).
fof(f20,axiom,
complement(r2,meet(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_of_a_meet_b) ).
fof(f21,negated_conjecture,
r1 != meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_lemma) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f8]) ).
tcf(c_76,plain,
! [X0: $i] : meet(X0,n0) = n0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_77,plain,
! [X0: $i] : join(X0,n0) = X0,
inference(cnf_transformation,[],[f11]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( join(X0,meet(X2,X1)) = meet(X1,join(X0,X2)) )
| ( meet(X0,X1) != X0 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( ( meet(X0,X1) = n0 )
| ~ complement(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_84,plain,
complement(r1,join(a,b)),
inference(cnf_transformation,[],[f19]) ).
tcf(c_85,plain,
complement(r2,meet(a,b)),
inference(cnf_transformation,[],[f20]) ).
tcf(c_86,negated_conjecture,
meet(join(r1,meet(r2,b)),join(r1,meet(r2,a))) != r1,
inference(cnf_transformation,[],[f21]) ).
tcf(c_100,negated_conjecture,
meet(join(r1,meet(a,r2)),join(r1,meet(b,r2))) != r1,
inference(theory_normalisation,[status(thm)],[c_86,c_74,c_72,c_75,c_73]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i] :
( ( meet(X1,X0) = n0 )
| ( X1 != r1 )
| ( join(a,b) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_84,c_81]) ).
tcf(c_181,plain,
meet(r1,join(a,b)) = n0,
inference(unflattening,[status(thm)],[c_180]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i] :
( ( meet(X1,X0) = n0 )
| ( X1 != r2 )
| ( meet(a,b) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_85,c_81]) ).
tcf(c_191,plain,
meet(r2,meet(a,b)) = n0,
inference(unflattening,[status(thm)],[c_190]) ).
tcf(c_199,plain,
meet(a,meet(b,r2)) = n0,
inference(theory_normalisation,[status(thm)],[c_191,c_74,c_72,c_75,c_73]) ).
tcf(c_244,definition,
iPr_def_10 = meet(a,r2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_245,definition,
iPr_def_11 = join(r1,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_246,definition,
iPr_def_12 = meet(b,r2),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_247,definition,
iPr_def_13 = join(r1,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_248,definition,
iPr_def_14 = meet(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_249,negated_conjecture,
iPr_def_14 != r1,
inference(demodulation,[status(thm)],[c_100,c_246,c_247,c_244,c_245,c_248]) ).
tcf(c_250,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_251,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_419,plain,
! [X0: $i] :
( ( iPr_def_14 = r1 )
| ( iPr_def_14 != X0 )
| ( r1 != X0 ) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_422,plain,
! [X0: $i,X1: $i] :
( ( r1 = X0 )
| ( r1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_423,plain,
! [X0: $i] :
( ( r1 = X0 )
| ( r1 != r1 )
| ( X0 != r1 ) ),
inference(instantiation,[status(thm)],[c_422]) ).
tcf(c_424,plain,
r1 = r1,
inference(instantiation,[status(thm)],[c_250]) ).
tcf(c_429,plain,
( ( r1 = join(r1,n0) )
| ( r1 != r1 )
| ( join(r1,n0) != r1 ) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_430,plain,
join(r1,n0) = r1,
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_528,plain,
! [X0: $i] :
( ( r1 = X0 )
| ( r1 != join(r1,n0) )
| ( X0 != join(r1,n0) ) ),
inference(instantiation,[status(thm)],[c_422]) ).
tcf(c_776,plain,
( ( r1 = join(n0,r1) )
| ( r1 != join(r1,n0) )
| ( join(n0,r1) != join(r1,n0) ) ),
inference(instantiation,[status(thm)],[c_528]) ).
tcf(c_777,plain,
join(n0,r1) = join(r1,n0),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_936,plain,
! [X0: $i] : meet(n0,X0) = n0,
inference(superposition,[status(thm)],[c_72,c_76]) ).
tcf(c_2010,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_250]) ).
tcf(c_2264,plain,
( ( iPr_def_14 = r1 )
| ( iPr_def_14 != join(n0,r1) )
| ( r1 != join(n0,r1) ) ),
inference(instantiation,[status(thm)],[c_419]) ).
tcf(c_2665,plain,
meet(a,iPr_def_12) = n0,
inference(light_normalisation,[status(thm)],[c_199,c_246]) ).
tcf(c_2666,plain,
meet(iPr_def_12,a) = n0,
inference(demodulation,[status(thm)],[c_2665,c_72]) ).
tcf(c_2668,plain,
! [X0: $i] : meet(iPr_def_12,meet(a,X0)) = meet(n0,X0),
inference(superposition,[status(thm)],[c_2666,c_74]) ).
tcf(c_2670,plain,
! [X0: $i] : meet(iPr_def_12,meet(a,X0)) = n0,
inference(light_normalisation,[status(thm)],[c_2668,c_936]) ).
tcf(c_5205,plain,
meet(iPr_def_12,iPr_def_10) = n0,
inference(superposition,[status(thm)],[c_244,c_2670]) ).
tcf(c_5211,plain,
meet(iPr_def_10,iPr_def_12) = n0,
inference(theory_normalisation,[status(thm)],[c_5205,c_75,c_73,c_74,c_72]) ).
tcf(c_210539,plain,
join(iPr_def_10,r1) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_245,c_75,c_73,c_74,c_72]) ).
tcf(c_210540,plain,
join(iPr_def_12,r1) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_247,c_75,c_73,c_74,c_72]) ).
tcf(c_210545,plain,
meet(iPr_def_10,iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_210539,c_70]) ).
tcf(c_210552,plain,
join(b,iPr_def_12) = b,
inference(superposition,[status(thm)],[c_246,c_71]) ).
tcf(c_210553,plain,
join(a,iPr_def_10) = a,
inference(superposition,[status(thm)],[c_244,c_71]) ).
tcf(c_210554,plain,
join(iPr_def_11,iPr_def_14) = iPr_def_11,
inference(superposition,[status(thm)],[c_248,c_71]) ).
tcf(c_210560,plain,
join(iPr_def_10,a) = a,
inference(theory_normalisation,[status(thm)],[c_210553,c_75,c_73,c_74,c_72]) ).
tcf(c_210561,plain,
join(iPr_def_12,b) = b,
inference(theory_normalisation,[status(thm)],[c_210552,c_75,c_73,c_74,c_72]) ).
tcf(c_210564,plain,
meet(iPr_def_10,a) = iPr_def_10,
inference(superposition,[status(thm)],[c_210560,c_70]) ).
tcf(c_210565,plain,
meet(iPr_def_12,b) = iPr_def_12,
inference(superposition,[status(thm)],[c_210561,c_70]) ).
tcf(c_210577,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_72,c_71]) ).
tcf(c_210578,plain,
! [X0: $i] : meet(n0,X0) = n0,
inference(superposition,[status(thm)],[c_72,c_76]) ).
tcf(c_210587,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_73,c_70]) ).
tcf(c_210588,plain,
! [X0: $i] : join(n0,X0) = X0,
inference(superposition,[status(thm)],[c_73,c_77]) ).
tcf(c_210600,plain,
! [X0: $i] : meet(r1,meet(join(a,b),X0)) = meet(n0,X0),
inference(superposition,[status(thm)],[c_181,c_74]) ).
tcf(c_210601,plain,
! [X0: $i] : meet(iPr_def_11,meet(iPr_def_13,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_248,c_74]) ).
tcf(c_210602,plain,
! [X0: $i] : meet(iPr_def_10,meet(iPr_def_11,X0)) = meet(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_210545,c_74]) ).
tcf(c_210604,plain,
! [X0: $i] : meet(iPr_def_10,meet(a,X0)) = meet(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_210564,c_74]) ).
tcf(c_210613,plain,
! [X0: $i] : meet(r1,meet(join(a,b),X0)) = n0,
inference(light_normalisation,[status(thm)],[c_210600,c_210578]) ).
tcf(c_210624,plain,
! [X0: $i] : join(iPr_def_10,join(r1,X0)) = join(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_210539,c_75]) ).
tcf(c_210625,plain,
! [X0: $i] : join(iPr_def_12,join(r1,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_210540,c_75]) ).
tcf(c_210627,plain,
! [X0: $i] : join(iPr_def_10,join(a,X0)) = join(a,X0),
inference(superposition,[status(thm)],[c_210560,c_75]) ).
tcf(c_210628,plain,
! [X0: $i] : join(iPr_def_12,join(b,X0)) = join(b,X0),
inference(superposition,[status(thm)],[c_210561,c_75]) ).
tcf(c_210707,plain,
join(r2,iPr_def_10) = r2,
inference(superposition,[status(thm)],[c_244,c_210577]) ).
tcf(c_210711,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_248,c_210577]) ).
tcf(c_210727,plain,
join(iPr_def_10,r2) = r2,
inference(theory_normalisation,[status(thm)],[c_210707,c_75,c_73,c_74,c_72]) ).
tcf(c_210738,plain,
meet(iPr_def_10,r2) = iPr_def_10,
inference(superposition,[status(thm)],[c_210727,c_70]) ).
tcf(c_210765,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,X2),join(X0,X1)),
inference(superposition,[status(thm)],[c_70,c_80]) ).
tcf(c_210766,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( join(X1,meet(X2,X0)) = meet(X0,join(X1,X2)) )
| ( meet(X0,X1) != X1 ) ),
inference(superposition,[status(thm)],[c_72,c_80]) ).
tcf(c_210776,plain,
! [X0: $i] : join(iPr_def_10,meet(X0,a)) = meet(a,join(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_210564,c_80]) ).
tcf(c_210777,plain,
! [X0: $i] : join(iPr_def_12,meet(X0,b)) = meet(b,join(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_210565,c_80]) ).
tcf(c_210827,plain,
! [X0: $i] : join(iPr_def_10,meet(X0,r2)) = meet(r2,join(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_210738,c_80]) ).
tcf(c_210847,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_75,c_210587]) ).
tcf(c_210853,plain,
meet(r1,iPr_def_11) = r1,
inference(superposition,[status(thm)],[c_210539,c_210587]) ).
tcf(c_210854,plain,
meet(r1,iPr_def_13) = r1,
inference(superposition,[status(thm)],[c_210540,c_210587]) ).
tcf(c_210858,plain,
meet(iPr_def_14,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_210711,c_210587]) ).
tcf(c_210864,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,join(X2,X0))) = meet(join(X2,X0),join(X0,X1)),
inference(superposition,[status(thm)],[c_210587,c_80]) ).
tcf(c_210868,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X0,X1),
inference(superposition,[status(thm)],[c_210587,c_74]) ).
tcf(c_210871,plain,
meet(iPr_def_13,iPr_def_14) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_210858,c_75,c_73,c_74,c_72]) ).
tcf(c_210873,plain,
meet(iPr_def_13,r1) = r1,
inference(theory_normalisation,[status(thm)],[c_210854,c_75,c_73,c_74,c_72]) ).
tcf(c_210874,plain,
meet(iPr_def_11,r1) = r1,
inference(theory_normalisation,[status(thm)],[c_210853,c_75,c_73,c_74,c_72]) ).
tcf(c_211370,plain,
meet(iPr_def_11,r1) = meet(iPr_def_14,r1),
inference(superposition,[status(thm)],[c_210873,c_210601]) ).
tcf(c_211374,plain,
! [X0: $i] : join(iPr_def_11,meet(iPr_def_14,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_210601,c_71]) ).
tcf(c_211377,plain,
meet(iPr_def_14,r1) = r1,
inference(light_normalisation,[status(thm)],[c_211370,c_210874]) ).
tcf(c_211429,plain,
join(iPr_def_14,r1) = iPr_def_14,
inference(superposition,[status(thm)],[c_211377,c_71]) ).
tcf(c_211466,plain,
! [X0: $i] : meet(meet(iPr_def_14,X0),iPr_def_11) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_211374,c_210587]) ).
tcf(c_211467,plain,
! [X0: $i] : meet(iPr_def_11,meet(X0,iPr_def_14)) = meet(iPr_def_14,X0),
inference(theory_normalisation,[status(thm)],[c_211466,c_75,c_73,c_74,c_72]) ).
tcf(c_211561,plain,
meet(iPr_def_10,iPr_def_13) = meet(iPr_def_10,iPr_def_14),
inference(superposition,[status(thm)],[c_248,c_210602]) ).
tcf(c_211604,plain,
join(iPr_def_14,meet(iPr_def_10,iPr_def_13)) = iPr_def_14,
inference(superposition,[status(thm)],[c_211561,c_210577]) ).
tcf(c_211688,plain,
! [X0: $i] : meet(iPr_def_10,join(a,X0)) = meet(iPr_def_10,a),
inference(superposition,[status(thm)],[c_70,c_210604]) ).
tcf(c_211703,plain,
! [X0: $i] : meet(iPr_def_10,join(a,X0)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_211688,c_210564]) ).
tcf(c_211721,plain,
! [X0: $i,X1: $i] : join(iPr_def_10,meet(X0,join(a,X1))) = meet(join(a,X1),join(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_211703,c_80]) ).
tcf(c_211857,plain,
! [X0: $i] : meet(r1,meet(X0,join(a,b))) = n0,
inference(superposition,[status(thm)],[c_72,c_210613]) ).
tcf(c_211931,plain,
! [X0: $i] : join(iPr_def_10,join(X0,r1)) = join(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_73,c_210624]) ).
tcf(c_211988,plain,
! [X0: $i] : join(iPr_def_12,join(X0,r1)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_73,c_210625]) ).
tcf(c_212216,plain,
! [X0: $i] : join(iPr_def_12,join(X0,b)) = join(X0,b),
inference(superposition,[status(thm)],[c_73,c_210628]) ).
tcf(c_213076,plain,
! [X0: $i] : meet(iPr_def_14,join(X0,iPr_def_11)) = iPr_def_14,
inference(superposition,[status(thm)],[c_210554,c_210847]) ).
tcf(c_213298,plain,
! [X0: $i] : meet(iPr_def_14,join(iPr_def_11,X0)) = iPr_def_14,
inference(superposition,[status(thm)],[c_73,c_213076]) ).
tcf(c_213443,plain,
! [X0: $i,X1: $i] : meet(iPr_def_14,meet(join(iPr_def_11,X0),X1)) = meet(iPr_def_14,X1),
inference(superposition,[status(thm)],[c_213298,c_74]) ).
tcf(c_215489,plain,
meet(r1,a) = n0,
inference(superposition,[status(thm)],[c_70,c_211857]) ).
tcf(c_215494,plain,
meet(r1,b) = n0,
inference(superposition,[status(thm)],[c_210587,c_211857]) ).
tcf(c_216157,plain,
join(iPr_def_10,iPr_def_14) = join(iPr_def_11,iPr_def_14),
inference(superposition,[status(thm)],[c_211429,c_211931]) ).
tcf(c_216164,plain,
join(a,r1) = join(iPr_def_11,a),
inference(superposition,[status(thm)],[c_211931,c_210627]) ).
tcf(c_216171,plain,
join(r1,a) = join(iPr_def_11,a),
inference(theory_normalisation,[status(thm)],[c_216164,c_75,c_73,c_74,c_72]) ).
tcf(c_216174,plain,
join(iPr_def_10,iPr_def_14) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_216157,c_210554]) ).
tcf(c_216433,plain,
join(iPr_def_12,iPr_def_14) = join(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_211429,c_211988]) ).
tcf(c_216440,plain,
join(b,r1) = join(iPr_def_13,b),
inference(superposition,[status(thm)],[c_211988,c_210628]) ).
tcf(c_216448,plain,
join(r1,b) = join(iPr_def_13,b),
inference(theory_normalisation,[status(thm)],[c_216440,c_75,c_73,c_74,c_72]) ).
tcf(c_216451,plain,
join(iPr_def_12,iPr_def_14) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_216433,c_210711]) ).
tcf(c_216468,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_14,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_216451,c_75]) ).
tcf(c_217319,plain,
! [X0: $i,X1: $i] :
( ( X1 = join(n0,r1) )
| ( X1 != X0 )
| ( join(n0,r1) != X0 ) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_226069,plain,
join(iPr_def_13,b) = join(iPr_def_14,b),
inference(superposition,[status(thm)],[c_216468,c_212216]) ).
tcf(c_243404,plain,
meet(join(a,b),join(a,r1)) = join(a,n0),
inference(superposition,[status(thm)],[c_181,c_210765]) ).
tcf(c_243822,plain,
meet(join(r1,a),join(a,b)) = join(n0,a),
inference(theory_normalisation,[status(thm)],[c_243404,c_75,c_73,c_74,c_72]) ).
tcf(c_243823,plain,
meet(join(iPr_def_11,a),join(a,b)) = join(n0,a),
inference(light_normalisation,[status(thm)],[c_243822,c_216171]) ).
tcf(c_244366,plain,
meet(a,join(iPr_def_10,r1)) = join(iPr_def_10,n0),
inference(superposition,[status(thm)],[c_215489,c_210776]) ).
tcf(c_244385,plain,
join(iPr_def_10,n0) = meet(a,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_244366,c_210539]) ).
tcf(c_244386,plain,
join(iPr_def_10,n0) = meet(iPr_def_11,a),
inference(theory_normalisation,[status(thm)],[c_244385,c_75,c_73,c_74,c_72]) ).
tcf(c_244463,plain,
meet(b,join(iPr_def_12,r1)) = join(iPr_def_12,n0),
inference(superposition,[status(thm)],[c_215494,c_210777]) ).
tcf(c_244481,plain,
join(iPr_def_12,n0) = meet(b,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_244463,c_210540]) ).
tcf(c_244482,plain,
join(iPr_def_12,n0) = meet(iPr_def_13,b),
inference(theory_normalisation,[status(thm)],[c_244481,c_75,c_73,c_74,c_72]) ).
tcf(c_244513,plain,
meet(r2,join(iPr_def_10,n0)) = join(iPr_def_10,n0),
inference(superposition,[status(thm)],[c_210578,c_210827]) ).
tcf(c_244537,plain,
meet(r2,meet(iPr_def_11,a)) = meet(iPr_def_11,a),
inference(light_normalisation,[status(thm)],[c_244513,c_244386]) ).
tcf(c_244538,plain,
meet(iPr_def_11,meet(a,r2)) = meet(iPr_def_11,a),
inference(theory_normalisation,[status(thm)],[c_244537,c_75,c_73,c_74,c_72]) ).
tcf(c_244539,plain,
meet(iPr_def_11,a) = meet(iPr_def_11,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_244538,c_244]) ).
tcf(c_244540,plain,
meet(iPr_def_10,iPr_def_11) = meet(iPr_def_11,a),
inference(theory_normalisation,[status(thm)],[c_244539,c_75,c_73,c_74,c_72]) ).
tcf(c_244541,plain,
meet(iPr_def_11,a) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_244540,c_210545]) ).
tcf(c_244620,plain,
! [X0: $i] : meet(iPr_def_11,meet(a,X0)) = meet(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_244541,c_74]) ).
tcf(c_244722,plain,
meet(iPr_def_13,b) = iPr_def_12,
inference(demodulation,[status(thm)],[c_244482,c_77]) ).
tcf(c_244882,plain,
! [X0: $i] : join(iPr_def_14,meet(X0,iPr_def_13)) = meet(iPr_def_13,join(iPr_def_14,X0)),
inference(superposition,[status(thm)],[c_210871,c_210766]) ).
tcf(c_244884,plain,
! [X0: $i] : join(r1,meet(X0,iPr_def_13)) = meet(iPr_def_13,join(r1,X0)),
inference(superposition,[status(thm)],[c_210873,c_210766]) ).
tcf(c_245378,plain,
meet(iPr_def_13,join(iPr_def_14,iPr_def_10)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_211604,c_244882]) ).
tcf(c_245379,plain,
meet(iPr_def_13,join(iPr_def_10,iPr_def_14)) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_245378,c_75,c_73,c_74,c_72]) ).
tcf(c_245380,plain,
meet(iPr_def_13,iPr_def_11) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_245379,c_216174]) ).
tcf(c_245381,plain,
meet(iPr_def_11,iPr_def_13) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_245380,c_75,c_73,c_74,c_72]) ).
tcf(c_246022,plain,
meet(iPr_def_10,iPr_def_14) = meet(iPr_def_14,a),
inference(superposition,[status(thm)],[c_244620,c_211467]) ).
tcf(c_246047,plain,
meet(iPr_def_10,iPr_def_13) = meet(iPr_def_14,a),
inference(light_normalisation,[status(thm)],[c_246022,c_211561]) ).
tcf(c_251782,plain,
! [X0: $i] :
( ( iPr_def_14 = join(n0,r1) )
| ( iPr_def_14 != X0 )
| ( join(n0,r1) != X0 ) ),
inference(instantiation,[status(thm)],[c_217319]) ).
tcf(c_261395,plain,
( ( iPr_def_14 = join(n0,r1) )
| ( iPr_def_14 != iPr_def_14 )
| ( join(n0,r1) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_251782]) ).
tcf(c_264808,plain,
meet(join(a,b),join(b,r1)) = join(b,n0),
inference(superposition,[status(thm)],[c_181,c_210864]) ).
tcf(c_265297,plain,
meet(join(r1,b),join(a,b)) = join(n0,b),
inference(theory_normalisation,[status(thm)],[c_264808,c_75,c_73,c_74,c_72]) ).
tcf(c_265298,plain,
meet(join(iPr_def_13,b),join(a,b)) = join(n0,b),
inference(light_normalisation,[status(thm)],[c_265297,c_216448]) ).
tcf(c_358556,plain,
meet(join(a,b),join(iPr_def_10,r1)) = join(iPr_def_10,n0),
inference(superposition,[status(thm)],[c_181,c_211721]) ).
tcf(c_358734,plain,
meet(join(iPr_def_10,r1),join(a,b)) = join(iPr_def_10,n0),
inference(theory_normalisation,[status(thm)],[c_358556,c_75,c_73,c_74,c_72]) ).
tcf(c_358735,plain,
meet(iPr_def_11,join(a,b)) = join(iPr_def_10,n0),
inference(light_normalisation,[status(thm)],[c_358734,c_210539]) ).
tcf(c_359791,plain,
meet(iPr_def_11,join(a,b)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_358735,c_77]) ).
tcf(c_359808,plain,
meet(join(a,b),join(a,iPr_def_11)) = join(a,iPr_def_10),
inference(superposition,[status(thm)],[c_359791,c_210765]) ).
tcf(c_359846,plain,
meet(join(iPr_def_11,a),join(a,b)) = join(iPr_def_10,a),
inference(theory_normalisation,[status(thm)],[c_359808,c_75,c_73,c_74,c_72]) ).
tcf(c_359847,plain,
meet(join(iPr_def_11,a),join(a,b)) = a,
inference(light_normalisation,[status(thm)],[c_359846,c_210560,c_243823]) ).
tcf(c_362741,plain,
meet(iPr_def_14,join(a,b)) = meet(iPr_def_14,a),
inference(superposition,[status(thm)],[c_359847,c_213443]) ).
tcf(c_362752,plain,
meet(iPr_def_14,join(a,b)) = meet(iPr_def_10,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_362741,c_246047]) ).
tcf(c_372249,plain,
meet(join(a,b),join(b,iPr_def_14)) = join(b,meet(iPr_def_10,iPr_def_13)),
inference(superposition,[status(thm)],[c_362752,c_210864]) ).
tcf(c_372301,plain,
meet(join(iPr_def_14,b),join(a,b)) = join(b,meet(iPr_def_10,iPr_def_13)),
inference(theory_normalisation,[status(thm)],[c_372249,c_75,c_73,c_74,c_72]) ).
tcf(c_372302,plain,
join(b,meet(iPr_def_10,iPr_def_13)) = join(n0,b),
inference(light_normalisation,[status(thm)],[c_372301,c_226069,c_265298]) ).
tcf(c_385657,plain,
join(b,meet(iPr_def_10,iPr_def_13)) = b,
inference(demodulation,[status(thm)],[c_372302,c_210588]) ).
tcf(c_385684,plain,
meet(iPr_def_10,meet(iPr_def_13,b)) = meet(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_385657,c_210868]) ).
tcf(c_385693,plain,
meet(iPr_def_10,iPr_def_13) = n0,
inference(light_normalisation,[status(thm)],[c_385684,c_5211,c_244722]) ).
tcf(c_563124,plain,
meet(iPr_def_13,join(r1,iPr_def_10)) = join(r1,n0),
inference(superposition,[status(thm)],[c_385693,c_244884]) ).
tcf(c_563192,plain,
meet(iPr_def_13,join(iPr_def_10,r1)) = join(n0,r1),
inference(theory_normalisation,[status(thm)],[c_563124,c_75,c_73,c_74,c_72]) ).
tcf(c_563193,plain,
join(n0,r1) = meet(iPr_def_13,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_563192,c_210539]) ).
tcf(c_563194,plain,
join(n0,r1) = meet(iPr_def_11,iPr_def_13),
inference(theory_normalisation,[status(thm)],[c_563193,c_75,c_73,c_74,c_72]) ).
tcf(c_563195,plain,
join(n0,r1) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_563194,c_245381]) ).
tcf(c_563294,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_563195,c_261395,c_2264,c_2010,c_777,c_776,c_430,c_429,c_424,c_249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.39 % Computer : n013.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Wed Sep 23 19:58:36 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.47
% 0.13/0.47 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.47
% 0.13/0.47 % Detected problem language: tptp
% 0.21/0.49 % Proving...
% 148.32/23.99 % SZS status Started for theBenchmark.p
% 148.32/23.99 % SZS status Unsatisfiable for theBenchmark.p
% 148.32/23.99
% 148.32/23.99 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 148.32/23.99
% 148.32/23.99 % ------ iProver source info
% 148.32/23.99
% 148.32/23.99 % git: date: 2026-07-19 20:42:38 +0200
% 148.32/23.99 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 148.32/23.99 % git: non_committed_changes: false
% 148.32/23.99
% 148.32/23.99 % ------ Parsing...% successful
% 148.32/23.99
% 148.32/23.99
% 148.32/23.99 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 148.32/23.99
% 148.32/23.99 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 148.32/23.99
% 148.32/23.99 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 148.32/23.99
% 148.32/23.99 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 148.32/23.99 % ------ Proving...
% 148.32/23.99 % ------ Problem Properties
% 148.32/23.99
% 148.32/23.99 %
% 148.32/23.99 % clauses 23
% 148.32/23.99 % conjectures 1
% 148.32/23.99 % EPR 1
% 148.32/23.99 % Horn 23
% 148.32/23.99 % unary 22
% 148.32/23.99 % binary 1
% 148.32/23.99 % lits 24
% 148.32/23.99 % lits eq 24
% 148.32/23.99 % fd_pure 0
% 148.32/23.99 % fd_pseudo 0
% 148.32/23.99 % fd_cond 0
% 148.32/23.99 % fd_pseudo_cond 0
% 148.32/23.99 % AC symbols 2
% 148.32/23.99
% 148.32/23.99 % ------ Schedule dynamic 5 is on
% 148.32/23.99
% 148.32/23.99 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 148.32/23.99
% 148.32/23.99
% 148.32/23.99 % ------
% 148.32/23.99 % Current options:
% 148.32/23.99 % ------
% 148.32/23.99
% 148.32/23.99
% 148.32/23.99 %
% 148.32/23.99
% 148.32/23.99 % ------ Proving...
% 148.32/23.99 % Proof_search_loop: time out after: 3887 full_loop iterations
% 148.32/23.99
% 148.32/23.99 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 148.32/23.99
% 148.32/23.99
% 148.32/23.99 % ------
% 148.32/23.99 % Current options:
% 148.32/23.99 % ------
% 148.32/23.99
% 148.32/23.99
% 148.32/23.99 %
% 148.32/23.99
% 148.32/23.99 % ------ Proving...
% 148.32/23.99 %
% 148.32/23.99
% 148.32/23.99 % SZS status Unsatisfiable for theBenchmark.p
% 148.32/23.99
% 148.32/23.99 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 148.32/23.99
% 148.32/23.99
%------------------------------------------------------------------------------