%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SET772+4 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/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:48:32 PM UTC 2026
% Result : Theorem 10.59s 2.27s
% Output : CNFRefutation 10.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 7
% Syntax : Number of formulae : 437 ( 31 unt; 1 def)
% Number of atoms : 2277 ( 254 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 1904 ( 738 ~;1002 |; 117 &)
% ( 9 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 552 ( 0 sgn 502 !; 50 ?; 337 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( member(X2,X0)
=> member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax',subset) ).
fof(f13,axiom,
! [X0,X1] :
( partition(X0,X1)
<=> ( ! [X2,X3] :
( ( member(X3,X0)
& member(X2,X0) )
=> ( ? [X4] :
( member(X4,X3)
& member(X4,X2) )
=> X2 = X3 ) )
& ! [X2] :
( member(X2,X1)
=> ? [X3] :
( member(X2,X3)
& member(X3,X0) ) )
& ! [X2] :
( member(X2,X0)
=> subset(X2,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET006+2.ax',partition) ).
fof(f14,axiom,
! [X0,X1] :
( equivalence(X1,X0)
<=> ( ! [X2,X3,X4] :
( ( member(X4,X0)
& member(X3,X0)
& member(X2,X0) )
=> ( ( apply(X1,X3,X4)
& apply(X1,X2,X3) )
=> apply(X1,X2,X4) ) )
& ! [X2,X3] :
( ( member(X3,X0)
& member(X2,X0) )
=> ( apply(X1,X2,X3)
=> apply(X1,X3,X2) ) )
& ! [X2] :
( member(X2,X0)
=> apply(X1,X2,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET006+2.ax',equivalence) ).
fof(f17,conjecture,
! [X0,X1,X2] :
( partition(X0,X1)
=> ( ! [X3,X4] :
( ( member(X4,X1)
& member(X3,X1) )
=> ( apply(X2,X3,X4)
<=> ? [X5] :
( member(X4,X5)
& member(X3,X5)
& member(X5,X0) ) ) )
=> equivalence(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thIII08) ).
fof(f18,negated_conjecture,
~ ! [X0,X1,X2] :
( partition(X0,X1)
=> ( ! [X3,X4] :
( ( member(X4,X1)
& member(X3,X1) )
=> ( apply(X2,X3,X4)
<=> ? [X5] :
( member(X4,X5)
& member(X3,X5)
& member(X5,X0) ) ) )
=> equivalence(X2,X1) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1] :
( partition(X0,X1)
<=> ( ! [X5,X6] :
( ( member(X6,X0)
& member(X5,X0) )
=> ( ? [X7] :
( member(X7,X6)
& member(X7,X5) )
=> X5 = X6 ) )
& ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X3,X4)
& member(X4,X0) ) )
& ! [X2] :
( member(X2,X0)
=> subset(X2,X1) ) ) ),
inference(rectify,[],[f13]) ).
fof(f20,plain,
! [X0,X1] :
( equivalence(X1,X0)
<=> ( ! [X5,X6,X7] :
( ( member(X7,X0)
& member(X6,X0)
& member(X5,X0) )
=> ( ( apply(X1,X6,X7)
& apply(X1,X5,X6) )
=> apply(X1,X5,X7) ) )
& ! [X3,X4] :
( ( member(X4,X0)
& member(X3,X0) )
=> ( apply(X1,X3,X4)
=> apply(X1,X4,X3) ) )
& ! [X2] :
( member(X2,X0)
=> apply(X1,X2,X2) ) ) ),
inference(rectify,[],[f14]) ).
fof(f21,plain,
! [X0,X1] :
( ( ! [X5,X6,X7] :
( ( member(X7,X0)
& member(X6,X0)
& member(X5,X0) )
=> ( ( apply(X1,X6,X7)
& apply(X1,X5,X6) )
=> apply(X1,X5,X7) ) )
& ! [X3,X4] :
( ( member(X4,X0)
& member(X3,X0) )
=> ( apply(X1,X3,X4)
=> apply(X1,X4,X3) ) )
& ! [X2] :
( member(X2,X0)
=> apply(X1,X2,X2) ) )
=> equivalence(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( partition(X0,X1)
=> ( ! [X5,X6] :
( ( member(X6,X0)
& member(X5,X0) )
=> ( ? [X7] :
( member(X7,X6)
& member(X7,X5) )
=> X5 = X6 ) )
& ! [X3] :
( member(X3,X1)
=> ? [X4] :
( member(X3,X4)
& member(X4,X0) ) )
& ! [X2] :
( member(X2,X0)
=> subset(X2,X1) ) ) ),
inference(unused_predicate_definition_removal,[],[f19]) ).
fof(f23,plain,
! [X0,X1] :
( subset(X0,X1)
=> ! [X2] :
( member(X2,X0)
=> member(X2,X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f24,plain,
? [X0,X1,X2] :
( partition(X0,X1)
& ! [X3,X4] :
( ~ member(X4,X1)
| ~ member(X3,X1)
| ( apply(X2,X3,X4)
<=> ? [X5] :
( member(X4,X5)
& member(X3,X5)
& member(X5,X0) ) ) )
& ~ equivalence(X2,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f25,plain,
? [X0,X1,X2] :
( partition(X0,X1)
& ! [X3,X4] :
( ~ member(X4,X1)
| ~ member(X3,X1)
| ( apply(X2,X3,X4)
<=> ? [X5] :
( member(X4,X5)
& member(X3,X5)
& member(X5,X0) ) ) )
& ~ equivalence(X2,X1) ),
inference(flattening,[],[f24]) ).
fof(f26,plain,
! [X0,X1] :
( ~ partition(X0,X1)
| ( ! [X5,X6] :
( ~ member(X6,X0)
| ~ member(X5,X0)
| ! [X7] :
( ~ member(X7,X6)
| ~ member(X7,X5) )
| X5 = X6 )
& ! [X3] :
( ~ member(X3,X1)
| ? [X4] :
( member(X3,X4)
& member(X4,X0) ) )
& ! [X2] :
( ~ member(X2,X0)
| subset(X2,X1) ) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f27,plain,
! [X0,X1] :
( ~ partition(X0,X1)
| ( ! [X5,X6] :
( ~ member(X6,X0)
| ~ member(X5,X0)
| ! [X7] :
( ~ member(X7,X6)
| ~ member(X7,X5) )
| X5 = X6 )
& ! [X3] :
( ~ member(X3,X1)
| ? [X4] :
( member(X3,X4)
& member(X4,X0) ) )
& ! [X2] :
( ~ member(X2,X0)
| subset(X2,X1) ) ) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( ? [X5,X6,X7] :
( member(X7,X0)
& member(X6,X0)
& member(X5,X0)
& apply(X1,X6,X7)
& apply(X1,X5,X6)
& ~ apply(X1,X5,X7) )
| ? [X3,X4] :
( member(X4,X0)
& member(X3,X0)
& apply(X1,X3,X4)
& ~ apply(X1,X4,X3) )
| ? [X2] :
( member(X2,X0)
& ~ apply(X1,X2,X2) )
| equivalence(X1,X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f29,plain,
! [X0,X1] :
( ? [X5,X6,X7] :
( member(X7,X0)
& member(X6,X0)
& member(X5,X0)
& apply(X1,X6,X7)
& apply(X1,X5,X6)
& ~ apply(X1,X5,X7) )
| ? [X3,X4] :
( member(X4,X0)
& member(X3,X0)
& apply(X1,X3,X4)
& ~ apply(X1,X4,X3) )
| ? [X2] :
( member(X2,X0)
& ~ apply(X1,X2,X2) )
| equivalence(X1,X0) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ! [X2] :
( ~ member(X2,X0)
| member(X2,X1) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f33,plain,
? [X0,X1,X2] :
( partition(X0,X1)
& ! [X3,X4] :
( ~ member(X4,X1)
| ~ member(X3,X1)
| ( ( ~ apply(X2,X3,X4)
| ? [X5] :
( member(X4,X5)
& member(X3,X5)
& member(X5,X0) ) )
& ( ! [X5] :
( ~ member(X4,X5)
| ~ member(X3,X5)
| ~ member(X5,X0) )
| apply(X2,X3,X4) ) ) )
& ~ equivalence(X2,X1) ),
inference(nnf_transformation,[],[f25]) ).
fof(f34,plain,
? [X0,X1,X2] :
( partition(X0,X1)
& ! [X3,X4] :
( ~ member(X4,X1)
| ~ member(X3,X1)
| ( ( ~ apply(X2,X3,X4)
| ? [X6] :
( member(X4,X6)
& member(X3,X6)
& member(X6,X0) ) )
& ( ! [X5] :
( ~ member(X4,X5)
| ~ member(X3,X5)
| ~ member(X5,X0) )
| apply(X2,X3,X4) ) ) )
& ~ equivalence(X2,X1) ),
inference(rectify,[],[f33]) ).
fof(f35,plain,
( partition(sK1,sK2)
& ! [X3,X4] :
( ~ member(X4,sK2)
| ~ member(X3,sK2)
| ( ( ~ apply(sK3,X3,X4)
| ( member(X4,sK4(X3,X4))
& member(X3,sK4(X3,X4))
& member(sK4(X3,X4),sK1) ) )
& ( ! [X5] :
( ~ member(X4,X5)
| ~ member(X3,X5)
| ~ member(X5,sK1) )
| apply(sK3,X3,X4) ) ) )
& ~ equivalence(sK3,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X6,sK4(X3,X4))],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ~ partition(X0,X1)
| ( ! [X5,X6] :
( ~ member(X6,X0)
| ~ member(X5,X0)
| ! [X7] :
( ~ member(X7,X6)
| ~ member(X7,X5) )
| X5 = X6 )
& ! [X3] :
( ~ member(X3,X1)
| ( member(X3,sK5(X0,X3))
& member(sK5(X0,X3),X0) ) )
& ! [X2] :
( ~ member(X2,X0)
| subset(X2,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X4,sK5(X0,X3))],[f27]) ).
fof(f40,plain,
! [X0,X1] :
( sP0(X1,X0)
| ( member(sK11(X0,X1),X0)
& member(sK10(X0,X1),X0)
& apply(X1,sK10(X0,X1),sK11(X0,X1))
& ~ apply(X1,sK11(X0,X1),sK10(X0,X1)) )
| ( member(sK9(X0,X1),X0)
& ~ apply(X1,sK9(X0,X1),sK9(X0,X1)) )
| equivalence(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X2,sK9(X0,X1)),skolemize(X3,sK10(X0,X1)),skolemize(X4,sK11(X0,X1))],[f32]) ).
fof(f41,plain,
partition(sK1,sK2),
inference(cnf_transformation,[],[f35]) ).
fof(f42,plain,
! [X3,X4] :
( ~ member(X4,sK2)
| ~ member(X3,sK2)
| ~ apply(sK3,X3,X4)
| member(X4,sK4(X3,X4)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f43,plain,
! [X3,X4] :
( ~ member(X4,sK2)
| ~ member(X3,sK2)
| ~ apply(sK3,X3,X4)
| member(X3,sK4(X3,X4)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f44,plain,
! [X3,X4] :
( ~ member(X4,sK2)
| ~ member(X3,sK2)
| ~ apply(sK3,X3,X4)
| member(sK4(X3,X4),sK1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f45,plain,
! [X3,X4,X5] :
( ~ member(X4,sK2)
| ~ member(X3,sK2)
| ~ member(X4,X5)
| ~ member(X3,X5)
| ~ member(X5,sK1)
| apply(sK3,X3,X4) ),
inference(cnf_transformation,[],[f35]) ).
fof(f46,plain,
~ equivalence(sK3,sK2),
inference(cnf_transformation,[],[f35]) ).
fof(f47,plain,
! [X0,X1,X6,X7,X5] :
( ~ partition(X0,X1)
| ~ member(X6,X0)
| ~ member(X5,X0)
| ~ member(X7,X6)
| ~ member(X7,X5)
| X5 = X6 ),
inference(cnf_transformation,[],[f36]) ).
fof(f48,plain,
! [X3,X0,X1] :
( ~ partition(X0,X1)
| ~ member(X3,X1)
| member(X3,sK5(X0,X3)) ),
inference(cnf_transformation,[],[f36]) ).
fof(f49,plain,
! [X3,X0,X1] :
( ~ partition(X0,X1)
| ~ member(X3,X1)
| member(sK5(X0,X3),X0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ partition(X0,X1)
| ~ member(X2,X0)
| subset(X2,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f57,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK11(X0,X1),X0)
| member(sK9(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f58,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK10(X0,X1),X0)
| member(sK9(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f59,plain,
! [X0,X1] :
( sP0(X1,X0)
| apply(X1,sK10(X0,X1),sK11(X0,X1))
| member(sK9(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f60,plain,
! [X0,X1] :
( sP0(X1,X0)
| ~ apply(X1,sK11(X0,X1),sK10(X0,X1))
| member(sK9(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f61,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK11(X0,X1),X0)
| ~ apply(X1,sK9(X0,X1),sK9(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f62,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK10(X0,X1),X0)
| ~ apply(X1,sK9(X0,X1),sK9(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f63,plain,
! [X0,X1] :
( sP0(X1,X0)
| apply(X1,sK10(X0,X1),sK11(X0,X1))
| ~ apply(X1,sK9(X0,X1),sK9(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f64,plain,
! [X0,X1] :
( sP0(X1,X0)
| ~ apply(X1,sK11(X0,X1),sK10(X0,X1))
| ~ apply(X1,sK9(X0,X1),sK9(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f65,plain,
! [X2,X0,X1] :
( ~ subset(X0,X1)
| ~ member(X2,X0)
| member(X2,X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_49,negated_conjecture,
~ equivalence(sK3,sK2),
inference(cnf_transformation,[],[f46]) ).
tcf(c_50,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X2,sK2)
| ~ member(X1,sK1)
| ~ member(X0,sK2)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_51,negated_conjecture,
! [X0: $i,X1: $i] :
( member(sK4(X0,X1),sK1)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_52,negated_conjecture,
! [X0: $i,X1: $i] :
( member(X0,sK4(X0,X1))
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_53,negated_conjecture,
! [X0: $i,X1: $i] :
( member(X1,sK4(X0,X1))
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_54,negated_conjecture,
partition(sK1,sK2),
inference(cnf_transformation,[],[f41]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ~ partition(X1,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(sK5(X2,X0),X2)
| ~ partition(X2,X1)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,sK5(X2,X0))
| ~ partition(X2,X1)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X0 = X2 )
| ~ partition(X1,X4)
| ~ member(X3,X2)
| ~ member(X3,X0)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| ~ apply(X0,sK11(X1,X0),sK10(X1,X0))
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0)) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| apply(X0,sK10(X1,X0),sK11(X1,X0))
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0)) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK10(X1,X0),X1)
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0)) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK11(X1,X0),X1)
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0)) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK9(X1,X0),X1)
| ~ apply(X0,sK11(X1,X0),sK10(X1,X0)) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK9(X1,X0),X1)
| apply(X0,sK10(X1,X0),sK11(X1,X0)) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0)
| equivalence(X1,X0)
| member(sK10(X0,X1),X0)
| member(sK9(X0,X1),X0) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0)
| equivalence(X1,X0)
| member(sK11(X0,X1),X0)
| member(sK9(X0,X1),X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X0,X2)
| ~ subset(X1,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_424,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( member(X5,X3)
| ~ partition(X4,X2)
| ~ member(X5,X1)
| ~ member(X0,X4)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_73]) ).
tcf(c_425,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X2,X3)
| ~ partition(X1,X3)
| ~ member(X2,X0)
| ~ member(X0,X1) ),
inference(unflattening,[status(thm)],[c_424]) ).
tcf(c_442,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X2,sK5(X1,X2))
| ~ member(X2,X0)
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_57]) ).
tcf(c_443,plain,
! [X0: $i] :
( member(X0,sK5(sK1,X0))
| ~ member(X0,sK2) ),
inference(unflattening,[status(thm)],[c_442]) ).
tcf(c_451,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(sK5(X1,X2),X1)
| ~ member(X2,X0)
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_56]) ).
tcf(c_452,plain,
! [X0: $i] :
( member(sK5(sK1,X0),sK1)
| ~ member(X0,sK2) ),
inference(unflattening,[status(thm)],[c_451]) ).
tcf(c_460,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X2 = X3 )
| ~ member(X4,X3)
| ~ member(X4,X2)
| ~ member(X3,X1)
| ~ member(X2,X1)
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_58]) ).
tcf(c_461,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK1)
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(unflattening,[status(thm)],[c_460]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X3,X0)
| ~ member(X3,X2)
| ~ member(X2,X1)
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_425]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i] :
( member(X0,sK2)
| ~ member(X1,sK1)
| ~ member(X0,X1) ),
inference(unflattening,[status(thm)],[c_478]) ).
tcf(c_501,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X2,sK2)
| ~ member(X1,sK1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_50,c_479]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK9(X1,X0),X1)
| apply(X0,sK10(X1,X0),sK11(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_70]) ).
tcf(c_503,plain,
( sP0(sK3,sK2)
| member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_502]) ).
tcf(c_513,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK9(X1,X0),X1)
| ~ apply(X0,sK11(X1,X0),sK10(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_69]) ).
tcf(c_514,plain,
( sP0(sK3,sK2)
| member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_513]) ).
tcf(c_524,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK11(X1,X0),X1)
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_68]) ).
tcf(c_525,plain,
( sP0(sK3,sK2)
| member(sK11(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_524]) ).
tcf(c_535,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK10(X1,X0),X1)
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_67]) ).
tcf(c_536,plain,
( sP0(sK3,sK2)
| member(sK10(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_535]) ).
tcf(c_546,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| apply(X0,sK10(X1,X0),sK11(X1,X0))
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_66]) ).
tcf(c_547,plain,
( sP0(sK3,sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_546]) ).
tcf(c_557,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| ~ apply(X0,sK11(X1,X0),sK10(X1,X0))
| ~ apply(X0,sK9(X1,X0),sK9(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_65]) ).
tcf(c_558,plain,
( sP0(sK3,sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_557]) ).
tcf(c_568,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK11(X1,X0),X1)
| member(sK9(X1,X0),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_72]) ).
tcf(c_569,plain,
( sP0(sK3,sK2)
| member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2) ),
inference(unflattening,[status(thm)],[c_568]) ).
tcf(c_579,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK10(X1,X0),X1)
| member(sK9(X1,X0),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_71]) ).
tcf(c_580,plain,
( sP0(sK3,sK2)
| member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2) ),
inference(unflattening,[status(thm)],[c_579]) ).
tcf(c_1286,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_1290,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(X0,X2)
| ~ member(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1329,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X1,sK1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_501,c_479]) ).
tcf(c_2189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sK4(X1,X2) = X3 )
| ~ member(X3,sK1)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ member(X0,X3)
| ~ apply(sK3,X1,X2)
| ~ member(X0,sK4(X1,X2)) ),
inference(superposition,[status(thm)],[c_51,c_461]) ).
tcf(c_2190,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(sK1,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK2)
| ~ member(X0,X2)
| ~ member(X0,sK5(sK1,X1)) ),
inference(superposition,[status(thm)],[c_452,c_461]) ).
tcf(c_2205,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X0,X1)
| ~ member(X2,X1)
| ~ member(X1,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_501,c_1329]) ).
tcf(c_2206,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X1,sK1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(renaming,[status(thm)],[c_2205]) ).
tcf(c_2217,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(sK4(X1,X2),sK1)
| ~ member(X0,sK4(X1,X2)) ),
inference(superposition,[status(thm)],[c_53,c_2206]) ).
tcf(c_2218,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X1,X0)
| ~ member(X1,sK2)
| ~ member(sK5(sK1,X1),sK1)
| ~ member(X0,sK5(sK1,X1)) ),
inference(superposition,[status(thm)],[c_443,c_2206]) ).
tcf(c_2449,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(X0,sK4(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2217,c_51]) ).
tcf(c_2465,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_52,c_2449]) ).
tcf(c_2525,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK4(X0,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ member(X1,X2)
| ~ apply(sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_53,c_2189]) ).
tcf(c_2842,plain,
( member(sK9(sK2,sK3),sK5(sK1,sK9(sK2,sK3)))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_2843,plain,
( member(sK5(sK1,sK9(sK2,sK3)),sK1)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK4(X0,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X0,sK2)
| ~ member(X1,X2)
| ~ apply(sK3,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2525,c_479]) ).
tcf(c_3305,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X0,X1)
| ~ member(sK5(sK1,sK9(sK2,sK3)),sK1)
| ~ member(X1,sK5(sK1,sK9(sK2,sK3)))
| ~ member(X0,sK5(sK1,sK9(sK2,sK3))) ),
inference(instantiation,[status(thm)],[c_1329]) ).
tcf(c_3315,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK5(sK1,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2218,c_452]) ).
tcf(c_3325,plain,
! [X0: $i] :
( apply(sK3,X0,X0)
| ~ member(X0,sK2) ),
inference(superposition,[status(thm)],[c_443,c_3315]) ).
tcf(c_3333,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,sK2)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_3325,c_2856]) ).
tcf(c_3369,plain,
( member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ~ member(sK8(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_3370,plain,
( member(sK5(sK1,sK8(sK3,sK2)),sK1)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_3458,plain,
( member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2)))
| ~ member(sK7(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_3459,plain,
( member(sK5(sK1,sK7(sK3,sK2)),sK1)
| ~ member(sK7(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_3576,plain,
( member(sK6(sK3,sK2),sK5(sK1,sK6(sK3,sK2)))
| ~ member(sK6(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_3577,plain,
( member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_3913,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3333,c_479,c_3333]) ).
tcf(c_3924,plain,
! [X0: $i] :
( ( sK4(X0,X0) = sK5(sK1,X0) )
| ~ member(X0,sK2)
| ~ member(sK5(sK1,X0),sK1) ),
inference(superposition,[status(thm)],[c_443,c_3913]) ).
tcf(c_4045,plain,
! [X0: $i] :
( ( sK4(X0,X0) = sK5(sK1,X0) )
| ~ member(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_3924,c_452,c_3924]) ).
tcf(c_4246,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X0,X1)
| ~ member(sK5(sK1,sK8(sK3,sK2)),sK1)
| ~ member(X1,sK5(sK1,sK8(sK3,sK2)))
| ~ member(X0,sK5(sK1,sK8(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_1329]) ).
tcf(c_4558,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sK4(X1,X2) = X3 )
| ~ member(X3,sK1)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ member(X0,X3)
| ~ apply(sK3,X1,X2)
| ~ member(X0,sK4(X1,X2)) ),
inference(superposition,[status(thm)],[c_51,c_461]) ).
tcf(c_4574,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X0,X1)
| ~ member(X2,X1)
| ~ member(X1,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_501,c_1329]) ).
tcf(c_4575,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X1,sK1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(renaming,[status(thm)],[c_4574]) ).
tcf(c_4585,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X1,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(sK4(X1,X2),sK1)
| ~ member(X0,sK4(X1,X2)) ),
inference(superposition,[status(thm)],[c_52,c_4575]) ).
tcf(c_4918,plain,
! [X0: $i] :
( apply(sK3,sK9(sK2,sK3),X0)
| ~ member(sK5(sK1,sK9(sK2,sK3)),sK1)
| ~ member(X0,sK5(sK1,sK9(sK2,sK3)))
| ~ member(sK9(sK2,sK3),sK5(sK1,sK9(sK2,sK3))) ),
inference(instantiation,[status(thm)],[c_3305]) ).
tcf(c_5533,plain,
! [X0: $i,X1: $i] :
( ( sK5(sK1,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,sK2)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_443,c_2190]) ).
tcf(c_5551,plain,
! [X0: $i,X1: $i] :
( ( sK5(sK1,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5533,c_479,c_5533]) ).
tcf(c_5560,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X0) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1)
| ~ member(sK4(X0,X1),sK1) ),
inference(superposition,[status(thm)],[c_52,c_5551]) ).
tcf(c_5561,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1)
| ~ member(sK4(X0,X1),sK1) ),
inference(superposition,[status(thm)],[c_53,c_5551]) ).
tcf(c_5659,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X1,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(X0,sK4(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4585,c_51]) ).
tcf(c_5675,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X0,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_52,c_5659]) ).
tcf(c_5684,plain,
! [X0: $i] :
( apply(sK3,X0,X0)
| ~ member(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_5675,c_3325]) ).
tcf(c_5940,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK4(X0,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ member(X0,X2)
| ~ apply(sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_52,c_4558]) ).
tcf(c_6018,plain,
sK8(sK3,sK2) = sK8(sK3,sK2),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_6039,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X0) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5560,c_51,c_5560]) ).
tcf(c_6190,plain,
sK7(sK3,sK2) = sK7(sK3,sK2),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_6252,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5561,c_51,c_5561]) ).
tcf(c_6454,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK4(X0,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK2)
| ~ member(X0,X2)
| ~ apply(sK3,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5940,c_479]) ).
tcf(c_6477,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,sK2)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_5684,c_6454]) ).
tcf(c_6523,plain,
( apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ member(sK5(sK1,sK9(sK2,sK3)),sK1)
| ~ member(sK9(sK2,sK3),sK5(sK1,sK9(sK2,sK3))) ),
inference(instantiation,[status(thm)],[c_4918]) ).
tcf(c_7007,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_6477,c_3913]) ).
tcf(c_7018,plain,
! [X0: $i] :
( ( sK4(X0,X0) = sK5(sK1,X0) )
| ~ member(X0,sK2)
| ~ member(sK5(sK1,X0),sK1) ),
inference(superposition,[status(thm)],[c_443,c_7007]) ).
tcf(c_8441,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ~ member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ( X1 != sK5(sK1,sK8(sK3,sK2)) )
| ( X0 != sK8(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_8443,plain,
! [X0: $i] :
( apply(sK3,sK8(sK3,sK2),X0)
| ~ member(sK5(sK1,sK8(sK3,sK2)),sK1)
| ~ member(X0,sK5(sK1,sK8(sK3,sK2)))
| ~ member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_4246]) ).
tcf(c_8448,plain,
! [X0: $i,X1: $i] :
( member(X0,X1)
| ~ member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2)))
| ( X1 != sK5(sK1,sK7(sK3,sK2)) )
| ( X0 != sK7(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_8502,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X0,X1)
| ~ member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ member(X1,sK5(sK1,sK6(sK3,sK2)))
| ~ member(X0,sK5(sK1,sK6(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_1329]) ).
tcf(c_8689,plain,
! [X0: $i] :
( ( sK4(X0,X0) = sK5(sK1,X0) )
| ~ member(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_7018,c_452,c_3924]) ).
tcf(c_8780,plain,
! [X0: $i] :
( apply(sK3,sK6(sK3,sK2),X0)
| ~ member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ member(X0,sK5(sK1,sK6(sK3,sK2)))
| ~ member(sK6(sK3,sK2),sK5(sK1,sK6(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_8502]) ).
tcf(c_8788,plain,
! [X0: $i] :
( member(sK8(sK3,sK2),X0)
| ~ member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ( X0 != sK5(sK1,sK8(sK3,sK2)) )
| ( sK8(sK3,sK2) != sK8(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_8441]) ).
tcf(c_9084,plain,
! [X0: $i] :
( member(sK7(sK3,sK2),X0)
| ~ member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2)))
| ( X0 != sK5(sK1,sK7(sK3,sK2)) )
| ( sK7(sK3,sK2) != sK7(sK3,sK2) ) ),
inference(instantiation,[status(thm)],[c_8448]) ).
tcf(c_9730,plain,
( apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK5(sK1,sK8(sK3,sK2)),sK1)
| ~ member(sK7(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ~ member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_8443]) ).
tcf(c_28778,plain,
( apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2))
| ~ member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ member(sK8(sK3,sK2),sK5(sK1,sK6(sK3,sK2)))
| ~ member(sK6(sK3,sK2),sK5(sK1,sK6(sK3,sK2))) ),
inference(instantiation,[status(thm)],[c_8780]) ).
tcf(c_30618,plain,
( member(sK7(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ~ member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2)))
| ( sK7(sK3,sK2) != sK7(sK3,sK2) )
| ( sK5(sK1,sK8(sK3,sK2)) != sK5(sK1,sK7(sK3,sK2)) ) ),
inference(instantiation,[status(thm)],[c_9084]) ).
tcf(c_31159,plain,
( member(sK8(sK3,sK2),sK5(sK1,sK6(sK3,sK2)))
| ~ member(sK8(sK3,sK2),sK5(sK1,sK8(sK3,sK2)))
| ( sK8(sK3,sK2) != sK8(sK3,sK2) )
| ( sK5(sK1,sK6(sK3,sK2)) != sK5(sK1,sK8(sK3,sK2)) ) ),
inference(instantiation,[status(thm)],[c_8788]) ).
tcf(c_39612,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(sK1,X1) = X2 )
| ~ member(X2,sK1)
| ~ member(X1,sK2)
| ~ member(X0,X2)
| ~ member(X0,sK5(sK1,X1)) ),
inference(superposition,[status(thm)],[c_452,c_461]) ).
tcf(c_39625,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X0,X1)
| ~ member(X2,X1)
| ~ member(X1,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_501,c_1329]) ).
tcf(c_39626,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X0,X2)
| ~ member(X1,sK1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(renaming,[status(thm)],[c_39625]) ).
tcf(c_39637,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(sK4(X1,X2),sK1)
| ~ member(X0,sK4(X1,X2)) ),
inference(superposition,[status(thm)],[c_53,c_39626]) ).
tcf(c_39727,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK3,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ apply(sK3,X1,X2)
| ~ member(X0,sK4(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_39637,c_51]) ).
tcf(c_39743,plain,
! [X0: $i,X1: $i] :
( apply(sK3,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(superposition,[status(thm)],[c_52,c_39727]) ).
tcf(c_41185,plain,
! [X0: $i,X1: $i] :
( ( sK5(sK1,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,sK2)
| ~ member(X0,X1) ),
inference(superposition,[status(thm)],[c_443,c_39612]) ).
tcf(c_41205,plain,
! [X0: $i,X1: $i] :
( ( sK5(sK1,X0) = X1 )
| ~ member(X1,sK1)
| ~ member(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_41185,c_5551]) ).
tcf(c_41214,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X0) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1)
| ~ member(sK4(X0,X1),sK1) ),
inference(superposition,[status(thm)],[c_52,c_41205]) ).
tcf(c_41215,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1)
| ~ member(sK4(X0,X1),sK1) ),
inference(superposition,[status(thm)],[c_53,c_41205]) ).
tcf(c_41350,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X0) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_41214,c_6039]) ).
tcf(c_41410,plain,
! [X0: $i,X1: $i] :
( ( sK4(X0,X1) = sK5(sK1,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK3,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_41215,c_6252]) ).
fof(f31,definition,
! [X1,X0] :
( ~ sP0(X1,X0)
| ? [X5,X6,X7] :
( member(X7,X0)
& member(X6,X0)
& member(X5,X0)
& apply(X1,X6,X7)
& apply(X1,X5,X6)
& ~ apply(X1,X5,X7) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f32,plain,
! [X0,X1] :
( sP0(X1,X0)
| ? [X3,X4] :
( member(X4,X0)
& member(X3,X0)
& apply(X1,X3,X4)
& ~ apply(X1,X4,X3) )
| ? [X2] :
( member(X2,X0)
& ~ apply(X1,X2,X2) )
| equivalence(X1,X0) ),
inference(definition_folding,[],[f29,f31]) ).
fof(f37,plain,
! [X1,X0] :
( ~ sP0(X1,X0)
| ? [X5,X6,X7] :
( member(X7,X0)
& member(X6,X0)
& member(X5,X0)
& apply(X1,X6,X7)
& apply(X1,X5,X6)
& ~ apply(X1,X5,X7) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f38,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ? [X2,X3,X4] :
( member(X4,X1)
& member(X3,X1)
& member(X2,X1)
& apply(X0,X3,X4)
& apply(X0,X2,X3)
& ~ apply(X0,X2,X4) ) ),
inference(rectify,[],[f37]) ).
fof(f39,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( member(sK8(X0,X1),X1)
& member(sK7(X0,X1),X1)
& member(sK6(X0,X1),X1)
& apply(X0,sK7(X0,X1),sK8(X0,X1))
& apply(X0,sK6(X0,X1),sK7(X0,X1))
& ~ apply(X0,sK6(X0,X1),sK8(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X2,sK6(X0,X1)),skolemize(X3,sK7(X0,X1)),skolemize(X4,sK8(X0,X1))],[f38]) ).
fof(f51,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK8(X0,X1),X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f52,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f53,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK6(X0,X1),X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f54,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK7(X0,X1),sK8(X0,X1)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f55,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK6(X0,X1),sK7(X0,X1)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f56,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1)) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1)) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( member(sK6(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_614,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_580]) ).
tcf(c_615,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_614]) ).
tcf(c_625,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_569]) ).
tcf(c_626,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_625]) ).
tcf(c_636,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_558]) ).
tcf(c_637,plain,
( member(sK8(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_636]) ).
tcf(c_647,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_547]) ).
tcf(c_648,plain,
( member(sK8(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_647]) ).
tcf(c_658,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_536]) ).
tcf(c_659,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_658]) ).
tcf(c_669,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_525]) ).
tcf(c_670,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_669]) ).
tcf(c_680,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_514]) ).
tcf(c_681,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_680]) ).
tcf(c_691,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK8(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_503]) ).
tcf(c_692,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_691]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_580]) ).
tcf(c_703,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_702]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_569]) ).
tcf(c_714,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_713]) ).
tcf(c_724,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_558]) ).
tcf(c_725,plain,
( member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_724]) ).
tcf(c_735,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_547]) ).
tcf(c_736,plain,
( member(sK7(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_735]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_536]) ).
tcf(c_747,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_746]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_525]) ).
tcf(c_758,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_757]) ).
tcf(c_768,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_514]) ).
tcf(c_769,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_768]) ).
tcf(c_779,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK7(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_503]) ).
tcf(c_780,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_779]) ).
tcf(c_790,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_580]) ).
tcf(c_791,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_790]) ).
tcf(c_801,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_569]) ).
tcf(c_802,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_801]) ).
tcf(c_812,plain,
! [X0: $i,X1: $i] :
( member(sK6(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_558]) ).
tcf(c_813,plain,
( member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_812]) ).
tcf(c_823,plain,
! [X0: $i,X1: $i] :
( member(sK6(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_547]) ).
tcf(c_824,plain,
( member(sK6(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_823]) ).
tcf(c_834,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_536]) ).
tcf(c_835,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_834]) ).
tcf(c_845,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_525]) ).
tcf(c_846,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_845]) ).
tcf(c_856,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_514]) ).
tcf(c_857,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_856]) ).
tcf(c_867,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| member(sK6(X0,X1),X1)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_503]) ).
tcf(c_868,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_867]) ).
tcf(c_878,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_580]) ).
tcf(c_879,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_878]) ).
tcf(c_889,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_569]) ).
tcf(c_890,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_889]) ).
tcf(c_900,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_558]) ).
tcf(c_901,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_900]) ).
tcf(c_911,plain,
! [X0: $i,X1: $i] :
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_547]) ).
tcf(c_912,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_911]) ).
tcf(c_922,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_536]) ).
tcf(c_923,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_922]) ).
tcf(c_933,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_525]) ).
tcf(c_934,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_933]) ).
tcf(c_944,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_514]) ).
tcf(c_945,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_944]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_503]) ).
tcf(c_956,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_955]) ).
tcf(c_966,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_580]) ).
tcf(c_967,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_966]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_569]) ).
tcf(c_978,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_977]) ).
tcf(c_988,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_558]) ).
tcf(c_989,plain,
( apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_988]) ).
tcf(c_999,plain,
! [X0: $i,X1: $i] :
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_547]) ).
tcf(c_1000,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_999]) ).
tcf(c_1010,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_536]) ).
tcf(c_1011,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_1010]) ).
tcf(c_1021,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_525]) ).
tcf(c_1022,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_1021]) ).
tcf(c_1032,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_514]) ).
tcf(c_1033,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(unflattening,[status(thm)],[c_1032]) ).
tcf(c_1043,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(X0,sK6(X0,X1),sK7(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_503]) ).
tcf(c_1044,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1043]) ).
tcf(c_1054,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_580]) ).
tcf(c_1055,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1054]) ).
tcf(c_1065,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_569]) ).
tcf(c_1066,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1065]) ).
tcf(c_1076,plain,
! [X0: $i,X1: $i] :
( ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_558]) ).
tcf(c_1077,plain,
( ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1076]) ).
tcf(c_1087,plain,
! [X0: $i,X1: $i] :
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_547]) ).
tcf(c_1088,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1087]) ).
tcf(c_1098,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_536]) ).
tcf(c_1099,plain,
( member(sK10(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1098]) ).
tcf(c_1109,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_525]) ).
tcf(c_1110,plain,
( member(sK11(sK2,sK3),sK2)
| ~ apply(sK3,sK9(sK2,sK3),sK9(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1109]) ).
tcf(c_1120,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_514]) ).
tcf(c_1121,plain,
( member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1120]) ).
tcf(c_1131,plain,
! [X0: $i,X1: $i] :
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(X0,sK6(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_503]) ).
tcf(c_1132,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(unflattening,[status(thm)],[c_1131]) ).
tcf(c_2552,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_692,c_2465]) ).
tcf(c_2576,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_780,c_2465]) ).
tcf(c_2600,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_868,c_2465]) ).
tcf(c_3078,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_681,c_615,c_626,c_681,c_2552]) ).
tcf(c_3103,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_769,c_703,c_714,c_769,c_2576]) ).
tcf(c_3134,plain,
( member(sK9(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_857,c_791,c_802,c_857,c_2600]) ).
tcf(c_3336,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_846]) ).
tcf(c_3337,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK6(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_835]) ).
tcf(c_3338,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_758]) ).
tcf(c_3339,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK7(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_747]) ).
tcf(c_3340,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_670]) ).
tcf(c_3341,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2)
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_659]) ).
tcf(c_3342,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_912]) ).
tcf(c_3379,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_956,c_956,c_3342]) ).
tcf(c_3380,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(renaming,[status(thm)],[c_3379]) ).
tcf(c_3387,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_3380,c_2465]) ).
tcf(c_3436,plain,
( member(sK8(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_648]) ).
tcf(c_3474,plain,
( member(sK7(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_736]) ).
tcf(c_3484,plain,
( member(sK6(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_824]) ).
tcf(c_3494,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_923]) ).
tcf(c_3504,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_1000]) ).
tcf(c_3514,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_934]) ).
tcf(c_3530,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_1011]) ).
tcf(c_3540,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK9(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_3325,c_1022]) ).
tcf(c_3873,plain,
( member(sK10(sK2,sK3),sK2)
| ~ member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_3325,c_1099]) ).
tcf(c_3883,plain,
( member(sK11(sK2,sK3),sK2)
| ~ member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_3325,c_1110]) ).
tcf(c_3887,plain,
( member(sK11(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_3340,c_615,c_626,c_681,c_2552,c_3340]) ).
tcf(c_3900,plain,
( member(sK10(sK2,sK3),sK2)
| member(sK8(sK3,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_3341,c_615,c_626,c_681,c_2552,c_3341]) ).
tcf(c_4057,plain,
( member(sK9(sK2,sK3),sK2)
| ( sK4(sK7(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(superposition,[status(thm)],[c_3103,c_4045]) ).
tcf(c_5086,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ member(sK9(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_3325,c_1088]) ).
tcf(c_5090,plain,
( member(sK8(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_3436,c_615,c_626,c_681,c_2552,c_3436]) ).
tcf(c_5101,plain,
( member(sK8(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_5090,c_2465]) ).
tcf(c_5147,plain,
( member(sK7(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_3474,c_703,c_714,c_769,c_2576,c_3474]) ).
tcf(c_5158,plain,
( member(sK7(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_5147,c_2465]) ).
tcf(c_5194,plain,
( member(sK6(sK3,sK2),sK2)
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_3484,c_3134,c_3484]) ).
tcf(c_5205,plain,
( member(sK6(sK3,sK2),sK2)
| apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_5194,c_2465]) ).
tcf(c_5234,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3494,c_879,c_3494]) ).
tcf(c_5245,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5234,c_2465]) ).
tcf(c_5292,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3514,c_890,c_3514]) ).
tcf(c_5303,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5292,c_2465]) ).
tcf(c_5350,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3530,c_967,c_3530]) ).
tcf(c_5398,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3540,c_978,c_3540]) ).
tcf(c_6056,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5398,c_6039]) ).
tcf(c_6057,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5350,c_6039]) ).
tcf(c_6268,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5398,c_6252]) ).
tcf(c_6269,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5350,c_6252]) ).
tcf(c_9908,plain,
( apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_989,c_989,c_1033,c_2843,c_2842,c_6523]) ).
tcf(c_9914,plain,
member(sK8(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_659,c_637,c_2843,c_2842,c_3078,c_3887,c_3900,c_5101,c_6523]) ).
tcf(c_9933,plain,
member(sK7(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_747,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3339,c_3338,c_5158,c_6523]) ).
tcf(c_9936,plain,
sK4(sK7(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)),
inference(superposition,[status(thm)],[c_9933,c_8689]) ).
tcf(c_10123,plain,
sK4(sK7(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)),
inference(global_subsumption_just,[status(thm)],[c_4057,c_9936]) ).
tcf(c_10130,plain,
( member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2)))
| ~ member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK7(sK3,sK2),sK7(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_10123,c_53]) ).
tcf(c_10132,plain,
( member(sK5(sK1,sK7(sK3,sK2)),sK1)
| ~ member(sK7(sK3,sK2),sK2)
| ~ apply(sK3,sK7(sK3,sK2),sK7(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_10123,c_51]) ).
tcf(c_10170,plain,
member(sK5(sK1,sK7(sK3,sK2)),sK1),
inference(global_subsumption_just,[status(thm)],[c_10132,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3339,c_3338,c_3459,c_5158,c_6523]) ).
tcf(c_10192,plain,
member(sK7(sK3,sK2),sK5(sK1,sK7(sK3,sK2))),
inference(global_subsumption_just,[status(thm)],[c_10130,c_3458,c_9933]) ).
tcf(c_10197,plain,
( member(sK7(sK3,sK2),sK2)
| ~ member(sK5(sK1,sK7(sK3,sK2)),sK1) ),
inference(superposition,[status(thm)],[c_10192,c_479]) ).
tcf(c_10200,plain,
member(sK7(sK3,sK2),sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_10197,c_10170]) ).
tcf(c_12069,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1000,c_1044,c_3504]) ).
tcf(c_12599,plain,
member(sK8(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_5101,c_637,c_2843,c_2842,c_3078,c_3887,c_3900,c_5101,c_6523]) ).
tcf(c_13065,plain,
member(sK6(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_835,c_791,c_802,c_813,c_857,c_2600,c_2843,c_2842,c_3337,c_3336,c_5205,c_6523]) ).
tcf(c_13083,plain,
( member(sK10(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3873,c_1055,c_3873]) ).
tcf(c_13165,plain,
( member(sK11(sK2,sK3),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1066,c_1066,c_3883]) ).
tcf(c_13176,plain,
( ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1077,c_1077,c_1121,c_2843,c_2842,c_6523]) ).
tcf(c_14985,plain,
member(sK6(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_5205,c_13065]) ).
tcf(c_15010,plain,
sK4(sK6(sK3,sK2),sK6(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)),
inference(superposition,[status(thm)],[c_14985,c_4045]) ).
tcf(c_15129,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_5245,c_637,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3078,c_3339,c_3338,c_3887,c_3900,c_5101,c_5158,c_5245,c_6523]) ).
tcf(c_15135,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_15129,c_6252]) ).
tcf(c_15136,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_15129,c_6039]) ).
tcf(c_15154,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15136,c_10200,c_12599]) ).
tcf(c_15157,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15135,c_10200,c_12599]) ).
tcf(c_15172,plain,
( member(sK11(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_5303,c_637,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3078,c_3339,c_3338,c_3887,c_3900,c_5101,c_5158,c_5303,c_6523]) ).
tcf(c_15178,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_15172,c_6252]) ).
tcf(c_15179,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_15172,c_6039]) ).
tcf(c_15197,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15179,c_10200,c_12599]) ).
tcf(c_15200,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15178,c_10200,c_12599]) ).
tcf(c_15407,plain,
( member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK6(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_15010,c_51]) ).
tcf(c_15411,plain,
( member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ apply(sK3,sK6(sK3,sK2),sK6(sK3,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15407,c_14985]) ).
tcf(c_15453,plain,
member(sK5(sK1,sK6(sK3,sK2)),sK1),
inference(global_subsumption_just,[status(thm)],[c_15411,c_791,c_802,c_813,c_857,c_2600,c_2843,c_2842,c_3337,c_3336,c_3577,c_5205,c_6523]) ).
tcf(c_15725,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ~ apply(sK3,sK6(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1088,c_1132,c_5086]) ).
tcf(c_15742,plain,
( ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_945,c_901,c_945,c_2843,c_2842,c_6523]) ).
tcf(c_15743,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ~ apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_15742]) ).
tcf(c_17712,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3387,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3339,c_3338,c_3387,c_5158,c_6523,c_9914]) ).
tcf(c_17719,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_17712,c_6252]) ).
tcf(c_17720,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_17712,c_6039]) ).
tcf(c_17738,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17720,c_10200,c_12599]) ).
tcf(c_17741,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17719,c_10200,c_12599]) ).
tcf(c_19787,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3504,c_12069]) ).
tcf(c_19794,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_19787,c_6252]) ).
tcf(c_19795,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_19787,c_6039]) ).
tcf(c_19816,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19795,c_10200,c_14985]) ).
tcf(c_19819,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19794,c_10200,c_14985]) ).
tcf(c_20533,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_17738,c_2465]) ).
tcf(c_20822,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_17741,c_2465]) ).
tcf(c_20892,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_19816,c_2465]) ).
tcf(c_20981,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_19819,c_2465]) ).
tcf(c_24231,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6056,c_703,c_714,c_725,c_769,c_791,c_802,c_813,c_857,c_2576,c_2600,c_2843,c_2842,c_3339,c_3338,c_3337,c_3336,c_5158,c_5205,c_6056,c_6523]) ).
tcf(c_24264,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6057,c_703,c_714,c_725,c_769,c_791,c_802,c_813,c_857,c_2576,c_2600,c_2843,c_2842,c_3339,c_3338,c_3337,c_3336,c_5158,c_5205,c_6057,c_6523]) ).
tcf(c_24397,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6268,c_703,c_714,c_725,c_769,c_791,c_802,c_813,c_857,c_2576,c_2600,c_2843,c_2842,c_3339,c_3338,c_3337,c_3336,c_5158,c_5205,c_6268,c_6523]) ).
tcf(c_24430,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6269,c_703,c_714,c_725,c_769,c_791,c_802,c_813,c_857,c_2576,c_2600,c_2843,c_2842,c_3339,c_3338,c_3337,c_3336,c_5158,c_5205,c_6269,c_6523]) ).
tcf(c_34924,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_20533,c_15154,c_15197,c_20533]) ).
tcf(c_34956,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(superposition,[status(thm)],[c_34924,c_945]) ).
tcf(c_35191,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_20822,c_15157,c_15200,c_20822]) ).
tcf(c_35976,plain,
( ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_34956,c_879,c_890,c_3494,c_3514,c_15743,c_20533]) ).
tcf(c_35977,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(renaming,[status(thm)],[c_35976]) ).
tcf(c_36004,plain,
( apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_35977,c_2465]) ).
tcf(c_36005,plain,
( apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36004,c_10200,c_12599]) ).
tcf(c_36160,plain,
( ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_36005,c_6039]) ).
tcf(c_36168,plain,
sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_36160,c_10200,c_12599]) ).
tcf(c_36170,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_35191,c_36168]) ).
tcf(c_36742,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_20892,c_20892,c_24231,c_24264]) ).
tcf(c_36773,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(superposition,[status(thm)],[c_36742,c_1033]) ).
tcf(c_36946,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_20981,c_20981,c_24397,c_24430]) ).
tcf(c_38072,plain,
( member(sK9(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(superposition,[status(thm)],[c_36170,c_945]) ).
tcf(c_39666,plain,
member(sK8(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_615,c_637,c_2843,c_2842,c_3078,c_3887,c_3900,c_5101,c_6523]) ).
tcf(c_39670,plain,
member(sK7(sK3,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_703,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3339,c_3338,c_5158,c_6523]) ).
tcf(c_40328,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_879,c_879,c_3494]) ).
tcf(c_40339,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_40328,c_39743]) ).
tcf(c_40340,plain,
( member(sK10(sK2,sK3),sK2)
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40339,c_39670,c_39666]) ).
tcf(c_40859,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_956,c_956,c_3342]) ).
tcf(c_40860,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(renaming,[status(thm)],[c_40859]) ).
tcf(c_40870,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_40860,c_39743]) ).
tcf(c_40871,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40870,c_39670,c_39666]) ).
tcf(c_41790,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_40340,c_41350]) ).
tcf(c_41808,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41790,c_39670,c_39666]) ).
tcf(c_42700,plain,
sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)),
inference(global_subsumption_just,[status(thm)],[c_41808,c_36168]) ).
tcf(c_43015,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_40871,c_41410]) ).
tcf(c_43036,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(light_normalisation,[status(thm)],[c_43015,c_42700]) ).
tcf(c_43037,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_43036,c_39670,c_39666]) ).
tcf(c_44816,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_43037,c_39743]) ).
tcf(c_45799,plain,
( ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_38072,c_5234,c_5292,c_15743,c_44816]) ).
tcf(c_45800,plain,
( apply(sK3,sK7(sK3,sK2),sK8(sK3,sK2))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(renaming,[status(thm)],[c_45799]) ).
tcf(c_45829,plain,
( apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_45800,c_2465]) ).
tcf(c_45830,plain,
( apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2))
| ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_45829,c_10200,c_12599]) ).
tcf(c_46003,plain,
apply(sK3,sK8(sK3,sK2),sK7(sK3,sK2)),
inference(global_subsumption_just,[status(thm)],[c_45830,c_703,c_714,c_725,c_769,c_2576,c_2843,c_2842,c_3339,c_3338,c_3370,c_3369,c_3458,c_5158,c_6190,c_6523,c_9730,c_9914,c_30618,c_45830]) ).
tcf(c_46026,plain,
( ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_46003,c_6252]) ).
tcf(c_46032,plain,
! [X0: $i] :
( ( sK4(sK8(sK3,sK2),sK7(sK3,sK2)) = X0 )
| ~ member(X0,sK1)
| ~ member(sK8(sK3,sK2),sK2)
| ~ member(sK7(sK3,sK2),X0) ),
inference(superposition,[status(thm)],[c_46003,c_2856]) ).
tcf(c_46038,plain,
! [X0: $i] :
( ( sK5(sK1,sK8(sK3,sK2)) = X0 )
| ~ member(X0,sK1)
| ~ member(sK8(sK3,sK2),sK2)
| ~ member(sK7(sK3,sK2),X0) ),
inference(light_normalisation,[status(thm)],[c_46032,c_36168]) ).
tcf(c_46039,plain,
! [X0: $i] :
( ( sK5(sK1,sK8(sK3,sK2)) = X0 )
| ~ member(X0,sK1)
| ~ member(sK7(sK3,sK2),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_46038,c_12599]) ).
tcf(c_46043,plain,
( ( sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK8(sK3,sK2),sK2) ),
inference(light_normalisation,[status(thm)],[c_46026,c_36168]) ).
tcf(c_46044,plain,
sK5(sK1,sK8(sK3,sK2)) = sK5(sK1,sK7(sK3,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_46043,c_10200,c_12599]) ).
tcf(c_46087,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_36946,c_46044]) ).
tcf(c_46097,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_24430,c_46044]) ).
tcf(c_46098,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_24397,c_46044]) ).
tcf(c_46102,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_19819,c_46044]) ).
tcf(c_49228,plain,
( ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_36773,c_5350,c_5398,c_9908,c_20892]) ).
tcf(c_49229,plain,
( apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2))
| ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) ) ),
inference(renaming,[status(thm)],[c_49228]) ).
tcf(c_49251,plain,
( ( sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)) )
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2) ),
inference(superposition,[status(thm)],[c_49229,c_6039]) ).
tcf(c_49260,plain,
sK4(sK6(sK3,sK2),sK7(sK3,sK2)) = sK5(sK1,sK6(sK3,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_49251,c_10200,c_14985]) ).
tcf(c_49261,plain,
( apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3))
| ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_46102,c_49260]) ).
tcf(c_49262,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_46087,c_49260]) ).
tcf(c_49263,plain,
( member(sK11(sK2,sK3),sK2)
| ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_46098,c_49260]) ).
tcf(c_49264,plain,
( member(sK10(sK2,sK3),sK2)
| ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) ) ),
inference(demodulation,[status(thm)],[c_46097,c_49260]) ).
tcf(c_49290,plain,
( member(sK7(sK3,sK2),sK5(sK1,sK6(sK3,sK2)))
| ~ member(sK7(sK3,sK2),sK2)
| ~ member(sK6(sK3,sK2),sK2)
| ~ apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_49260,c_53]) ).
tcf(c_49296,plain,
( member(sK7(sK3,sK2),sK5(sK1,sK6(sK3,sK2)))
| ~ apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_49290,c_10200,c_14985]) ).
tcf(c_49307,plain,
member(sK11(sK2,sK3),sK2),
inference(global_subsumption_just,[status(thm)],[c_49263,c_637,c_791,c_802,c_813,c_857,c_2600,c_2843,c_2842,c_3078,c_3337,c_3336,c_3369,c_3577,c_3576,c_3887,c_3900,c_5101,c_5205,c_6018,c_6523,c_13165,c_28778,c_31159,c_49263]) ).
tcf(c_49678,plain,
( ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ member(sK5(sK1,sK6(sK3,sK2)),sK1)
| ~ apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(superposition,[status(thm)],[c_49296,c_46039]) ).
tcf(c_49687,plain,
( ( sK5(sK1,sK6(sK3,sK2)) = sK5(sK1,sK8(sK3,sK2)) )
| ~ apply(sK3,sK6(sK3,sK2),sK7(sK3,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_49678,c_15453]) ).
tcf(c_49924,plain,
member(sK10(sK2,sK3),sK2),
inference(global_subsumption_just,[status(thm)],[c_49264,c_637,c_791,c_802,c_813,c_857,c_2600,c_2843,c_2842,c_3078,c_3337,c_3336,c_3369,c_3577,c_3576,c_3887,c_3900,c_5101,c_5205,c_6018,c_6523,c_9908,c_13083,c_13176,c_28778,c_31159,c_49262,c_49687]) ).
tcf(c_50001,plain,
apply(sK3,sK10(sK2,sK3),sK11(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_49261,c_3369,c_3577,c_3576,c_6018,c_9908,c_9914,c_13065,c_13176,c_15725,c_28778,c_31159,c_49262,c_49687]) ).
tcf(c_50027,plain,
( apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3))
| ~ member(sK10(sK2,sK3),sK2)
| ~ member(sK11(sK2,sK3),sK2) ),
inference(superposition,[status(thm)],[c_50001,c_2465]) ).
tcf(c_50028,plain,
apply(sK3,sK11(sK2,sK3),sK10(sK2,sK3)),
inference(forward_subsumption_resolution,[status(thm)],[c_50027,c_49924,c_49307]) ).
tcf(c_50115,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_50028,c_49687,c_31159,c_28778,c_13176,c_13065,c_9914,c_9908,c_6018,c_3576,c_3577,c_3369]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET772+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n009.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 : Thu Sep 24 11:54:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/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.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 10.59/2.27 % SZS status Started for theBenchmark.p
% 10.59/2.27 % SZS status Theorem for theBenchmark.p
% 10.59/2.27
% 10.59/2.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.59/2.27
% 10.59/2.27 % ------ iProver source info
% 10.59/2.27
% 10.59/2.27 % git: date: 2026-07-19 20:42:38 +0200
% 10.59/2.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.59/2.27 % git: non_committed_changes: false
% 10.59/2.27
% 10.59/2.27 % ------ Parsing...
% 10.59/2.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.59/2.27
% 10.59/2.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e %
% 10.59/2.27
% 10.59/2.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.59/2.27
% 10.59/2.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 10.59/2.27 % ------ Proving...
% 10.59/2.27 % ------ Problem Properties
% 10.59/2.27
% 10.59/2.27 %
% 10.59/2.27 % clauses 56
% 10.59/2.27 % conjectures 3
% 10.59/2.27 % EPR 3
% 10.59/2.27 % Horn 18
% 10.59/2.27 % unary 0
% 10.59/2.27 % binary 2
% 10.59/2.27 % lits 173
% 10.59/2.27 % lits eq 1
% 10.59/2.27 % fd_pure 0
% 10.59/2.27 % fd_pseudo 0
% 10.59/2.27 % fd_cond 0
% 10.59/2.27 % fd_pseudo_cond 1
% 10.59/2.27 % AC symbols 0
% 10.59/2.27
% 10.59/2.27 % ------ Schedule dynamic 5 is on
% 10.59/2.27
% 10.59/2.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.59/2.27
% 10.59/2.27
% 10.59/2.27 % ------
% 10.59/2.27 % Current options:
% 10.59/2.27 % ------
% 10.59/2.27
% 10.59/2.27
% 10.59/2.27 %
% 10.59/2.27
% 10.59/2.27 % ------ Proving...
% 10.59/2.27 %
% 10.59/2.27
% 10.59/2.27 % SZS status Theorem for theBenchmark.p
% 10.59/2.27
% 10.59/2.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.59/2.29
% 10.59/2.29
%------------------------------------------------------------------------------