%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU364+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n004.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:57:13 PM UTC 2026
% Result : Theorem 23.16s 14.59s
% Output : CNFRefutation 23.16s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f41ERROR: Could not build tree for root c_31528ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1,X2] :
( ( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e11_2_1__waybel_0__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1,X2] :
( ( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f24,plain,
? [X0,X1,X2] :
( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0)
& ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f25,plain,
? [X0,X1,X2] :
( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0)
& ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) ) ),
inference(flattening,[],[f24]) ).
fof(f42,plain,
? [X0,X1,X2] :
( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) )
& ( ~ in(X4,X3)
| ! [X5] :
( ! [X6] :
( ~ relstr_set_smaller(X0,X5,X6)
| ~ in(X6,X1)
| ~ element(X6,the_carrier(X0)) )
| X4 != X5 )
| ~ in(X4,powerset(X2)) ) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f43,plain,
? [X0,X1,X2] :
( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X5 = X4 )
& in(X4,powerset(X2)) ) )
& ( ~ in(X4,X3)
| ! [X5] :
( ! [X6] :
( ~ relstr_set_smaller(X0,X5,X6)
| ~ in(X6,X1)
| ~ element(X6,the_carrier(X0)) )
| X4 != X5 )
| ~ in(X4,powerset(X2)) ) ) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
? [X0,X1,X2] :
( element(X2,powerset(X1))
& finite(X2)
& element(X1,powerset(the_carrier(X0)))
& rel_str(X0)
& transitive_relstr(X0)
& ~ empty_carrier(X0)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X7] :
( ? [X8] :
( relstr_set_smaller(X0,X7,X8)
& in(X8,X1)
& element(X8,the_carrier(X0)) )
& X4 = X7 )
& in(X4,powerset(X2)) ) )
& ( ~ in(X4,X3)
| ! [X5] :
( ! [X6] :
( ~ relstr_set_smaller(X0,X5,X6)
| ~ in(X6,X1)
| ~ element(X6,the_carrier(X0)) )
| X4 != X5 )
| ~ in(X4,powerset(X2)) ) ) ),
inference(rectify,[],[f43]) ).
fof(f45,plain,
( element(sK4,powerset(sK3))
& finite(sK4)
& element(sK3,powerset(the_carrier(sK2)))
& rel_str(sK2)
& transitive_relstr(sK2)
& ~ empty_carrier(sK2)
& ! [X3] :
( ( in(sK5(X3),X3)
| ( relstr_set_smaller(sK2,sK6(X3),sK7(X3))
& in(sK7(X3),sK3)
& element(sK7(X3),the_carrier(sK2))
& sK5(X3) = sK6(X3)
& in(sK5(X3),powerset(sK4)) ) )
& ( ~ in(sK5(X3),X3)
| ! [X5] :
( ! [X6] :
( ~ relstr_set_smaller(sK2,X5,X6)
| ~ in(X6,sK3)
| ~ element(X6,the_carrier(sK2)) )
| sK5(X3) != X5 )
| ~ in(sK5(X3),powerset(sK4)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X4,sK5(X3)),skolemize(X7,sK6(X3)),skolemize(X8,sK7(X3))],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| ? [X3,X4,X5] :
( sP0(X5,X0,X1)
& X3 = X5
& ? [X6] :
( ? [X7] :
( relstr_set_smaller(X0,X6,X7)
& in(X7,X1)
& element(X7,the_carrier(X0)) )
& X6 = X4 )
& X3 = X4
& X4 != X5 ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f47,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| ? [X2,X3,X4] :
( sP0(X4,X0,X1)
& X2 = X4
& ? [X5] :
( ? [X6] :
( relstr_set_smaller(X0,X5,X6)
& in(X6,X1)
& element(X6,the_carrier(X0)) )
& X3 = X5 )
& X2 = X3
& X3 != X4 ) ),
inference(rectify,[],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| ( sP0(sK10(X0,X1),X0,X1)
& sK8(X0,X1) = sK10(X0,X1)
& relstr_set_smaller(X0,sK11(X0,X1),sK12(X0,X1))
& in(sK12(X0,X1),X1)
& element(sK12(X0,X1),the_carrier(X0))
& sK9(X0,X1) = sK11(X0,X1)
& sK8(X0,X1) = sK9(X0,X1)
& sK9(X0,X1) != sK10(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12]),skolemize(X2,sK8(X0,X1)),skolemize(X3,sK9(X0,X1)),skolemize(X4,sK10(X0,X1)),skolemize(X5,sK11(X0,X1)),skolemize(X6,sK12(X0,X1))],[f47]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ? [X10] :
! [X11] :
( ( ~ in(X11,X10)
| ? [X12] :
( ? [X13] :
( ? [X14] :
( relstr_set_smaller(X0,X13,X14)
& in(X14,X1)
& element(X14,the_carrier(X0)) )
& X11 = X13 )
& X11 = X12
& in(X12,powerset(X2)) ) )
& ( ! [X12] :
( ! [X13] :
( ! [X14] :
( ~ relstr_set_smaller(X0,X13,X14)
| ~ in(X14,X1)
| ~ element(X14,the_carrier(X0)) )
| X11 != X13 )
| X11 != X12
| ~ in(X12,powerset(X2)) )
| in(X11,X10) ) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ? [X3] :
! [X4] :
( ( ~ in(X4,X3)
| ? [X8] :
( ? [X9] :
( ? [X10] :
( relstr_set_smaller(X0,X9,X10)
& in(X10,X1)
& element(X10,the_carrier(X0)) )
& X4 = X9 )
& X4 = X8
& in(X8,powerset(X2)) ) )
& ( ! [X5] :
( ! [X6] :
( ! [X7] :
( ~ relstr_set_smaller(X0,X6,X7)
| ~ in(X7,X1)
| ~ element(X7,the_carrier(X0)) )
| X4 != X6 )
| X4 != X5
| ~ in(X5,powerset(X2)) )
| in(X4,X3) ) ) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ! [X4] :
( ( ~ in(X4,sK15(X0,X1,X2))
| ( relstr_set_smaller(X0,sK17(X0,X1,X4),sK18(X0,X1,X4))
& in(sK18(X0,X1,X4),X1)
& element(sK18(X0,X1,X4),the_carrier(X0))
& sK17(X0,X1,X4) = X4
& sK16(X0,X1,X2,X4) = X4
& in(sK16(X0,X1,X2,X4),powerset(X2)) ) )
& ( ! [X5] :
( ! [X6] :
( ! [X7] :
( ~ relstr_set_smaller(X0,X6,X7)
| ~ in(X7,X1)
| ~ element(X7,the_carrier(X0)) )
| X4 != X6 )
| X4 != X5
| ~ in(X5,powerset(X2)) )
| in(X4,sK15(X0,X1,X2)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17,sK18]),skolemize(X3,sK15(X0,X1,X2)),skolemize(X8,sK16(X0,X1,X2,X4)),skolemize(X9,sK17(X0,X1,X4)),skolemize(X10,sK18(X0,X1,X4))],[f53]) ).
fof(f64,plain,
element(sK4,powerset(sK3)),
inference(cnf_transformation,[],[f45]) ).
fof(f65,plain,
finite(sK4),
inference(cnf_transformation,[],[f45]) ).
fof(f66,plain,
element(sK3,powerset(the_carrier(sK2))),
inference(cnf_transformation,[],[f45]) ).
fof(f67,plain,
rel_str(sK2),
inference(cnf_transformation,[],[f45]) ).
fof(f68,plain,
transitive_relstr(sK2),
inference(cnf_transformation,[],[f45]) ).
fof(f69,plain,
~ empty_carrier(sK2),
inference(cnf_transformation,[],[f45]) ).
fof(f70,plain,
! [X3] :
( in(sK5(X3),X3)
| relstr_set_smaller(sK2,sK6(X3),sK7(X3)) ),
inference(cnf_transformation,[],[f45]) ).
fof(f71,plain,
! [X3] :
( in(sK5(X3),X3)
| in(sK7(X3),sK3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f72,plain,
! [X3] :
( in(sK5(X3),X3)
| element(sK7(X3),the_carrier(sK2)) ),
inference(cnf_transformation,[],[f45]) ).
fof(f73,plain,
! [X3] :
( in(sK5(X3),X3)
| sK5(X3) = sK6(X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f74,plain,
! [X3] :
( in(sK5(X3),X3)
| in(sK5(X3),powerset(sK4)) ),
inference(cnf_transformation,[],[f45]) ).
fof(f75,plain,
! [X3,X6,X5] :
( ~ in(sK5(X3),X3)
| ~ relstr_set_smaller(sK2,X5,X6)
| ~ in(X6,sK3)
| ~ element(X6,the_carrier(sK2))
| sK5(X3) != X5
| ~ in(sK5(X3),powerset(sK4)) ),
inference(cnf_transformation,[],[f45]) ).
fof(f77,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK8(X0,X1) = sK10(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f81,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK9(X0,X1) = sK11(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f82,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK8(X0,X1) = sK9(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f83,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK9(X0,X1) != sK10(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f88,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| relstr_set_smaller(X0,sK17(X0,X1,X4),sK18(X0,X1,X4)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f89,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| in(sK18(X0,X1,X4),X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f90,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| element(sK18(X0,X1,X4),the_carrier(X0)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f91,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| sK17(X0,X1,X4) = X4 ),
inference(cnf_transformation,[],[f54]) ).
fof(f92,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| sK16(X0,X1,X2,X4) = X4 ),
inference(cnf_transformation,[],[f54]) ).
fof(f93,plain,
! [X2,X0,X1,X4] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ in(X4,sK15(X0,X1,X2))
| in(sK16(X0,X1,X2,X4),powerset(X2)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f94,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| ~ in(X7,X1)
| ~ element(X7,the_carrier(X0))
| X4 != X6
| X4 != X5
| ~ in(X5,powerset(X2))
| in(X4,sK15(X0,X1,X2)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f119,plain,
! [X3,X6] :
( ~ in(sK5(X3),X3)
| ~ relstr_set_smaller(sK2,sK5(X3),X6)
| ~ in(X6,sK3)
| ~ element(X6,the_carrier(sK2))
| ~ in(sK5(X3),powerset(sK4)) ),
inference(equality_resolution,[],[f75]) ).
fof(f120,plain,
! [X2,X0,X1,X6,X7,X5] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| ~ in(X7,X1)
| ~ element(X7,the_carrier(X0))
| X5 != X6
| ~ in(X5,powerset(X2))
| in(X5,sK15(X0,X1,X2)) ),
inference(equality_resolution,[],[f94]) ).
fof(f121,plain,
! [X2,X0,X1,X6,X7] :
( ~ element(X2,powerset(X1))
| ~ finite(X2)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0)
| ~ transitive_relstr(X0)
| empty_carrier(X0)
| sP1(X0,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| ~ in(X7,X1)
| ~ element(X7,the_carrier(X0))
| ~ in(X6,powerset(X2))
| in(X6,sK15(X0,X1,X2)) ),
inference(equality_resolution,[],[f120]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ in(X1,sK3)
| ~ element(X1,the_carrier(sK2))
| ~ in(sK5(X0),X0)
| ~ in(sK5(X0),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(X0),X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_50,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),X0)
| in(sK5(X0),powerset(sK4)) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),X0)
| ( sK5(X0) = sK6(X0) ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),X0)
| element(sK7(X0),the_carrier(sK2)) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_53,negated_conjecture,
! [X0: $i] :
( in(sK7(X0),sK3)
| in(sK5(X0),X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_54,negated_conjecture,
! [X0: $i] :
( in(sK5(X0),X0)
| relstr_set_smaller(sK2,sK6(X0),sK7(X0)) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_55,negated_conjecture,
~ empty_carrier(sK2),
inference(cnf_transformation,[],[f69]) ).
tcf(c_56,negated_conjecture,
transitive_relstr(sK2),
inference(cnf_transformation,[],[f68]) ).
tcf(c_57,negated_conjecture,
rel_str(sK2),
inference(cnf_transformation,[],[f67]) ).
tcf(c_58,negated_conjecture,
element(sK3,powerset(the_carrier(sK2))),
inference(cnf_transformation,[],[f66]) ).
tcf(c_59,negated_conjecture,
finite(sK4),
inference(cnf_transformation,[],[f65]) ).
tcf(c_60,negated_conjecture,
element(sK4,powerset(sK3)),
inference(cnf_transformation,[],[f64]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X0,X1)
| ( sK9(X0,X1) != sK10(X0,X1) ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( ( sK9(X0,X1) = sK8(X0,X1) )
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( ( sK9(X0,X1) = sK11(X0,X1) )
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( ( sK10(X0,X1) = sK8(X0,X1) )
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( empty_carrier(X1)
| sP1(X1,X0)
| in(X2,sK15(X1,X0,X4))
| ~ finite(X4)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ in(X3,X0)
| ~ element(X4,powerset(X0))
| ~ element(X3,the_carrier(X1))
| ~ in(X2,powerset(X4))
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| in(sK16(X1,X2,X3,X0),powerset(X3))
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| ( sK16(X1,X2,X3,X0) = X0 )
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| ( sK17(X1,X2,X0) = X0 )
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| element(sK18(X1,X2,X0),the_carrier(X1))
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| in(sK18(X1,X2,X0),X2)
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| sP1(X1,X2)
| relstr_set_smaller(X1,sK17(X1,X2,X0),sK18(X1,X2,X0))
| ~ finite(X3)
| ~ rel_str(X1)
| ~ transitive_relstr(X1)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2,X3)) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_857,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| relstr_set_smaller(X0,sK17(X0,X2,X1),sK18(X0,X2,X1))
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_79]) ).
tcf(c_858,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| relstr_set_smaller(sK2,sK17(sK2,X1,X0),sK18(sK2,X1,X0))
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_857]) ).
tcf(c_860,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| relstr_set_smaller(sK2,sK17(sK2,X1,X0),sK18(sK2,X1,X0))
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_858,c_57,c_55,c_858]) ).
tcf(c_861,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| relstr_set_smaller(sK2,sK17(sK2,X1,X0),sK18(sK2,X1,X0))
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_860]) ).
tcf(c_881,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| in(sK18(X0,X2,X1),X2)
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_78]) ).
tcf(c_882,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| in(sK18(sK2,X1,X0),X1)
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_881]) ).
tcf(c_884,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| in(sK18(sK2,X1,X0),X1)
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_882,c_57,c_55,c_882]) ).
tcf(c_885,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| in(sK18(sK2,X1,X0),X1)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_884]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| element(sK18(X0,X2,X1),the_carrier(X0))
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_77]) ).
tcf(c_906,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| element(sK18(sK2,X1,X0),the_carrier(sK2))
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_905]) ).
tcf(c_908,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| element(sK18(sK2,X1,X0),the_carrier(sK2))
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_906,c_57,c_55,c_906]) ).
tcf(c_909,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| element(sK18(sK2,X1,X0),the_carrier(sK2))
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_908]) ).
tcf(c_929,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| ( sK17(X0,X2,X1) = X1 )
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_76]) ).
tcf(c_930,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_929]) ).
tcf(c_932,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| ( sK17(sK2,X1,X0) = X0 )
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_930,c_57,c_55,c_930]) ).
tcf(c_933,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_932]) ).
tcf(c_953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| ( sK16(X0,X2,X3,X1) = X1 )
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_75]) ).
tcf(c_954,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| ( sK16(sK2,X1,X2,X0) = X0 )
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_953]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| ( sK16(sK2,X1,X2,X0) = X0 )
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_954,c_57,c_55,c_954]) ).
tcf(c_957,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| ( sK16(sK2,X1,X2,X0) = X0 )
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_956]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X0)
| sP1(X0,X2)
| in(sK16(X0,X2,X3,X1),powerset(X3))
| ~ finite(X3)
| ~ rel_str(X0)
| ~ element(X3,powerset(X2))
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2,X3))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_74]) ).
tcf(c_978,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(sK2)
| sP1(sK2,X1)
| in(sK16(sK2,X1,X2,X0),powerset(X2))
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(unflattening,[status(thm)],[c_977]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2))
| in(sK16(sK2,X1,X2,X0),powerset(X2))
| sP1(sK2,X1) ),
inference(global_subsumption_just,[status(thm)],[c_978,c_57,c_55,c_978]) ).
tcf(c_981,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X1)
| in(sK16(sK2,X1,X2,X0),powerset(X2))
| ~ finite(X2)
| ~ element(X2,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1,X2)) ),
inference(renaming,[status(thm)],[c_980]) ).
tcf(c_1001,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( empty_carrier(X0)
| sP1(X0,X1)
| in(X2,sK15(X0,X1,X4))
| ~ finite(X4)
| ~ rel_str(X0)
| ~ in(X3,X1)
| ~ element(X4,powerset(X1))
| ~ element(X3,the_carrier(X0))
| ~ in(X2,powerset(X4))
| ~ relstr_set_smaller(X0,X2,X3)
| ~ element(X1,powerset(the_carrier(X0)))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_56,c_73]) ).
tcf(c_1002,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(sK2)
| sP1(sK2,X0)
| in(X1,sK15(sK2,X0,X2))
| ~ rel_str(sK2)
| ~ finite(X2)
| ~ in(X3,X0)
| ~ element(X3,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,X1,X3)
| ~ element(X2,powerset(X0))
| ~ in(X1,powerset(X2))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(unflattening,[status(thm)],[c_1001]) ).
tcf(c_1003,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ finite(X2)
| ~ in(X3,X0)
| ~ element(X3,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,X1,X3)
| ~ element(X2,powerset(X0))
| ~ in(X1,powerset(X2))
| ~ element(X0,powerset(the_carrier(sK2)))
| in(X1,sK15(sK2,X0,X2))
| sP1(sK2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1002,c_57,c_55,c_1002]) ).
tcf(c_1004,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(sK2,X0)
| in(X1,sK15(sK2,X0,X2))
| ~ finite(X2)
| ~ in(X3,X0)
| ~ element(X3,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,X1,X3)
| ~ element(X2,powerset(X0))
| ~ in(X1,powerset(X2))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(renaming,[status(thm)],[c_1003]) ).
tcf(c_1198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP1(sK2,X3)
| in(sK5(X0),X0)
| in(X1,sK15(sK2,X3,X4))
| ~ finite(X4)
| ~ in(X2,X3)
| ~ element(X2,the_carrier(sK2))
| ~ element(X4,powerset(X3))
| ~ in(X1,powerset(X4))
| ~ element(X3,powerset(the_carrier(sK2)))
| ( sK2 != sK2 )
| ( sK7(X0) != X2 )
| ( sK6(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_1004]) ).
tcf(c_1199,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| in(sK6(X0),sK15(sK2,X2,X1))
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ element(sK7(X0),the_carrier(sK2))
| ~ in(sK6(X0),powerset(X1)) ),
inference(unflattening,[status(thm)],[c_1198]) ).
tcf(c_1201,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| in(sK6(X0),sK15(sK2,X2,X1))
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ in(sK6(X0),powerset(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_1199,c_52,c_1199]) ).
tcf(c_7181,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| in(sK18(sK2,X0,sK5(sK15(sK2,X0,X1))),X0)
| ( sK5(sK15(sK2,X0,X1)) = sK6(sK15(sK2,X0,X1)) )
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_51,c_885]) ).
tcf(c_7184,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| in(sK7(sK15(sK2,X0,X1)),sK3)
| in(sK18(sK2,X0,sK5(sK15(sK2,X0,X1))),X0)
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_53,c_885]) ).
tcf(c_7225,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| element(sK18(sK2,X0,sK5(sK15(sK2,X0,X1))),the_carrier(sK2))
| ( sK5(sK15(sK2,X0,X1)) = sK6(sK15(sK2,X0,X1)) )
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_51,c_909]) ).
tcf(c_7228,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| in(sK7(sK15(sK2,X0,X1)),sK3)
| element(sK18(sK2,X0,sK5(sK15(sK2,X0,X1))),the_carrier(sK2))
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_53,c_909]) ).
tcf(c_7269,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| ( sK5(sK15(sK2,X0,X1)) = sK6(sK15(sK2,X0,X1)) )
| ( sK17(sK2,X0,sK5(sK15(sK2,X0,X1))) = sK5(sK15(sK2,X0,X1)) )
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_51,c_933]) ).
tcf(c_7313,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| ( sK5(sK15(sK2,X0,X1)) = sK6(sK15(sK2,X0,X1)) )
| ( sK16(sK2,X0,X1,sK5(sK15(sK2,X0,X1))) = sK5(sK15(sK2,X0,X1)) )
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_51,c_957]) ).
tcf(c_7392,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| relstr_set_smaller(sK2,sK17(sK2,X0,sK5(sK15(sK2,X0,X1))),sK18(sK2,X0,sK5(sK15(sK2,X0,X1))))
| ( sK5(sK15(sK2,X0,X1)) = sK6(sK15(sK2,X0,X1)) )
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_51,c_861]) ).
tcf(c_7395,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| in(sK7(sK15(sK2,X0,X1)),sK3)
| relstr_set_smaller(sK2,sK17(sK2,X0,sK5(sK15(sK2,X0,X1))),sK18(sK2,X0,sK5(sK15(sK2,X0,X1))))
| ~ finite(X1)
| ~ element(X1,powerset(X0))
| ~ element(X0,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_53,c_861]) ).
tcf(c_8026,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,X0),the_carrier(sK2))
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,sK3,X1)) ),
inference(instantiation,[status(thm)],[c_909]) ).
tcf(c_8184,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| in(sK6(X0),sK15(sK2,X2,X1))
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ element(sK7(X0),the_carrier(sK2))
| ~ in(sK6(X0),powerset(X1)) ),
inference(superposition,[status(thm)],[c_54,c_1004]) ).
tcf(c_8359,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,X0)) = sK6(sK15(sK2,sK3,X0)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,X0))) = sK5(sK15(sK2,sK3,X0)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_58,c_7269]) ).
tcf(c_8422,plain,
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4) ),
inference(superposition,[status(thm)],[c_60,c_8359]) ).
tcf(c_8427,plain,
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8422,c_59]) ).
tcf(c_8470,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8427,c_67]) ).
tcf(c_8471,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8427,c_63]) ).
tcf(c_8472,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8427,c_62]) ).
tcf(c_8497,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,X0)) = sK6(sK15(sK2,sK3,X0)) )
| ( sK16(sK2,sK3,X0,sK5(sK15(sK2,sK3,X0))) = sK5(sK15(sK2,sK3,X0)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_58,c_7313]) ).
tcf(c_8557,plain,
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4) ),
inference(superposition,[status(thm)],[c_60,c_8497]) ).
tcf(c_8562,plain,
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8557,c_59]) ).
tcf(c_8597,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8562,c_67]) ).
tcf(c_8598,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8562,c_63]) ).
tcf(c_8599,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_8562,c_62]) ).
tcf(c_8612,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| in(sK6(X0),sK15(sK2,X2,X1))
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ in(sK6(X0),powerset(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_8184,c_1201]) ).
tcf(c_8639,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| ( sK16(sK2,X2,X1,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ in(sK6(X0),powerset(X1)) ),
inference(superposition,[status(thm)],[c_8612,c_957]) ).
tcf(c_8640,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK2,X2)
| in(sK5(X0),X0)
| ( sK17(sK2,X2,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(X2))
| ~ in(sK7(X0),X2)
| ~ element(X2,powerset(the_carrier(sK2)))
| ~ in(sK6(X0),powerset(X1)) ),
inference(superposition,[status(thm)],[c_8612,c_933]) ).
tcf(c_9431,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_8597,c_981]) ).
tcf(c_9433,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9431,c_59,c_60,c_58]) ).
tcf(c_9491,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_8598,c_981]) ).
tcf(c_9493,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9491,c_59,c_60,c_58]) ).
tcf(c_9518,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_8599,c_981]) ).
tcf(c_9520,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9518,c_59,c_60,c_58]) ).
tcf(c_9592,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9433,c_67,c_51]) ).
tcf(c_9602,plain,
! [X0: $i] :
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_9592,c_49]) ).
tcf(c_9619,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9493,c_63,c_51]) ).
tcf(c_9629,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_9619,c_49]) ).
tcf(c_9646,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9520,c_62,c_51]) ).
tcf(c_9656,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_9646,c_49]) ).
tcf(c_9900,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_8472,c_7392]) ).
tcf(c_9901,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_8471,c_7392]) ).
tcf(c_9902,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_8470,c_7392]) ).
tcf(c_9909,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9902,c_59,c_60,c_58]) ).
tcf(c_9914,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9901,c_59,c_60,c_58]) ).
tcf(c_9919,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9900,c_59,c_60,c_58]) ).
tcf(c_10007,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9909,c_67]) ).
tcf(c_10033,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9914,c_63]) ).
tcf(c_10059,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9919,c_62]) ).
tcf(c_10431,plain,
! [X0: $i] :
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9602,c_51]) ).
tcf(c_10450,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_10007,c_10431]) ).
tcf(c_10476,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9629,c_51]) ).
tcf(c_10494,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_10033,c_10476]) ).
tcf(c_10516,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9656,c_51]) ).
tcf(c_10533,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_10059,c_10516]) ).
tcf(c_10790,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| in(sK5(X0),X0)
| ( sK17(sK2,sK3,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK7(X0),sK3)
| ~ in(sK6(X0),powerset(X1)) ),
inference(superposition,[status(thm)],[c_58,c_8640]) ).
tcf(c_10847,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,X0),the_carrier(sK2))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,sK3,sK4)) ),
inference(instantiation,[status(thm)],[c_8026]) ).
tcf(c_10852,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| in(sK5(X0),X0)
| ( sK17(sK2,sK3,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK6(X0),powerset(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_10790,c_53,c_10790]) ).
tcf(c_11455,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| in(sK5(X0),X0)
| ( sK16(sK2,sK3,X1,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK7(X0),sK3)
| ~ in(sK6(X0),powerset(X1)) ),
inference(superposition,[status(thm)],[c_58,c_8639]) ).
tcf(c_11512,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| in(sK5(X0),X0)
| ( sK16(sK2,sK3,X1,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK6(X0),powerset(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_11455,c_53,c_11455]) ).
tcf(c_11618,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(superposition,[status(thm)],[c_7225,c_10450]) ).
tcf(c_11622,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11618,c_59,c_60,c_58]) ).
tcf(c_11657,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11622,c_67]) ).
tcf(c_11667,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7181,c_11657]) ).
tcf(c_11671,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11667,c_59,c_60,c_58]) ).
tcf(c_11688,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11671,c_67]) ).
tcf(c_11696,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_11688,c_11512]) ).
tcf(c_11698,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_11688,c_10852]) ).
tcf(c_11701,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_11688,c_8612]) ).
tcf(c_11892,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(superposition,[status(thm)],[c_7225,c_10494]) ).
tcf(c_11896,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11892,c_59,c_60,c_58]) ).
tcf(c_11984,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11896,c_63]) ).
tcf(c_11994,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7181,c_11984]) ).
tcf(c_11998,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11994,c_59,c_60,c_58]) ).
tcf(c_12015,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11998,c_63]) ).
tcf(c_12024,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_12015,c_11512]) ).
tcf(c_12151,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(superposition,[status(thm)],[c_7225,c_10533]) ).
tcf(c_12155,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12151,c_59,c_60,c_58]) ).
tcf(c_12190,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12155,c_62]) ).
tcf(c_12200,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7181,c_12190]) ).
tcf(c_12204,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12200,c_59,c_60,c_58]) ).
tcf(c_12221,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12204,c_62]) ).
tcf(c_12230,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_12221,c_11512]) ).
tcf(c_12232,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_12221,c_10852]) ).
tcf(c_15225,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11698,c_67]) ).
tcf(c_15244,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_15225]) ).
tcf(c_15247,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15244,c_59,c_60]) ).
tcf(c_15263,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_15247,c_933]) ).
tcf(c_15279,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15263,c_59,c_60,c_58]) ).
tcf(c_15348,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15279,c_67]) ).
tcf(c_15360,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_11688,c_15348]) ).
tcf(c_16675,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12232,c_62]) ).
tcf(c_16694,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_16675]) ).
tcf(c_16697,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16694,c_59,c_60]) ).
tcf(c_16713,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_16697,c_933]) ).
tcf(c_16729,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16713,c_59,c_60,c_58]) ).
tcf(c_16780,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16729,c_62]) ).
tcf(c_16790,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_12221,c_16780]) ).
tcf(c_16961,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_16790,c_7395]) ).
tcf(c_16966,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16961,c_59,c_60,c_58]) ).
tcf(c_16985,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16966,c_62]) ).
tcf(c_17517,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11696,c_67]) ).
tcf(c_17536,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_17517]) ).
tcf(c_17539,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17536,c_59,c_60]) ).
tcf(c_17550,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_17539,c_861]) ).
tcf(c_17551,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_17539,c_957]) ).
tcf(c_17553,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_17539,c_909]) ).
tcf(c_17554,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_17539,c_885]) ).
tcf(c_17558,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17554,c_59,c_60,c_58]) ).
tcf(c_17563,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17553,c_59,c_60,c_58]) ).
tcf(c_17568,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17551,c_59,c_60,c_58]) ).
tcf(c_17573,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17550,c_59,c_60,c_58]) ).
tcf(c_17582,plain,
( in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17558,c_67]) ).
tcf(c_17600,plain,
( element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17563,c_67]) ).
tcf(c_17614,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17568,c_67]) ).
tcf(c_17626,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_11688,c_17614]) ).
tcf(c_17637,plain,
( relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17573,c_67]) ).
tcf(c_17649,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_15360,c_17637]) ).
tcf(c_17761,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_17626,c_981]) ).
tcf(c_17763,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17761,c_59,c_60,c_58]) ).
tcf(c_17777,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17763,c_67,c_50]) ).
tcf(c_17784,plain,
! [X0: $i] :
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_17777,c_49]) ).
tcf(c_17816,plain,
! [X0: $i] :
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_17539,c_17784]) ).
tcf(c_18222,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_17649,c_17816]) ).
tcf(c_18263,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12024,c_63]) ).
tcf(c_18282,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_18263]) ).
tcf(c_18286,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18282,c_59,c_60]) ).
tcf(c_18305,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_18286,c_957]) ).
tcf(c_18329,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18305,c_59,c_60,c_58]) ).
tcf(c_18424,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18329,c_63]) ).
tcf(c_18435,plain,
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_12015,c_18424]) ).
tcf(c_18488,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12230,c_62]) ).
tcf(c_18507,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_18488]) ).
tcf(c_18511,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18507,c_59,c_60]) ).
tcf(c_18528,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_18511,c_957]) ).
tcf(c_18552,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18528,c_59,c_60,c_58]) ).
tcf(c_18599,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_18435,c_981]) ).
tcf(c_18601,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18599,c_59,c_60,c_58]) ).
tcf(c_18663,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK11(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18601,c_63,c_50]) ).
tcf(c_18670,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_18663,c_49]) ).
tcf(c_18869,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18552,c_62]) ).
tcf(c_18879,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(superposition,[status(thm)],[c_12221,c_18869]) ).
tcf(c_19162,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_18879,c_981]) ).
tcf(c_19164,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19162,c_59,c_60,c_58]) ).
tcf(c_19180,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19164,c_62,c_50]) ).
tcf(c_19187,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_19180,c_49]) ).
tcf(c_19218,plain,
! [X0: $i] :
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_53,c_19187]) ).
tcf(c_19276,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_16985,c_19218]) ).
tcf(c_19400,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(superposition,[status(thm)],[c_7228,c_19276]) ).
tcf(c_19408,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19400,c_59,c_60,c_58]) ).
tcf(c_19550,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19408,c_62]) ).
tcf(c_19563,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7184,c_19550]) ).
tcf(c_19570,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19563,c_59,c_60,c_58]) ).
tcf(c_19582,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19570,c_62]) ).
tcf(c_20821,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(instantiation,[status(thm)],[c_10847]) ).
tcf(c_20823,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_20824,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_20826,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_20890,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK16(sK2,sK3,sK4,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18222,c_17582,c_17600]) ).
tcf(c_20900,plain,
( sP1(sK2,sK3)
| in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_20890,c_981]) ).
tcf(c_20902,plain,
( sP1(sK2,sK3)
| in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20900,c_59,c_60,c_58]) ).
tcf(c_20916,plain,
( in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20902,c_67]) ).
tcf(c_20929,plain,
( in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_11688,c_20916]) ).
tcf(c_23715,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| sP1(sK2,X1)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ finite(X0)
| ~ element(sK4,powerset(sK3))
| ~ element(X0,powerset(X1))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_11701,c_885]) ).
tcf(c_23736,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(equality_factoring,[status(thm)],[c_11701]) ).
tcf(c_23738,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23736,c_59,c_60,c_58]) ).
tcf(c_23870,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,sK3)
| sP1(sK2,X1)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23715,c_59,c_60,c_58]) ).
tcf(c_23973,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_23738,c_20824,c_23738]) ).
tcf(c_23979,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23973,c_67]) ).
tcf(c_23990,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_23979,c_861]) ).
tcf(c_23993,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_23979,c_909]) ).
tcf(c_23994,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_23979,c_885]) ).
tcf(c_24001,plain,
! [X0: $i] :
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_23979,c_17784]) ).
tcf(c_24029,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23994,c_59,c_60,c_58]) ).
tcf(c_24034,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23993,c_59,c_60,c_58]) ).
tcf(c_24039,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23990,c_59,c_60,c_58]) ).
tcf(c_24333,plain,
( relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24039,c_67]) ).
tcf(c_24345,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_15360,c_24333]) ).
tcf(c_24387,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23870,c_67]) ).
tcf(c_24427,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ~ finite(sK4)
| ~ in(X0,sK3)
| ~ element(sK4,powerset(sK3))
| ~ element(X0,the_carrier(sK2))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_24387,c_18670]) ).
tcf(c_24428,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ finite(sK4)
| ~ in(X0,sK3)
| ~ element(sK4,powerset(sK3))
| ~ element(X0,the_carrier(sK2))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_24387,c_17784]) ).
tcf(c_24498,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24428,c_59,c_60,c_58]) ).
tcf(c_24516,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ( sK9(sK2,sK3) = sK11(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24427,c_59,c_60,c_58]) ).
tcf(c_24735,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_24345,c_24001]) ).
tcf(c_24775,plain,
( sP1(sK2,sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK10(sK2,sK3) = sK8(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_24498,c_24029,c_24034,c_24735]) ).
tcf(c_24776,plain,
( sP1(sK2,sK3)
| ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(renaming,[status(thm)],[c_24775]) ).
tcf(c_24780,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24776,c_67]) ).
tcf(c_24787,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_20929,c_24780]) ).
tcf(c_24835,plain,
( ( sK10(sK2,sK3) = sK8(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_11688,c_24780]) ).
tcf(c_24844,plain,
sK10(sK2,sK3) = sK8(sK2,sK3),
inference(global_subsumption_just,[status(thm)],[c_24516,c_20826,c_24787,c_24835]) ).
tcf(c_24862,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(demodulation,[status(thm)],[c_19582,c_24844]) ).
tcf(c_24864,plain,
! [X0: $i] :
( ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(demodulation,[status(thm)],[c_19187,c_24844]) ).
tcf(c_24865,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(demodulation,[status(thm)],[c_19180,c_24844]) ).
tcf(c_24880,plain,
( ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(demodulation,[status(thm)],[c_16790,c_24844]) ).
tcf(c_24896,plain,
( ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(demodulation,[status(thm)],[c_12221,c_24844]) ).
tcf(c_25257,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_24896,c_8612]) ).
tcf(c_29372,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(equality_factoring,[status(thm)],[c_25257]) ).
tcf(c_29374,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29372,c_59,c_60,c_58]) ).
tcf(c_29597,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_29374,c_24862,c_29374]) ).
tcf(c_29608,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_29597,c_861]) ).
tcf(c_29611,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_29597,c_909]) ).
tcf(c_29612,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_29597,c_885]) ).
tcf(c_29615,plain,
! [X0: $i] :
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_29597,c_24864]) ).
tcf(c_29626,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29612,c_59,c_60,c_58]) ).
tcf(c_29631,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29611,c_59,c_60,c_58]) ).
tcf(c_29636,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29608,c_59,c_60,c_58]) ).
tcf(c_29847,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_24880,c_29636]) ).
tcf(c_30420,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_29847,c_29615]) ).
tcf(c_30438,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_30420,c_29626,c_29631,c_30420]) ).
tcf(c_30454,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(superposition,[status(thm)],[c_24896,c_30438]) ).
tcf(c_30458,plain,
( sP1(sK2,sK3)
| ( sK9(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_30454,c_24865,c_30454]) ).
tcf(c_30467,plain,
( ( sK9(sK2,sK3) = sK8(sK2,sK3) )
| ( sK9(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_30458,c_62]) ).
tcf(c_30468,plain,
sK9(sK2,sK3) = sK10(sK2,sK3),
inference(light_normalisation,[status(thm)],[c_30467,c_24844]) ).
tcf(c_30551,plain,
~ sP1(sK2,sK3),
inference(superposition,[status(thm)],[c_30468,c_61]) ).
tcf(c_30561,plain,
! [X0: $i,X1: $i] :
( in(sK5(X0),X0)
| ( sK16(sK2,sK3,X1,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK6(X0),powerset(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_11512,c_30551]) ).
tcf(c_30565,plain,
! [X0: $i,X1: $i] :
( in(sK5(X0),X0)
| ( sK17(sK2,sK3,sK6(X0)) = sK6(X0) )
| ~ finite(X1)
| ~ element(X1,powerset(sK3))
| ~ in(sK6(X0),powerset(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_10852,c_30551]) ).
tcf(c_30570,plain,
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8562,c_30551]) ).
tcf(c_30574,plain,
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8427,c_30551]) ).
tcf(c_30653,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_30574,c_7392]) ).
tcf(c_30657,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30653,c_59,c_60,c_58]) ).
tcf(c_30676,plain,
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4)))) ),
inference(global_subsumption_just,[status(thm)],[c_30657,c_30551,c_30657]) ).
tcf(c_30677,plain,
( relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(renaming,[status(thm)],[c_30676]) ).
tcf(c_30731,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_30570,c_981]) ).
tcf(c_30733,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30731,c_30551,c_59,c_60,c_58]) ).
tcf(c_30758,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) ) ),
inference(global_subsumption_just,[status(thm)],[c_30733,c_20823,c_30733]) ).
tcf(c_30764,plain,
! [X0: $i] :
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_30758,c_49]) ).
tcf(c_30791,plain,
! [X0: $i] :
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_30764,c_20823,c_30764]) ).
tcf(c_30802,plain,
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_30677,c_30791]) ).
tcf(c_30830,plain,
( ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(global_subsumption_just,[status(thm)],[c_30802,c_59,c_60,c_58,c_20821,c_20823,c_30551,c_30802]) ).
tcf(c_30836,plain,
( sP1(sK2,sK3)
| ( sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7181,c_30830]) ).
tcf(c_30840,plain,
sK5(sK15(sK2,sK3,sK4)) = sK6(sK15(sK2,sK3,sK4)),
inference(forward_subsumption_resolution,[status(thm)],[c_30836,c_30551,c_59,c_60,c_58]) ).
tcf(c_30905,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK16(sK2,sK3,X0,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_30840,c_30561]) ).
tcf(c_30906,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK17(sK2,sK3,sK6(sK15(sK2,sK3,sK4))) = sK6(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_30840,c_30565]) ).
tcf(c_30914,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK6(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(superposition,[status(thm)],[c_30840,c_8612]) ).
tcf(c_30919,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(light_normalisation,[status(thm)],[c_30906,c_30840]) ).
tcf(c_30925,plain,
! [X0: $i] :
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK16(sK2,sK3,X0,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(X0)
| ~ element(X0,powerset(sK3))
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(light_normalisation,[status(thm)],[c_30905,c_30840]) ).
tcf(c_30931,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,X1,X0))
| ~ finite(X0)
| ~ element(X0,powerset(X1))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),X1)
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(X0)) ),
inference(light_normalisation,[status(thm)],[c_30914,c_30840]) ).
tcf(c_31086,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_30919]) ).
tcf(c_31089,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31086,c_59,c_60]) ).
tcf(c_31101,plain,
( sP1(sK2,sK3)
| ( sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31089,c_933]) ).
tcf(c_31106,plain,
sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)),
inference(forward_subsumption_resolution,[status(thm)],[c_31101,c_30551,c_59,c_60,c_58]) ).
tcf(c_31110,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31106,c_7395]) ).
tcf(c_31111,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31110,c_30551,c_59,c_60,c_58]) ).
tcf(c_31262,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3)) ),
inference(superposition,[status(thm)],[c_50,c_30925]) ).
tcf(c_31265,plain,
( in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31262,c_59,c_60]) ).
tcf(c_31274,plain,
( sP1(sK2,sK3)
| ( sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)) )
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31265,c_957]) ).
tcf(c_31280,plain,
sK16(sK2,sK3,sK4,sK5(sK15(sK2,sK3,sK4))) = sK5(sK15(sK2,sK3,sK4)),
inference(forward_subsumption_resolution,[status(thm)],[c_31274,c_30551,c_59,c_60,c_58]) ).
tcf(c_31281,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_31280,c_981]) ).
tcf(c_31283,plain,
( in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4))
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31281,c_30551,c_59,c_60,c_58]) ).
tcf(c_31289,plain,
in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4)),
inference(global_subsumption_just,[status(thm)],[c_31283,c_20826,c_31283]) ).
tcf(c_31291,plain,
! [X0: $i] :
( ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0)
| ~ in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)) ),
inference(superposition,[status(thm)],[c_31289,c_49]) ).
tcf(c_31313,plain,
! [X0: $i] :
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(superposition,[status(thm)],[c_53,c_31291]) ).
tcf(c_31345,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_31111,c_31313]) ).
tcf(c_31405,plain,
( in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3) ),
inference(global_subsumption_just,[status(thm)],[c_31345,c_59,c_60,c_58,c_20821,c_20824,c_30551,c_31345]) ).
tcf(c_31414,plain,
( sP1(sK2,sK3)
| in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_7184,c_31405]) ).
tcf(c_31415,plain,
in(sK7(sK15(sK2,sK3,sK4)),sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_31414,c_30551,c_59,c_60,c_58]) ).
tcf(c_31458,plain,
( sP1(sK2,sK3)
| in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ in(sK7(sK15(sK2,sK3,sK4)),sK3)
| ~ in(sK5(sK15(sK2,sK3,sK4)),powerset(sK4)) ),
inference(equality_factoring,[status(thm)],[c_30931]) ).
tcf(c_31460,plain,
in(sK5(sK15(sK2,sK3,sK4)),sK15(sK2,sK3,sK4)),
inference(forward_subsumption_resolution,[status(thm)],[c_31458,c_30551,c_59,c_60,c_58,c_31415,c_31289]) ).
tcf(c_31461,plain,
! [X0: $i] :
( ~ in(X0,sK3)
| ~ element(X0,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_31291,c_31460]) ).
tcf(c_31467,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK17(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31460,c_861]) ).
tcf(c_31470,plain,
( sP1(sK2,sK3)
| element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31460,c_909]) ).
tcf(c_31471,plain,
( sP1(sK2,sK3)
| in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(superposition,[status(thm)],[c_31460,c_885]) ).
tcf(c_31472,plain,
in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_31471,c_30551,c_59,c_60,c_58]) ).
tcf(c_31473,plain,
element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)),
inference(forward_subsumption_resolution,[status(thm)],[c_31470,c_30551,c_59,c_60,c_58]) ).
tcf(c_31474,plain,
( sP1(sK2,sK3)
| relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))))
| ~ finite(sK4)
| ~ element(sK4,powerset(sK3))
| ~ element(sK3,powerset(the_carrier(sK2))) ),
inference(light_normalisation,[status(thm)],[c_31467,c_31106]) ).
tcf(c_31475,plain,
relstr_set_smaller(sK2,sK5(sK15(sK2,sK3,sK4)),sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4)))),
inference(forward_subsumption_resolution,[status(thm)],[c_31474,c_30551,c_59,c_60,c_58]) ).
tcf(c_31527,plain,
( ~ in(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),sK3)
| ~ element(sK18(sK2,sK3,sK5(sK15(sK2,sK3,sK4))),the_carrier(sK2)) ),
inference(superposition,[status(thm)],[c_31475,c_31461]) ).
tcf(c_31528,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_31527,c_31472,c_31473]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU364+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.20/10.47 % Computer : n004.cluster.edu
% 0.20/10.47 % Model : x86_64 x86_64
% 0.20/10.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/10.47 % Memory : 8046.5625MB
% 0.20/10.47 % OS : Linux 6.8.0-71-generic
% 0.20/10.47 % CPULimit : 300
% 0.20/10.47 % WCLimit : 300
% 0.20/10.47 % DateTime : Thu Sep 24 13:51:17 UTC 2026
% 0.20/10.48 % CPUTime :
% 0.20/10.48 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/10.54 Running first-order theorem proving
% 0.24/10.54 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.24/10.56
% 0.24/10.56 % ======== iProver multi-core TPTP/SMT =========
% 0.24/10.56
% 0.24/10.56 % Detected problem language: tptp
% 0.24/10.58 % Proving...
% 23.16/14.59 % SZS status Started for theBenchmark.p
% 23.16/14.59 % SZS status Theorem for theBenchmark.p
% 23.16/14.59
% 23.16/14.59 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 23.16/14.59
% 23.16/14.59 % ------ iProver source info
% 23.16/14.59
% 23.16/14.59 % git: date: 2026-07-19 20:42:38 +0200
% 23.16/14.59 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 23.16/14.59 % git: non_committed_changes: false
% 23.16/14.59
% 23.16/14.59 % ------ Parsing...
% 23.16/14.59 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 23.16/14.59
% 23.16/14.59 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 23.16/14.59
% 23.16/14.59 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 23.16/14.59
% 23.16/14.59 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 23.16/14.59 % ------ Proving...
% 23.16/14.59 % ------ Problem Properties
% 23.16/14.59
% 23.16/14.59 %
% 23.16/14.59 % clauses 51
% 23.16/14.59 % conjectures 9
% 23.16/14.59 % EPR 7
% 23.16/14.59 % Horn 34
% 23.16/14.59 % unary 16
% 23.16/14.59 % binary 26
% 23.16/14.59 % lits 121
% 23.16/14.59 % lits eq 8
% 23.16/14.59 % fd_pure 0
% 23.16/14.59 % fd_pseudo 0
% 23.16/14.59 % fd_cond 0
% 23.16/14.59 % fd_pseudo_cond 0
% 23.16/14.59 % AC symbols 0
% 23.16/14.59
% 23.16/14.59 % ------ Schedule dynamic 5 is on
% 23.16/14.59
% 23.16/14.59 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 23.16/14.59
% 23.16/14.59
% 23.16/14.59 % ------
% 23.16/14.59 % Current options:
% 23.16/14.59 % ------
% 23.16/14.59
% 23.16/14.59
% 23.16/14.59 %
% 23.16/14.59
% 23.16/14.59 % ------ Proving...
% 23.16/14.59 %
% 23.16/14.59
% 23.16/14.59 % SZS status Theorem for theBenchmark.p
% 23.16/14.59
% 23.16/14.59 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 23.16/14.59
% 23.16/14.59
%------------------------------------------------------------------------------