%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU272+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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 02:56:26 PM UTC 2026
% Result : Theorem 8.17s 1.77s
% Output : CNFRefutation 8.17s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f29ERROR: Could not build tree for root c_16966ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ordinal(X1)
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( in(X4,X0)
& X3 = X4
& ordinal(X4) )
& in(X3,succ(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e8_6__wellord2__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ordinal(X1)
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( in(X4,X0)
& X3 = X4
& ordinal(X4) )
& in(X3,succ(X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f18,plain,
? [X0,X1] :
( ordinal(X1)
& ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( ? [X4] :
( in(X4,X0)
& X3 = X4
& ordinal(X4) )
& in(X3,succ(X1)) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f30,plain,
? [X0,X1] :
( ordinal(X1)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( in(X4,X0)
& X3 = X4
& ordinal(X4) )
& in(X3,succ(X1)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ in(X4,X0)
| X3 != X4
| ~ ordinal(X4) )
| ~ in(X3,succ(X1)) ) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f31,plain,
? [X0,X1] :
( ordinal(X1)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( in(X4,X0)
& X3 = X4
& ordinal(X4) )
& in(X3,succ(X1)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ in(X4,X0)
| X3 != X4
| ~ ordinal(X4) )
| ~ in(X3,succ(X1)) ) ) ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
? [X0,X1] :
( ordinal(X1)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X5] :
( in(X5,X0)
& X3 = X5
& ordinal(X5) )
& in(X3,succ(X1)) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ in(X4,X0)
| X3 != X4
| ~ ordinal(X4) )
| ~ in(X3,succ(X1)) ) ) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
( ordinal(sK3)
& ! [X2] :
( ( in(sK4(X2),X2)
| ( in(sK5(X2),sK2)
& sK4(X2) = sK5(X2)
& ordinal(sK5(X2))
& in(sK4(X2),succ(sK3)) ) )
& ( ~ in(sK4(X2),X2)
| ! [X4] :
( ~ in(X4,sK2)
| sK4(X2) != X4
| ~ ordinal(X4) )
| ~ in(sK4(X2),succ(sK3)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X3,sK4(X2)),skolemize(X5,sK5(X2))],[f32]) ).
fof(f38,plain,
! [X0] :
( ~ sP1(X0)
| ? [X2,X3,X4] :
( sP0(X4,X0)
& X2 = X4
& ? [X5] :
( in(X5,X0)
& X3 = X5
& ordinal(X5) )
& X2 = X3
& X3 != X4 ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f39,plain,
! [X0] :
( ~ sP1(X0)
| ? [X1,X2,X3] :
( sP0(X3,X0)
& X1 = X3
& ? [X4] :
( in(X4,X0)
& X2 = X4
& ordinal(X4) )
& X1 = X2
& X2 != X3 ) ),
inference(rectify,[],[f38]) ).
fof(f40,plain,
! [X0] :
( ~ sP1(X0)
| ( sP0(sK12(X0),X0)
& sK10(X0) = sK12(X0)
& in(sK13(X0),X0)
& sK11(X0) = sK13(X0)
& ordinal(sK13(X0))
& sK10(X0) = sK11(X0)
& sK11(X0) != sK12(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13]),skolemize(X1,sK10(X0)),skolemize(X2,sK11(X0)),skolemize(X3,sK12(X0)),skolemize(X4,sK13(X0))],[f39]) ).
fof(f44,plain,
! [X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ? [X7] :
! [X8] :
( ( ~ in(X8,X7)
| ? [X9] :
( ? [X10] :
( in(X10,X0)
& X8 = X10
& ordinal(X10) )
& X8 = X9
& in(X9,succ(X1)) ) )
& ( ! [X9] :
( ! [X10] :
( ~ in(X10,X0)
| X8 != X10
| ~ ordinal(X10) )
| X8 != X9
| ~ in(X9,succ(X1)) )
| in(X8,X7) ) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f45,plain,
! [X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ? [X2] :
! [X3] :
( ( ~ in(X3,X2)
| ? [X6] :
( ? [X7] :
( in(X7,X0)
& X3 = X7
& ordinal(X7) )
& X3 = X6
& in(X6,succ(X1)) ) )
& ( ! [X4] :
( ! [X5] :
( ~ in(X5,X0)
| X3 != X5
| ~ ordinal(X5) )
| X3 != X4
| ~ in(X4,succ(X1)) )
| in(X3,X2) ) ) ),
inference(rectify,[],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ! [X3] :
( ( ~ in(X3,sK15(X0,X1))
| ( in(sK17(X0,X3),X0)
& sK17(X0,X3) = X3
& ordinal(sK17(X0,X3))
& sK16(X0,X1,X3) = X3
& in(sK16(X0,X1,X3),succ(X1)) ) )
& ( ! [X4] :
( ! [X5] :
( ~ in(X5,X0)
| X3 != X5
| ~ ordinal(X5) )
| X3 != X4
| ~ in(X4,succ(X1)) )
| in(X3,sK15(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X2,sK15(X0,X1)),skolemize(X6,sK16(X0,X1,X3)),skolemize(X7,sK17(X0,X3))],[f45]) ).
fof(f47,plain,
ordinal(sK3),
inference(cnf_transformation,[],[f33]) ).
fof(f48,plain,
! [X2] :
( in(sK4(X2),X2)
| in(sK5(X2),sK2) ),
inference(cnf_transformation,[],[f33]) ).
fof(f49,plain,
! [X2] :
( in(sK4(X2),X2)
| sK4(X2) = sK5(X2) ),
inference(cnf_transformation,[],[f33]) ).
fof(f50,plain,
! [X2] :
( in(sK4(X2),X2)
| ordinal(sK5(X2)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f51,plain,
! [X2] :
( in(sK4(X2),X2)
| in(sK4(X2),succ(sK3)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f52,plain,
! [X2,X4] :
( ~ in(sK4(X2),X2)
| ~ in(X4,sK2)
| sK4(X2) != X4
| ~ ordinal(X4)
| ~ in(sK4(X2),succ(sK3)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f75,plain,
! [X0] :
( ~ sP1(X0)
| sK10(X0) = sK12(X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f78,plain,
! [X0] :
( ~ sP1(X0)
| ordinal(sK13(X0)) ),
inference(cnf_transformation,[],[f40]) ).
fof(f79,plain,
! [X0] :
( ~ sP1(X0)
| sK10(X0) = sK11(X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f80,plain,
! [X0] :
( ~ sP1(X0)
| sK11(X0) != sK12(X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f84,plain,
! [X3,X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X3,sK15(X0,X1))
| in(sK17(X0,X3),X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f85,plain,
! [X3,X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X3,sK15(X0,X1))
| sK17(X0,X3) = X3 ),
inference(cnf_transformation,[],[f46]) ).
fof(f86,plain,
! [X3,X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X3,sK15(X0,X1))
| ordinal(sK17(X0,X3)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f87,plain,
! [X3,X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X3,sK15(X0,X1))
| sK16(X0,X1,X3) = X3 ),
inference(cnf_transformation,[],[f46]) ).
fof(f88,plain,
! [X3,X0,X1] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X3,sK15(X0,X1))
| in(sK16(X0,X1,X3),succ(X1)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f89,plain,
! [X3,X0,X1,X4,X5] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X5,X0)
| X3 != X5
| ~ ordinal(X5)
| X3 != X4
| ~ in(X4,succ(X1))
| in(X3,sK15(X0,X1)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f90,plain,
! [X2] :
( ~ in(sK4(X2),X2)
| ~ in(sK4(X2),sK2)
| ~ ordinal(sK4(X2))
| ~ in(sK4(X2),succ(sK3)) ),
inference(equality_resolution,[],[f52]) ).
fof(f91,plain,
! [X0,X1,X4,X5] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X5,X0)
| X4 != X5
| ~ ordinal(X5)
| ~ in(X4,succ(X1))
| in(X4,sK15(X0,X1)) ),
inference(equality_resolution,[],[f89]) ).
fof(f92,plain,
! [X0,X1,X5] :
( ~ ordinal(X1)
| sP1(X0)
| ~ in(X5,X0)
| ~ ordinal(X5)
| ~ in(X5,succ(X1))
| in(X5,sK15(X0,X1)) ),
inference(equality_resolution,[],[f91]) ).
tcf(c_49,negated_conjecture,
! [X0: $i] :
( ~ ordinal(sK4(X0))
| ~ in(sK4(X0),sK2)
| ~ in(sK4(X0),X0)
| ~ in(sK4(X0),succ(sK3)) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_50,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| in(sK4(X0),succ(sK3)) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( ordinal(sK5(X0))
| in(sK4(X0),X0) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| ( sK4(X0) = sK5(X0) ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_53,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),sK2)
| in(sK4(X0),X0) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_54,negated_conjecture,
ordinal(sK3),
inference(cnf_transformation,[],[f47]) ).
tcf(c_76,plain,
! [X0: $i] :
( ~ sP1(X0)
| ( sK11(X0) != sK12(X0) ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_77,plain,
! [X0: $i] :
( ( sK11(X0) = sK10(X0) )
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_78,plain,
! [X0: $i] :
( ordinal(sK13(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_81,plain,
! [X0: $i] :
( ( sK12(X0) = sK10(X0) )
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X2)
| in(X0,sK15(X2,X1))
| ~ ordinal(X1)
| ~ ordinal(X0)
| ~ in(X0,X2)
| ~ in(X0,succ(X1)) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| in(sK16(X1,X2,X0),succ(X2))
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| ( sK16(X1,X2,X0) = X0 )
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| ordinal(sK17(X1,X0))
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| ( sK17(X1,X0) = X0 )
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1)
| in(sK17(X1,X0),X1)
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_2934,definition,
iPr_def_10 = succ(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_2935,negated_conjecture,
ordinal(sK3),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_2936,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),sK2)
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_2937,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| ( sK4(X0) = sK5(X0) ) ),
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_2938,negated_conjecture,
! [X0: $i] :
( ordinal(sK5(X0))
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_2939,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),iPr_def_10)
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_50,c_2934]) ).
tcf(c_2940,negated_conjecture,
! [X0: $i] :
( ~ ordinal(sK4(X0))
| ~ in(sK4(X0),iPr_def_10)
| ~ in(sK4(X0),sK2)
| ~ in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_49]) ).
tcf(c_2943,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_3521,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ordinal(sK17(X1,sK4(sK15(X1,X0))))
| ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2937,c_89]) ).
tcf(c_3524,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ordinal(sK5(sK15(X1,X0)))
| ordinal(sK17(X1,sK4(sK15(X1,X0))))
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2938,c_89]) ).
tcf(c_3572,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK17(X1,sK4(sK15(X1,X0))),X1)
| ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2937,c_91]) ).
tcf(c_3574,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK5(sK15(X1,X0)),sK2)
| in(sK17(X1,sK4(sK15(X1,X0))),X1)
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2936,c_91]) ).
tcf(c_3623,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ( sK17(X1,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2937,c_90]) ).
tcf(c_3624,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK4(sK15(X1,X0)),iPr_def_10)
| ( sK17(X1,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2939,c_90]) ).
tcf(c_3625,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK5(sK15(X1,X0)),sK2)
| ( sK17(X1,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2936,c_90]) ).
tcf(c_3626,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ordinal(sK5(sK15(X1,X0)))
| ( sK17(X1,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2938,c_90]) ).
tcf(c_3628,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X2)
| ( sK17(X2,X0) = X0 )
| ~ ordinal(X1)
| ~ ordinal(X0)
| ~ in(X0,X2)
| ~ in(X0,succ(X1)) ),
inference(superposition,[status(thm)],[c_86,c_90]) ).
tcf(c_3682,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK16(X1,sK3,X0),iPr_def_10)
| ~ ordinal(sK3)
| ~ in(X0,sK15(X1,sK3)) ),
inference(superposition,[status(thm)],[c_2934,c_87]) ).
tcf(c_3684,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK16(X1,sK3,X0),iPr_def_10)
| ~ in(X0,sK15(X1,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3682,c_2935]) ).
tcf(c_3694,plain,
! [X0: $i,X1: $i] :
( ( sK11(X0) = sK12(X0) )
| ( sK12(X0) != X1 )
| ( sK11(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_2943]) ).
tcf(c_3945,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ( sK16(X1,X0,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2937,c_88]) ).
tcf(c_3946,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| in(sK4(sK15(X1,X0)),iPr_def_10)
| ( sK16(X1,X0,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2939,c_88]) ).
tcf(c_4022,plain,
! [X0: $i] :
( ( sK11(X0) = sK12(X0) )
| ( sK12(X0) != sK10(X0) )
| ( sK11(X0) != sK10(X0) ) ),
inference(instantiation,[status(thm)],[c_3694]) ).
tcf(c_4395,plain,
! [X0: $i] :
( sP1(X0)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ( sK17(X0,sK4(sK15(X0,sK3))) = sK4(sK15(X0,sK3)) ) ),
inference(superposition,[status(thm)],[c_2935,c_3623]) ).
tcf(c_5010,plain,
! [X0: $i] : ~ sP1(X0),
inference(global_subsumption_just,[status(thm)],[c_78,c_81,c_77,c_76,c_4022]) ).
tcf(c_5133,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ( sK17(X1,X0) = X0 )
| ~ ordinal(sK3)
| ~ ordinal(X0)
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_2934,c_3628]) ).
tcf(c_5134,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ( sK17(X1,X0) = X0 )
| ~ ordinal(X0)
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5133,c_2935]) ).
tcf(c_5787,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK16(X1,X2,X0) = X0 )
| ~ ordinal(X2)
| ~ in(X0,sK15(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_88,c_5010]) ).
tcf(c_5797,plain,
! [X0: $i,X1: $i] :
( ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ( sK16(X1,X0,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(superposition,[status(thm)],[c_2937,c_5787]) ).
tcf(c_6460,plain,
! [X0: $i] :
( ( sK17(X0,sK4(sK15(X0,sK3))) = sK4(sK15(X0,sK3)) )
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(global_subsumption_just,[status(thm)],[c_4395,c_4395,c_5010]) ).
tcf(c_6461,plain,
! [X0: $i] :
( ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ( sK17(X0,sK4(sK15(X0,sK3))) = sK4(sK15(X0,sK3)) ) ),
inference(renaming,[status(thm)],[c_6460]) ).
tcf(c_6474,plain,
! [X0: $i] :
( sP1(X0)
| in(sK4(sK15(X0,sK3)),X0)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_6461,c_3572]) ).
tcf(c_6475,plain,
! [X0: $i] :
( sP1(X0)
| ordinal(sK4(sK15(X0,sK3)))
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_6461,c_3521]) ).
tcf(c_6482,plain,
! [X0: $i] :
( sP1(X0)
| ordinal(sK4(sK15(X0,sK3)))
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6475,c_2935]) ).
tcf(c_6489,plain,
! [X0: $i] :
( sP1(X0)
| in(sK4(sK15(X0,sK3)),X0)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6474,c_2935]) ).
tcf(c_6590,plain,
! [X0: $i] :
( ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ordinal(sK4(sK15(X0,sK3))) ),
inference(global_subsumption_just,[status(thm)],[c_6482,c_81,c_77,c_76,c_4022,c_6482]) ).
tcf(c_6591,plain,
! [X0: $i] :
( ordinal(sK4(sK15(X0,sK3)))
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(renaming,[status(thm)],[c_6590]) ).
tcf(c_6612,plain,
! [X0: $i] :
( ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| in(sK4(sK15(X0,sK3)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_6489,c_5010,c_6489]) ).
tcf(c_6613,plain,
! [X0: $i] :
( in(sK4(sK15(X0,sK3)),X0)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(renaming,[status(thm)],[c_6612]) ).
tcf(c_6619,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6613,c_2940]) ).
tcf(c_8404,plain,
! [X0: $i,X1: $i] :
( ~ ordinal(X0)
| ( sK16(X1,X0,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) ) ),
inference(global_subsumption_just,[status(thm)],[c_3945,c_5797]) ).
tcf(c_8405,plain,
! [X0: $i,X1: $i] :
( ( sK4(sK15(X1,X0)) = sK5(sK15(X1,X0)) )
| ( sK16(X1,X0,sK4(sK15(X1,X0))) = sK4(sK15(X1,X0)) )
| ~ ordinal(X0) ),
inference(renaming,[status(thm)],[c_8404]) ).
tcf(c_8412,plain,
! [X0: $i] :
( ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ( sK16(X0,sK3,sK4(sK15(X0,sK3))) = sK4(sK15(X0,sK3)) ) ),
inference(superposition,[status(thm)],[c_2935,c_8405]) ).
tcf(c_8725,plain,
! [X0: $i] :
( sP1(X0)
| in(sK4(sK15(X0,sK3)),iPr_def_10)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ~ in(sK4(sK15(X0,sK3)),sK15(X0,sK3)) ),
inference(superposition,[status(thm)],[c_8412,c_3684]) ).
tcf(c_11553,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6619,c_6591,c_2937]) ).
tcf(c_13068,plain,
! [X0: $i] :
( ~ in(sK4(sK15(X0,sK3)),sK15(X0,sK3))
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| in(sK4(sK15(X0,sK3)),iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_8725,c_81,c_77,c_76,c_4022,c_8725]) ).
tcf(c_13069,plain,
! [X0: $i] :
( in(sK4(sK15(X0,sK3)),iPr_def_10)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) )
| ~ in(sK4(sK15(X0,sK3)),sK15(X0,sK3)) ),
inference(renaming,[status(thm)],[c_13068]) ).
tcf(c_13074,plain,
! [X0: $i] :
( in(sK4(sK15(X0,sK3)),iPr_def_10)
| ( sK4(sK15(X0,sK3)) = sK5(sK15(X0,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13069,c_2939]) ).
tcf(c_13081,plain,
sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)),
inference(backward_subsumption_resolution,[status(thm)],[c_11553,c_13074]) ).
tcf(c_13329,plain,
( in(sK4(sK15(sK2,sK3)),sK2)
| in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_13081,c_2936]) ).
tcf(c_13334,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_13081,c_3625]) ).
tcf(c_13335,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_13081,c_3626]) ).
tcf(c_13340,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13335,c_2935]) ).
tcf(c_13347,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13334,c_2935]) ).
tcf(c_13407,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| in(sK17(sK2,sK4(sK15(sK2,sK3))),sK2)
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_13329,c_91]) ).
tcf(c_13415,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| in(sK17(sK2,sK4(sK15(sK2,sK3))),sK2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13407,c_2935]) ).
tcf(c_13738,plain,
( sP1(sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(superposition,[status(thm)],[c_13347,c_5134]) ).
tcf(c_13904,plain,
( sP1(sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_13738,c_13340,c_13738]) ).
tcf(c_13914,plain,
( sP1(sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_3624,c_13904]) ).
tcf(c_13916,plain,
( sP1(sK2)
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13914,c_2935]) ).
tcf(c_13926,plain,
( ( sK12(sK2) = sK10(sK2) )
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_13916,c_81]) ).
tcf(c_13928,plain,
( ( sK11(sK2) = sK10(sK2) )
| ( sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_13916,c_77]) ).
tcf(c_13962,plain,
( sP1(sK2)
| ordinal(sK5(sK15(sK2,sK3)))
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_13926,c_3524]) ).
tcf(c_13967,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2) = sK10(sK2) ) ),
inference(superposition,[status(thm)],[c_13926,c_13415]) ).
tcf(c_13983,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK3) ),
inference(light_normalisation,[status(thm)],[c_13962,c_13081]) ).
tcf(c_13984,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK12(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13983,c_2935]) ).
tcf(c_14061,plain,
( ordinal(sK4(sK15(sK2,sK3)))
| ( sK12(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13984,c_81]) ).
tcf(c_14323,plain,
( sP1(sK2)
| ordinal(sK5(sK15(sK2,sK3)))
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_13928,c_3524]) ).
tcf(c_14328,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2) = sK10(sK2) ) ),
inference(superposition,[status(thm)],[c_13928,c_13415]) ).
tcf(c_14344,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK3) ),
inference(light_normalisation,[status(thm)],[c_14323,c_13081]) ).
tcf(c_14345,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ( sK11(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14344,c_2935]) ).
tcf(c_14670,plain,
( ordinal(sK4(sK15(sK2,sK3)))
| ( sK11(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14345,c_77]) ).
tcf(c_14701,plain,
( in(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13967,c_81]) ).
tcf(c_14708,plain,
( ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_14701,c_2940]) ).
tcf(c_14815,plain,
( ( sK12(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14708,c_14061]) ).
tcf(c_14831,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),succ(sK3)) ),
inference(superposition,[status(thm)],[c_86,c_14815]) ).
tcf(c_14846,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2) ),
inference(light_normalisation,[status(thm)],[c_14831,c_2934]) ).
tcf(c_14847,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14846,c_2935]) ).
tcf(c_14933,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_14847,c_13984,c_13967,c_14847]) ).
tcf(c_14938,plain,
( ( sK12(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14933,c_81]) ).
tcf(c_14945,plain,
( in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK12(sK2) = sK10(sK2) ) ),
inference(superposition,[status(thm)],[c_2939,c_14938]) ).
tcf(c_14946,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_3946,c_14938]) ).
tcf(c_14951,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14946,c_2935]) ).
tcf(c_14958,plain,
( in(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2) = sK10(sK2) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14328,c_77]) ).
tcf(c_14965,plain,
( ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_14958,c_2940]) ).
tcf(c_15410,plain,
( ( sK12(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14951,c_81]) ).
tcf(c_15419,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ( sK12(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_15410,c_3684]) ).
tcf(c_15463,plain,
( ( sK11(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14965,c_14670]) ).
tcf(c_15479,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),succ(sK3)) ),
inference(superposition,[status(thm)],[c_86,c_15463]) ).
tcf(c_15502,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2) ),
inference(light_normalisation,[status(thm)],[c_15479,c_2934]) ).
tcf(c_15503,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15502,c_2935]) ).
tcf(c_15509,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_15503,c_14345,c_14328,c_15503]) ).
tcf(c_15514,plain,
( ( sK11(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15509,c_77]) ).
tcf(c_15521,plain,
( in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK11(sK2) = sK10(sK2) ) ),
inference(superposition,[status(thm)],[c_2939,c_15514]) ).
tcf(c_15522,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_3946,c_15514]) ).
tcf(c_15527,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15522,c_2935]) ).
tcf(c_15692,plain,
( ( sK11(sK2) = sK10(sK2) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15527,c_77]) ).
tcf(c_15701,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ( sK11(sK2) = sK10(sK2) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_15692,c_3684]) ).
tcf(c_16500,plain,
( sP1(sK2)
| ( sK12(sK2) = sK10(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_15419,c_14933,c_14945,c_15419]) ).
tcf(c_16504,plain,
sK12(sK2) = sK10(sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_16500,c_81]) ).
tcf(c_16600,plain,
( sP1(sK2)
| ( sK11(sK2) = sK10(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_15701,c_15509,c_15521,c_15701]) ).
tcf(c_16602,plain,
( sP1(sK2)
| ( sK11(sK2) = sK12(sK2) ) ),
inference(light_normalisation,[status(thm)],[c_16600,c_16504]) ).
tcf(c_16612,plain,
( ( sK11(sK2) = sK10(sK2) )
| ( sK11(sK2) = sK12(sK2) ) ),
inference(superposition,[status(thm)],[c_16602,c_77]) ).
tcf(c_16613,plain,
sK11(sK2) = sK12(sK2),
inference(light_normalisation,[status(thm)],[c_16612,c_16504]) ).
tcf(c_16803,plain,
~ sP1(sK2),
inference(superposition,[status(thm)],[c_16613,c_76]) ).
tcf(c_16804,plain,
sK17(sK2,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)),
inference(backward_subsumption_resolution,[status(thm)],[c_13916,c_16803]) ).
tcf(c_16849,plain,
( sP1(sK2)
| in(sK5(sK15(sK2,sK3)),sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_16804,c_3574]) ).
tcf(c_16854,plain,
( sP1(sK2)
| ordinal(sK5(sK15(sK2,sK3)))
| ordinal(sK4(sK15(sK2,sK3)))
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_16804,c_3524]) ).
tcf(c_16855,plain,
( sP1(sK2)
| ordinal(sK4(sK15(sK2,sK3)))
| ~ ordinal(sK3) ),
inference(light_normalisation,[status(thm)],[c_16854,c_13081]) ).
tcf(c_16856,plain,
ordinal(sK4(sK15(sK2,sK3))),
inference(forward_subsumption_resolution,[status(thm)],[c_16855,c_16803,c_2935]) ).
tcf(c_16871,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),sK2)
| ~ ordinal(sK3) ),
inference(light_normalisation,[status(thm)],[c_16849,c_13081]) ).
tcf(c_16872,plain,
in(sK4(sK15(sK2,sK3)),sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_16871,c_16803,c_2935]) ).
tcf(c_16886,plain,
( ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_16872,c_2940]) ).
tcf(c_16890,plain,
( ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16886,c_16856]) ).
tcf(c_16934,plain,
( sP1(sK2)
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),succ(sK3)) ),
inference(superposition,[status(thm)],[c_86,c_16890]) ).
tcf(c_16946,plain,
( sP1(sK2)
| ~ ordinal(sK3)
| ~ ordinal(sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK2) ),
inference(light_normalisation,[status(thm)],[c_16934,c_2934]) ).
tcf(c_16947,plain,
~ in(sK4(sK15(sK2,sK3)),iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_16946,c_16803,c_2935,c_16856,c_16872]) ).
tcf(c_16948,plain,
in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)),
inference(superposition,[status(thm)],[c_2939,c_16947]) ).
tcf(c_16949,plain,
( sP1(sK2)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ ordinal(sK3) ),
inference(superposition,[status(thm)],[c_3946,c_16947]) ).
tcf(c_16952,plain,
sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)),
inference(forward_subsumption_resolution,[status(thm)],[c_16949,c_16803,c_2935]) ).
tcf(c_16964,plain,
( sP1(sK2)
| in(sK4(sK15(sK2,sK3)),iPr_def_10)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_16952,c_3684]) ).
tcf(c_16966,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_16964,c_16803,c_16947,c_16948]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU272+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 13:29:13 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 8.17/1.77 % SZS status Started for theBenchmark.p
% 8.17/1.77 % SZS status Theorem for theBenchmark.p
% 8.17/1.77
% 8.17/1.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.17/1.77
% 8.17/1.77 % ------ iProver source info
% 8.17/1.77
% 8.17/1.77 % git: date: 2026-07-19 20:42:38 +0200
% 8.17/1.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.17/1.77 % git: non_committed_changes: false
% 8.17/1.77
% 8.17/1.77 % ------ Parsing...
% 8.17/1.77 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.17/1.77
% 8.17/1.77 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 5 0s sf_e pe_s pe_e %
% 8.17/1.77
% 8.17/1.77 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.17/1.77
% 8.17/1.77 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.17/1.77 % ------ Proving...
% 8.17/1.77 % ------ Problem Properties
% 8.17/1.77
% 8.17/1.77 %
% 8.17/1.77 % clauses 30
% 8.17/1.77 % conjectures 6
% 8.17/1.77 % EPR 7
% 8.17/1.77 % Horn 20
% 8.17/1.77 % unary 8
% 8.17/1.77 % binary 15
% 8.17/1.77 % lits 68
% 8.17/1.77 % lits eq 12
% 8.17/1.77 % fd_pure 0
% 8.17/1.77 % fd_pseudo 0
% 8.17/1.77 % fd_cond 0
% 8.17/1.77 % fd_pseudo_cond 0
% 8.17/1.77 % AC symbols 0
% 8.17/1.77
% 8.17/1.77 % ------ Schedule dynamic 5 is on
% 8.17/1.77
% 8.17/1.77 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.17/1.77
% 8.17/1.77
% 8.17/1.77 % ------
% 8.17/1.77 % Current options:
% 8.17/1.77 % ------
% 8.17/1.77
% 8.17/1.77
% 8.17/1.77 %
% 8.17/1.77
% 8.17/1.77 % ------ Proving...
% 8.17/1.77 %
% 8.17/1.77
% 8.17/1.77 % SZS status Theorem for theBenchmark.p
% 8.17/1.77
% 8.17/1.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.17/1.77
% 8.17/1.77
%------------------------------------------------------------------------------