%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU314+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 : n002.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:56:36 PM UTC 2026
% Result : Theorem 3.51s 1.75s
% Output : CNFRefutation 3.51s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e1_40__pre_topc__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f30,axiom,
! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0) )
=> ( ! [X2,X3,X4] :
( ( ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) )
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3 )
=> X3 = X4 )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ? [X4] :
( ? [X7] :
( subset(X1,X3)
& closed_subset(X7,X0)
& X7 = X3
& element(X7,powerset(the_carrier(X0))) )
& X4 = X3
& in(X4,powerset(the_carrier(X0))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_tarski__e1_40__pre_topc__1) ).
fof(f32,plain,
! [X0,X1] :
( ( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0) )
=> ( ! [X2,X3,X4] :
( ( ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) )
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3 )
=> X3 = X4 )
=> ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( subset(X1,X8)
& closed_subset(X10,X0)
& X8 = X10
& element(X10,powerset(the_carrier(X0))) )
& X8 = X9
& in(X9,powerset(the_carrier(X0))) ) ) ) ),
inference(rectify,[],[f30]) ).
fof(f49,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f50,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) ) ),
inference(flattening,[],[f49]) ).
fof(f65,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2,X3,X4] :
( ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) )
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3
& X3 != X4 )
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( subset(X1,X8)
& closed_subset(X10,X0)
& X8 = X10
& element(X10,powerset(the_carrier(X0))) )
& X8 = X9
& in(X9,powerset(the_carrier(X0))) ) ) ),
inference(ennf_transformation,[],[f32]) ).
fof(f66,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| ? [X2,X3,X4] :
( ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) )
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3
& X3 != X4 )
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( subset(X1,X8)
& closed_subset(X10,X0)
& X8 = X10
& element(X10,powerset(the_carrier(X0))) )
& X8 = X9
& in(X9,powerset(the_carrier(X0))) ) ) ),
inference(flattening,[],[f65]) ).
fof(f70,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ subset(X1,X3)
| ~ closed_subset(X4,X0)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X3,powerset(the_carrier(X0))) ) ) ),
inference(nnf_transformation,[],[f50]) ).
fof(f71,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X4] :
( subset(X1,X3)
& closed_subset(X4,X0)
& X4 = X3
& element(X4,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ subset(X1,X3)
| ~ closed_subset(X4,X0)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X3,powerset(the_carrier(X0))) ) ) ),
inference(flattening,[],[f70]) ).
fof(f72,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(X0)))
& top_str(X0)
& topological_space(X0)
& ! [X2] :
? [X3] :
( ( in(X3,X2)
| ( ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X3 = X5
& element(X5,powerset(the_carrier(X0))) )
& in(X3,powerset(the_carrier(X0))) ) )
& ( ~ in(X3,X2)
| ! [X4] :
( ~ subset(X1,X3)
| ~ closed_subset(X4,X0)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X3,powerset(the_carrier(X0))) ) ) ),
inference(rectify,[],[f71]) ).
fof(f73,plain,
( element(sK3,powerset(the_carrier(sK2)))
& top_str(sK2)
& topological_space(sK2)
& ! [X2] :
( ( in(sK4(X2),X2)
| ( subset(sK3,sK4(X2))
& closed_subset(sK5(X2),sK2)
& sK4(X2) = sK5(X2)
& element(sK5(X2),powerset(the_carrier(sK2)))
& in(sK4(X2),powerset(the_carrier(sK2))) ) )
& ( ~ in(sK4(X2),X2)
| ! [X4] :
( ~ subset(sK3,sK4(X2))
| ~ closed_subset(X4,sK2)
| sK4(X2) != X4
| ~ element(X4,powerset(the_carrier(sK2))) )
| ~ in(sK4(X2),powerset(the_carrier(sK2))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X3,sK4(X2)),skolemize(X5,sK5(X2))],[f72]) ).
fof(f78,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| ? [X2,X3,X4] :
( sP0(X0,X4,X1)
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3
& X3 != X4 ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f79,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| ( sP0(X0,sK12(X0,X1),X1)
& sK10(X0,X1) = sK12(X0,X1)
& subset(X1,sK11(X0,X1))
& closed_subset(sK13(X0,X1),X0)
& sK11(X0,X1) = sK13(X0,X1)
& element(sK13(X0,X1),powerset(the_carrier(X0)))
& sK10(X0,X1) = sK11(X0,X1)
& sK11(X0,X1) != sK12(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13]),skolemize(X2,sK10(X0,X1)),skolemize(X3,sK11(X0,X1)),skolemize(X4,sK12(X0,X1)),skolemize(X5,sK13(X0,X1))],[f78]) ).
fof(f83,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ? [X7] :
! [X8] :
( ( ~ in(X8,X7)
| ? [X9] :
( ? [X10] :
( subset(X1,X8)
& closed_subset(X10,X0)
& X8 = X10
& element(X10,powerset(the_carrier(X0))) )
& X8 = X9
& in(X9,powerset(the_carrier(X0))) ) )
& ( ! [X9] :
( ! [X10] :
( ~ subset(X1,X8)
| ~ closed_subset(X10,X0)
| X8 != X10
| ~ element(X10,powerset(the_carrier(X0))) )
| X8 != X9
| ~ in(X9,powerset(the_carrier(X0))) )
| in(X8,X7) ) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f84,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ? [X2] :
! [X3] :
( ( ~ in(X3,X2)
| ? [X6] :
( ? [X7] :
( subset(X1,X3)
& closed_subset(X7,X0)
& X3 = X7
& element(X7,powerset(the_carrier(X0))) )
& X3 = X6
& in(X6,powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( ! [X5] :
( ~ subset(X1,X3)
| ~ closed_subset(X5,X0)
| X3 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
| X3 != X4
| ~ in(X4,powerset(the_carrier(X0))) )
| in(X3,X2) ) ) ),
inference(rectify,[],[f83]) ).
fof(f85,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ! [X3] :
( ( ~ in(X3,sK15(X0,X1))
| ( subset(X1,X3)
& closed_subset(sK17(X0,X1,X3),X0)
& sK17(X0,X1,X3) = X3
& element(sK17(X0,X1,X3),powerset(the_carrier(X0)))
& sK16(X0,X1,X3) = X3
& in(sK16(X0,X1,X3),powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( ! [X5] :
( ~ subset(X1,X3)
| ~ closed_subset(X5,X0)
| X3 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
| X3 != X4
| ~ in(X4,powerset(the_carrier(X0))) )
| in(X3,sK15(X0,X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X2,sK15(X0,X1)),skolemize(X6,sK16(X0,X1,X3)),skolemize(X7,sK17(X0,X1,X3))],[f84]) ).
fof(f86,plain,
element(sK3,powerset(the_carrier(sK2))),
inference(cnf_transformation,[],[f73]) ).
fof(f87,plain,
top_str(sK2),
inference(cnf_transformation,[],[f73]) ).
fof(f88,plain,
topological_space(sK2),
inference(cnf_transformation,[],[f73]) ).
fof(f89,plain,
! [X2] :
( in(sK4(X2),X2)
| subset(sK3,sK4(X2)) ),
inference(cnf_transformation,[],[f73]) ).
fof(f90,plain,
! [X2] :
( in(sK4(X2),X2)
| closed_subset(sK5(X2),sK2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f91,plain,
! [X2] :
( in(sK4(X2),X2)
| sK4(X2) = sK5(X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f92,plain,
! [X2] :
( in(sK4(X2),X2)
| element(sK5(X2),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f73]) ).
fof(f93,plain,
! [X2] :
( in(sK4(X2),X2)
| in(sK4(X2),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f73]) ).
fof(f94,plain,
! [X2,X4] :
( ~ in(sK4(X2),X2)
| ~ subset(sK3,sK4(X2))
| ~ closed_subset(X4,sK2)
| sK4(X2) != X4
| ~ element(X4,powerset(the_carrier(sK2)))
| ~ in(sK4(X2),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f73]) ).
fof(f134,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sP0(X0,sK12(X0,X1),X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f135,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK10(X0,X1) = sK12(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f140,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK10(X0,X1) = sK11(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f141,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK11(X0,X1) != sK12(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f146,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| subset(X1,X3) ),
inference(cnf_transformation,[],[f85]) ).
fof(f147,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| closed_subset(sK17(X0,X1,X3),X0) ),
inference(cnf_transformation,[],[f85]) ).
fof(f148,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| sK17(X0,X1,X3) = X3 ),
inference(cnf_transformation,[],[f85]) ).
fof(f149,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| element(sK17(X0,X1,X3),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f150,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| sK16(X0,X1,X3) = X3 ),
inference(cnf_transformation,[],[f85]) ).
fof(f151,plain,
! [X3,X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ in(X3,sK15(X0,X1))
| in(sK16(X0,X1,X3),powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f152,plain,
! [X3,X0,X1,X4,X5] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ subset(X1,X3)
| ~ closed_subset(X5,X0)
| X3 != X5
| ~ element(X5,powerset(the_carrier(X0)))
| X3 != X4
| ~ in(X4,powerset(the_carrier(X0)))
| in(X3,sK15(X0,X1)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
! [X2] :
( ~ in(sK4(X2),X2)
| ~ subset(sK3,sK4(X2))
| ~ closed_subset(sK4(X2),sK2)
| ~ element(sK4(X2),powerset(the_carrier(sK2)))
| ~ in(sK4(X2),powerset(the_carrier(sK2))) ),
inference(equality_resolution,[],[f94]) ).
fof(f154,plain,
! [X0,X1,X4,X5] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ subset(X1,X4)
| ~ closed_subset(X5,X0)
| X4 != X5
| ~ element(X5,powerset(the_carrier(X0)))
| ~ in(X4,powerset(the_carrier(X0)))
| in(X4,sK15(X0,X1)) ),
inference(equality_resolution,[],[f152]) ).
fof(f155,plain,
! [X0,X1,X5] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ~ subset(X1,X5)
| ~ closed_subset(X5,X0)
| ~ element(X5,powerset(the_carrier(X0)))
| ~ in(X5,powerset(the_carrier(X0)))
| in(X5,sK15(X0,X1)) ),
inference(equality_resolution,[],[f154]) ).
tcf(c_49,negated_conjecture,
! [X0: $i] :
( ~ subset(sK3,sK4(X0))
| ~ closed_subset(sK4(X0),sK2)
| ~ in(sK4(X0),X0)
| ~ element(sK4(X0),powerset(the_carrier(sK2)))
| ~ in(sK4(X0),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_50,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| in(sK4(X0),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| element(sK5(X0),powerset(the_carrier(sK2))) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| ( sK4(X0) = sK5(X0) ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_53,negated_conjecture,
! [X0: $i] :
( closed_subset(sK5(X0),sK2)
| in(sK4(X0),X0) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_54,negated_conjecture,
! [X0: $i] :
( subset(sK3,sK4(X0))
| in(sK4(X0),X0) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_55,negated_conjecture,
topological_space(sK2),
inference(cnf_transformation,[],[f88]) ).
tcf(c_56,negated_conjecture,
top_str(sK2),
inference(cnf_transformation,[],[f87]) ).
tcf(c_57,negated_conjecture,
element(sK3,powerset(the_carrier(sK2))),
inference(cnf_transformation,[],[f86]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X0,X1)
| ( sK11(X0,X1) != sK12(X0,X1) ) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] :
( ( sK11(X0,X1) = sK10(X0,X1) )
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i] :
( ( sK12(X0,X1) = sK10(X0,X1) )
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i] :
( sP0(X0,sK12(X0,X1),X1)
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| in(X0,sK15(X1,X2))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ subset(X2,X0)
| ~ closed_subset(X0,X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ element(X0,powerset(the_carrier(X1)))
| ~ in(X0,powerset(the_carrier(X1))) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| in(sK16(X1,X2,X0),powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| ( sK16(X1,X2,X0) = X0 )
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| element(sK17(X1,X2,X0),powerset(the_carrier(X1)))
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| ( sK17(X1,X2,X0) = X0 )
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| closed_subset(sK17(X1,X2,X0),X1)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X1,X2)
| subset(X2,X0)
| ~ top_str(X1)
| ~ topological_space(X1)
| ~ element(X2,powerset(the_carrier(X1)))
| ~ in(X0,sK15(X1,X2)) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_885,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| subset(X2,X1)
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_115]) ).
tcf(c_886,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| subset(X1,X0)
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_885]) ).
tcf(c_887,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| subset(X1,X0)
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_886,c_56,c_886]) ).
tcf(c_888,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| subset(X1,X0)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_887]) ).
tcf(c_901,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| closed_subset(sK17(X0,X2,X1),X0)
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_114]) ).
tcf(c_902,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| closed_subset(sK17(sK2,X1,X0),sK2)
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_901]) ).
tcf(c_904,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| closed_subset(sK17(sK2,X1,X0),sK2)
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_902,c_56,c_902]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| closed_subset(sK17(sK2,X1,X0),sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_904]) ).
tcf(c_919,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| ( sK17(X0,X2,X1) = X1 )
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_113]) ).
tcf(c_920,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_919]) ).
tcf(c_922,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_920,c_56,c_920]) ).
tcf(c_923,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_922]) ).
tcf(c_937,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| element(sK17(X0,X2,X1),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_112]) ).
tcf(c_938,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| element(sK17(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_937]) ).
tcf(c_940,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| element(sK17(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_938,c_56,c_938]) ).
tcf(c_941,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| element(sK17(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_940]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| ( sK16(X0,X2,X1) = X1 )
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_111]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK16(sK2,X1,X0) = X0 )
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_955]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK16(sK2,X1,X0) = X0 )
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_956,c_56,c_956]) ).
tcf(c_959,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK16(sK2,X1,X0) = X0 )
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_958]) ).
tcf(c_973,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| in(sK16(X0,X2,X1),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ in(X1,sK15(X0,X2))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_110]) ).
tcf(c_974,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK16(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(unflattening,[status(thm)],[c_973]) ).
tcf(c_976,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK16(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1))
| ~ element(X1,powerset(the_carrier(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_974,c_56,c_974]) ).
tcf(c_977,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK16(sK2,X1,X0),powerset(the_carrier(sK2)))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ in(X0,sK15(sK2,X1)) ),
inference(renaming,[status(thm)],[c_976]) ).
tcf(c_991,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0,X2)
| in(X1,sK15(X0,X2))
| ~ top_str(X0)
| ~ subset(X2,X1)
| ~ closed_subset(X1,X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ in(X1,powerset(the_carrier(X0)))
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_109]) ).
tcf(c_992,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(X0,sK15(sK2,X1))
| ~ top_str(sK2)
| ~ closed_subset(X0,sK2)
| ~ subset(X1,X0)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ element(X0,powerset(the_carrier(sK2)))
| ~ in(X0,powerset(the_carrier(sK2))) ),
inference(unflattening,[status(thm)],[c_991]) ).
tcf(c_994,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(X0,sK15(sK2,X1))
| ~ in(X0,powerset(the_carrier(sK2)))
| ~ element(X0,powerset(the_carrier(sK2)))
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ subset(X1,X0)
| ~ closed_subset(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_992,c_56,c_992]) ).
tcf(c_995,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(X0,sK15(sK2,X1))
| ~ closed_subset(X0,sK2)
| ~ subset(X1,X0)
| ~ element(X1,powerset(the_carrier(sK2)))
| ~ element(X0,powerset(the_carrier(sK2)))
| ~ in(X0,powerset(the_carrier(sK2))) ),
inference(renaming,[status(thm)],[c_994]) ).
tcf(c_5571,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| in(X1,sK15(sK2,X0))
| ~ closed_subset(X1,sK2)
| ~ element(X1,iPr_def_12)
| ~ element(X0,iPr_def_12)
| ~ in(X1,iPr_def_12)
| ~ subset(X0,X1) ),
inference(demodulation,[status(thm)],[c_995]) ).
tcf(c_5572,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| in(sK16(sK2,X1,X0),iPr_def_12)
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_977]) ).
tcf(c_5573,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK16(sK2,X1,X0) = X0 )
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_959]) ).
tcf(c_5574,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| element(sK17(sK2,X1,X0),iPr_def_12)
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_941]) ).
tcf(c_5575,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| ( sK17(sK2,X1,X0) = X0 )
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_923]) ).
tcf(c_5576,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| closed_subset(sK17(sK2,X1,X0),sK2)
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_905]) ).
tcf(c_5577,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X1)
| subset(X1,X0)
| ~ element(X1,iPr_def_12)
| ~ in(X0,sK15(sK2,X1)) ),
inference(demodulation,[status(thm)],[c_888]) ).
tcf(c_5578,negated_conjecture,
element(sK3,iPr_def_12),
inference(demodulation,[status(thm)],[c_57]) ).
tcf(c_5579,negated_conjecture,
! [X0: $i] :
( subset(sK3,sK4(X0))
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_5580,negated_conjecture,
! [X0: $i] :
( closed_subset(sK5(X0),sK2)
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_5581,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| ( sK4(X0) = sK5(X0) ) ),
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_5582,negated_conjecture,
! [X0: $i] :
( element(sK5(X0),iPr_def_12)
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_5583,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),iPr_def_12)
| in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_50]) ).
tcf(c_5584,negated_conjecture,
! [X0: $i] :
( ~ subset(sK3,sK4(X0))
| ~ closed_subset(sK4(X0),sK2)
| ~ element(sK4(X0),iPr_def_12)
| ~ in(sK4(X0),iPr_def_12)
| ~ in(sK4(X0),X0) ),
inference(demodulation,[status(thm)],[c_49]) ).
tcf(c_6163,plain,
! [X0: $i] :
( sP1(sK2,X0)
| subset(sK3,sK4(sK15(sK2,X0)))
| subset(X0,sK4(sK15(sK2,X0)))
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5579,c_5577]) ).
tcf(c_6221,plain,
( sP1(sK2,sK3)
| subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK3,iPr_def_12) ),
inference(equality_factoring,[status(thm)],[c_6163]) ).
tcf(c_6223,plain,
( sP1(sK2,sK3)
| subset(sK3,sK4(sK15(sK2,sK3))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6221,c_5578]) ).
tcf(c_6391,plain,
! [X0: $i] :
( sP1(sK2,X0)
| ( sK4(sK15(sK2,X0)) = sK5(sK15(sK2,X0)) )
| ( sK16(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5581,c_5573]) ).
tcf(c_6392,plain,
! [X0: $i] :
( sP1(sK2,X0)
| in(sK4(sK15(sK2,X0)),iPr_def_12)
| ( sK16(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5583,c_5573]) ).
tcf(c_6393,plain,
! [X0: $i] :
( sP1(sK2,X0)
| element(sK5(sK15(sK2,X0)),iPr_def_12)
| ( sK16(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5582,c_5573]) ).
tcf(c_6394,plain,
! [X0: $i] :
( sP1(sK2,X0)
| closed_subset(sK5(sK15(sK2,X0)),sK2)
| ( sK16(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5580,c_5573]) ).
tcf(c_6469,plain,
( sP1(sK2,sK3)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_5578,c_6391]) ).
tcf(c_6512,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6469,c_103]) ).
tcf(c_6514,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6469,c_98]) ).
tcf(c_6532,plain,
! [X0: $i] :
( sP1(sK2,X0)
| ( sK4(sK15(sK2,X0)) = sK5(sK15(sK2,X0)) )
| ( sK17(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5581,c_5575]) ).
tcf(c_6533,plain,
! [X0: $i] :
( sP1(sK2,X0)
| in(sK4(sK15(sK2,X0)),iPr_def_12)
| ( sK17(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5583,c_5575]) ).
tcf(c_6534,plain,
! [X0: $i] :
( sP1(sK2,X0)
| element(sK5(sK15(sK2,X0)),iPr_def_12)
| ( sK17(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5582,c_5575]) ).
tcf(c_6535,plain,
! [X0: $i] :
( sP1(sK2,X0)
| closed_subset(sK5(sK15(sK2,X0)),sK2)
| ( sK17(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5580,c_5575]) ).
tcf(c_6568,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6512,c_5572]) ).
tcf(c_6569,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6568,c_5578]) ).
tcf(c_6695,plain,
( sP1(sK2,sK3)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_5578,c_6532]) ).
tcf(c_6767,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6695,c_103]) ).
tcf(c_6769,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6695,c_98]) ).
tcf(c_6895,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6514,c_5572]) ).
tcf(c_6897,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6895,c_5578]) ).
tcf(c_6971,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| ( sK17(sK2,X0,X1) = X1 )
| ~ closed_subset(X1,sK2)
| ~ element(X1,iPr_def_12)
| ~ element(X0,iPr_def_12)
| ~ in(X1,iPr_def_12)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_5571,c_5575]) ).
tcf(c_6972,plain,
! [X0: $i,X1: $i] :
( sP1(sK2,X0)
| ( sK16(sK2,X0,X1) = X1 )
| ~ closed_subset(X1,sK2)
| ~ element(X1,iPr_def_12)
| ~ element(X0,iPr_def_12)
| ~ in(X1,iPr_def_12)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_5571,c_5573]) ).
tcf(c_7058,plain,
( sP1(sK2,sK3)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_6223,c_6971]) ).
tcf(c_7085,plain,
( sP1(sK2,sK3)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7058,c_5578]) ).
tcf(c_7137,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ sP1(sK2,sK3) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_7139,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ~ sP1(sK2,sK3) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_7140,plain,
( ~ sP1(sK2,sK3)
| ( sK11(sK2,sK3) != sK12(sK2,sK3) ) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_7252,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_6897,c_6897,c_7139]) ).
tcf(c_7253,plain,
( in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_7252]) ).
tcf(c_7414,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6767,c_5576]) ).
tcf(c_7415,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6767,c_5574]) ).
tcf(c_7416,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7415,c_5578]) ).
tcf(c_7422,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7414,c_5578]) ).
tcf(c_7460,plain,
( sP1(sK2,sK3)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_6223,c_6972]) ).
tcf(c_7487,plain,
( sP1(sK2,sK3)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7460,c_5578]) ).
tcf(c_7698,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7416,c_7137,c_7416]) ).
tcf(c_7699,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_7698]) ).
tcf(c_7750,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_7422,c_7137,c_7422]) ).
tcf(c_7751,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_7750]) ).
tcf(c_7756,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7751,c_5581]) ).
tcf(c_7768,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_7756,c_5584]) ).
tcf(c_7836,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_7768,c_6223,c_6569,c_7137,c_7699,c_7768]) ).
tcf(c_7841,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7836,c_5581]) ).
tcf(c_7850,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_7841,c_5580]) ).
tcf(c_7851,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7841,c_6535]) ).
tcf(c_7852,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7841,c_6534]) ).
tcf(c_7853,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7841,c_6394]) ).
tcf(c_7854,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7841,c_6393]) ).
tcf(c_7858,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7854,c_5578]) ).
tcf(c_7863,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7853,c_5578]) ).
tcf(c_7868,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7852,c_5578]) ).
tcf(c_7873,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7851,c_5578]) ).
tcf(c_7999,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7858,c_7137,c_7858]) ).
tcf(c_8000,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_7999]) ).
tcf(c_8042,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_7863,c_7137,c_7863]) ).
tcf(c_8043,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_8042]) ).
tcf(c_8052,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_8043,c_5584]) ).
tcf(c_8107,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7868,c_7137,c_7868]) ).
tcf(c_8108,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_8107]) ).
tcf(c_8148,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_7873,c_7137,c_7873]) ).
tcf(c_8149,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_8148]) ).
tcf(c_8487,plain,
( in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(instantiation,[status(thm)],[c_5581]) ).
tcf(c_8488,plain,
( in(sK4(sK15(sK2,sK3)),iPr_def_12)
| in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_5583]) ).
tcf(c_8571,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6769,c_5576]) ).
tcf(c_8572,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6769,c_5574]) ).
tcf(c_8573,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8572,c_5578]) ).
tcf(c_8579,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8571,c_5578]) ).
tcf(c_8770,plain,
! [X0: $i] :
( sP1(sK2,X0)
| ( sK4(sK15(sK2,X0)) = sK5(sK15(sK2,X0)) )
| ( sK16(sK2,X0,sK4(sK15(sK2,X0))) = sK4(sK15(sK2,X0)) )
| ~ element(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5581,c_5573]) ).
tcf(c_8908,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_8573,c_7139,c_8487,c_8573]) ).
tcf(c_8909,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_8908]) ).
tcf(c_8929,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_8579,c_7139,c_8487,c_8579]) ).
tcf(c_8930,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_8929]) ).
tcf(c_8939,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_8930,c_5584]) ).
tcf(c_9037,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(global_subsumption_just,[status(thm)],[c_8939,c_6223,c_7139,c_7253,c_8487,c_8909,c_8939]) ).
tcf(c_9046,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9037,c_6535]) ).
tcf(c_9047,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9037,c_6534]) ).
tcf(c_9048,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9037,c_6394]) ).
tcf(c_9049,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_9037,c_6393]) ).
tcf(c_9053,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9049,c_5578]) ).
tcf(c_9058,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9048,c_5578]) ).
tcf(c_9063,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9047,c_5578]) ).
tcf(c_9068,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9046,c_5578]) ).
tcf(c_9109,plain,
( sP1(sK2,sK3)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_5578,c_8770]) ).
tcf(c_9177,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_9058,c_7139,c_9058]) ).
tcf(c_9178,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_9177]) ).
tcf(c_9187,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9178,c_5584]) ).
tcf(c_9190,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_9178,c_7487]) ).
tcf(c_9292,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_9109,c_103]) ).
tcf(c_9360,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_9068,c_7139,c_9068]) ).
tcf(c_9361,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_9360]) ).
tcf(c_9370,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9361,c_5584]) ).
tcf(c_9520,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_8052,c_7137,c_7487,c_8000,c_8043]) ).
tcf(c_9529,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6533,c_9520]) ).
tcf(c_9530,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6392,c_9520]) ).
tcf(c_9532,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9530,c_5578]) ).
tcf(c_9539,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9529,c_5578]) ).
tcf(c_9547,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_9532,c_7137,c_9532]) ).
tcf(c_9548,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_9547]) ).
tcf(c_9553,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9548,c_5572]) ).
tcf(c_9555,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9553,c_5578]) ).
tcf(c_9565,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9555,c_7137,c_8488,c_9555]) ).
tcf(c_9566,plain,
( in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(renaming,[status(thm)],[c_9565]) ).
tcf(c_9576,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_9539,c_7085,c_7137,c_8108,c_8149,c_9566]) ).
tcf(c_9577,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_9576]) ).
tcf(c_9582,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9577,c_5576]) ).
tcf(c_9583,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9577,c_5574]) ).
tcf(c_9584,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9583,c_5578]) ).
tcf(c_9589,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9582,c_5578]) ).
tcf(c_9594,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9584,c_7137,c_9584]) ).
tcf(c_9595,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_9594]) ).
tcf(c_9604,plain,
( element(sK5(sK15(sK2,sK3)),iPr_def_12)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_5582,c_9595]) ).
tcf(c_9666,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_7841,c_9604]) ).
tcf(c_9693,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_9589,c_7137,c_7850,c_9589]) ).
tcf(c_9694,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(renaming,[status(thm)],[c_9693]) ).
tcf(c_9701,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_9694,c_5584]) ).
tcf(c_9721,plain,
( ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_9701,c_6223,c_7137,c_9566,c_9595,c_9701]) ).
tcf(c_9729,plain,
( element(sK5(sK15(sK2,sK3)),iPr_def_12)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_5582,c_9721]) ).
tcf(c_9731,plain,
( subset(sK3,sK4(sK15(sK2,sK3)))
| ( sK12(sK2,sK3) = sK10(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_5579,c_9721]) ).
tcf(c_9732,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_5571,c_9721]) ).
tcf(c_9741,plain,
( sP1(sK2,sK3)
| ( sK12(sK2,sK3) = sK10(sK2,sK3) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9732,c_5578]) ).
tcf(c_9748,plain,
sK12(sK2,sK3) = sK10(sK2,sK3),
inference(global_subsumption_just,[status(thm)],[c_9292,c_7137,c_7850,c_9566,c_9589,c_9666,c_9731,c_9741]) ).
tcf(c_9750,plain,
sK12(sK2,sK3) = sK10(sK2,sK3),
inference(global_subsumption_just,[status(thm)],[c_9729,c_9748]) ).
tcf(c_9759,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(demodulation,[status(thm)],[c_9178,c_9750]) ).
tcf(c_9762,plain,
( ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(demodulation,[status(thm)],[c_9037,c_9750]) ).
tcf(c_10358,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9187,c_7139,c_9053,c_9190]) ).
tcf(c_10360,plain,
( ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_10358,c_9750]) ).
tcf(c_10372,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6392,c_10360]) ).
tcf(c_10373,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10372,c_5578]) ).
tcf(c_10394,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_10373,c_98]) ).
tcf(c_10395,plain,
( ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(light_normalisation,[status(thm)],[c_10394,c_9750]) ).
tcf(c_10400,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_9370,c_7085,c_7139,c_9063,c_9361]) ).
tcf(c_10402,plain,
( ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_10400,c_9750]) ).
tcf(c_10413,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6533,c_10402]) ).
tcf(c_10415,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10413,c_5578]) ).
tcf(c_10446,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10395,c_5572]) ).
tcf(c_10448,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10446,c_5578]) ).
tcf(c_10589,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_10415,c_98]) ).
tcf(c_10591,plain,
( ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(light_normalisation,[status(thm)],[c_10589,c_9750]) ).
tcf(c_10594,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_10448,c_8488,c_10448]) ).
tcf(c_10791,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10591,c_5576]) ).
tcf(c_10792,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10591,c_5574]) ).
tcf(c_10793,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10792,c_5578]) ).
tcf(c_10798,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10791,c_5578]) ).
tcf(c_10999,plain,
( sP1(sK2,sK3)
| element(sK5(sK15(sK2,sK3)),iPr_def_12)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_5582,c_10793]) ).
fof(f67,definition,
! [X0,X4,X1] :
( ~ sP0(X0,X4,X1)
| ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f68,definition,
! [X0,X1] :
( ~ sP1(X0,X1)
| ? [X2,X3,X4] :
( sP0(X0,X4,X1)
& X2 = X4
& ? [X5] :
( subset(X1,X3)
& closed_subset(X5,X0)
& X5 = X3
& element(X5,powerset(the_carrier(X0))) )
& X2 = X3
& X3 != X4 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f69,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0)
| sP1(X0,X1)
| ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( ? [X10] :
( subset(X1,X8)
& closed_subset(X10,X0)
& X8 = X10
& element(X10,powerset(the_carrier(X0))) )
& X8 = X9
& in(X9,powerset(the_carrier(X0))) ) ) ),
inference(definition_folding,[],[f66,f68,f67]) ).
fof(f80,plain,
! [X0,X4,X1] :
( ~ sP0(X0,X4,X1)
| ? [X6] :
( subset(X1,X4)
& closed_subset(X6,X0)
& X6 = X4
& element(X6,powerset(the_carrier(X0))) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ? [X3] :
( subset(X2,X1)
& closed_subset(X3,X0)
& X1 = X3
& element(X3,powerset(the_carrier(X0))) ) ),
inference(rectify,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( subset(X2,X1)
& closed_subset(sK14(X0,X1,X2),X0)
& sK14(X0,X1,X2) = X1
& element(sK14(X0,X1,X2),powerset(the_carrier(X0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1,X2))],[f81]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| closed_subset(sK14(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f144,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| sK14(X0,X1,X2) = X1 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK14(X0,X1,X2) = X1 )
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( closed_subset(sK14(X0,X1,X2),X0)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( closed_subset(sK14(X3,X2,X4),X3)
| ~ sP1(X0,X1)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK12(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_104,c_107]) ).
tcf(c_851,plain,
! [X0: $i,X1: $i] :
( closed_subset(sK14(X0,sK12(X0,X1),X1),X0)
| ~ sP1(X0,X1) ),
inference(unflattening,[status(thm)],[c_850]) ).
tcf(c_859,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( sK14(X3,X2,X4) = X2 )
| ~ sP1(X0,X1)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK12(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_104,c_106]) ).
tcf(c_860,plain,
! [X0: $i,X1: $i] :
( ( sK14(X0,sK12(X0,X1),X1) = sK12(X0,X1) )
| ~ sP1(X0,X1) ),
inference(unflattening,[status(thm)],[c_859]) ).
tcf(c_6598,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6469,c_860]) ).
tcf(c_6766,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_6695,c_860]) ).
tcf(c_7134,plain,
( ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ sP1(sK2,sK3) ),
inference(instantiation,[status(thm)],[c_860]) ).
tcf(c_7309,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6598,c_5572]) ).
tcf(c_7311,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7309,c_5578]) ).
tcf(c_7814,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7311,c_7134,c_7311]) ).
tcf(c_7815,plain,
( in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(renaming,[status(thm)],[c_7814]) ).
tcf(c_8541,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6766,c_5576]) ).
tcf(c_8542,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_6766,c_5574]) ).
tcf(c_8543,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8542,c_5578]) ).
tcf(c_8549,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8541,c_5578]) ).
tcf(c_8962,plain,
( ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_8543,c_7134,c_8487,c_8543]) ).
tcf(c_8963,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) ) ),
inference(renaming,[status(thm)],[c_8962]) ).
tcf(c_8996,plain,
( ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_8549,c_7134,c_8487,c_8549]) ).
tcf(c_8997,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) ) ),
inference(renaming,[status(thm)],[c_8996]) ).
tcf(c_9006,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_8997,c_5584]) ).
tcf(c_10342,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK14(sK2,sK12(sK2,sK3),sK3) = sK12(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_9006,c_6223,c_7134,c_7815,c_8487,c_8963,c_9006]) ).
tcf(c_10349,plain,
( closed_subset(sK12(sK2,sK3),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ sP1(sK2,sK3) ),
inference(superposition,[status(thm)],[c_10342,c_851]) ).
tcf(c_10512,plain,
( ~ sP1(sK2,sK3)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(global_subsumption_just,[status(thm)],[c_10349,c_7140,c_9762]) ).
tcf(c_10513,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ sP1(sK2,sK3) ),
inference(renaming,[status(thm)],[c_10512]) ).
tcf(c_10518,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6695,c_10513]) ).
tcf(c_10519,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6469,c_10513]) ).
tcf(c_10534,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10518,c_5576]) ).
tcf(c_10535,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10518,c_5574]) ).
tcf(c_10536,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10535,c_5578]) ).
tcf(c_10541,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10534,c_5578]) ).
tcf(c_10568,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10519,c_5572]) ).
tcf(c_10570,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10568,c_5578]) ).
tcf(c_10609,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_10536,c_8487,c_10513,c_10536]) ).
tcf(c_10610,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_10609]) ).
tcf(c_10627,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_10541,c_8487,c_10513,c_10541]) ).
tcf(c_10628,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_10627]) ).
tcf(c_10635,plain,
( ( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10628,c_5584]) ).
tcf(c_10655,plain,
sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_10570,c_6223,c_8487,c_10513,c_10570,c_10610,c_10635]) ).
tcf(c_10663,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10655,c_5580]) ).
tcf(c_10664,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10655,c_6535]) ).
tcf(c_10665,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10655,c_6534]) ).
tcf(c_10666,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10655,c_6394]) ).
tcf(c_10667,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_10655,c_6393]) ).
tcf(c_10670,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10667,c_5578]) ).
tcf(c_10674,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10666,c_5578]) ).
tcf(c_10678,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10665,c_5578]) ).
tcf(c_10682,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10664,c_5578]) ).
tcf(c_10831,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_10674,c_7140,c_9759,c_10674]) ).
tcf(c_10832,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_10831]) ).
tcf(c_10839,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10832,c_5584]) ).
tcf(c_10959,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
inference(global_subsumption_just,[status(thm)],[c_10682,c_7140,c_10591,c_10682]) ).
tcf(c_10960,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_10959]) ).
tcf(c_10967,plain,
( ( sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10960,c_5584]) ).
tcf(c_11009,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(light_normalisation,[status(thm)],[c_10999,c_10655]) ).
tcf(c_11016,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_10798,c_10663,c_10798]) ).
tcf(c_11026,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_11016,c_5584]) ).
tcf(c_11059,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_11026,c_6223,c_10594,c_11009,c_11026]) ).
tcf(c_11072,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ element(sK3,iPr_def_12)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_5571,c_11059]) ).
tcf(c_11076,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) )
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11072,c_5578]) ).
tcf(c_11091,plain,
( sP1(sK2,sK3)
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(global_subsumption_just,[status(thm)],[c_11076,c_6223,c_10594,c_11009,c_11016,c_11076]) ).
tcf(c_11100,plain,
( ( sK11(sK2,sK3) = sK10(sK2,sK3) )
| ( sK11(sK2,sK3) = sK12(sK2,sK3) ) ),
inference(superposition,[status(thm)],[c_11091,c_98]) ).
tcf(c_11101,plain,
sK11(sK2,sK3) = sK12(sK2,sK3),
inference(light_normalisation,[status(thm)],[c_11100,c_9750]) ).
tcf(c_11106,plain,
( ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_10839,c_7140,c_7487,c_10674,c_10670,c_11101]) ).
tcf(c_11114,plain,
( sP1(sK2,sK3)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) )
| ~ element(sK3,iPr_def_12) ),
inference(superposition,[status(thm)],[c_6392,c_11106]) ).
tcf(c_11115,plain,
( sP1(sK2,sK3)
| ( sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11114,c_5578]) ).
tcf(c_11124,plain,
sK16(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_11115,c_7140,c_11101,c_11115]) ).
tcf(c_11127,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_11124,c_5572]) ).
tcf(c_11129,plain,
( sP1(sK2,sK3)
| in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11127,c_5578]) ).
tcf(c_11137,plain,
in(sK4(sK15(sK2,sK3)),iPr_def_12),
inference(global_subsumption_just,[status(thm)],[c_11129,c_7140,c_8488,c_11101,c_11129]) ).
tcf(c_11141,plain,
~ sP1(sK2,sK3),
inference(superposition,[status(thm)],[c_11101,c_97]) ).
tcf(c_11149,plain,
subset(sK3,sK4(sK15(sK2,sK3))),
inference(backward_subsumption_resolution,[status(thm)],[c_6223,c_11141]) ).
tcf(c_11187,plain,
sK17(sK2,sK3,sK4(sK15(sK2,sK3))) = sK4(sK15(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_10967,c_7085,c_7140,c_10682,c_10678,c_11101,c_11137]) ).
tcf(c_11189,plain,
( sP1(sK2,sK3)
| closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_11187,c_5576]) ).
tcf(c_11190,plain,
( sP1(sK2,sK3)
| element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ element(sK3,iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_11187,c_5574]) ).
tcf(c_11191,plain,
( element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11190,c_11141,c_5578]) ).
tcf(c_11194,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11189,c_11141,c_5578]) ).
tcf(c_11203,plain,
( element(sK5(sK15(sK2,sK3)),iPr_def_12)
| element(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_5582,c_11191]) ).
tcf(c_11211,plain,
element(sK4(sK15(sK2,sK3)),iPr_def_12),
inference(light_normalisation,[status(thm)],[c_11203,c_10655]) ).
tcf(c_11212,plain,
closed_subset(sK4(sK15(sK2,sK3)),sK2),
inference(global_subsumption_just,[status(thm)],[c_11194,c_10663,c_11194]) ).
tcf(c_11215,plain,
( ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(superposition,[status(thm)],[c_11212,c_5584]) ).
tcf(c_11218,plain,
( ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11215,c_11149,c_11137]) ).
tcf(c_11314,plain,
~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_11218,c_11211,c_11218]) ).
tcf(c_11321,plain,
( sP1(sK2,sK3)
| ~ element(sK3,iPr_def_12)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK4(sK15(sK2,sK3)),iPr_def_12)
| ~ in(sK4(sK15(sK2,sK3)),iPr_def_12) ),
inference(superposition,[status(thm)],[c_5571,c_11314]) ).
tcf(c_11324,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_11321,c_11141,c_5578,c_11149,c_11212,c_11211,c_11137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 13:42:34 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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.11/0.44
% 0.11/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.44
% 0.11/0.44 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 3.51/1.75 % SZS status Started for theBenchmark.p
% 3.51/1.75 % SZS status Theorem for theBenchmark.p
% 3.51/1.75
% 3.51/1.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.51/1.75
% 3.51/1.75 % ------ iProver source info
% 3.51/1.75
% 3.51/1.75 % git: date: 2026-07-19 20:42:38 +0200
% 3.51/1.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.51/1.75 % git: non_committed_changes: false
% 3.51/1.75
% 3.51/1.75 % ------ Parsing...
% 3.51/1.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.51/1.75
% 3.51/1.75 % ------ Preprocessing... sup_sim: 0 sf_s rm: 35 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 9 0s sf_e pe_s pe_e %
% 3.51/1.75
% 3.51/1.75 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.51/1.75
% 3.51/1.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.51/1.75 % ------ Proving...
% 3.51/1.75 % ------ Problem Properties
% 3.51/1.75
% 3.51/1.75 %
% 3.51/1.75 % clauses 38
% 3.51/1.75 % conjectures 7
% 3.51/1.75 % EPR 6
% 3.51/1.75 % Horn 25
% 3.51/1.75 % unary 11
% 3.51/1.75 % binary 19
% 3.51/1.75 % lits 85
% 3.51/1.75 % lits eq 11
% 3.51/1.75 % fd_pure 0
% 3.51/1.75 % fd_pseudo 0
% 3.51/1.75 % fd_cond 0
% 3.51/1.75 % fd_pseudo_cond 0
% 3.51/1.75 % AC symbols 0
% 3.51/1.75
% 3.51/1.75 % ------ Schedule dynamic 5 is on
% 3.51/1.75
% 3.51/1.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.51/1.75
% 3.51/1.75
% 3.51/1.75 % ------
% 3.51/1.75 % Current options:
% 3.51/1.75 % ------
% 3.51/1.75
% 3.51/1.75
% 3.51/1.75 %
% 3.51/1.75
% 3.51/1.75 % ------ Proving...
% 3.51/1.75 %
% 3.51/1.75
% 3.51/1.75 % SZS status Theorem for theBenchmark.p
% 3.51/1.75
% 3.51/1.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.51/1.76
% 3.51/1.76
%------------------------------------------------------------------------------