%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n010.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:57 PM UTC 2026
% Result : Theorem 2.96s 1.27s
% Output : CNFRefutation 2.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 5
% Syntax : Number of formulae : 218 ( 31 unt; 4 def)
% Number of atoms : 1010 ( 432 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 550 ( 215 ~; 302 |; 23 &)
% ( 3 <=>; 6 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 80 ( 0 sgn 64 !; 16 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ? [X0] :
( ! [X1] :
( X1 = f(g(X1))
=> X1 = X0 )
& X0 = f(g(X0)) )
<=> ? [X0] :
( ! [X1] :
( X1 = g(f(X1))
=> X1 = X0 )
& X0 = g(f(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_cute_thing) ).
fof(f2,negated_conjecture,
~ ( ? [X0] :
( ! [X1] :
( X1 = f(g(X1))
=> X1 = X0 )
& X0 = f(g(X0)) )
<=> ? [X0] :
( ! [X1] :
( X1 = g(f(X1))
=> X1 = X0 )
& X0 = g(f(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ( ? [X0] :
( ! [X1] :
( X1 = f(g(X1))
=> X1 = X0 )
& X0 = f(g(X0)) )
<=> ? [X2] :
( ! [X3] :
( g(f(X3)) = X3
=> X2 = X3 )
& g(f(X2)) = X2 ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
( ? [X0] :
( ! [X1] :
( f(g(X1)) != X1
| X1 = X0 )
& X0 = f(g(X0)) )
<~> ? [X2] :
( ! [X3] :
( g(f(X3)) != X3
| X2 = X3 )
& g(f(X2)) = X2 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ? [X0] :
( ! [X1] :
( f(g(X1)) != X1
| X1 = X0 )
& X0 = f(g(X0)) )
| ? [X2] :
( ! [X3] :
( g(f(X3)) != X3
| X2 = X3 )
& g(f(X2)) = X2 ) )
& ( ! [X0] :
( ? [X1] :
( f(g(X1)) = X1
& X0 != X1 )
| f(g(X0)) != X0 )
| ! [X2] :
( ? [X3] :
( g(f(X3)) = X3
& X2 != X3 )
| g(f(X2)) != X2 ) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f6,plain,
( ( ? [X6] :
( ! [X7] :
( f(g(X7)) != X7
| X6 = X7 )
& f(g(X6)) = X6 )
| ? [X4] :
( ! [X5] :
( g(f(X5)) != X5
| X4 = X5 )
& g(f(X4)) = X4 ) )
& ( ! [X2] :
( ? [X3] :
( f(g(X3)) = X3
& X2 != X3 )
| f(g(X2)) != X2 )
| ! [X0] :
( ? [X1] :
( g(f(X1)) = X1
& X0 != X1 )
| g(f(X0)) != X0 ) ) ),
inference(rectify,[],[f5]) ).
fof(f7,plain,
( ( ( ! [X7] :
( f(g(X7)) != X7
| sK3 = X7 )
& sK3 = f(g(sK3)) )
| ( ! [X5] :
( g(f(X5)) != X5
| sK2 = X5 )
& sK2 = g(f(sK2)) ) )
& ( ! [X2] :
( ( sK1(X2) = f(g(sK1(X2)))
& sK1(X2) != X2 )
| f(g(X2)) != X2 )
| ! [X0] :
( ( sK0(X0) = g(f(sK0(X0)))
& sK0(X0) != X0 )
| g(f(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,
! [X5] :
( sK3 = f(g(sK3))
| g(f(X5)) != X5
| sK2 = X5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f10,plain,
! [X7] :
( f(g(X7)) != X7
| sK3 = X7
| sK2 = g(f(sK2)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f11,plain,
( sK3 = f(g(sK3))
| sK2 = g(f(sK2)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f12,plain,
! [X2,X0] :
( sK1(X2) = f(g(sK1(X2)))
| f(g(X2)) != X2
| sK0(X0) = g(f(sK0(X0)))
| g(f(X0)) != X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f13,plain,
! [X2,X0] :
( sK1(X2) != X2
| f(g(X2)) != X2
| sK0(X0) = g(f(sK0(X0)))
| g(f(X0)) != X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f14,plain,
! [X2,X0] :
( sK1(X2) = f(g(sK1(X2)))
| f(g(X2)) != X2
| sK0(X0) != X0
| g(f(X0)) != X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f15,plain,
! [X2,X0] :
( sK1(X2) != X2
| f(g(X2)) != X2
| sK0(X0) != X0
| g(f(X0)) != X0 ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i] :
( ( sK1(X0) != X0 )
| ( sK0(X1) != X1 )
| ( g(f(X1)) != X1 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_50,negated_conjecture,
! [X0: $i,X1: $i] :
( ( f(g(sK1(X0))) = sK1(X0) )
| ( sK0(X1) != X1 )
| ( g(f(X1)) != X1 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_51,negated_conjecture,
! [X0: $i,X1: $i] :
( ( g(f(sK0(X1))) = sK0(X1) )
| ( sK1(X0) != X0 )
| ( g(f(X1)) != X1 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_52,negated_conjecture,
! [X0: $i,X1: $i] :
( ( g(f(sK0(X1))) = sK0(X1) )
| ( f(g(sK1(X0))) = sK1(X0) )
| ( g(f(X1)) != X1 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_53,negated_conjecture,
( ( g(f(sK2)) = sK2 )
| ( f(g(sK3)) = sK3 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_54,negated_conjecture,
! [X0: $i] :
( ( X0 = sK3 )
| ( g(f(sK2)) = sK2 )
| ( f(g(X0)) != X0 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_55,negated_conjecture,
! [X0: $i] :
( ( X0 = sK2 )
| ( f(g(sK3)) = sK3 )
| ( g(f(X0)) != X0 ) ),
inference(cnf_transformation,[],[f9]) ).
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
| ( g(f(sK0(X0))) = sK0(X0) )
| ( g(f(X0)) != 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) )
| ( f(g(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(X0)) != 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
| ( g(f(X0)) != X0 )
| ( sK0(X0) != 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] :
( ( g(f(sK0(X0))) = sK0(X0) )
| ~ iPr_def_12
| ( g(f(X0)) != X0 ) ),
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_206,negated_conjecture,
! [X0: $i] :
( ( f(g(sK1(X0))) = sK1(X0) )
| ~ iPr_def_13
| ( f(g(X0)) != X0 ) ),
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(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_184]) ).
tcf(c_210,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ( sK0(X0) != X0 )
| ( g(f(X0)) != 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_434,plain,
( ~ iPr_def_14
| ( sK1(sK3) != sK3 )
| ( f(iPr_def_16) != sK3 ) ),
inference(superposition,[status(thm)],[c_189,c_209]) ).
tcf(c_435,plain,
( ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 )
| ( f(iPr_def_19) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_192,c_209]) ).
tcf(c_436,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 )
| ( f(iPr_def_16) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_354,c_209]) ).
tcf(c_440,plain,
( ~ iPr_def_14
| ( sK3 != iPr_def_17 )
| ( sK1(sK3) != sK3 ) ),
inference(light_normalisation,[status(thm)],[c_434,c_190]) ).
tcf(c_444,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 ) ),
inference(ground_joinability,[status(thm)],[c_436,c_190]) ).
tcf(c_454,plain,
( ~ iPr_def_15
| ( sK0(sK2) != sK2 )
| ( g(iPr_def_18) != sK2 ) ),
inference(superposition,[status(thm)],[c_191,c_210]) ).
tcf(c_455,plain,
( ~ iPr_def_15
| ( sK0(iPr_def_16) != iPr_def_16 )
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_210]) ).
tcf(c_459,plain,
( ~ iPr_def_15
| ( sK2 != iPr_def_19 )
| ( sK0(sK2) != sK2 ) ),
inference(light_normalisation,[status(thm)],[c_454,c_192]) ).
tcf(c_469,plain,
( ( g(f(sK0(sK2))) = sK0(sK2) )
| ~ iPr_def_12
| ( g(iPr_def_18) != sK2 ) ),
inference(superposition,[status(thm)],[c_191,c_204]) ).
tcf(c_470,plain,
( ( g(f(sK0(iPr_def_16))) = sK0(iPr_def_16) )
| ~ iPr_def_12
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_190,c_204]) ).
tcf(c_474,plain,
( ( g(f(sK0(sK2))) = sK0(sK2) )
| ~ iPr_def_12
| ( sK2 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_469,c_192]) ).
tcf(c_484,plain,
( ( f(g(sK1(sK3))) = sK1(sK3) )
| ~ iPr_def_13
| ( f(iPr_def_16) != sK3 ) ),
inference(superposition,[status(thm)],[c_189,c_206]) ).
tcf(c_485,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_13
| ( f(iPr_def_19) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_192,c_206]) ).
tcf(c_486,plain,
( ( sK2 = iPr_def_19 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_13
| ( f(iPr_def_16) != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_354,c_206]) ).
tcf(c_490,plain,
( ( f(g(sK1(sK3))) = sK1(sK3) )
| ~ iPr_def_13
| ( sK3 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_484,c_190]) ).
tcf(c_494,plain,
( ( sK2 = iPr_def_19 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_13 ),
inference(ground_joinability,[status(thm)],[c_486,c_190]) ).
tcf(c_580,plain,
( iPr_def_12
| ( sK2 = iPr_def_19 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_199,c_494]) ).
tcf(c_598,plain,
( ( sK2 = iPr_def_19 )
| ( g(f(sK0(iPr_def_16))) = sK0(iPr_def_16) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_354,c_470]) ).
tcf(c_614,plain,
( ( sK2 = iPr_def_19 )
| ( g(f(sK0(iPr_def_16))) = sK0(iPr_def_16) )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_580,c_598]) ).
tcf(c_649,plain,
( ( sK2 = iPr_def_19 )
| ( f(sK0(iPr_def_16)) = sK3 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_614,c_197]) ).
tcf(c_694,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = sK3 )
| ( f(sK0(iPr_def_16)) = sK3 ) ),
inference(superposition,[status(thm)],[c_649,c_197]) ).
tcf(c_744,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = sK3 )
| ( g(sK3) = sK0(iPr_def_16) )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_694,c_614]) ).
tcf(c_745,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = sK3 )
| ( sK0(iPr_def_16) = iPr_def_16 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(light_normalisation,[status(thm)],[c_744,c_189]) ).
tcf(c_993,plain,
( ( sK2 = iPr_def_19 )
| ( g(iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_198,c_189]) ).
tcf(c_997,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_1097,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = sK3 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(global_subsumption_just,[status(thm)],[c_745,c_205,c_354,c_455,c_494,c_745]) ).
tcf(c_1111,plain,
( ( sK2 = iPr_def_19 )
| ( sK1(iPr_def_17) = sK3 ) ),
inference(superposition,[status(thm)],[c_1097,c_197]) ).
tcf(c_1124,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14
| ( sK3 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1111,c_444]) ).
tcf(c_1133,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_1137,plain,
( ( sK2 = iPr_def_19 )
| ~ iPr_def_14 ),
inference(global_subsumption_just,[status(thm)],[c_1124,c_422,c_1124]) ).
tcf(c_1143,plain,
( iPr_def_12
| ( sK2 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_202,c_1137]) ).
tcf(c_1150,plain,
( ( sK2 = iPr_def_19 )
| ( g(f(sK0(iPr_def_16))) = sK0(iPr_def_16) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_598,c_1143]) ).
tcf(c_1164,plain,
( ( sK2 = iPr_def_19 )
| ( f(sK0(iPr_def_16)) = sK3 ) ),
inference(superposition,[status(thm)],[c_1150,c_197]) ).
tcf(c_1203,plain,
( ( sK2 = iPr_def_19 )
| ( g(sK3) = sK0(iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_1164,c_1150]) ).
tcf(c_1204,plain,
( ( sK2 = iPr_def_19 )
| ( sK0(iPr_def_16) = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_1203,c_189]) ).
tcf(c_1208,plain,
sK2 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_1204,c_208,c_354,c_422,c_455,c_1124,c_1204]) ).
tcf(c_1218,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ~ iPr_def_12
| ( iPr_def_19 != iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_474,c_1208]) ).
tcf(c_1222,plain,
( ~ iPr_def_15
| ( iPr_def_19 != iPr_def_19 )
| ( sK0(iPr_def_19) != iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_459,c_1208]) ).
tcf(c_1226,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_358,c_1208]) ).
tcf(c_1228,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( X0 = iPr_def_19 )
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_196,c_1208]) ).
tcf(c_1229,plain,
f(iPr_def_19) = iPr_def_18,
inference(demodulation,[status(thm)],[c_191,c_1208]) ).
tcf(c_1230,plain,
! [X0: $i] :
( ( X0 = iPr_def_19 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_195,c_1208]) ).
tcf(c_1238,plain,
( ~ iPr_def_15
| ( sK0(iPr_def_19) != iPr_def_19 ) ),
inference(equality_resolution_simp,[status(thm)],[c_1222]) ).
tcf(c_1247,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ~ iPr_def_12 ),
inference(equality_resolution_simp,[status(thm)],[c_1218]) ).
tcf(c_1250,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_13 ),
inference(backward_subsumption_resolution,[status(thm)],[c_485,c_1229]) ).
tcf(c_1251,plain,
( ~ iPr_def_14
| ( sK1(iPr_def_18) != iPr_def_18 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_435,c_1229]) ).
tcf(c_1252,plain,
( ( sK3 = iPr_def_18 )
| ~ iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_363,c_1229]) ).
tcf(c_1265,plain,
( iPr_def_10
| ( sK3 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_193,c_1252]) ).
tcf(c_1308,plain,
( iPr_def_12
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_199,c_1250]) ).
tcf(c_1329,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_1308,c_1247]) ).
tcf(c_1370,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_1329,c_1228]) ).
tcf(c_1371,plain,
( ( sK0(iPr_def_19) = iPr_def_19 )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_1329,c_1230]) ).
tcf(c_1372,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(iPr_def_19)))) = sK0(sK0(iPr_def_19)) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_1329,c_204]) ).
tcf(c_1398,plain,
( ~ iPr_def_10
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(global_subsumption_just,[status(thm)],[c_1371,c_205,c_1238,c_1250,c_1371]) ).
tcf(c_1399,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_10 ),
inference(renaming,[status(thm)],[c_1398]) ).
tcf(c_1502,plain,
sK2 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_993,c_208,c_354,c_422,c_455,c_1124,c_1204]) ).
tcf(c_1504,plain,
! [X0: $i] :
( ( sK3 = iPr_def_17 )
| ( X0 = iPr_def_19 )
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_196,c_1502]) ).
tcf(c_1505,plain,
f(iPr_def_19) = iPr_def_18,
inference(demodulation,[status(thm)],[c_191,c_1502]) ).
tcf(c_1527,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10
| ( g(iPr_def_17) != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_997,c_1502]) ).
tcf(c_1547,plain,
( ( sK3 = iPr_def_18 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_1133,c_363,c_1229]) ).
tcf(c_1553,plain,
( iPr_def_10
| ( sK3 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_193,c_1547]) ).
tcf(c_1711,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(iPr_def_19)))) = sK0(sK0(iPr_def_19)) ) ),
inference(global_subsumption_just,[status(thm)],[c_1372,c_1308,c_1372]) ).
tcf(c_1719,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(iPr_def_19))))) = sK0(sK0(sK0(iPr_def_19))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_1711,c_204]) ).
tcf(c_1800,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ~ iPr_def_12
| ( g(iPr_def_18) != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1505,c_204]) ).
tcf(c_1801,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ~ iPr_def_12 ),
inference(ground_joinability,[status(thm)],[c_1800,c_192]) ).
tcf(c_1838,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(iPr_def_19))))) = sK0(sK0(sK0(iPr_def_19))) ) ),
inference(global_subsumption_just,[status(thm)],[c_1719,c_1308,c_1719]) ).
tcf(c_1846,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(iPr_def_19)))))) = sK0(sK0(sK0(sK0(iPr_def_19)))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_1838,c_204]) ).
tcf(c_1850,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( f(sK0(sK0(sK0(iPr_def_19)))) = sK3 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_1838,c_194]) ).
tcf(c_1887,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_13
| ( f(iPr_def_19) != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_192,c_206]) ).
tcf(c_1888,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ~ iPr_def_13 ),
inference(ground_joinability,[status(thm)],[c_1887,c_1505]) ).
tcf(c_1904,plain,
( ( sK3 = iPr_def_17 )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(global_subsumption_just,[status(thm)],[c_1370,c_205,c_1238,c_1250,c_1370]) ).
tcf(c_1912,plain,
( ( sK3 = iPr_def_17 )
| ( g(sK1(iPr_def_18)) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1904,c_1228]) ).
tcf(c_1914,plain,
( ( sK3 = iPr_def_17 )
| ( g(f(sK0(g(sK1(iPr_def_18))))) = sK0(g(sK1(iPr_def_18))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_1904,c_204]) ).
tcf(c_1915,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_15
| ( sK0(g(sK1(iPr_def_18))) != g(sK1(iPr_def_18)) ) ),
inference(superposition,[status(thm)],[c_1904,c_210]) ).
tcf(c_1996,plain,
( iPr_def_12
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_199,c_1888]) ).
tcf(c_2091,plain,
( ( g(f(sK0(iPr_def_19))) = sK0(iPr_def_19) )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_1996,c_1801]) ).
tcf(c_2118,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_2091,c_1504]) ).
tcf(c_2120,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(iPr_def_19)))) = sK0(sK0(iPr_def_19)) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_2091,c_204]) ).
tcf(c_2155,plain,
( ( sK3 = iPr_def_17 )
| ( f(iPr_def_19) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_1912,c_1904]) ).
tcf(c_2160,plain,
( ( sK3 = iPr_def_17 )
| ( sK1(iPr_def_18) = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2155,c_1229]) ).
tcf(c_2185,plain,
( ( sK3 = iPr_def_17 )
| ~ iPr_def_14 ),
inference(superposition,[status(thm)],[c_2160,c_1251]) ).
tcf(c_2202,plain,
( ~ iPr_def_14
| ( sK1(sK3) != sK3 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_440,c_2185]) ).
tcf(c_2205,plain,
( iPr_def_12
| ( sK3 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_202,c_2185]) ).
tcf(c_2221,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(g(sK1(iPr_def_18))) != g(sK1(iPr_def_18)) ) ),
inference(global_subsumption_just,[status(thm)],[c_1915,c_208,c_1915,c_2185]) ).
tcf(c_2227,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1912,c_2221]) ).
tcf(c_2256,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( f(sK0(sK0(sK0(iPr_def_19)))) = sK3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1850,c_193,c_1399,c_1850]) ).
tcf(c_2266,plain,
( ( sK0(sK0(sK0(iPr_def_19))) = g(sK3) )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(superposition,[status(thm)],[c_2256,c_1838]) ).
tcf(c_2267,plain,
( ( sK0(sK0(sK0(iPr_def_19))) = iPr_def_16 )
| ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) ) ),
inference(light_normalisation,[status(thm)],[c_2266,c_189]) ).
tcf(c_2275,plain,
( ( sK3 = iPr_def_17 )
| ( g(f(sK0(g(sK1(iPr_def_18))))) = sK0(g(sK1(iPr_def_18))) ) ),
inference(global_subsumption_just,[status(thm)],[c_1914,c_1914,c_2205]) ).
tcf(c_2285,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(g(sK1(iPr_def_18))) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2275,c_1228]) ).
tcf(c_2756,plain,
( ( sK3 = iPr_def_17 )
| ( sK0(iPr_def_19) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1912,c_2285]) ).
tcf(c_2809,plain,
sK3 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_2756,c_2227,c_2756]) ).
tcf(c_2822,plain,
( ~ iPr_def_14
| ( sK1(iPr_def_17) != iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_2202,c_2809]) ).
tcf(c_2857,plain,
( iPr_def_10
| ( iPr_def_17 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1265,c_2809]) ).
tcf(c_2859,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_13
| ( iPr_def_17 != iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_490,c_2809]) ).
tcf(c_2860,plain,
g(iPr_def_17) = iPr_def_16,
inference(demodulation,[status(thm)],[c_189,c_2809]) ).
tcf(c_2861,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ~ iPr_def_11
| ( f(g(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_194,c_2809]) ).
tcf(c_2889,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_13 ),
inference(equality_resolution_simp,[status(thm)],[c_2859]) ).
tcf(c_2930,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1226,c_2860]) ).
tcf(c_2931,plain,
( ( g(f(sK0(iPr_def_16))) = sK0(iPr_def_16) )
| ~ iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_470,c_2860]) ).
tcf(c_2932,plain,
( ~ iPr_def_15
| ( sK0(iPr_def_16) != iPr_def_16 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_455,c_2860]) ).
tcf(c_2977,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(iPr_def_19)))))) = sK0(sK0(sK0(sK0(iPr_def_19)))) ) ),
inference(global_subsumption_just,[status(thm)],[c_1846,c_1308,c_1846]) ).
tcf(c_2984,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(iPr_def_19))))))) = sK0(sK0(sK0(sK0(sK0(iPr_def_19))))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_2977,c_204]) ).
tcf(c_3083,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2857,c_2930]) ).
tcf(c_3111,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(iPr_def_19))))))) = sK0(sK0(sK0(sK0(sK0(iPr_def_19))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_2984,c_1308,c_2984]) ).
tcf(c_3118,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_19)))))))) = sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_19)))))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_3111,c_204]) ).
tcf(c_3239,plain,
sK3 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_2118,c_2227,c_2756]) ).
tcf(c_3250,plain,
( iPr_def_10
| ( iPr_def_17 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1553,c_3239]) ).
tcf(c_3252,plain,
g(iPr_def_17) = iPr_def_16,
inference(demodulation,[status(thm)],[c_189,c_3239]) ).
tcf(c_3253,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ~ iPr_def_11
| ( f(g(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_194,c_3239]) ).
tcf(c_3281,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1527,c_3252]) ).
tcf(c_3309,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_3250,c_3281]) ).
tcf(c_3327,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( f(iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_3309,c_1505]) ).
tcf(c_3328,plain,
iPr_def_17 = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_3327,c_190]) ).
tcf(c_3331,plain,
( iPr_def_12
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(demodulation,[status(thm)],[c_1996,c_3328]) ).
tcf(c_3335,plain,
g(iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_192,c_3328]) ).
tcf(c_3336,plain,
iPr_def_16 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_3335,c_3252]) ).
tcf(c_3373,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(iPr_def_19)))) = sK0(sK0(iPr_def_19)) ) ),
inference(global_subsumption_just,[status(thm)],[c_2120,c_1308,c_1372]) ).
tcf(c_3375,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(iPr_def_16)))) = sK0(sK0(iPr_def_16)) ) ),
inference(light_normalisation,[status(thm)],[c_3373,c_3328,c_3336]) ).
tcf(c_3384,plain,
( ( f(sK0(sK0(iPr_def_16))) = iPr_def_17 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_3375,c_3253]) ).
tcf(c_3430,plain,
iPr_def_17 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_3083,c_3328]) ).
tcf(c_3453,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_10 ),
inference(demodulation,[status(thm)],[c_1399,c_3430]) ).
tcf(c_3459,plain,
g(iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_192,c_3430]) ).
tcf(c_3460,plain,
iPr_def_16 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_3459,c_2860]) ).
tcf(c_3499,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ~ iPr_def_10
| ( g(f(X0)) != X0 ) ),
inference(demodulation,[status(thm)],[c_1230,c_3460]) ).
tcf(c_3510,plain,
( ( f(g(sK1(iPr_def_18))) = sK1(iPr_def_18) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_19)))))))) = sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_19)))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_3118,c_1308,c_3118]) ).
tcf(c_3512,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))) = sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))) ) ),
inference(light_normalisation,[status(thm)],[c_3510,c_3430,c_3460]) ).
tcf(c_3519,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))))) = sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_3512,c_204]) ).
tcf(c_3520,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_15
| ( sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))) != sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))) ) ),
inference(superposition,[status(thm)],[c_3512,c_210]) ).
tcf(c_3551,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))) != sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_3520,c_205,c_2889,c_3520]) ).
tcf(c_3577,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))))) = sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_3519,c_3331,c_3519]) ).
tcf(c_3583,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))))) = sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))) )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_3577,c_204]) ).
tcf(c_3617,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( g(f(sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))))) = sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_3583,c_3331,c_3583]) ).
tcf(c_3624,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ~ iPr_def_15
| ( sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))))) != sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))) ) ),
inference(superposition,[status(thm)],[c_3617,c_210]) ).
tcf(c_3671,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16))))))))) != sK0(sK0(sK0(sK0(sK0(sK0(sK0(sK0(iPr_def_16)))))))) ) ),
inference(global_subsumption_just,[status(thm)],[c_3624,c_205,c_2889,c_3624]) ).
tcf(c_5821,plain,
( ( f(sK0(sK0(iPr_def_16))) = iPr_def_17 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(global_subsumption_just,[status(thm)],[c_3384,c_193,c_3384,c_3453]) ).
tcf(c_5831,plain,
( ( sK0(sK0(iPr_def_16)) = g(iPr_def_17) )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_5821,c_3375]) ).
tcf(c_5832,plain,
( ( sK0(sK0(iPr_def_16)) = iPr_def_16 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(light_normalisation,[status(thm)],[c_5831,c_3252]) ).
tcf(c_6040,plain,
( ( sK0(sK0(sK0(iPr_def_16))) = iPr_def_16 )
| ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) ) ),
inference(light_normalisation,[status(thm)],[c_2267,c_3430,c_3460]) ).
tcf(c_6059,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( sK0(sK0(iPr_def_16)) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6040,c_3671]) ).
tcf(c_6065,plain,
( ( f(g(sK1(iPr_def_17))) = sK1(iPr_def_17) )
| ( sK0(iPr_def_16) != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6040,c_3551]) ).
tcf(c_6084,plain,
f(g(sK1(iPr_def_17))) = sK1(iPr_def_17),
inference(global_subsumption_just,[status(thm)],[c_6065,c_5832,c_6059]) ).
tcf(c_6109,plain,
( ( g(sK1(iPr_def_17)) = iPr_def_16 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_6084,c_3499]) ).
tcf(c_6112,plain,
( ( sK1(iPr_def_17) = iPr_def_17 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_6084,c_2861]) ).
tcf(c_6176,plain,
( iPr_def_10
| ( sK1(iPr_def_17) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_193,c_6112]) ).
tcf(c_6188,plain,
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( g(sK1(iPr_def_17)) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_6176,c_6109]) ).
tcf(c_6199,plain,
( ( sK1(iPr_def_17) = iPr_def_17 )
| ( f(iPr_def_16) = sK1(iPr_def_17) ) ),
inference(superposition,[status(thm)],[c_6188,c_6084]) ).
tcf(c_6216,plain,
sK1(iPr_def_17) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_6199,c_190]) ).
tcf(c_6217,plain,
~ iPr_def_14,
inference(backward_subsumption_resolution,[status(thm)],[c_2822,c_6216]) ).
tcf(c_6274,plain,
iPr_def_15,
inference(backward_subsumption_resolution,[status(thm)],[c_208,c_6217]) ).
tcf(c_6275,plain,
iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_202,c_6217]) ).
tcf(c_6276,plain,
sK0(iPr_def_16) != iPr_def_16,
inference(backward_subsumption_resolution,[status(thm)],[c_2932,c_6274]) ).
tcf(c_6280,plain,
g(f(sK0(iPr_def_16))) = sK0(iPr_def_16),
inference(backward_subsumption_resolution,[status(thm)],[c_2931,c_6275]) ).
tcf(c_6366,plain,
( ( sK0(iPr_def_16) = iPr_def_16 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_6280,c_3499]) ).
tcf(c_6367,plain,
( ( f(sK0(iPr_def_16)) = iPr_def_17 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_6280,c_2861]) ).
tcf(c_6369,plain,
~ iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_6366,c_6276]) ).
tcf(c_6374,plain,
iPr_def_11,
inference(backward_subsumption_resolution,[status(thm)],[c_193,c_6369]) ).
tcf(c_6375,plain,
f(sK0(iPr_def_16)) = iPr_def_17,
inference(backward_subsumption_resolution,[status(thm)],[c_6367,c_6374]) ).
tcf(c_6376,plain,
g(iPr_def_17) = sK0(iPr_def_16),
inference(demodulation,[status(thm)],[c_6280,c_6375]) ).
tcf(c_6377,plain,
sK0(iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_6376,c_2860]) ).
tcf(c_6378,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6377,c_6276]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Fri Sep 25 01:44:13 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.02/0.40 Running first-order theorem proving
% 0.02/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.41
% 0.02/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.02/0.41
% 0.02/0.41 % Detected problem language: tptp
% 0.02/0.43 % Proving...
% 2.96/1.27 % SZS status Started for theBenchmark.p
% 2.96/1.27 % SZS status Theorem for theBenchmark.p
% 2.96/1.27
% 2.96/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.96/1.27
% 2.96/1.27 % ------ iProver source info
% 2.96/1.27
% 2.96/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 2.96/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.96/1.27 % git: non_committed_changes: false
% 2.96/1.27
% 2.96/1.27 % ------ Parsing...
% 2.96/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.96/1.27
% 2.96/1.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.96/1.27
% 2.96/1.27 % ------ Preprocessing... gs_s sp: 10 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.96/1.27
% 2.96/1.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 2.96/1.27 % ------ Proving...
% 2.96/1.27 % ------ Problem Properties
% 2.96/1.27
% 2.96/1.27 %
% 2.96/1.27 % clauses 18
% 2.96/1.27 % conjectures 14
% 2.96/1.27 % EPR 6
% 2.96/1.27 % Horn 10
% 2.96/1.27 % unary 4
% 2.96/1.27 % binary 6
% 2.96/1.27 % lits 40
% 2.96/1.27 % lits eq 24
% 2.96/1.27 % fd_pure 0
% 2.96/1.28 % fd_pseudo 0
% 2.96/1.28 % fd_cond 4
% 2.96/1.28 % fd_pseudo_cond 0
% 2.96/1.28 % AC symbols 0
% 2.96/1.28
% 2.96/1.28 % ------ Schedule dynamic 5 is on
% 2.96/1.28
% 2.96/1.28 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.96/1.28
% 2.96/1.28
% 2.96/1.28 % ------
% 2.96/1.28 % Current options:
% 2.96/1.28 % ------
% 2.96/1.28
% 2.96/1.28
% 2.96/1.28 %
% 2.96/1.28
% 2.96/1.28 % ------ Proving...
% 2.96/1.28 %
% 2.96/1.28
% 2.96/1.28 % SZS status Theorem for theBenchmark.p
% 2.96/1.28
% 2.96/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.96/1.28
% 2.96/1.28
%------------------------------------------------------------------------------