%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN551+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n020.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 03:40:47 PM UTC 2026
% Result : Theorem 3.17s 1.73s
% Output : CNFRefutation 3.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ? [X0] :
! [X1] :
( X1 = f(g(X1))
<=> X0 = X1 )
<=> ? [X0] :
! [X1] :
( X1 = g(f(X1))
<=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_cute_thing) ).
fof(f2,negated_conjecture,
~ ( ? [X0] :
! [X1] :
( X1 = f(g(X1))
<=> X0 = X1 )
<=> ? [X0] :
! [X1] :
( X1 = g(f(X1))
<=> X0 = X1 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ( ? [X0] :
! [X1] :
( X1 = f(g(X1))
<=> X0 = X1 )
<=> ? [X2] :
! [X3] :
( g(f(X3)) = X3
<=> X2 = X3 ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
( ? [X0] :
! [X1] :
( X1 = f(g(X1))
<=> X0 = X1 )
<~> ? [X2] :
! [X3] :
( g(f(X3)) = X3
<=> X2 = X3 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ? [X0] :
! [X1] :
( ( f(g(X1)) != X1
| X0 = X1 )
& ( X0 != X1
| X1 = f(g(X1)) ) )
| ? [X2] :
! [X3] :
( ( g(f(X3)) != X3
| X2 = X3 )
& ( X2 != X3
| g(f(X3)) = X3 ) ) )
& ( ! [X0] :
? [X1] :
( ( X1 = f(g(X1))
| X0 = X1 )
& ( f(g(X1)) != X1
| X0 != X1 ) )
| ! [X2] :
? [X3] :
( ( g(f(X3)) = X3
| X2 = X3 )
& ( g(f(X3)) != X3
| X2 != X3 ) ) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f6,plain,
( ( ? [X6] :
! [X7] :
( ( f(g(X7)) != X7
| X6 = X7 )
& ( X6 != X7
| f(g(X7)) = X7 ) )
| ? [X4] :
! [X5] :
( ( g(f(X5)) != X5
| X4 = X5 )
& ( X4 != X5
| g(f(X5)) = X5 ) ) )
& ( ! [X2] :
? [X3] :
( ( f(g(X3)) = X3
| X2 = X3 )
& ( f(g(X3)) != X3
| X2 != X3 ) )
| ! [X0] :
? [X1] :
( ( g(f(X1)) = X1
| X0 = X1 )
& ( g(f(X1)) != X1
| X0 != X1 ) ) ) ),
inference(rectify,[],[f5]) ).
fof(f7,plain,
( ( ! [X7] :
( ( f(g(X7)) != X7
| sK3 = X7 )
& ( sK3 != X7
| f(g(X7)) = X7 ) )
| ! [X5] :
( ( g(f(X5)) != X5
| sK2 = X5 )
& ( sK2 != X5
| g(f(X5)) = X5 ) ) )
& ( ! [X2] :
( ( sK1(X2) = f(g(sK1(X2)))
| sK1(X2) = X2 )
& ( sK1(X2) != f(g(sK1(X2)))
| sK1(X2) != X2 ) )
| ! [X0] :
( ( sK0(X0) = g(f(sK0(X0)))
| sK0(X0) = X0 )
& ( sK0(X0) != g(f(sK0(X0)))
| sK0(X0) != X0 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X1,sK0(X0)),skolemize(X3,sK1(X2)),skolemize(X4,sK2),skolemize(X6,sK3)],[f6]) ).
fof(f8,plain,
! [X7,X5] :
( f(g(X7)) != X7
| sK3 = X7
| g(f(X5)) != X5
| sK2 = X5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f9,plain,
! [X7,X5] :
( sK3 != X7
| f(g(X7)) = X7
| g(f(X5)) != X5
| sK2 = X5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f10,plain,
! [X7,X5] :
( f(g(X7)) != X7
| sK3 = X7
| sK2 != X5
| g(f(X5)) = X5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f11,plain,
! [X7,X5] :
( sK3 != X7
| f(g(X7)) = X7
| sK2 != X5
| g(f(X5)) = X5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f12,plain,
! [X2,X0] :
( sK1(X2) = f(g(sK1(X2)))
| sK1(X2) = X2
| sK0(X0) = g(f(sK0(X0)))
| sK0(X0) = X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f13,plain,
! [X2,X0] :
( sK1(X2) != f(g(sK1(X2)))
| sK1(X2) != X2
| sK0(X0) = g(f(sK0(X0)))
| sK0(X0) = X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f14,plain,
! [X2,X0] :
( sK1(X2) = f(g(sK1(X2)))
| sK1(X2) = X2
| sK0(X0) != g(f(sK0(X0)))
| sK0(X0) != X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f15,plain,
! [X2,X0] :
( sK1(X2) != f(g(sK1(X2)))
| sK1(X2) != X2
| sK0(X0) != g(f(sK0(X0)))
| sK0(X0) != X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f16,plain,
! [X7] :
( sK3 != X7
| f(g(X7)) = X7
| sK2 = g(f(sK2)) ),
inference(equality_resolution,[],[f11]) ).
fof(f17,plain,
( sK3 = f(g(sK3))
| sK2 = g(f(sK2)) ),
inference(equality_resolution,[],[f16]) ).
fof(f18,plain,
! [X7] :
( f(g(X7)) != X7
| sK3 = X7
| sK2 = g(f(sK2)) ),
inference(equality_resolution,[],[f10]) ).
fof(f19,plain,
! [X5] :
( sK3 = f(g(sK3))
| g(f(X5)) != X5
| sK2 = X5 ),
inference(equality_resolution,[],[f9]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sK1(X1) != X1 )
| ( sK0(X0) != X0 )
| ( g(f(sK0(X0))) != sK0(X0) )
| ( f(g(sK1(X1))) != sK1(X1) ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_50,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sK1(X1) = X1 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( sK0(X0) != X0 )
| ( g(f(sK0(X0))) != sK0(X0) ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_51,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ( sK1(X0) != X0 )
| ( f(g(sK1(X0))) != sK1(X0) ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_52,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sK1(X1) = X1 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) )
| ( f(g(sK1(X1))) = sK1(X1) ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_53,negated_conjecture,
( ( g(f(sK2)) = sK2 )
| ( f(g(sK3)) = sK3 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_54,negated_conjecture,
! [X0: $i] :
( ( X0 = sK3 )
| ( g(f(sK2)) = sK2 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_55,negated_conjecture,
! [X0: $i] :
( ( X0 = sK2 )
| ( f(g(sK3)) = sK3 )
| ( g(f(X0)) != X0 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_56,negated_conjecture,
! [X0: $i,X1: $i] :
( ( X1 = sK2 )
| ( X0 = sK3 )
| ( g(f(X1)) != X1 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_178,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( g(f(X0)) != X0 )
| ( X0 = sK2 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_56]) ).
tcf(c_179,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( f(g(X0)) != X0 )
| ( X0 = sK3 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_56]) ).
tcf(c_180,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_56]) ).
tcf(c_181,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_52]) ).
tcf(c_182,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( f(g(sK1(X0))) = sK1(X0) )
| ( sK1(X0) = X0 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_52]) ).
tcf(c_183,negated_conjecture,
( iPr_def_13
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_52]) ).
tcf(c_184,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( f(g(sK1(X0))) != sK1(X0) )
| ( sK1(X0) != X0 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_51]) ).
tcf(c_185,negated_conjecture,
( iPr_def_14
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_51]) ).
tcf(c_186,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(sK0(X0))) != sK0(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_50]) ).
tcf(c_187,negated_conjecture,
( iPr_def_15
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_50]) ).
tcf(c_188,negated_conjecture,
( iPr_def_15
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_49]) ).
tcf(c_189,definition,
iPr_def_16 = g(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_190,definition,
iPr_def_17 = f(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_191,definition,
iPr_def_18 = f(sK2),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_192,definition,
iPr_def_19 = g(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_193,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_180]) ).
tcf(c_194,negated_conjecture,
! [X0: $i] :
( ( X0 = sK3 )
| ~ iPr_def_11
| ( f(g(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_179]) ).
tcf(c_195,negated_conjecture,
! [X0: $i] :
( ( X0 = sK2 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_178]) ).
tcf(c_196,negated_conjecture,
! [X0: $i] :
( ( iPr_def_17 = sK3 )
| ( X0 = sK2 )
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_55,c_189,c_190]) ).
tcf(c_197,negated_conjecture,
! [X0: $i] :
( ( iPr_def_19 = sK2 )
| ( X0 = sK3 )
| ( f(g(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_54,c_191,c_192]) ).
tcf(c_198,negated_conjecture,
( ( iPr_def_19 = sK2 )
| ( iPr_def_17 = sK3 ) ),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_199,negated_conjecture,
( iPr_def_13
| iPr_def_12 ),
inference(demodulation,[status(thm)],[c_183]) ).
tcf(c_202,negated_conjecture,
( iPr_def_14
| iPr_def_12 ),
inference(demodulation,[status(thm)],[c_185]) ).
tcf(c_204,negated_conjecture,
! [X0: $i] :
( ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) )
| ~ iPr_def_12 ),
inference(demodulation,[status(thm)],[c_181]) ).
tcf(c_205,negated_conjecture,
( iPr_def_15
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_187]) ).
tcf(c_207,negated_conjecture,
! [X0: $i] :
( ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_13 ),
inference(demodulation,[status(thm)],[c_182]) ).
tcf(c_208,negated_conjecture,
( iPr_def_15
| iPr_def_14 ),
inference(demodulation,[status(thm)],[c_188]) ).
tcf(c_209,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( sK1(X0) != X0 )
| ( f(g(sK1(X0))) != sK1(X0) ) ),
inference(demodulation,[status(thm)],[c_184]) ).
tcf(c_210,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(sK0(X0))) != sK0(X0) ) ),
inference(demodulation,[status(thm)],[c_186]) ).
tcf(c_354,plain,
( ( sK2 = iPr_def_19 )
| ( g(iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_198,c_189]) ).
tcf(c_358,plain,
( ( sK2 = iPr_def_16 )
| ~ iPr_def_10
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_195]) ).
tcf(c_363,plain,
( ( sK3 = iPr_def_18 )
| ~ iPr_def_11
| ( f(iPr_def_19) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_192,c_194]) ).
tcf(c_421,plain,
( ( sK3 = iPr_def_17 )
| ( sK2 = iPr_def_19 )
| ( f(iPr_def_16) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_354,c_197]) ).
tcf(c_422,plain,
( ( sK3 = iPr_def_17 )
| ( sK2 = iPr_def_19 ) ),
inference(ground_joinability,[status(thm)],[c_421,c_190]) ).
tcf(c_440,plain,
! [X0: $i] :
( iPr_def_12
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_199,c_207]) ).
tcf(c_493,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_440,c_204]) ).
tcf(c_508,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = sK3 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_493,c_194]) ).
tcf(c_509,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = sK2 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_493,c_196]) ).
tcf(c_510,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = sK2 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_493,c_195]) ).
tcf(c_512,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X1) = sK3 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(superposition,[status(thm)],[c_493,c_197]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = sK2 )
| ( sK0(X1) = X1 )
| ( g(sK1(X0)) = sK2 ) ),
inference(superposition,[status(thm)],[c_509,c_196]) ).
tcf(c_587,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = sK2 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( X0 != sK2 ) ),
inference(equality_factoring,[status(thm)],[c_509]) ).
tcf(c_734,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = sK2 )
| ( g(sK1(X1)) = sK2 )
| ( X0 != sK2 ) ),
inference(equality_factoring,[status(thm)],[c_585]) ).
tcf(c_828,plain,
! [X0: $i,X1: $i] :
( iPr_def_10
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = sK3 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_193,c_508]) ).
tcf(c_845,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X3) = sK2 )
| ( sK0(X3) = X3 )
| ( sK0(X2) = X2 )
| ( f(sK0(X2)) = sK3 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_828,c_510]) ).
tcf(c_986,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ~ iPr_def_14
| ( sK1(X0) != X0 )
| ( f(g(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_512,c_209]) ).
tcf(c_988,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X1) = sK3 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = sK3 ) ),
inference(superposition,[status(thm)],[c_512,c_197]) ).
tcf(c_1115,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = sK3 )
| ( X0 != sK3 ) ),
inference(equality_factoring,[status(thm)],[c_988]) ).
tcf(c_1440,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(sK2) = sK2 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = sK2 ) ),
inference(equality_resolution,[status(thm)],[c_734]) ).
tcf(c_1481,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = sK3 ) ),
inference(equality_resolution,[status(thm)],[c_1115]) ).
tcf(c_1836,plain,
! [X0: $i] :
( iPr_def_12
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_199,c_207]) ).
tcf(c_1883,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_1836,c_204]) ).
tcf(c_1991,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = sK2 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_1883,c_196]) ).
tcf(c_2132,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ~ iPr_def_14
| ( f(g(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_986,c_512]) ).
tcf(c_2160,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) )
| ~ iPr_def_14
| ( f(iPr_def_16) != sK3 ) ),
inference(superposition,[status(thm)],[c_189,c_2132]) ).
tcf(c_2175,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) )
| ~ iPr_def_14
| ( sK3 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_2160,c_190]) ).
tcf(c_2238,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(sK2) = sK2 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(equality_resolution,[status(thm)],[c_587]) ).
tcf(c_2276,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_2175,c_202,c_204,c_422,c_2175]) ).
tcf(c_2287,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( sK0(X0) = g(sK3) ) ),
inference(superposition,[status(thm)],[c_1481,c_2276]) ).
tcf(c_2303,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = iPr_def_16 )
| ( sK0(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_2287,c_189]) ).
tcf(c_2375,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = iPr_def_16 )
| ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_2303,c_210]) ).
tcf(c_2381,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(equality_factoring,[status(thm)],[c_2303]) ).
tcf(c_2725,plain,
! [X0: $i,X1: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = sK2 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( X0 != sK2 ) ),
inference(equality_factoring,[status(thm)],[c_1991]) ).
tcf(c_2909,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(equality_resolution,[status(thm)],[c_2381]) ).
tcf(c_2926,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_422,c_2909]) ).
tcf(c_2934,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14
| ( sK1(sK3) != sK3 )
| ( f(g(sK3)) != sK3 ) ),
inference(superposition,[status(thm)],[c_2909,c_209]) ).
tcf(c_2938,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14
| ( sK3 != iPr_def_17 )
| ( sK1(sK3) != sK3 ) ),
inference(light_normalisation,[status(thm)],[c_2934,c_189,c_190]) ).
tcf(c_2982,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = iPr_def_16 )
| ~ iPr_def_15
| ( g(f(X0)) != X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_2375,c_2303,c_2375]) ).
tcf(c_2995,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( sK0(sK0(X0)) = iPr_def_16 )
| ~ iPr_def_15 ),
inference(superposition,[status(thm)],[c_2276,c_2982]) ).
tcf(c_4618,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 )
| ( f(g(iPr_def_17)) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2926,c_209]) ).
tcf(c_4832,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(sK2) = sK2 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(equality_resolution,[status(thm)],[c_2725]) ).
tcf(c_4837,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_4618,c_422,c_2909,c_2938]) ).
tcf(c_4845,plain,
( iPr_def_12
| ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_202,c_4837]) ).
tcf(c_4903,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(superposition,[status(thm)],[c_4845,c_204]) ).
tcf(c_4937,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = sK3 ) ),
inference(superposition,[status(thm)],[c_4903,c_197]) ).
tcf(c_5071,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( sK0(X0) = g(sK3) ) ),
inference(superposition,[status(thm)],[c_4937,c_4903]) ).
tcf(c_5084,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = iPr_def_16 )
| ( sK0(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5071,c_189]) ).
tcf(c_5350,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(sK2) = sK2 )
| ( sK1(X0) = sK3 )
| ( sK1(X0) = X0 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_4832,c_194]) ).
tcf(c_5766,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( iPr_def_16 != iPr_def_16 ) ),
inference(equality_factoring,[status(thm)],[c_5084]) ).
tcf(c_5768,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(equality_resolution_simp,[status(thm)],[c_5766]) ).
tcf(c_5784,plain,
! [X0: $i] :
( iPr_def_13
| ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK0(X0) = X0 )
| ( sK0(sK0(X0)) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_205,c_2995]) ).
tcf(c_5833,plain,
! [X0: $i,X1: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( sK0(sK0(X1)) = iPr_def_16 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_5784,c_207]) ).
tcf(c_5855,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_15
| ( sK0(iPr_def_16) != iPr_def_16 )
| ( g(f(iPr_def_16)) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5768,c_210]) ).
tcf(c_5860,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_15
| ( g(iPr_def_17) != iPr_def_16 )
| ( sK0(iPr_def_16) != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_5855,c_190]) ).
tcf(c_5875,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_15 ),
inference(global_subsumption_just,[status(thm)],[c_5860,c_354,c_5768,c_5860]) ).
tcf(c_5881,plain,
( iPr_def_14
| ( sK2 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_208,c_5875]) ).
tcf(c_5882,plain,
( iPr_def_13
| ( sK2 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_205,c_5875]) ).
tcf(c_5920,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_5882,c_207]) ).
tcf(c_5941,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ( sK1(X0) = X0 ) ),
inference(superposition,[status(thm)],[c_5920,c_197]) ).
tcf(c_5995,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ~ iPr_def_14
| ( sK1(X0) != X0 )
| ( f(g(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_5941,c_209]) ).
tcf(c_6043,plain,
! [X0: $i] :
( ( sK2 = iPr_def_19 )
| ( sK1(X0) = sK3 )
| ( f(g(X0)) != X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_5995,c_5881,c_5941,c_5995]) ).
tcf(c_6062,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( f(iPr_def_16) != sK3 ) ),
inference(superposition,[status(thm)],[c_189,c_6043]) ).
tcf(c_6071,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 )
| ( sK3 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_6062,c_190]) ).
tcf(c_6126,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(sK3) = sK3 ) ),
inference(global_subsumption_just,[status(thm)],[c_5833,c_422,c_6071]) ).
tcf(c_6132,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_422,c_6126]) ).
tcf(c_6140,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14
| ( sK1(sK3) != sK3 )
| ( f(g(sK3)) != sK3 ) ),
inference(superposition,[status(thm)],[c_6126,c_209]) ).
tcf(c_6143,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14
| ( sK3 != iPr_def_17 )
| ( sK1(sK3) != sK3 ) ),
inference(light_normalisation,[status(thm)],[c_6140,c_189,c_190]) ).
tcf(c_6148,plain,
sK2 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_6132,c_422,c_5881,c_6126,c_6143]) ).
tcf(c_6175,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1440,c_6148]) ).
tcf(c_6190,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_358,c_6148]) ).
tcf(c_6192,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( X0 = iPr_def_19 )
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_196,c_6148]) ).
tcf(c_6193,plain,
f(iPr_def_19) = iPr_def_18,
inference(demodulation,[status(thm)],[c_191,c_6148]) ).
tcf(c_6194,plain,
! [X0: $i] :
( ( X0 = iPr_def_19 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_195,c_6148]) ).
tcf(c_6304,plain,
( ( sK3 = iPr_def_18 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_363,c_6193]) ).
tcf(c_6366,plain,
( iPr_def_10
| ( sK3 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_193,c_6304]) ).
tcf(c_6448,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(light_normalisation,[status(thm)],[c_2238,c_6148]) ).
tcf(c_6461,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = X0 )
| ( sK1(X0) = f(iPr_def_19) ) ),
inference(superposition,[status(thm)],[c_6175,c_6448]) ).
tcf(c_6467,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = iPr_def_18 )
| ( sK1(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_6461,c_6193]) ).
tcf(c_6500,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = iPr_def_18 )
| ~ iPr_def_14
| ( sK1(X0) != X0 )
| ( f(g(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_6467,c_209]) ).
tcf(c_6501,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(equality_factoring,[status(thm)],[c_6467]) ).
tcf(c_6567,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK1(X0) = iPr_def_18 )
| ~ iPr_def_14
| ( f(g(X0)) != X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_6500,c_6467,c_6500]) ).
tcf(c_6585,plain,
( ( sK3 = iPr_def_17 )
| ( sK1(iPr_def_18) = iPr_def_18 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ~ iPr_def_14
| ( f(iPr_def_19) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_192,c_6567]) ).
tcf(c_6586,plain,
( ( sK3 = iPr_def_17 )
| ( sK1(iPr_def_18) = iPr_def_18 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ~ iPr_def_14 ),
inference(ground_joinability,[status(thm)],[c_6585,c_6193]) ).
tcf(c_6894,plain,
( ( sK3 = iPr_def_17 )
| ( sK1(iPr_def_18) = iPr_def_18 )
| ( sK0(iPr_def_19) = iPr_def_19 ) ),
inference(equality_resolution,[status(thm)],[c_6501]) ).
tcf(c_6908,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 )
| ( f(g(iPr_def_18)) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_6894,c_209]) ).
tcf(c_6913,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 ) ),
inference(ground_joinability,[status(thm)],[c_6908,c_192,c_6193]) ).
tcf(c_6918,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_6913,c_6586,c_6913]) ).
tcf(c_6926,plain,
( iPr_def_12
| ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_202,c_6918]) ).
tcf(c_6936,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(superposition,[status(thm)],[c_6926,c_204]) ).
tcf(c_6952,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( sK0(X0) = iPr_def_19 )
| ( sK0(X0) = X0 ) ),
inference(superposition,[status(thm)],[c_6936,c_6192]) ).
tcf(c_7024,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( iPr_def_19 != iPr_def_19 ) ),
inference(equality_factoring,[status(thm)],[c_6952]) ).
tcf(c_7026,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 ) ),
inference(equality_resolution_simp,[status(thm)],[c_7024]) ).
tcf(c_7271,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_15
| ( sK0(iPr_def_19) != iPr_def_19 )
| ( g(f(iPr_def_19)) != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_7026,c_210]) ).
tcf(c_7273,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_15
| ( sK0(iPr_def_19) != iPr_def_19 ) ),
inference(ground_joinability,[status(thm)],[c_7271,c_192,c_6193]) ).
tcf(c_7277,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_15 ),
inference(global_subsumption_just,[status(thm)],[c_7273,c_7026,c_7273]) ).
tcf(c_7283,plain,
( iPr_def_14
| ( sK3 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_208,c_7277]) ).
tcf(c_7284,plain,
( iPr_def_13
| ( sK3 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_205,c_7277]) ).
tcf(c_7297,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_7284,c_207]) ).
tcf(c_7311,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_7297,c_6192]) ).
tcf(c_7366,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( sK1(X0) = f(iPr_def_19) ) ),
inference(superposition,[status(thm)],[c_7311,c_7297]) ).
tcf(c_7370,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = iPr_def_18 )
| ( sK1(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_7366,c_6193]) ).
tcf(c_7455,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = iPr_def_18 )
| ~ iPr_def_14
| ( sK1(X0) != X0 )
| ( f(g(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_7370,c_209]) ).
tcf(c_7456,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( sK1(X0) = iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(equality_factoring,[status(thm)],[c_7370]) ).
tcf(c_7494,plain,
( ( sK3 = iPr_def_17 )
| ( sK1(iPr_def_18) = iPr_def_18 ) ),
inference(equality_resolution,[status(thm)],[c_7456]) ).
tcf(c_7504,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 )
| ( f(g(iPr_def_18)) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_7494,c_209]) ).
tcf(c_7505,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 ) ),
inference(ground_joinability,[status(thm)],[c_7504,c_192,c_6193]) ).
tcf(c_7509,plain,
sK3 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_7455,c_7283,c_7494,c_7505]) ).
tcf(c_7521,plain,
( iPr_def_10
| ( iPr_def_17 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_6366,c_7509]) ).
tcf(c_7528,plain,
g(iPr_def_17) = iPr_def_16,
inference(demodulation,[status(thm)],[c_189,c_7509]) ).
tcf(c_7529,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ~ iPr_def_11
| ( f(g(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_194,c_7509]) ).
tcf(c_7557,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6190,c_7528]) ).
tcf(c_7666,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_7521,c_7557]) ).
tcf(c_7709,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( f(iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_7666,c_6193]) ).
tcf(c_7710,plain,
iPr_def_17 = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_7709,c_190]) ).
tcf(c_7712,plain,
g(iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_192,c_7710]) ).
tcf(c_7713,plain,
iPr_def_16 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_7712,c_7528]) ).
tcf(c_7716,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_6194,c_7713]) ).
tcf(c_7717,plain,
sK2 = iPr_def_16,
inference(demodulation,[status(thm)],[c_6148,c_7713]) ).
tcf(c_7820,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X3) = iPr_def_16 )
| ( sK0(X3) = X3 )
| ( sK0(X2) = X2 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(light_normalisation,[status(thm)],[c_845,c_7509,c_7717]) ).
tcf(c_7872,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ( sK1(X0) != sK1(X0) ) ),
inference(equality_factoring,[status(thm)],[c_7820]) ).
tcf(c_7873,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(equality_resolution_simp,[status(thm)],[c_7872]) ).
tcf(c_8217,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X1) = X1 )
| ( sK0(X2) = X2 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_7873,c_210]) ).
tcf(c_8360,plain,
sK3 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_5350,c_7283,c_7494,c_7505]) ).
tcf(c_8782,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ~ iPr_def_11
| ( f(g(X0)) != X0 ) ),
inference(light_normalisation,[status(thm)],[c_194,c_8360]) ).
tcf(c_8798,plain,
g(iPr_def_17) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_189,c_8360]) ).
tcf(c_8800,plain,
( ( sK2 = iPr_def_16 )
| ~ iPr_def_10
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_195]) ).
tcf(c_8801,plain,
( ( sK2 = iPr_def_16 )
| ~ iPr_def_10 ),
inference(ground_joinability,[status(thm)],[c_8800,c_8798]) ).
tcf(c_8809,plain,
sK2 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_8801,c_7717]) ).
tcf(c_8812,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_195,c_8809]) ).
tcf(c_8835,plain,
! [X0: $i] :
( iPr_def_12
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_199,c_207]) ).
tcf(c_8864,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( g(f(sK0(X1))) = sK0(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_8835,c_204]) ).
tcf(c_8878,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_8864,c_8782]) ).
tcf(c_8879,plain,
! [X0: $i,X1: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X1) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_8864,c_8812]) ).
tcf(c_8958,plain,
! [X0: $i,X1: $i] :
( iPr_def_10
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_193,c_8878]) ).
tcf(c_8976,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X3) = iPr_def_16 )
| ( sK0(X3) = X3 )
| ( sK0(X2) = X2 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_8958,c_8879]) ).
tcf(c_9028,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ( sK1(X0) != sK1(X0) ) ),
inference(equality_factoring,[status(thm)],[c_8976]) ).
tcf(c_9029,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(equality_resolution_simp,[status(thm)],[c_9028]) ).
tcf(c_9149,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X1) = X1 )
| ( sK0(X2) = X2 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_9029,c_210]) ).
tcf(c_9269,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X1) = X1 )
| ( sK0(X2) = X2 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( g(f(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9149,c_9029]) ).
tcf(c_9295,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_9269]) ).
tcf(c_9296,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15 ),
inference(ground_joinability,[status(thm)],[c_9295,c_8798]) ).
tcf(c_9702,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_9296,c_205,c_207,c_9296]) ).
tcf(c_9836,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK1(X1) = X1 )
| ( sK0(X2) = X2 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X2)) = iPr_def_17 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( g(f(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8217,c_7873]) ).
tcf(c_9862,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_9836]) ).
tcf(c_9863,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15 ),
inference(ground_joinability,[status(thm)],[c_9862,c_7528]) ).
tcf(c_10038,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = X1 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_9863,c_9702]) ).
tcf(c_10053,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X2) = X2 )
| ( sK0(X2) = g(iPr_def_17) )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_10038,c_493]) ).
tcf(c_10073,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(light_normalisation,[status(thm)],[c_10053,c_7528]) ).
tcf(c_10534,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ( sK1(X0) != sK1(X0) ) ),
inference(equality_factoring,[status(thm)],[c_10073]) ).
tcf(c_10535,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( sK0(X1) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(equality_resolution_simp,[status(thm)],[c_10534]) ).
tcf(c_10582,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_10535,c_210]) ).
tcf(c_10586,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK0(X2) = iPr_def_16 )
| ( sK0(X2) = X2 )
| ( g(f(X2)) = X2 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(superposition,[status(thm)],[c_10535,c_493]) ).
tcf(c_10899,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(g(sK1(X1))) = sK1(X1) )
| ~ iPr_def_15
| ( g(f(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10582,c_10535]) ).
tcf(c_10925,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_10899]) ).
tcf(c_10926,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_15 ),
inference(ground_joinability,[status(thm)],[c_10925,c_7528]) ).
tcf(c_10958,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( f(g(sK1(X0))) = sK1(X0) )
| ( sK1(X0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_10586,c_205,c_207,c_10926]) ).
tcf(c_10959,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(renaming,[status(thm)],[c_10958]) ).
tcf(c_10968,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_10959,c_7529]) ).
tcf(c_10970,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_10959,c_7716]) ).
tcf(c_10997,plain,
! [X0: $i] :
( iPr_def_10
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 ) ),
inference(superposition,[status(thm)],[c_193,c_10968]) ).
tcf(c_11876,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_10997,c_10970]) ).
tcf(c_11921,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( sK1(X0) = f(iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_11876,c_10959]) ).
tcf(c_11940,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X1) = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_11921,c_190]) ).
tcf(c_12166,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( X0 != X0 ) ),
inference(equality_factoring,[status(thm)],[c_11940]) ).
tcf(c_12168,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 ) ),
inference(equality_resolution_simp,[status(thm)],[c_12166]) ).
tcf(c_12195,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK1(X0) = iPr_def_17 )
| ( X0 != iPr_def_17 ) ),
inference(equality_factoring,[status(thm)],[c_12168]) ).
tcf(c_13003,plain,
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(equality_resolution,[status(thm)],[c_12195]) ).
tcf(c_13014,plain,
( ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 )
| ( f(g(iPr_def_17)) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_13003,c_209]) ).
tcf(c_13015,plain,
( ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 ) ),
inference(ground_joinability,[status(thm)],[c_13014,c_190,c_7528]) ).
tcf(c_13019,plain,
( ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_13015,c_13003,c_13015]) ).
tcf(c_13025,plain,
( iPr_def_12
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_202,c_13019]) ).
tcf(c_13032,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( g(f(sK0(X0))) = sK0(X0) ) ),
inference(superposition,[status(thm)],[c_13025,c_204]) ).
tcf(c_13047,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = iPr_def_17 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_13032,c_7529]) ).
tcf(c_13049,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_13032,c_7716]) ).
tcf(c_13122,plain,
! [X0: $i] :
( iPr_def_10
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_193,c_13047]) ).
tcf(c_13136,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X1) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_13122,c_13049]) ).
tcf(c_13200,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X1)) = iPr_def_17 )
| ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_13136,c_210]) ).
tcf(c_13422,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( g(f(X0)) != X0 )
| ( sK0(X0) != X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_13200,c_208,c_13019,c_13200]) ).
tcf(c_13423,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( sK0(X0) != X0 )
| ( g(f(X0)) != X0 ) ),
inference(renaming,[status(thm)],[c_13422]) ).
tcf(c_13430,plain,
! [X0: $i,X1: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X1) = X1 )
| ( sK0(X0) = iPr_def_16 )
| ( f(sK0(X1)) = iPr_def_17 )
| ( g(f(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13423,c_13136]) ).
tcf(c_13453,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = iPr_def_17 )
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_13430]) ).
tcf(c_13454,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( f(sK0(X0)) = iPr_def_17 ) ),
inference(ground_joinability,[status(thm)],[c_13453,c_7528]) ).
tcf(c_13482,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = X0 )
| ( sK0(X0) = g(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_13454,c_13032]) ).
tcf(c_13488,plain,
! [X0: $i] :
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( sK0(X0) = iPr_def_16 )
| ( sK0(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_13482,c_7528]) ).
tcf(c_13564,plain,
( ( sK0(iPr_def_16) = iPr_def_16 )
| ( iPr_def_16 != iPr_def_16 ) ),
inference(equality_factoring,[status(thm)],[c_13488]) ).
tcf(c_13566,plain,
sK0(iPr_def_16) = iPr_def_16,
inference(equality_resolution_simp,[status(thm)],[c_13564]) ).
tcf(c_13572,plain,
( ~ iPr_def_15
| ( sK0(iPr_def_16) != iPr_def_16 )
| ( g(f(iPr_def_16)) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_13566,c_210]) ).
tcf(c_13575,plain,
( ~ iPr_def_15
| ( g(f(iPr_def_16)) != iPr_def_16 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13572,c_13566]) ).
tcf(c_13576,plain,
~ iPr_def_15,
inference(ground_joinability,[status(thm)],[c_13575,c_190,c_7528]) ).
tcf(c_13577,plain,
iPr_def_14,
inference(backward_subsumption_resolution,[status(thm)],[c_208,c_13576]) ).
tcf(c_13578,plain,
iPr_def_13,
inference(backward_subsumption_resolution,[status(thm)],[c_205,c_13576]) ).
tcf(c_13579,plain,
! [X0: $i] :
( ( sK1(X0) != X0 )
| ( f(g(sK1(X0))) != sK1(X0) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_209,c_13577]) ).
tcf(c_13582,plain,
! [X0: $i] :
( ( sK1(X0) = X0 )
| ( f(g(sK1(X0))) = sK1(X0) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_207,c_13578]) ).
tcf(c_13591,plain,
! [X0: $i] :
( ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_13582,c_7529]) ).
tcf(c_13592,plain,
! [X0: $i] :
( ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_13582,c_7716]) ).
tcf(c_13612,plain,
! [X0: $i] :
( iPr_def_10
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 ) ),
inference(superposition,[status(thm)],[c_193,c_13591]) ).
tcf(c_13645,plain,
! [X0: $i,X1: $i] :
( ( sK1(X1) = iPr_def_17 )
| ( sK1(X1) = X1 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_13612,c_13592]) ).
tcf(c_13669,plain,
! [X0: $i,X1: $i] :
( ( sK1(X1) = X1 )
| ( sK1(X0) = iPr_def_17 )
| ( g(sK1(X1)) = iPr_def_16 )
| ( sK1(X0) != X0 )
| ( f(g(X0)) != X0 ) ),
inference(superposition,[status(thm)],[c_13645,c_13579]) ).
tcf(c_13730,plain,
! [X0: $i,X1: $i] :
( ( sK1(X1) = X1 )
| ( sK1(X0) = iPr_def_17 )
| ( g(sK1(X1)) = iPr_def_16 )
| ( f(g(X0)) != X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13669,c_13645]) ).
tcf(c_13745,plain,
! [X0: $i] :
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 )
| ( f(iPr_def_16) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_7528,c_13730]) ).
tcf(c_13746,plain,
! [X0: $i] :
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( g(sK1(X0)) = iPr_def_16 ) ),
inference(ground_joinability,[status(thm)],[c_13745,c_190]) ).
tcf(c_13775,plain,
! [X0: $i] :
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK1(X0) = X0 )
| ( sK1(X0) = f(iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_13746,c_13582]) ).
tcf(c_13778,plain,
! [X0: $i] :
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( sK1(X0) = iPr_def_17 )
| ( sK1(X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_13775,c_190]) ).
tcf(c_13837,plain,
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( iPr_def_17 != iPr_def_17 ) ),
inference(equality_factoring,[status(thm)],[c_13778]) ).
tcf(c_13839,plain,
sK1(iPr_def_17) = iPr_def_17,
inference(equality_resolution_simp,[status(thm)],[c_13837]) ).
tcf(c_13841,plain,
( ( sK1(iPr_def_17) != iPr_def_17 )
| ( f(g(iPr_def_17)) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_13839,c_13579]) ).
tcf(c_13843,plain,
f(g(iPr_def_17)) != iPr_def_17,
inference(forward_subsumption_resolution,[status(thm)],[c_13841,c_13839]) ).
tcf(c_13844,plain,
$false,
inference(ground_joinability,[status(thm)],[c_13843,c_190,c_7528]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN551+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 01:45:05 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 3.17/1.73 % SZS status Started for theBenchmark.p
% 3.17/1.73 % SZS status Theorem for theBenchmark.p
% 3.17/1.73
% 3.17/1.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.17/1.73
% 3.17/1.73 % ------ iProver source info
% 3.17/1.73
% 3.17/1.73 % git: date: 2026-07-19 20:42:38 +0200
% 3.17/1.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.17/1.73 % git: non_committed_changes: false
% 3.17/1.73
% 3.17/1.73 % ------ Parsing...
% 3.17/1.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.17/1.73
% 3.17/1.73 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.17/1.73
% 3.17/1.73 % ------ Preprocessing... gs_s sp: 10 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.17/1.73
% 3.17/1.73 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 3.17/1.73 % ------ Proving...
% 3.17/1.73 % ------ Problem Properties
% 3.17/1.73
% 3.17/1.73 %
% 3.17/1.73 % clauses 18
% 3.17/1.73 % conjectures 14
% 3.17/1.73 % EPR 6
% 3.17/1.73 % Horn 8
% 3.17/1.73 % unary 4
% 3.17/1.73 % binary 6
% 3.17/1.73 % lits 40
% 3.17/1.73 % lits eq 24
% 3.17/1.73 % fd_pure 0
% 3.17/1.73 % fd_pseudo 0
% 3.17/1.73 % fd_cond 4
% 3.17/1.73 % fd_pseudo_cond 0
% 3.17/1.73 % AC symbols 0
% 3.17/1.73
% 3.17/1.73 % ------ Schedule dynamic 5 is on
% 3.17/1.73
% 3.17/1.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.17/1.73
% 3.17/1.73
% 3.17/1.73 % ------
% 3.17/1.73 % Current options:
% 3.17/1.73 % ------
% 3.17/1.73
% 3.17/1.73
% 3.17/1.73 %
% 3.17/1.73
% 3.17/1.73 % ------ Proving...
% 3.17/1.73 %
% 3.17/1.73
% 3.17/1.73 % SZS status Theorem for theBenchmark.p
% 3.17/1.73
% 3.17/1.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.17/1.74
% 3.17/1.74
%------------------------------------------------------------------------------