%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SET771+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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 8.18s 6.90s
% Output : CNFRefutation 8.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 4
% Syntax : Number of formulae : 370 ( 27 unt; 1 def)
% Number of atoms : 1952 ( 212 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 1595 ( 598 ~; 843 |; 116 &)
% ( 8 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 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 : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 442 ( 0 sgn 391 !; 51 ?; 233 :)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X3,X5,X6] :
( ( member(X6,X2)
& member(X5,X2)
& member(X3,X1) )
=> ( ( apply(X0,X3,X6)
& apply(X0,X3,X5) )
=> X5 = X6 ) )
& ! [X3] :
( member(X3,X1)
=> ? [X4] :
( apply(X0,X3,X4)
& member(X4,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET006+1.ax',maps) ).
fof(f31,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/sandbox2/benchmark/Axioms/SET006+2.ax',equivalence) ).
fof(f34,conjecture,
! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( ( member(X5,X1)
& member(X4,X1) )
=> ( apply(X3,X4,X5)
<=> ? [X6] :
( apply(X0,X5,X6)
& apply(X0,X4,X6)
& member(X6,X2) ) ) )
& maps(X0,X1,X2) )
=> equivalence(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thIII07) ).
fof(f35,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( ( member(X5,X1)
& member(X4,X1) )
=> ( apply(X3,X4,X5)
<=> ? [X6] :
( apply(X0,X5,X6)
& apply(X0,X4,X6)
& member(X6,X2) ) ) )
& maps(X0,X1,X2) )
=> equivalence(X3,X1) ),
inference(negated_conjecture,[status(cth)],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( maps(X0,X1,X2)
<=> ( ! [X5,X6,X7] :
( ( member(X7,X2)
& member(X6,X2)
& member(X5,X1) )
=> ( ( apply(X0,X5,X7)
& apply(X0,X5,X6) )
=> X6 = X7 ) )
& ! [X3] :
( member(X3,X1)
=> ? [X4] :
( apply(X0,X3,X4)
& member(X4,X2) ) ) ) ),
inference(rectify,[],[f12]) ).
fof(f37,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,[],[f31]) ).
fof(f38,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,[],[f37]) ).
fof(f39,plain,
! [X0,X1,X2] :
( maps(X0,X1,X2)
=> ( ! [X5,X6,X7] :
( ( member(X7,X2)
& member(X6,X2)
& member(X5,X1) )
=> ( ( apply(X0,X5,X7)
& apply(X0,X5,X6) )
=> X6 = X7 ) )
& ! [X3] :
( member(X3,X1)
=> ? [X4] :
( apply(X0,X3,X4)
& member(X4,X2) ) ) ) ),
inference(unused_predicate_definition_removal,[],[f36]) ).
fof(f40,plain,
? [X0,X1,X2,X3] :
( ! [X4,X5] :
( ~ member(X5,X1)
| ~ member(X4,X1)
| ( apply(X3,X4,X5)
<=> ? [X6] :
( apply(X0,X5,X6)
& apply(X0,X4,X6)
& member(X6,X2) ) ) )
& maps(X0,X1,X2)
& ~ equivalence(X3,X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f41,plain,
? [X0,X1,X2,X3] :
( ! [X4,X5] :
( ~ member(X5,X1)
| ~ member(X4,X1)
| ( apply(X3,X4,X5)
<=> ? [X6] :
( apply(X0,X5,X6)
& apply(X0,X4,X6)
& member(X6,X2) ) ) )
& maps(X0,X1,X2)
& ~ equivalence(X3,X1) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ~ maps(X0,X1,X2)
| ( ! [X5,X6,X7] :
( ~ member(X7,X2)
| ~ member(X6,X2)
| ~ member(X5,X1)
| ~ apply(X0,X5,X7)
| ~ apply(X0,X5,X6)
| X6 = X7 )
& ! [X3] :
( ~ member(X3,X1)
| ? [X4] :
( apply(X0,X3,X4)
& member(X4,X2) ) ) ) ),
inference(ennf_transformation,[],[f39]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ~ maps(X0,X1,X2)
| ( ! [X5,X6,X7] :
( ~ member(X7,X2)
| ~ member(X6,X2)
| ~ member(X5,X1)
| ~ apply(X0,X5,X7)
| ~ apply(X0,X5,X6)
| X6 = X7 )
& ! [X3] :
( ~ member(X3,X1)
| ? [X4] :
( apply(X0,X3,X4)
& member(X4,X2) ) ) ) ),
inference(flattening,[],[f42]) ).
fof(f44,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,[],[f38]) ).
fof(f45,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,[],[f44]) ).
fof(f48,plain,
? [X0,X1,X2,X3] :
( ! [X4,X5] :
( ~ member(X5,X1)
| ~ member(X4,X1)
| ( ( ~ apply(X3,X4,X5)
| ? [X6] :
( apply(X0,X5,X6)
& apply(X0,X4,X6)
& member(X6,X2) ) )
& ( ! [X6] :
( ~ apply(X0,X5,X6)
| ~ apply(X0,X4,X6)
| ~ member(X6,X2) )
| apply(X3,X4,X5) ) ) )
& maps(X0,X1,X2)
& ~ equivalence(X3,X1) ),
inference(nnf_transformation,[],[f41]) ).
fof(f49,plain,
? [X0,X1,X2,X3] :
( ! [X4,X5] :
( ~ member(X5,X1)
| ~ member(X4,X1)
| ( ( ~ apply(X3,X4,X5)
| ? [X7] :
( apply(X0,X5,X7)
& apply(X0,X4,X7)
& member(X7,X2) ) )
& ( ! [X6] :
( ~ apply(X0,X5,X6)
| ~ apply(X0,X4,X6)
| ~ member(X6,X2) )
| apply(X3,X4,X5) ) ) )
& maps(X0,X1,X2)
& ~ equivalence(X3,X1) ),
inference(rectify,[],[f48]) ).
fof(f50,plain,
( ! [X4,X5] :
( ~ member(X5,sK2)
| ~ member(X4,sK2)
| ( ( ~ apply(sK4,X4,X5)
| ( apply(sK1,X5,sK5(X4,X5))
& apply(sK1,X4,sK5(X4,X5))
& member(sK5(X4,X5),sK3) ) )
& ( ! [X6] :
( ~ apply(sK1,X5,X6)
| ~ apply(sK1,X4,X6)
| ~ member(X6,sK3) )
| apply(sK4,X4,X5) ) ) )
& maps(sK1,sK2,sK3)
& ~ equivalence(sK4,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X7,sK5(X4,X5))],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ~ maps(X0,X1,X2)
| ( ! [X5,X6,X7] :
( ~ member(X7,X2)
| ~ member(X6,X2)
| ~ member(X5,X1)
| ~ apply(X0,X5,X7)
| ~ apply(X0,X5,X6)
| X6 = X7 )
& ! [X3] :
( ~ member(X3,X1)
| ( apply(X0,X3,sK6(X0,X2,X3))
& member(sK6(X0,X2,X3),X2) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X4,sK6(X0,X2,X3))],[f43]) ).
fof(f55,plain,
! [X0,X1] :
( sP0(X1,X0)
| ( member(sK12(X0,X1),X0)
& member(sK11(X0,X1),X0)
& apply(X1,sK11(X0,X1),sK12(X0,X1))
& ~ apply(X1,sK12(X0,X1),sK11(X0,X1)) )
| ( member(sK10(X0,X1),X0)
& ~ apply(X1,sK10(X0,X1),sK10(X0,X1)) )
| equivalence(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X2,sK10(X0,X1)),skolemize(X3,sK11(X0,X1)),skolemize(X4,sK12(X0,X1))],[f47]) ).
fof(f56,plain,
! [X4,X5] :
( ~ member(X5,sK2)
| ~ member(X4,sK2)
| ~ apply(sK4,X4,X5)
| apply(sK1,X5,sK5(X4,X5)) ),
inference(cnf_transformation,[],[f50]) ).
fof(f57,plain,
! [X4,X5] :
( ~ member(X5,sK2)
| ~ member(X4,sK2)
| ~ apply(sK4,X4,X5)
| apply(sK1,X4,sK5(X4,X5)) ),
inference(cnf_transformation,[],[f50]) ).
fof(f58,plain,
! [X4,X5] :
( ~ member(X5,sK2)
| ~ member(X4,sK2)
| ~ apply(sK4,X4,X5)
| member(sK5(X4,X5),sK3) ),
inference(cnf_transformation,[],[f50]) ).
fof(f59,plain,
! [X6,X4,X5] :
( ~ member(X5,sK2)
| ~ member(X4,sK2)
| ~ apply(sK1,X5,X6)
| ~ apply(sK1,X4,X6)
| ~ member(X6,sK3)
| apply(sK4,X4,X5) ),
inference(cnf_transformation,[],[f50]) ).
fof(f60,plain,
maps(sK1,sK2,sK3),
inference(cnf_transformation,[],[f50]) ).
fof(f61,plain,
~ equivalence(sK4,sK2),
inference(cnf_transformation,[],[f50]) ).
fof(f62,plain,
! [X2,X0,X1,X6,X7,X5] :
( ~ maps(X0,X1,X2)
| ~ member(X7,X2)
| ~ member(X6,X2)
| ~ member(X5,X1)
| ~ apply(X0,X5,X7)
| ~ apply(X0,X5,X6)
| X6 = X7 ),
inference(cnf_transformation,[],[f51]) ).
fof(f63,plain,
! [X2,X3,X0,X1] :
( ~ maps(X0,X1,X2)
| ~ member(X3,X1)
| apply(X0,X3,sK6(X0,X2,X3)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f64,plain,
! [X2,X3,X0,X1] :
( ~ maps(X0,X1,X2)
| ~ member(X3,X1)
| member(sK6(X0,X2,X3),X2) ),
inference(cnf_transformation,[],[f51]) ).
fof(f71,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK12(X0,X1),X0)
| member(sK10(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f72,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK11(X0,X1),X0)
| member(sK10(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f73,plain,
! [X0,X1] :
( sP0(X1,X0)
| apply(X1,sK11(X0,X1),sK12(X0,X1))
| member(sK10(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f74,plain,
! [X0,X1] :
( sP0(X1,X0)
| ~ apply(X1,sK12(X0,X1),sK11(X0,X1))
| member(sK10(X0,X1),X0)
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f75,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK12(X0,X1),X0)
| ~ apply(X1,sK10(X0,X1),sK10(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f76,plain,
! [X0,X1] :
( sP0(X1,X0)
| member(sK11(X0,X1),X0)
| ~ apply(X1,sK10(X0,X1),sK10(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f77,plain,
! [X0,X1] :
( sP0(X1,X0)
| apply(X1,sK11(X0,X1),sK12(X0,X1))
| ~ apply(X1,sK10(X0,X1),sK10(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f78,plain,
! [X0,X1] :
( sP0(X1,X0)
| ~ apply(X1,sK12(X0,X1),sK11(X0,X1))
| ~ apply(X1,sK10(X0,X1),sK10(X0,X1))
| equivalence(X1,X0) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_49,negated_conjecture,
~ equivalence(sK4,sK2),
inference(cnf_transformation,[],[f61]) ).
tcf(c_50,negated_conjecture,
maps(sK1,sK2,sK3),
inference(cnf_transformation,[],[f60]) ).
tcf(c_51,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK4,X0,X2)
| ~ member(X2,sK2)
| ~ member(X1,sK3)
| ~ member(X0,sK2)
| ~ apply(sK1,X2,X1)
| ~ apply(sK1,X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_52,negated_conjecture,
! [X0: $i,X1: $i] :
( member(sK5(X0,X1),sK3)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_53,negated_conjecture,
! [X0: $i,X1: $i] :
( apply(sK1,X0,sK5(X0,X1))
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_54,negated_conjecture,
! [X0: $i,X1: $i] :
( apply(sK1,X1,sK5(X0,X1))
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(sK6(X0,X2,X3),X2)
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( apply(X0,X3,sK6(X0,X2,X3))
| ~ member(X3,X1)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X4 = X5 )
| ~ member(X5,X2)
| ~ member(X4,X2)
| ~ member(X3,X1)
| ~ apply(X0,X3,X5)
| ~ apply(X0,X3,X4)
| ~ maps(X0,X1,X2) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| ~ apply(X0,sK12(X1,X0),sK11(X1,X0))
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0)) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| apply(X0,sK11(X1,X0),sK12(X1,X0))
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0)) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK11(X1,X0),X1)
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0)) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK12(X1,X0),X1)
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0)) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK10(X1,X0),X1)
| ~ apply(X0,sK12(X1,X0),sK11(X1,X0)) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| equivalence(X0,X1)
| member(sK10(X1,X0),X1)
| apply(X0,sK11(X1,X0),sK12(X1,X0)) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0)
| equivalence(X1,X0)
| member(sK11(X0,X1),X0)
| member(sK10(X0,X1),X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( sP0(X1,X0)
| equivalence(X1,X0)
| member(sK12(X0,X1),X0)
| member(sK10(X0,X1),X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_401,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X4 = X5 )
| ~ member(X5,X2)
| ~ member(X4,X2)
| ~ member(X3,X0)
| ~ apply(X1,X3,X5)
| ~ apply(X1,X3,X4)
| ( X2 != sK3 )
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_57]) ).
tcf(c_402,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ member(X2,sK3)
| ~ member(X1,sK3)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,X2)
| ~ apply(sK1,X0,X1) ),
inference(unflattening,[status(thm)],[c_401]) ).
tcf(c_422,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( apply(X1,X3,sK6(X1,X2,X3))
| ~ member(X3,X0)
| ( X2 != sK3 )
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_56]) ).
tcf(c_423,plain,
! [X0: $i] :
( apply(sK1,X0,sK6(sK1,sK3,X0))
| ~ member(X0,sK2) ),
inference(unflattening,[status(thm)],[c_422]) ).
tcf(c_431,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( member(sK6(X1,X2,X3),X2)
| ~ member(X3,X0)
| ( X2 != sK3 )
| ( X1 != sK1 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_55]) ).
tcf(c_432,plain,
! [X0: $i] :
( member(sK6(sK1,sK3,X0),sK3)
| ~ member(X0,sK2) ),
inference(unflattening,[status(thm)],[c_431]) ).
tcf(c_450,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK10(X1,X0),X1)
| apply(X0,sK11(X1,X0),sK12(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_69]) ).
tcf(c_451,plain,
( sP0(sK4,sK2)
| member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_450]) ).
tcf(c_461,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK10(X1,X0),X1)
| ~ apply(X0,sK12(X1,X0),sK11(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_68]) ).
tcf(c_462,plain,
( sP0(sK4,sK2)
| member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_461]) ).
tcf(c_472,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK12(X1,X0),X1)
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_67]) ).
tcf(c_473,plain,
( sP0(sK4,sK2)
| member(sK12(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_472]) ).
tcf(c_483,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK11(X1,X0),X1)
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_66]) ).
tcf(c_484,plain,
( sP0(sK4,sK2)
| member(sK11(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_483]) ).
tcf(c_494,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| apply(X0,sK11(X1,X0),sK12(X1,X0))
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_65]) ).
tcf(c_495,plain,
( sP0(sK4,sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_494]) ).
tcf(c_505,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| ~ apply(X0,sK12(X1,X0),sK11(X1,X0))
| ~ apply(X0,sK10(X1,X0),sK10(X1,X0))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_64]) ).
tcf(c_506,plain,
( sP0(sK4,sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_505]) ).
tcf(c_516,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK12(X1,X0),X1)
| member(sK10(X1,X0),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_71]) ).
tcf(c_517,plain,
( sP0(sK4,sK2)
| member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2) ),
inference(unflattening,[status(thm)],[c_516]) ).
tcf(c_527,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| member(sK11(X1,X0),X1)
| member(sK10(X1,X0),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_70]) ).
tcf(c_528,plain,
( sP0(sK4,sK2)
| member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2) ),
inference(unflattening,[status(thm)],[c_527]) ).
tcf(c_2114,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK4,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X1,X2)
| ~ member(sK5(X1,X2),sK3)
| ~ apply(sK1,X0,sK5(X1,X2)) ),
inference(superposition,[status(thm)],[c_54,c_51]) ).
tcf(c_2137,plain,
! [X0: $i,X1: $i] :
( apply(sK4,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ member(sK6(sK1,sK3,X1),sK3)
| ~ apply(sK1,X0,sK6(sK1,sK3,X1)) ),
inference(superposition,[status(thm)],[c_423,c_51]) ).
tcf(c_2156,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(X0,X1) = X2 )
| ~ member(X2,sK3)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,X2)
| ~ apply(sK4,X0,X1)
| ~ member(sK5(X0,X1),sK3) ),
inference(superposition,[status(thm)],[c_53,c_402]) ).
tcf(c_2157,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(X0,X1) = X2 )
| ~ member(X2,sK3)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK1,X1,X2)
| ~ apply(sK4,X0,X1)
| ~ member(sK5(X0,X1),sK3) ),
inference(superposition,[status(thm)],[c_54,c_402]) ).
tcf(c_2158,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X0) = X1 )
| ~ member(X1,sK3)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,X1)
| ~ member(sK6(sK1,sK3,X0),sK3) ),
inference(superposition,[status(thm)],[c_423,c_402]) ).
tcf(c_2185,plain,
! [X0: $i,X1: $i] :
( apply(sK4,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,sK6(sK1,sK3,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2137,c_432]) ).
tcf(c_2198,plain,
! [X0: $i] :
( apply(sK4,X0,X0)
| ~ member(X0,sK2) ),
inference(superposition,[status(thm)],[c_423,c_2185]) ).
tcf(c_2295,plain,
! [X0: $i,X1: $i,X2: $i] :
( apply(sK4,X2,X0)
| ~ member(X2,sK2)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X1,X2)
| ~ apply(sK1,X0,sK5(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2114,c_52]) ).
tcf(c_2314,plain,
! [X0: $i,X1: $i] :
( apply(sK4,X1,X0)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(superposition,[status(thm)],[c_53,c_2295]) ).
tcf(c_2339,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(X0,X1) = X2 )
| ~ member(X2,sK3)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,X2)
| ~ apply(sK4,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2156,c_52,c_2156]) ).
tcf(c_2356,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X0) = sK5(X0,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1)
| ~ member(sK6(sK1,sK3,X0),sK3) ),
inference(superposition,[status(thm)],[c_423,c_2339]) ).
tcf(c_2378,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK5(X0,X1) = X2 )
| ~ member(X2,sK3)
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK1,X1,X2)
| ~ apply(sK4,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2157,c_52,c_2157]) ).
tcf(c_2833,plain,
( apply(sK1,sK10(sK2,sK4),sK6(sK1,sK3,sK10(sK2,sK4)))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_2834,plain,
( member(sK6(sK1,sK3,sK10(sK2,sK4)),sK3)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_2835,plain,
! [X0: $i,X1: $i] :
( apply(sK4,sK10(sK2,sK4),X1)
| ~ member(X1,sK2)
| ~ member(X0,sK3)
| ~ apply(sK1,X1,X0)
| ~ member(sK10(sK2,sK4),sK2)
| ~ apply(sK1,sK10(sK2,sK4),X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_3521,plain,
! [X0: $i] :
( apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ member(X0,sK3)
| ~ member(sK10(sK2,sK4),sK2)
| ~ apply(sK1,sK10(sK2,sK4),X0) ),
inference(instantiation,[status(thm)],[c_2835]) ).
tcf(c_3828,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X0) = X1 )
| ~ member(X1,sK3)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2158,c_432,c_2158]) ).
tcf(c_3839,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X0) = sK5(X0,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1)
| ~ member(sK5(X0,X1),sK3) ),
inference(superposition,[status(thm)],[c_53,c_3828]) ).
tcf(c_3840,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X1) = sK5(X0,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1)
| ~ member(sK5(X0,X1),sK3) ),
inference(superposition,[status(thm)],[c_54,c_3828]) ).
tcf(c_3853,plain,
( apply(sK1,sK9(sK4,sK2),sK6(sK1,sK3,sK9(sK4,sK2)))
| ~ member(sK9(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_3854,plain,
( member(sK6(sK1,sK3,sK9(sK4,sK2)),sK3)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_3865,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X0) = sK5(X0,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3839,c_432,c_2356]) ).
tcf(c_3882,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,X0) = sK5(X0,X0) )
| ~ member(X0,sK2) ),
inference(superposition,[status(thm)],[c_2198,c_3865]) ).
tcf(c_3911,plain,
! [X0: $i,X1: $i] :
( ( sK6(sK1,sK3,X1) = sK5(X0,X1) )
| ~ member(X1,sK2)
| ~ member(X0,sK2)
| ~ apply(sK4,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3840,c_52,c_3840]) ).
tcf(c_3974,plain,
( apply(sK1,sK8(sK4,sK2),sK6(sK1,sK3,sK8(sK4,sK2)))
| ~ member(sK8(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_3975,plain,
( member(sK6(sK1,sK3,sK8(sK4,sK2)),sK3)
| ~ member(sK8(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_4063,plain,
( apply(sK1,sK7(sK4,sK2),sK6(sK1,sK3,sK7(sK4,sK2)))
| ~ member(sK7(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_423]) ).
tcf(c_4064,plain,
( member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(instantiation,[status(thm)],[c_432]) ).
tcf(c_7522,plain,
( apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ member(sK10(sK2,sK4),sK2)
| ~ member(sK6(sK1,sK3,sK10(sK2,sK4)),sK3)
| ~ apply(sK1,sK10(sK2,sK4),sK6(sK1,sK3,sK10(sK2,sK4))) ),
inference(instantiation,[status(thm)],[c_3521]) ).
fof(f46,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(f47,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,[],[f45,f46]) ).
fof(f52,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,[],[f46]) ).
fof(f53,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,[],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( member(sK9(X0,X1),X1)
& member(sK8(X0,X1),X1)
& member(sK7(X0,X1),X1)
& apply(X0,sK8(X0,X1),sK9(X0,X1))
& apply(X0,sK7(X0,X1),sK8(X0,X1))
& ~ apply(X0,sK7(X0,X1),sK9(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X2,sK7(X0,X1)),skolemize(X3,sK8(X0,X1)),skolemize(X4,sK9(X0,X1))],[f53]) ).
fof(f65,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK9(X0,X1),X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f66,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK8(X0,X1),X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f67,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| member(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f68,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK8(X0,X1),sK9(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f69,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK7(X0,X1),sK8(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f70,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1)) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( member(sK9(X0,X1),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_528]) ).
tcf(c_563,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_562]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_517]) ).
tcf(c_574,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_573]) ).
tcf(c_584,plain,
! [X0: $i,X1: $i] :
( member(sK9(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_506]) ).
tcf(c_585,plain,
( member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_584]) ).
tcf(c_595,plain,
! [X0: $i,X1: $i] :
( member(sK9(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_495]) ).
tcf(c_596,plain,
( member(sK9(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_595]) ).
tcf(c_606,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_484]) ).
tcf(c_607,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_606]) ).
tcf(c_617,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_473]) ).
tcf(c_618,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_617]) ).
tcf(c_628,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_462]) ).
tcf(c_629,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_628]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK9(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_451]) ).
tcf(c_640,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_639]) ).
tcf(c_650,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_528]) ).
tcf(c_651,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_650]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_517]) ).
tcf(c_662,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_661]) ).
tcf(c_672,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_506]) ).
tcf(c_673,plain,
( member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_672]) ).
tcf(c_683,plain,
! [X0: $i,X1: $i] :
( member(sK8(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_495]) ).
tcf(c_684,plain,
( member(sK8(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_683]) ).
tcf(c_694,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_484]) ).
tcf(c_695,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_694]) ).
tcf(c_705,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_473]) ).
tcf(c_706,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_705]) ).
tcf(c_716,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_462]) ).
tcf(c_717,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_716]) ).
tcf(c_727,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK8(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_451]) ).
tcf(c_728,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_727]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_528]) ).
tcf(c_739,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_738]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_517]) ).
tcf(c_750,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2) ),
inference(unflattening,[status(thm)],[c_749]) ).
tcf(c_760,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_506]) ).
tcf(c_761,plain,
( member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_760]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] :
( member(sK7(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_495]) ).
tcf(c_772,plain,
( member(sK7(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_771]) ).
tcf(c_782,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_484]) ).
tcf(c_783,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_782]) ).
tcf(c_793,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_473]) ).
tcf(c_794,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_793]) ).
tcf(c_804,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_462]) ).
tcf(c_805,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_804]) ).
tcf(c_815,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| member(sK7(X0,X1),X1)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_451]) ).
tcf(c_816,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_815]) ).
tcf(c_826,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_528]) ).
tcf(c_827,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_826]) ).
tcf(c_837,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_517]) ).
tcf(c_838,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_837]) ).
tcf(c_848,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_506]) ).
tcf(c_849,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_848]) ).
tcf(c_859,plain,
! [X0: $i,X1: $i] :
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_495]) ).
tcf(c_860,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_859]) ).
tcf(c_870,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_484]) ).
tcf(c_871,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_870]) ).
tcf(c_881,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_473]) ).
tcf(c_882,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_881]) ).
tcf(c_892,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_462]) ).
tcf(c_893,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_892]) ).
tcf(c_903,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(X0,sK8(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_451]) ).
tcf(c_904,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_903]) ).
tcf(c_914,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_528]) ).
tcf(c_915,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_914]) ).
tcf(c_925,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_517]) ).
tcf(c_926,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_925]) ).
tcf(c_936,plain,
! [X0: $i,X1: $i] :
( apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_506]) ).
tcf(c_937,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_936]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i] :
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_495]) ).
tcf(c_948,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_947]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_484]) ).
tcf(c_959,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_958]) ).
tcf(c_969,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_473]) ).
tcf(c_970,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_969]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_462]) ).
tcf(c_981,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(unflattening,[status(thm)],[c_980]) ).
tcf(c_991,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(X0,sK7(X0,X1),sK8(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_451]) ).
tcf(c_992,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_991]) ).
tcf(c_1002,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_528]) ).
tcf(c_1003,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1002]) ).
tcf(c_1013,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_517]) ).
tcf(c_1014,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1013]) ).
tcf(c_1024,plain,
! [X0: $i,X1: $i] :
( ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_506]) ).
tcf(c_1025,plain,
( ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1024]) ).
tcf(c_1035,plain,
! [X0: $i,X1: $i] :
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_495]) ).
tcf(c_1036,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1035]) ).
tcf(c_1046,plain,
! [X0: $i,X1: $i] :
( member(sK11(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_484]) ).
tcf(c_1047,plain,
( member(sK11(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1046]) ).
tcf(c_1057,plain,
! [X0: $i,X1: $i] :
( member(sK12(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_473]) ).
tcf(c_1058,plain,
( member(sK12(sK2,sK4),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1057]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_462]) ).
tcf(c_1069,plain,
( member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1068]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i] :
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(X0,sK7(X0,X1),sK9(X0,X1))
| ( X1 != sK2 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_451]) ).
tcf(c_1080,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(unflattening,[status(thm)],[c_1079]) ).
tcf(c_2332,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_640,c_2314]) ).
tcf(c_2449,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_860]) ).
tcf(c_2460,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_728,c_2314]) ).
tcf(c_2481,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_816,c_2314]) ).
tcf(c_2585,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_607]) ).
tcf(c_2589,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2585,c_563,c_2585]) ).
tcf(c_2849,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_618]) ).
tcf(c_2853,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_629,c_563,c_574,c_629,c_2332,c_2585]) ).
tcf(c_2865,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_695]) ).
tcf(c_2875,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_706]) ).
tcf(c_2879,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_717,c_651,c_662,c_717,c_2460]) ).
tcf(c_2897,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_783]) ).
tcf(c_2907,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_794]) ).
tcf(c_2911,plain,
( member(sK10(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_805,c_739,c_750,c_805,c_2481]) ).
tcf(c_2923,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK9(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2849,c_2849,c_2853]) ).
tcf(c_2929,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2865,c_2865,c_2879]) ).
tcf(c_2935,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK8(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2875,c_651,c_662,c_717,c_2460,c_2875]) ).
tcf(c_2941,plain,
( member(sK11(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2897,c_2897,c_2911]) ).
tcf(c_2953,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_904,c_904,c_2449]) ).
tcf(c_2954,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(renaming,[status(thm)],[c_2953]) ).
tcf(c_3325,plain,
( member(sK9(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_596]) ).
tcf(c_3335,plain,
( member(sK8(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_684]) ).
tcf(c_3347,plain,
( member(sK7(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_772]) ).
tcf(c_3359,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_948]) ).
tcf(c_3371,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_871]) ).
tcf(c_3383,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_882]) ).
tcf(c_3401,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_959]) ).
tcf(c_3405,plain,
( member(sK12(sK2,sK4),sK2)
| member(sK7(sK4,sK2),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_2907,c_739,c_750,c_805,c_2481,c_2907]) ).
tcf(c_3413,plain,
( member(sK9(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_3325,c_563,c_574,c_629,c_2332,c_2585,c_3325]) ).
tcf(c_3425,plain,
( member(sK9(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_3413,c_2314]) ).
tcf(c_3466,plain,
( member(sK8(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_3335,c_651,c_662,c_717,c_2460,c_3335]) ).
tcf(c_3478,plain,
( member(sK8(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_3466,c_2314]) ).
tcf(c_3523,plain,
( member(sK7(sK4,sK2),sK2)
| apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_3347,c_739,c_750,c_805,c_2481,c_3347]) ).
tcf(c_3535,plain,
( member(sK7(sK4,sK2),sK2)
| apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_3523,c_2314]) ).
tcf(c_3586,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_970]) ).
tcf(c_3602,plain,
( member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_585,c_585,c_2589,c_2923,c_3425]) ).
tcf(c_3608,plain,
( member(sK9(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_3602]) ).
tcf(c_3611,plain,
( member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_673,c_673,c_2929,c_2935,c_3478]) ).
tcf(c_3617,plain,
( member(sK8(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_3611]) ).
tcf(c_3620,plain,
( member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_761,c_761,c_2941,c_3405,c_3535]) ).
tcf(c_3626,plain,
( member(sK7(sK4,sK2),sK2)
| ~ member(sK10(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_2198,c_3620]) ).
tcf(c_3635,plain,
( member(sK11(sK2,sK4),sK2)
| ~ member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_2198,c_1047]) ).
tcf(c_3645,plain,
( member(sK12(sK2,sK4),sK2)
| ~ member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_2198,c_1058]) ).
tcf(c_3673,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ member(sK10(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_2198,c_1036]) ).
tcf(c_3677,plain,
member(sK9(sK4,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_3608,c_2853,c_3608]) ).
tcf(c_3679,plain,
member(sK8(sK4,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_3617,c_2879,c_3617]) ).
tcf(c_3681,plain,
member(sK7(sK4,sK2),sK2),
inference(global_subsumption_just,[status(thm)],[c_3626,c_2911,c_3626]) ).
tcf(c_3683,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3371,c_827,c_3371]) ).
tcf(c_3770,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3383,c_838,c_3383]) ).
tcf(c_3876,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_3770,c_3865]) ).
tcf(c_3877,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_3683,c_3865]) ).
tcf(c_3878,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_2954,c_3865]) ).
tcf(c_3889,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3877,c_3679,c_3677]) ).
tcf(c_3892,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3876,c_3679,c_3677]) ).
tcf(c_3895,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3878,c_3679,c_3677]) ).
tcf(c_3921,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_3770,c_3911]) ).
tcf(c_3922,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_3683,c_3911]) ).
tcf(c_3923,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_2954,c_3911]) ).
tcf(c_3932,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3922,c_3679,c_3677]) ).
tcf(c_3935,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3921,c_3679,c_3677]) ).
tcf(c_3938,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3923,c_3679,c_3677]) ).
tcf(c_3990,plain,
sK5(sK9(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)),
inference(superposition,[status(thm)],[c_3677,c_3882]) ).
tcf(c_3991,plain,
sK5(sK8(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)),
inference(superposition,[status(thm)],[c_3679,c_3882]) ).
tcf(c_3992,plain,
sK5(sK7(sK4,sK2),sK7(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)),
inference(superposition,[status(thm)],[c_3681,c_3882]) ).
tcf(c_4162,plain,
( member(sK11(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3401,c_915,c_3401]) ).
tcf(c_4168,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_4162,c_3911]) ).
tcf(c_4169,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_4162,c_3865]) ).
tcf(c_4180,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4169,c_3679,c_3681]) ).
tcf(c_4183,plain,
( member(sK11(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4168,c_3679,c_3681]) ).
tcf(c_4302,plain,
( member(sK12(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3586,c_926,c_3586]) ).
tcf(c_4308,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_4302,c_3911]) ).
tcf(c_4309,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_4302,c_3865]) ).
tcf(c_4320,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4309,c_3679,c_3681]) ).
tcf(c_4323,plain,
( member(sK12(sK2,sK4),sK2)
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4308,c_3679,c_3681]) ).
tcf(c_4413,plain,
( apply(sK1,sK9(sK4,sK2),sK6(sK1,sK3,sK9(sK4,sK2)))
| ~ member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK9(sK4,sK2),sK9(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3990,c_54]) ).
tcf(c_4415,plain,
( member(sK6(sK1,sK3,sK9(sK4,sK2)),sK3)
| ~ member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,sK9(sK4,sK2),sK9(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3990,c_52]) ).
tcf(c_4418,plain,
( member(sK6(sK1,sK3,sK9(sK4,sK2)),sK3)
| ~ apply(sK4,sK9(sK4,sK2),sK9(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4415,c_3677]) ).
tcf(c_4421,plain,
( apply(sK1,sK9(sK4,sK2),sK6(sK1,sK3,sK9(sK4,sK2)))
| ~ apply(sK4,sK9(sK4,sK2),sK9(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4413,c_3677]) ).
tcf(c_4434,plain,
( apply(sK1,sK8(sK4,sK2),sK6(sK1,sK3,sK8(sK4,sK2)))
| ~ member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK8(sK4,sK2),sK8(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3991,c_54]) ).
tcf(c_4436,plain,
( member(sK6(sK1,sK3,sK8(sK4,sK2)),sK3)
| ~ member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK8(sK4,sK2),sK8(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3991,c_52]) ).
tcf(c_4439,plain,
( member(sK6(sK1,sK3,sK8(sK4,sK2)),sK3)
| ~ apply(sK4,sK8(sK4,sK2),sK8(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4436,c_3679]) ).
tcf(c_4442,plain,
( apply(sK1,sK8(sK4,sK2),sK6(sK1,sK3,sK8(sK4,sK2)))
| ~ apply(sK4,sK8(sK4,sK2),sK8(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4434,c_3679]) ).
tcf(c_4495,plain,
( apply(sK1,sK7(sK4,sK2),sK6(sK1,sK3,sK7(sK4,sK2)))
| ~ member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK7(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3992,c_54]) ).
tcf(c_4497,plain,
( member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3)
| ~ member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK7(sK4,sK2)) ),
inference(superposition,[status(thm)],[c_3992,c_52]) ).
tcf(c_4500,plain,
( member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3)
| ~ apply(sK4,sK7(sK4,sK2),sK7(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4497,c_3681]) ).
tcf(c_4503,plain,
( apply(sK1,sK7(sK4,sK2),sK6(sK1,sK3,sK7(sK4,sK2)))
| ~ apply(sK4,sK7(sK4,sK2),sK7(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4495,c_3681]) ).
tcf(c_4516,plain,
member(sK6(sK1,sK3,sK9(sK4,sK2)),sK3),
inference(global_subsumption_just,[status(thm)],[c_4418,c_2853,c_3608,c_3854]) ).
tcf(c_4526,plain,
member(sK6(sK1,sK3,sK8(sK4,sK2)),sK3),
inference(global_subsumption_just,[status(thm)],[c_4439,c_2879,c_3617,c_3975]) ).
tcf(c_4538,plain,
member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3),
inference(global_subsumption_just,[status(thm)],[c_4500,c_2911,c_3626,c_4064]) ).
tcf(c_4540,plain,
apply(sK1,sK9(sK4,sK2),sK6(sK1,sK3,sK9(sK4,sK2))),
inference(global_subsumption_just,[status(thm)],[c_4421,c_3677,c_3853]) ).
tcf(c_4544,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK9(sK4,sK2)) = sK5(X0,sK9(sK4,sK2)) )
| ~ member(X0,sK2)
| ~ member(sK9(sK4,sK2),sK2)
| ~ apply(sK4,X0,sK9(sK4,sK2))
| ~ member(sK6(sK1,sK3,sK9(sK4,sK2)),sK3) ),
inference(superposition,[status(thm)],[c_4540,c_2378]) ).
tcf(c_4557,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK9(sK4,sK2)) = sK5(X0,sK9(sK4,sK2)) )
| ~ member(X0,sK2)
| ~ apply(sK4,X0,sK9(sK4,sK2)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4544,c_3677,c_4516]) ).
tcf(c_4608,plain,
apply(sK1,sK8(sK4,sK2),sK6(sK1,sK3,sK8(sK4,sK2))),
inference(global_subsumption_just,[status(thm)],[c_4442,c_2879,c_3617,c_3974]) ).
tcf(c_4610,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK8(sK4,sK2)) = sK5(sK8(sK4,sK2),X0) )
| ~ member(X0,sK2)
| ~ member(sK8(sK4,sK2),sK2)
| ~ apply(sK4,sK8(sK4,sK2),X0)
| ~ member(sK6(sK1,sK3,sK8(sK4,sK2)),sK3) ),
inference(superposition,[status(thm)],[c_4608,c_2339]) ).
tcf(c_4629,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK8(sK4,sK2)) = sK5(sK8(sK4,sK2),X0) )
| ~ member(X0,sK2)
| ~ apply(sK4,sK8(sK4,sK2),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4610,c_3679,c_4526]) ).
tcf(c_4642,plain,
apply(sK1,sK7(sK4,sK2),sK6(sK1,sK3,sK7(sK4,sK2))),
inference(global_subsumption_just,[status(thm)],[c_4503,c_2911,c_3626,c_4063]) ).
tcf(c_4644,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK7(sK4,sK2)) = sK5(sK7(sK4,sK2),X0) )
| ~ member(X0,sK2)
| ~ member(sK7(sK4,sK2),sK2)
| ~ apply(sK4,sK7(sK4,sK2),X0)
| ~ member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3) ),
inference(superposition,[status(thm)],[c_4642,c_2339]) ).
tcf(c_4648,plain,
! [X0: $i] :
( apply(sK4,sK7(sK4,sK2),X0)
| ~ member(X0,sK2)
| ~ member(sK7(sK4,sK2),sK2)
| ~ member(sK6(sK1,sK3,sK7(sK4,sK2)),sK3)
| ~ apply(sK1,X0,sK6(sK1,sK3,sK7(sK4,sK2))) ),
inference(superposition,[status(thm)],[c_4642,c_51]) ).
tcf(c_4651,plain,
! [X0: $i] :
( apply(sK4,sK7(sK4,sK2),X0)
| ~ member(X0,sK2)
| ~ apply(sK1,X0,sK6(sK1,sK3,sK7(sK4,sK2))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4648,c_3681,c_4538]) ).
tcf(c_4663,plain,
! [X0: $i] :
( ( sK6(sK1,sK3,sK7(sK4,sK2)) = sK5(sK7(sK4,sK2),X0) )
| ~ member(X0,sK2)
| ~ apply(sK4,sK7(sK4,sK2),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4644,c_3681,c_4538]) ).
tcf(c_4752,plain,
( member(sK11(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3635,c_1003,c_3635]) ).
tcf(c_4758,plain,
( member(sK12(sK2,sK4),sK2)
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3645,c_1014,c_3645]) ).
tcf(c_5118,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3359,c_992,c_3359]) ).
tcf(c_5124,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5118,c_3911]) ).
tcf(c_5125,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_5118,c_3865]) ).
tcf(c_5136,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5125,c_3679,c_3681]) ).
tcf(c_5139,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5124,c_3679,c_3681]) ).
tcf(c_5362,plain,
( apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4))
| ~ apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_3673,c_1080,c_3673]) ).
tcf(c_5380,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_3895,c_2314]) ).
tcf(c_5463,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_3938,c_2314]) ).
tcf(c_5694,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_5380,c_3892,c_3889,c_5380]) ).
tcf(c_5712,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(superposition,[status(thm)],[c_5694,c_893]) ).
tcf(c_5810,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_5463,c_3935,c_3932,c_5463]) ).
tcf(c_5828,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(superposition,[status(thm)],[c_5810,c_893]) ).
tcf(c_6429,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_5136,c_2314]) ).
tcf(c_6495,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_5139,c_2314]) ).
tcf(c_6785,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6429,c_4180,c_4320,c_6429]) ).
tcf(c_6802,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(superposition,[status(thm)],[c_6785,c_981]) ).
tcf(c_6804,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(superposition,[status(thm)],[c_6785,c_937]) ).
tcf(c_6908,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_6495,c_4183,c_4323,c_6495]) ).
tcf(c_6925,plain,
( member(sK10(sK2,sK4),sK2)
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(superposition,[status(thm)],[c_6908,c_981]) ).
tcf(c_6927,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ apply(sK4,sK10(sK2,sK4),sK10(sK2,sK4)) ),
inference(superposition,[status(thm)],[c_6908,c_937]) ).
tcf(c_8959,plain,
( ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_893,c_849,c_893,c_2834,c_2833,c_7522]) ).
tcf(c_8960,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ~ apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)) ),
inference(renaming,[status(thm)],[c_8959]) ).
tcf(c_9006,plain,
( ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_5712,c_827,c_838,c_849,c_893,c_2834,c_2833,c_3371,c_3383,c_5380,c_7522]) ).
tcf(c_9007,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(renaming,[status(thm)],[c_9006]) ).
tcf(c_9021,plain,
( ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_9007,c_4629]) ).
tcf(c_9024,plain,
sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_9021,c_3677]) ).
tcf(c_9157,plain,
( ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_5828,c_3683,c_3770,c_5463,c_8960]) ).
tcf(c_9158,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(renaming,[status(thm)],[c_9157]) ).
tcf(c_9159,plain,
( apply(sK4,sK8(sK4,sK2),sK9(sK4,sK2))
| ( sK6(sK1,sK3,sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(light_normalisation,[status(thm)],[c_9158,c_9024]) ).
tcf(c_9176,plain,
( ( sK6(sK1,sK3,sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ( sK5(sK8(sK4,sK2),sK9(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_9159,c_4557]) ).
tcf(c_9180,plain,
( ( sK6(sK1,sK3,sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2) ),
inference(light_normalisation,[status(thm)],[c_9176,c_9024]) ).
tcf(c_9181,plain,
sK6(sK1,sK3,sK9(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_9180,c_3679]) ).
tcf(c_10131,plain,
( ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_6802,c_2834,c_2833,c_6802,c_6804,c_7522]) ).
tcf(c_10132,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) ) ),
inference(renaming,[status(thm)],[c_10131]) ).
tcf(c_10146,plain,
( ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_10132,c_4663]) ).
tcf(c_10147,plain,
sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK7(sK4,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_10146,c_3679]) ).
tcf(c_10153,plain,
( ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_6925,c_2834,c_2833,c_6925,c_6927,c_7522]) ).
tcf(c_10154,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) ) ),
inference(renaming,[status(thm)],[c_10153]) ).
tcf(c_10155,plain,
( apply(sK4,sK7(sK4,sK2),sK8(sK4,sK2))
| ( sK6(sK1,sK3,sK7(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) ) ),
inference(light_normalisation,[status(thm)],[c_10154,c_9181,c_10147]) ).
tcf(c_10162,plain,
( ( sK6(sK1,sK3,sK7(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ( sK5(sK7(sK4,sK2),sK8(sK4,sK2)) = sK6(sK1,sK3,sK8(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_10155,c_3911]) ).
tcf(c_10175,plain,
( ( sK6(sK1,sK3,sK7(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)) )
| ~ member(sK8(sK4,sK2),sK2)
| ~ member(sK7(sK4,sK2),sK2) ),
inference(light_normalisation,[status(thm)],[c_10162,c_9181,c_10147]) ).
tcf(c_10176,plain,
sK6(sK1,sK3,sK7(sK4,sK2)) = sK6(sK1,sK3,sK9(sK4,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_10175,c_3679,c_3681]) ).
tcf(c_10195,plain,
apply(sK1,sK9(sK4,sK2),sK6(sK1,sK3,sK7(sK4,sK2))),
inference(demodulation,[status(thm)],[c_4540,c_10176]) ).
tcf(c_10309,plain,
( apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2))
| ~ member(sK9(sK4,sK2),sK2) ),
inference(superposition,[status(thm)],[c_10195,c_4651]) ).
tcf(c_10310,plain,
apply(sK4,sK7(sK4,sK2),sK9(sK4,sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_10309,c_3677]) ).
tcf(c_10315,plain,
apply(sK4,sK11(sK2,sK4),sK12(sK2,sK4)),
inference(backward_subsumption_resolution,[status(thm)],[c_5362,c_10310]) ).
tcf(c_10316,plain,
member(sK12(sK2,sK4),sK2),
inference(backward_subsumption_resolution,[status(thm)],[c_4758,c_10310]) ).
tcf(c_10317,plain,
member(sK11(sK2,sK4),sK2),
inference(backward_subsumption_resolution,[status(thm)],[c_4752,c_10310]) ).
tcf(c_10449,plain,
( apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4))
| ~ member(sK11(sK2,sK4),sK2)
| ~ member(sK12(sK2,sK4),sK2) ),
inference(superposition,[status(thm)],[c_10315,c_2314]) ).
tcf(c_10450,plain,
apply(sK4,sK12(sK2,sK4),sK11(sK2,sK4)),
inference(forward_subsumption_resolution,[status(thm)],[c_10449,c_10317,c_10316]) ).
tcf(c_10473,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_10450,c_10310,c_7522,c_2833,c_2834,c_1069,c_1025]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET771+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.60 % Computer : n014.cluster.edu
% 0.11/5.60 % Model : x86_64 x86_64
% 0.11/5.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.60 % Memory : 8046.5625MB
% 0.11/5.60 % OS : Linux 6.8.0-71-generic
% 0.11/5.61 % CPULimit : 300
% 0.11/5.61 % WCLimit : 300
% 0.11/5.61 % DateTime : Thu Sep 24 11:54:24 UTC 2026
% 0.11/5.61 % CPUTime :
% 0.11/5.61 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.64 Running first-order theorem proving
% 0.11/5.64 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.66
% 0.11/5.66 % ======== iProver multi-core TPTP/SMT =========
% 0.11/5.66
% 0.11/5.66 % Detected problem language: tptp
% 0.11/5.67 % Proving...
% 8.18/6.90 % SZS status Started for theBenchmark.p
% 8.18/6.90 % SZS status Theorem for theBenchmark.p
% 8.18/6.90
% 8.18/6.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.18/6.90
% 8.18/6.90 % ------ iProver source info
% 8.18/6.90
% 8.18/6.90 % git: date: 2026-07-19 20:42:38 +0200
% 8.18/6.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.18/6.90 % git: non_committed_changes: false
% 8.18/6.90
% 8.18/6.90 % ------ Parsing...
% 8.18/6.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.18/6.90
% 8.18/6.90 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e %
% 8.18/6.90
% 8.18/6.90 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.18/6.90
% 8.18/6.90 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.18/6.90 % ------ Proving...
% 8.18/6.90 % ------ Problem Properties
% 8.18/6.90
% 8.18/6.90 %
% 8.18/6.90 % clauses 55
% 8.18/6.90 % conjectures 4
% 8.18/6.90 % EPR 2
% 8.18/6.90 % Horn 17
% 8.18/6.90 % unary 0
% 8.18/6.90 % binary 2
% 8.18/6.90 % lits 172
% 8.18/6.90 % lits eq 1
% 8.18/6.90 % fd_pure 0
% 8.18/6.90 % fd_pseudo 0
% 8.18/6.90 % fd_cond 0
% 8.18/6.90 % fd_pseudo_cond 1
% 8.18/6.90 % AC symbols 0
% 8.18/6.90
% 8.18/6.90 % ------ Schedule dynamic 5 is on
% 8.18/6.90
% 8.18/6.90 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.18/6.90
% 8.18/6.90
% 8.18/6.90 % ------
% 8.18/6.90 % Current options:
% 8.18/6.90 % ------
% 8.18/6.90
% 8.18/6.90
% 8.18/6.90 %
% 8.18/6.90
% 8.18/6.90 % ------ Proving...
% 8.18/6.90 %
% 8.18/6.90
% 8.18/6.90 % SZS status Theorem for theBenchmark.p
% 8.18/6.90
% 8.18/6.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.18/6.91
% 8.18/6.91
%------------------------------------------------------------------------------