%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU128+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 : n011.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:55:30 PM UTC 2026
% Result : Theorem 3.81s 21.34s
% Output : CNFRefutation 3.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 15
% Syntax : Number of formulae : 758 ( 77 unt; 1 def)
% Number of atoms : 2906 ( 241 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 2038 ( 847 ~;1144 |; 38 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-3 aty)
% Number of variables : 1370 ( 2 sgn1357 !; 13 ?;1244 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f2,axiom,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f3,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f4,axiom,
! [X0,X1,X2] :
( X2 = set_intersection2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X1)
& in(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f7,axiom,
empty(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f8,axiom,
! [X0,X1] : set_intersection2(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
fof(f9,axiom,
? [X0] : empty(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(f10,axiom,
? [X0] : ~ empty(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f11,axiom,
! [X0,X1] : subset(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f12,conjecture,
! [X0,X1,X2] :
( ( subset(X0,X2)
& subset(X0,X1) )
=> subset(X0,set_intersection2(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_xboole_1) ).
fof(f13,negated_conjecture,
~ ! [X0,X1,X2] :
( ( subset(X0,X2)
& subset(X0,X1) )
=> subset(X0,set_intersection2(X1,X2)) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f14,axiom,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_boole) ).
fof(f15,axiom,
! [X0] :
( empty(X0)
=> X0 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(f16,axiom,
! [X0,X1] :
~ ( empty(X1)
& in(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f17,axiom,
! [X0,X1] :
~ ( empty(X1)
& X0 != X1
& empty(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(f18,plain,
! [X0] : set_intersection2(X0,X0) = X0,
inference(rectify,[],[f8]) ).
fof(f19,plain,
! [X0] : subset(X0,X0),
inference(rectify,[],[f11]) ).
fof(f20,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f21,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f22,plain,
? [X0,X1,X2] :
( subset(X0,X2)
& subset(X0,X1)
& ~ subset(X0,set_intersection2(X1,X2)) ),
inference(ennf_transformation,[],[f13]) ).
fof(f23,plain,
? [X0,X1,X2] :
( subset(X0,X2)
& subset(X0,X1)
& ~ subset(X0,set_intersection2(X1,X2)) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(ennf_transformation,[],[f15]) ).
fof(f25,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f26,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f27,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X2] :
( ~ in(X2,X0)
| in(X2,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f28,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ? [X2] :
( in(X2,X0)
& ~ in(X2,X1) )
| subset(X0,X1) ) ),
inference(rectify,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( ( ~ subset(X0,X1)
| ! [X3] :
( ~ in(X3,X0)
| in(X3,X1) ) )
& ( ( in(sK0(X0,X1),X0)
& ~ in(sK0(X0,X1),X1) )
| subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f28]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ( set_intersection2(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| ( in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| ~ in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_intersection2(X0,X1) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( set_intersection2(X0,X1) != X2
| ! [X3] :
( ( ~ in(X3,X2)
| ( in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| ~ in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_intersection2(X0,X1) ) ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( set_intersection2(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| ( in(X4,X1)
& in(X4,X0) ) )
& ( ~ in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ) ) )
& ( ? [X3] :
( ( in(X3,X2)
| ( in(X3,X1)
& in(X3,X0) ) )
& ( ~ in(X3,X2)
| ~ in(X3,X1)
| ~ in(X3,X0) ) )
| X2 = set_intersection2(X0,X1) ) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ( set_intersection2(X0,X1) != X2
| ! [X4] :
( ( ~ in(X4,X2)
| ( in(X4,X1)
& in(X4,X0) ) )
& ( ~ in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ) ) )
& ( ( ( in(sK1(X0,X1,X2),X2)
| ( in(sK1(X0,X1,X2),X1)
& in(sK1(X0,X1,X2),X0) ) )
& ( ~ in(sK1(X0,X1,X2),X2)
| ~ in(sK1(X0,X1,X2),X1)
| ~ in(sK1(X0,X1,X2),X0) ) )
| X2 = set_intersection2(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f32]) ).
fof(f34,plain,
empty(sK2),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f9]) ).
fof(f35,plain,
~ empty(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f10]) ).
fof(f36,plain,
( subset(sK4,sK6)
& subset(sK4,sK5)
& ~ subset(sK4,set_intersection2(sK5,sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f23]) ).
fof(f37,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f40,plain,
! [X0,X1] :
( in(sK0(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f41,plain,
! [X0,X1] :
( ~ in(sK0(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f42,plain,
! [X2,X0,X1,X4] :
( set_intersection2(X0,X1) != X2
| ~ in(X4,X2)
| in(X4,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f43,plain,
! [X2,X0,X1,X4] :
( set_intersection2(X0,X1) != X2
| ~ in(X4,X2)
| in(X4,X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f44,plain,
! [X2,X0,X1,X4] :
( set_intersection2(X0,X1) != X2
| ~ in(X4,X1)
| ~ in(X4,X0)
| in(X4,X2) ),
inference(cnf_transformation,[],[f33]) ).
fof(f45,plain,
! [X2,X0,X1] :
( in(sK1(X0,X1,X2),X2)
| in(sK1(X0,X1,X2),X1)
| set_intersection2(X0,X1) = X2 ),
inference(cnf_transformation,[],[f33]) ).
fof(f46,plain,
! [X2,X0,X1] :
( in(sK1(X0,X1,X2),X2)
| in(sK1(X0,X1,X2),X0)
| set_intersection2(X0,X1) = X2 ),
inference(cnf_transformation,[],[f33]) ).
fof(f47,plain,
! [X2,X0,X1] :
( ~ in(sK1(X0,X1,X2),X2)
| ~ in(sK1(X0,X1,X2),X1)
| ~ in(sK1(X0,X1,X2),X0)
| set_intersection2(X0,X1) = X2 ),
inference(cnf_transformation,[],[f33]) ).
fof(f48,plain,
empty(empty_set),
inference(cnf_transformation,[],[f7]) ).
fof(f49,plain,
! [X0] : set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[],[f18]) ).
fof(f50,plain,
empty(sK2),
inference(cnf_transformation,[],[f34]) ).
fof(f51,plain,
~ empty(sK3),
inference(cnf_transformation,[],[f35]) ).
fof(f52,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[],[f19]) ).
fof(f53,plain,
subset(sK4,sK6),
inference(cnf_transformation,[],[f36]) ).
fof(f54,plain,
subset(sK4,sK5),
inference(cnf_transformation,[],[f36]) ).
fof(f55,plain,
~ subset(sK4,set_intersection2(sK5,sK6)),
inference(cnf_transformation,[],[f36]) ).
fof(f56,plain,
! [X0] : empty_set = set_intersection2(X0,empty_set),
inference(cnf_transformation,[],[f14]) ).
fof(f57,plain,
! [X0] :
( ~ empty(X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f24]) ).
fof(f58,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f59,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[],[f26]) ).
fof(f60,plain,
! [X0,X1,X4] :
( ~ in(X4,X1)
| ~ in(X4,X0)
| in(X4,set_intersection2(X0,X1)) ),
inference(equality_resolution,[],[f44]) ).
fof(f61,plain,
! [X0,X1,X4] :
( ~ in(X4,set_intersection2(X0,X1))
| in(X4,X0) ),
inference(equality_resolution,[],[f43]) ).
fof(f62,plain,
! [X0,X1,X4] :
( ~ in(X4,set_intersection2(X0,X1))
| in(X4,X1) ),
inference(equality_resolution,[],[f42]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[],[f38]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ in(sK0(X0,X1),X1) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),X0) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| ~ subset(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( set_intersection2(X0,X1) = X2 )
| ~ in(sK1(X0,X1,X2),X2)
| ~ in(sK1(X0,X1,X2),X1)
| ~ in(sK1(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,X2),X2)
| in(sK1(X0,X1,X2),X0)
| ( set_intersection2(X0,X1) = X2 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,X2),X2)
| in(sK1(X0,X1,X2),X1)
| ( set_intersection2(X0,X1) = X2 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_intersection2(X2,X1))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X1)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,X2)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_60,plain,
empty(empty_set),
inference(cnf_transformation,[],[f48]) ).
tcf(c_61,plain,
! [X0: $i] : set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[],[f49]) ).
tcf(c_62,plain,
empty(sK2),
inference(cnf_transformation,[],[f50]) ).
tcf(c_63,plain,
~ empty(sK3),
inference(cnf_transformation,[],[f51]) ).
tcf(c_64,plain,
! [X0: $i] : subset(X0,X0),
inference(cnf_transformation,[],[f52]) ).
tcf(c_65,negated_conjecture,
~ subset(sK4,set_intersection2(sK5,sK6)),
inference(cnf_transformation,[],[f55]) ).
tcf(c_66,negated_conjecture,
subset(sK4,sK5),
inference(cnf_transformation,[],[f54]) ).
tcf(c_67,negated_conjecture,
subset(sK4,sK6),
inference(cnf_transformation,[],[f53]) ).
tcf(c_68,plain,
! [X0: $i] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[],[f56]) ).
tcf(c_69,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ~ empty(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ empty(X1)
| ~ empty(X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_324,definition,
iPr_def_10 = set_intersection2(sK5,sK6),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_325,negated_conjecture,
subset(sK4,sK6),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_326,negated_conjecture,
subset(sK4,sK5),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_327,negated_conjecture,
~ subset(sK4,iPr_def_10),
inference(demodulation,[status(thm)],[c_65,c_324]) ).
tcf(c_587,plain,
! [X0: $i] : set_intersection2(empty_set,X0) = empty_set,
inference(superposition,[status(thm)],[c_50,c_68]) ).
tcf(c_594,plain,
empty_set = sK2,
inference(superposition,[status(thm)],[c_62,c_69]) ).
tcf(c_612,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ in(X0,sK0(X0,X1)) ),
inference(superposition,[status(thm)],[c_52,c_49]) ).
tcf(c_613,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_52,c_70]) ).
tcf(c_622,plain,
~ empty(sK4),
inference(superposition,[status(thm)],[c_613,c_327]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| in(sK0(set_intersection2(X0,X1),X2),X0) ),
inference(superposition,[status(thm)],[c_52,c_58]) ).
tcf(c_636,plain,
! [X0: $i] :
( in(X0,sK5)
| ~ in(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_324,c_58]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i] :
( in(X0,X1)
| ~ in(X0,empty_set) ),
inference(superposition,[status(thm)],[c_68,c_58]) ).
tcf(c_651,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_52,c_636]) ).
tcf(c_659,plain,
! [X0: $i,X1: $i] :
( subset(empty_set,X0)
| in(sK0(empty_set,X0),X1) ),
inference(superposition,[status(thm)],[c_52,c_637]) ).
tcf(c_666,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_651,c_49]) ).
tcf(c_667,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(sK5) ),
inference(superposition,[status(thm)],[c_651,c_70]) ).
tcf(c_668,plain,
subset(iPr_def_10,sK5),
inference(superposition,[status(thm)],[c_651,c_51]) ).
tcf(c_681,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| in(sK0(X0,X2),X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_52,c_53]) ).
tcf(c_682,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| in(sK0(iPr_def_10,X1),X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_651,c_53]) ).
tcf(c_694,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| in(sK0(set_intersection2(X0,X1),X2),X1) ),
inference(superposition,[status(thm)],[c_52,c_59]) ).
tcf(c_698,plain,
! [X0: $i] :
( in(X0,sK6)
| ~ in(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_324,c_59]) ).
tcf(c_722,plain,
! [X0: $i] :
( in(X0,iPr_def_10)
| ~ in(X0,sK6)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_324,c_57]) ).
tcf(c_725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X3,X2)
| ~ in(X3,X1)
| ~ in(X3,X0)
| ~ subset(set_intersection2(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_57,c_53]) ).
tcf(c_726,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ in(X2,X1)
| ~ in(X2,X0)
| ~ in(set_intersection2(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_57,c_49]) ).
tcf(c_727,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ in(X2,X1)
| ~ in(X2,X0)
| ~ empty(set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_57,c_70]) ).
tcf(c_728,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,set_intersection2(X1,X2))
| ~ in(sK0(X0,set_intersection2(X1,X2)),X2)
| ~ in(sK0(X0,set_intersection2(X1,X2)),X1) ),
inference(superposition,[status(thm)],[c_57,c_51]) ).
tcf(c_755,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X2,X3,X0),X2)
| in(sK1(X2,X3,X0),X1)
| ( set_intersection2(X2,X3) = X0 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_55,c_53]) ).
tcf(c_756,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X2,X0),X1)
| ( set_intersection2(X1,X2) = X0 )
| ~ in(X0,sK1(X1,X2,X0)) ),
inference(superposition,[status(thm)],[c_55,c_49]) ).
tcf(c_757,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X2,X0),X1)
| ( set_intersection2(X1,X2) = X0 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_55,c_70]) ).
tcf(c_758,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,X1,set_intersection2(X2,X3)),X3)
| in(sK1(X0,X1,set_intersection2(X2,X3)),X0)
| ( set_intersection2(X0,X1) = set_intersection2(X2,X3) ) ),
inference(superposition,[status(thm)],[c_55,c_59]) ).
tcf(c_759,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,X1,set_intersection2(X2,X3)),X2)
| in(sK1(X0,X1,set_intersection2(X2,X3)),X0)
| ( set_intersection2(X0,X1) = set_intersection2(X2,X3) ) ),
inference(superposition,[status(thm)],[c_55,c_58]) ).
tcf(c_760,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,iPr_def_10),sK5)
| in(sK1(X0,X1,iPr_def_10),X0)
| ( set_intersection2(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_55,c_636]) ).
tcf(c_761,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,empty_set),X2)
| in(sK1(X0,X1,empty_set),X0)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_55,c_637]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,X2,X3),X3)
| in(sK1(X0,X2,X3),X1)
| ( set_intersection2(X0,X2) = X3 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_55,c_53]) ).
tcf(c_763,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,X2),X2)
| ( set_intersection2(X0,X1) = X2 )
| ~ in(X0,sK1(X0,X1,X2)) ),
inference(superposition,[status(thm)],[c_55,c_49]) ).
tcf(c_764,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,X2),X2)
| ( set_intersection2(X0,X1) = X2 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_55,c_70]) ).
tcf(c_765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(set_intersection2(X0,X1),X2,X3),X3)
| in(sK1(set_intersection2(X0,X1),X2,X3),X1)
| ( set_intersection2(set_intersection2(X0,X1),X2) = X3 ) ),
inference(superposition,[status(thm)],[c_55,c_59]) ).
tcf(c_766,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(set_intersection2(X0,X1),X2,X3),X3)
| in(sK1(set_intersection2(X0,X1),X2,X3),X0)
| ( set_intersection2(set_intersection2(X0,X1),X2) = X3 ) ),
inference(superposition,[status(thm)],[c_55,c_58]) ).
tcf(c_767,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X0,X1),sK5)
| in(sK1(iPr_def_10,X0,X1),X1)
| ( set_intersection2(iPr_def_10,X0) = X1 ) ),
inference(superposition,[status(thm)],[c_55,c_636]) ).
tcf(c_768,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(empty_set,X0,X1),X2)
| in(sK1(empty_set,X0,X1),X1)
| ( set_intersection2(empty_set,X0) = X1 ) ),
inference(superposition,[status(thm)],[c_55,c_637]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,X0),X0)
| ( set_intersection2(X0,X1) = X0 ) ),
inference(equality_factoring,[status(thm)],[c_55]) ).
tcf(c_779,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(empty_set,X1,X0),X2)
| in(sK1(empty_set,X1,X0),X0)
| ( X0 = empty_set ) ),
inference(light_normalisation,[status(thm)],[c_768,c_587]) ).
tcf(c_822,plain,
( subset(sK4,iPr_def_10)
| in(sK0(sK4,iPr_def_10),sK4) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_830,plain,
! [X0: $i] :
( in(sK0(sK4,iPr_def_10),X0)
| ~ subset(sK4,X0)
| ~ in(sK0(sK4,iPr_def_10),sK4) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_843,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_52,c_698]) ).
tcf(c_844,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X0,X1),sK6)
| in(sK1(iPr_def_10,X0,X1),X1)
| ( set_intersection2(iPr_def_10,X0) = X1 ) ),
inference(superposition,[status(thm)],[c_55,c_698]) ).
tcf(c_845,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,iPr_def_10),sK6)
| in(sK1(X0,X1,iPr_def_10),X0)
| ( set_intersection2(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_55,c_698]) ).
tcf(c_864,plain,
! [X0: $i] : subset(empty_set,X0),
inference(superposition,[status(thm)],[c_659,c_51]) ).
tcf(c_874,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| in(sK0(iPr_def_10,X1),X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_843,c_53]) ).
tcf(c_875,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_843,c_49]) ).
tcf(c_876,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(sK6) ),
inference(superposition,[status(thm)],[c_843,c_70]) ).
tcf(c_877,plain,
subset(iPr_def_10,sK6),
inference(superposition,[status(thm)],[c_843,c_51]) ).
tcf(c_917,plain,
! [X0: $i] :
( subset(sK5,X0)
| in(sK0(sK5,X0),iPr_def_10)
| ~ in(sK0(sK5,X0),sK6) ),
inference(superposition,[status(thm)],[c_52,c_722]) ).
tcf(c_918,plain,
! [X0: $i,X1: $i] :
( in(sK1(sK5,X0,X1),iPr_def_10)
| in(sK1(sK5,X0,X1),X1)
| ( set_intersection2(sK5,X0) = X1 )
| ~ in(sK1(sK5,X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_55,c_722]) ).
tcf(c_919,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),iPr_def_10)
| in(sK1(X0,X1,sK5),X0)
| ( set_intersection2(X0,X1) = sK5 )
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_55,c_722]) ).
tcf(c_920,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),iPr_def_10)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_651,c_722]) ).
tcf(c_943,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| in(sK0(set_intersection2(X0,X1),X2),X1) ),
inference(superposition,[status(thm)],[c_50,c_632]) ).
tcf(c_945,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,X0),X1)
| in(sK0(X0,X1),X0) ),
inference(superposition,[status(thm)],[c_61,c_632]) ).
tcf(c_946,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,sK6),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_324,c_632]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,empty_set),X0)
| in(sK0(empty_set,X0),X1) ),
inference(superposition,[status(thm)],[c_68,c_632]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i] :
( in(sK0(empty_set,X1),empty_set)
| subset(set_intersection2(empty_set,X0),X1) ),
inference(superposition,[status(thm)],[c_587,c_632]) ).
tcf(c_949,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,X2),X3)
| in(sK0(set_intersection2(X0,X2),X3),X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_632,c_53]) ).
tcf(c_950,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| ~ in(X0,sK0(set_intersection2(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_632,c_49]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_632,c_70]) ).
tcf(c_952,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(X0,X1),X0),
inference(superposition,[status(thm)],[c_632,c_51]) ).
tcf(c_953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(set_intersection2(X0,X1),X2),X3)
| in(sK0(set_intersection2(set_intersection2(X0,X1),X2),X3),X1) ),
inference(superposition,[status(thm)],[c_632,c_59]) ).
tcf(c_954,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(set_intersection2(X0,X1),X2),X3)
| in(sK0(set_intersection2(set_intersection2(X0,X1),X2),X3),X0) ),
inference(superposition,[status(thm)],[c_632,c_58]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| in(sK0(set_intersection2(sK5,X0),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_632,c_722]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_632,c_698]) ).
tcf(c_957,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),sK5) ),
inference(superposition,[status(thm)],[c_632,c_636]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(empty_set,X0),X1)
| in(sK0(set_intersection2(empty_set,X0),X1),X2) ),
inference(superposition,[status(thm)],[c_632,c_637]) ).
tcf(c_961,plain,
! [X0: $i] :
( subset(empty_set,X0)
| in(sK0(empty_set,X0),empty_set) ),
inference(light_normalisation,[status(thm)],[c_948,c_587]) ).
tcf(c_1005,plain,
( in(sK0(sK4,iPr_def_10),sK5)
| ~ subset(sK4,sK5)
| ~ in(sK0(sK4,iPr_def_10),sK4) ),
inference(instantiation,[status(thm)],[c_830]) ).
tcf(c_1006,plain,
( in(sK0(sK4,iPr_def_10),sK6)
| ~ subset(sK4,sK6)
| ~ in(sK0(sK4,iPr_def_10),sK4) ),
inference(instantiation,[status(thm)],[c_830]) ).
tcf(c_1009,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(X0,X1),X1),
inference(superposition,[status(thm)],[c_50,c_952]) ).
tcf(c_1014,plain,
subset(empty_set,empty_set),
inference(superposition,[status(thm)],[c_587,c_952]) ).
tcf(c_1021,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X2,X3,X0),X3)
| in(sK1(X2,X3,X0),X1)
| ( set_intersection2(X2,X3) = X0 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_1022,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X2,X0),X2)
| ( set_intersection2(X1,X2) = X0 )
| ~ in(X0,sK1(X1,X2,X0)) ),
inference(superposition,[status(thm)],[c_56,c_49]) ).
tcf(c_1023,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X2,X0),X2)
| ( set_intersection2(X1,X2) = X0 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_56,c_70]) ).
tcf(c_1024,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,X1,set_intersection2(X2,X3)),X3)
| in(sK1(X0,X1,set_intersection2(X2,X3)),X1)
| ( set_intersection2(X0,X1) = set_intersection2(X2,X3) ) ),
inference(superposition,[status(thm)],[c_56,c_59]) ).
tcf(c_1025,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,X1,set_intersection2(X2,X3)),X2)
| in(sK1(X0,X1,set_intersection2(X2,X3)),X1)
| ( set_intersection2(X0,X1) = set_intersection2(X2,X3) ) ),
inference(superposition,[status(thm)],[c_56,c_58]) ).
tcf(c_1026,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),iPr_def_10)
| in(sK1(X0,X1,sK5),X1)
| ( set_intersection2(X0,X1) = sK5 )
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_56,c_722]) ).
tcf(c_1027,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,iPr_def_10),sK6)
| in(sK1(X0,X1,iPr_def_10),X1)
| ( set_intersection2(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_56,c_698]) ).
tcf(c_1028,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,iPr_def_10),sK5)
| in(sK1(X0,X1,iPr_def_10),X1)
| ( set_intersection2(X0,X1) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_56,c_636]) ).
tcf(c_1029,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X1,empty_set),X2)
| in(sK1(X0,X1,empty_set),X1)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_56,c_637]) ).
tcf(c_1030,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X2,X0,X3),X3)
| in(sK1(X2,X0,X3),X1)
| ( set_intersection2(X2,X0) = X3 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_53]) ).
tcf(c_1031,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X0,X2),X2)
| ( set_intersection2(X1,X0) = X2 )
| ~ in(X0,sK1(X1,X0,X2)) ),
inference(superposition,[status(thm)],[c_56,c_49]) ).
tcf(c_1032,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,X0,X2),X2)
| ( set_intersection2(X1,X0) = X2 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_56,c_70]) ).
tcf(c_1033,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,set_intersection2(X1,X2),X3),X3)
| in(sK1(X0,set_intersection2(X1,X2),X3),X2)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = X3 ) ),
inference(superposition,[status(thm)],[c_56,c_59]) ).
tcf(c_1034,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(sK1(X0,set_intersection2(X1,X2),X3),X3)
| in(sK1(X0,set_intersection2(X1,X2),X3),X1)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = X3 ) ),
inference(superposition,[status(thm)],[c_56,c_58]) ).
tcf(c_1035,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,sK5,X1),iPr_def_10)
| in(sK1(X0,sK5,X1),X1)
| ( set_intersection2(X0,sK5) = X1 )
| ~ in(sK1(X0,sK5,X1),sK6) ),
inference(superposition,[status(thm)],[c_56,c_722]) ).
tcf(c_1036,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,iPr_def_10,X1),sK6)
| in(sK1(X0,iPr_def_10,X1),X1)
| ( set_intersection2(X0,iPr_def_10) = X1 ) ),
inference(superposition,[status(thm)],[c_56,c_698]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,iPr_def_10,X1),sK5)
| in(sK1(X0,iPr_def_10,X1),X1)
| ( set_intersection2(X0,iPr_def_10) = X1 ) ),
inference(superposition,[status(thm)],[c_56,c_636]) ).
tcf(c_1038,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,empty_set,X1),X2)
| in(sK1(X0,empty_set,X1),X1)
| ( set_intersection2(X0,empty_set) = X1 ) ),
inference(superposition,[status(thm)],[c_56,c_637]) ).
tcf(c_1039,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,X1),X1)
| ( set_intersection2(X0,X1) = X1 ) ),
inference(equality_factoring,[status(thm)],[c_56]) ).
tcf(c_1049,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X1,empty_set,X0),X2)
| in(sK1(X1,empty_set,X0),X0)
| ( X0 = empty_set ) ),
inference(light_normalisation,[status(thm)],[c_1038,c_68]) ).
tcf(c_1175,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( set_intersection2(X0,set_intersection2(X1,X2)) = X3 )
| ~ in(sK1(X0,set_intersection2(X1,X2),X3),X3)
| ~ in(sK1(X0,set_intersection2(X1,X2),X3),X2)
| ~ in(sK1(X0,set_intersection2(X1,X2),X3),X1)
| ~ in(sK1(X0,set_intersection2(X1,X2),X3),X0) ),
inference(superposition,[status(thm)],[c_57,c_54]) ).
tcf(c_1200,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_50,c_951]) ).
tcf(c_1204,plain,
! [X0: $i,X1: $i] :
( subset(empty_set,X1)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_68,c_951]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X3)
| in(sK0(X0,X3),X2)
| ~ subset(X1,X2)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_681,c_53]) ).
tcf(c_1233,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X1,X2)
| ~ subset(X1,X0)
| ~ in(X0,sK0(X1,X2)) ),
inference(superposition,[status(thm)],[c_681,c_49]) ).
tcf(c_1234,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ~ empty(X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_681,c_70]) ).
tcf(c_1236,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X3)
| in(sK0(X0,X3),X2)
| ~ subset(X0,set_intersection2(X1,X2)) ),
inference(superposition,[status(thm)],[c_681,c_59]) ).
tcf(c_1237,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X3)
| in(sK0(X0,X3),X1)
| ~ subset(X0,set_intersection2(X1,X2)) ),
inference(superposition,[status(thm)],[c_681,c_58]) ).
tcf(c_1238,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),iPr_def_10)
| ~ subset(X0,sK5)
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_681,c_722]) ).
tcf(c_1239,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| subset(sK0(X0,X1),X2)
| ~ subset(X0,sK0(sK0(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_681,c_612]) ).
tcf(c_1240,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),sK6)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_681,c_698]) ).
tcf(c_1241,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),sK5)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_681,c_636]) ).
tcf(c_1242,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),X2)
| ~ subset(X0,empty_set) ),
inference(superposition,[status(thm)],[c_681,c_637]) ).
tcf(c_1276,plain,
( ~ empty(sK5)
| ~ in(sK0(sK4,iPr_def_10),sK5) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_1278,plain,
! [X0: $i] :
( in(sK0(sK4,iPr_def_10),X0)
| ~ subset(sK5,X0)
| ~ in(sK0(sK4,iPr_def_10),sK5) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_1279,plain,
( in(sK0(sK4,iPr_def_10),empty_set)
| ~ subset(sK5,empty_set)
| ~ in(sK0(sK4,iPr_def_10),sK5) ),
inference(instantiation,[status(thm)],[c_1278]) ).
tcf(c_1294,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ~ empty(X1)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_1234]) ).
tcf(c_1296,plain,
! [X0: $i] :
( subset(sK4,X0)
| ~ empty(sK5) ),
inference(superposition,[status(thm)],[c_326,c_1234]) ).
tcf(c_1297,plain,
! [X0: $i] :
( subset(sK4,X0)
| ~ empty(sK6) ),
inference(superposition,[status(thm)],[c_325,c_1234]) ).
tcf(c_1298,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,X2),X3)
| ~ empty(X1)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_1234]) ).
tcf(c_1299,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ empty(sK6)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_876,c_1234]) ).
tcf(c_1300,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ empty(sK5)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_667,c_1234]) ).
tcf(c_1304,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X2,X0),X3)
| ~ empty(X1)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_1234]) ).
tcf(c_1334,plain,
( ~ empty(sK6)
| ~ in(sK0(sK4,iPr_def_10),sK6) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_1336,plain,
! [X0: $i] :
( in(sK0(sK4,iPr_def_10),X0)
| ~ subset(sK6,X0)
| ~ in(sK0(sK4,iPr_def_10),sK6) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_1337,plain,
( in(sK0(sK4,iPr_def_10),empty_set)
| ~ subset(sK6,empty_set)
| ~ in(sK0(sK4,iPr_def_10),sK6) ),
inference(instantiation,[status(thm)],[c_1336]) ).
tcf(c_1358,plain,
~ empty(sK5),
inference(global_subsumption_just,[status(thm)],[c_1296,c_66,c_327,c_822,c_1005,c_1276]) ).
tcf(c_1360,plain,
~ empty(sK6),
inference(global_subsumption_just,[status(thm)],[c_1297,c_67,c_327,c_822,c_1006,c_1334]) ).
tcf(c_1372,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X1)
| ~ subset(sK5,X0)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_682,c_53]) ).
tcf(c_1373,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK5,X0)
| ~ in(X0,sK0(iPr_def_10,X1)) ),
inference(superposition,[status(thm)],[c_682,c_49]) ).
tcf(c_1374,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ empty(X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_682,c_70]) ).
tcf(c_1375,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_682,c_51]) ).
tcf(c_1376,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X1)
| ~ subset(sK5,set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_682,c_59]) ).
tcf(c_1377,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X0)
| ~ subset(sK5,set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_682,c_58]) ).
tcf(c_1378,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),iPr_def_10)
| ~ subset(sK5,sK5)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_682,c_722]) ).
tcf(c_1379,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| subset(sK0(iPr_def_10,X0),X1)
| ~ subset(sK5,sK0(sK0(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_682,c_612]) ).
tcf(c_1382,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),X1)
| ~ subset(sK5,empty_set) ),
inference(superposition,[status(thm)],[c_682,c_637]) ).
tcf(c_1417,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| subset(sK0(X0,X1),X2)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_1239]) ).
tcf(c_1418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,X1),X2)
| subset(sK0(set_intersection2(X0,X1),X2),X3)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_1239]) ).
tcf(c_1420,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X1,X0),X2)
| subset(sK0(set_intersection2(X1,X0),X2),X3)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_1239]) ).
tcf(c_1461,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| in(sK0(set_intersection2(X0,X1),X2),X0) ),
inference(superposition,[status(thm)],[c_50,c_694]) ).
tcf(c_1464,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,sK6),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_324,c_694]) ).
tcf(c_1465,plain,
! [X0: $i,X1: $i] :
( in(sK0(empty_set,X1),empty_set)
| subset(set_intersection2(X0,empty_set),X1) ),
inference(superposition,[status(thm)],[c_68,c_694]) ).
tcf(c_1466,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(empty_set,X1),X0)
| in(sK0(empty_set,X0),X1) ),
inference(superposition,[status(thm)],[c_587,c_694]) ).
tcf(c_1467,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X2,X0),X3)
| in(sK0(set_intersection2(X2,X0),X3),X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_694,c_53]) ).
tcf(c_1468,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| ~ in(X0,sK0(set_intersection2(X1,X0),X2)) ),
inference(superposition,[status(thm)],[c_694,c_49]) ).
tcf(c_1471,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,set_intersection2(X1,X2)),X3)
| in(sK0(set_intersection2(X0,set_intersection2(X1,X2)),X3),X2) ),
inference(superposition,[status(thm)],[c_694,c_59]) ).
tcf(c_1472,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,set_intersection2(X1,X2)),X3)
| in(sK0(set_intersection2(X0,set_intersection2(X1,X2)),X3),X1) ),
inference(superposition,[status(thm)],[c_694,c_58]) ).
tcf(c_1473,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| in(sK0(set_intersection2(X0,sK5),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_694,c_722]) ).
tcf(c_1474,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_694,c_698]) ).
tcf(c_1475,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),sK5) ),
inference(superposition,[status(thm)],[c_694,c_636]) ).
tcf(c_1476,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,empty_set),X1)
| in(sK0(set_intersection2(X0,empty_set),X1),X2) ),
inference(superposition,[status(thm)],[c_694,c_637]) ).
tcf(c_1536,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X2,X0),X1)
| ( set_intersection2(X0,X2) = X0 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_769,c_53]) ).
tcf(c_1537,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = X0 )
| ~ in(X0,sK1(X0,X1,X0)) ),
inference(superposition,[status(thm)],[c_769,c_49]) ).
tcf(c_1538,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = X0 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_769,c_70]) ).
tcf(c_1540,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(set_intersection2(X0,X1),X2,set_intersection2(X0,X1)),X1)
| ( set_intersection2(set_intersection2(X0,X1),X2) = set_intersection2(X0,X1) ) ),
inference(superposition,[status(thm)],[c_769,c_59]) ).
tcf(c_1541,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(set_intersection2(X0,X1),X2,set_intersection2(X0,X1)),X0)
| ( set_intersection2(set_intersection2(X0,X1),X2) = set_intersection2(X0,X1) ) ),
inference(superposition,[status(thm)],[c_769,c_58]) ).
tcf(c_1542,plain,
! [X0: $i] :
( in(sK1(sK5,X0,sK5),iPr_def_10)
| ( set_intersection2(sK5,X0) = sK5 )
| ~ in(sK1(sK5,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_769,c_722]) ).
tcf(c_1543,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,iPr_def_10),sK6)
| ( set_intersection2(iPr_def_10,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_769,c_698]) ).
tcf(c_1544,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,iPr_def_10),sK5)
| ( set_intersection2(iPr_def_10,X0) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_769,c_636]) ).
tcf(c_1596,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X1)
| ~ subset(sK6,X0)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_874,c_53]) ).
tcf(c_1597,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK6,X0)
| ~ in(X0,sK0(iPr_def_10,X1)) ),
inference(superposition,[status(thm)],[c_874,c_49]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ empty(X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_874,c_70]) ).
tcf(c_1599,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_874,c_51]) ).
tcf(c_1600,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X1)
| ~ subset(sK6,set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_874,c_59]) ).
tcf(c_1601,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK0(iPr_def_10,X2),X0)
| ~ subset(sK6,set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_874,c_58]) ).
tcf(c_1602,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),iPr_def_10)
| ~ subset(sK6,sK5)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_874,c_722]) ).
tcf(c_1603,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| subset(sK0(iPr_def_10,X0),X1)
| ~ subset(sK6,sK0(sK0(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_874,c_612]) ).
tcf(c_1606,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),X1)
| ~ subset(sK6,empty_set) ),
inference(superposition,[status(thm)],[c_874,c_637]) ).
tcf(c_1653,plain,
! [X0: $i] :
( ~ empty(X0)
| ~ in(sK0(sK4,iPr_def_10),X0) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_1657,plain,
( ~ empty(empty_set)
| ~ in(sK0(sK4,iPr_def_10),empty_set) ),
inference(instantiation,[status(thm)],[c_1653]) ).
tcf(c_1673,plain,
! [X0: $i] :
( ~ subset(sK6,X0)
| ~ empty(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1598,c_67,c_327,c_822,c_1006,c_1336,c_1653]) ).
tcf(c_1674,plain,
! [X0: $i] :
( ~ empty(X0)
| ~ subset(sK6,X0) ),
inference(renaming,[status(thm)],[c_1673]) ).
tcf(c_1689,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,sK5),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_324,c_943]) ).
tcf(c_1692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X0,X2),X3)
| in(sK0(set_intersection2(X2,X0),X3),X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_943,c_53]) ).
tcf(c_1693,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| ~ in(X0,sK0(set_intersection2(X1,X0),X2)) ),
inference(superposition,[status(thm)],[c_943,c_49]) ).
tcf(c_1696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(set_intersection2(X1,X2),X0),X3)
| in(sK0(set_intersection2(X0,set_intersection2(X1,X2)),X3),X2) ),
inference(superposition,[status(thm)],[c_943,c_59]) ).
tcf(c_1697,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(set_intersection2(X1,X2),X0),X3)
| in(sK0(set_intersection2(X0,set_intersection2(X1,X2)),X3),X1) ),
inference(superposition,[status(thm)],[c_943,c_58]) ).
tcf(c_1698,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| in(sK0(set_intersection2(X0,sK5),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_943,c_722]) ).
tcf(c_1699,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_943,c_698]) ).
tcf(c_1700,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),sK5) ),
inference(superposition,[status(thm)],[c_943,c_636]) ).
tcf(c_1701,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(empty_set,X0),X1)
| in(sK0(set_intersection2(X0,empty_set),X1),X2) ),
inference(superposition,[status(thm)],[c_943,c_637]) ).
tcf(c_1748,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_61,c_956]) ).
tcf(c_1749,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,empty_set),X0)
| in(sK0(empty_set,X0),sK6) ),
inference(superposition,[status(thm)],[c_68,c_956]) ).
tcf(c_1750,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(iPr_def_10,X1),X2)
| in(sK0(set_intersection2(iPr_def_10,X1),X2),X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_956,c_53]) ).
tcf(c_1751,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(sK6,sK0(set_intersection2(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_956,c_49]) ).
tcf(c_1753,plain,
! [X0: $i] : subset(set_intersection2(iPr_def_10,X0),sK6),
inference(superposition,[status(thm)],[c_956,c_51]) ).
tcf(c_1809,plain,
! [X0: $i] : subset(set_intersection2(X0,iPr_def_10),sK6),
inference(superposition,[status(thm)],[c_50,c_1753]) ).
tcf(c_1812,plain,
subset(empty_set,sK6),
inference(superposition,[status(thm)],[c_68,c_1753]) ).
tcf(c_1834,plain,
! [X0: $i] :
( subset(empty_set,X0)
| in(sK0(empty_set,X0),sK6) ),
inference(demodulation,[status(thm)],[c_1749,c_68]) ).
tcf(c_1839,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X2,X0,X0),X1)
| ( set_intersection2(X2,X0) = X0 )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_1039,c_53]) ).
tcf(c_1840,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X1,X0) = X0 )
| ~ in(X0,sK1(X1,X0,X0)) ),
inference(superposition,[status(thm)],[c_1039,c_49]) ).
tcf(c_1841,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X1,X0) = X0 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1039,c_70]) ).
tcf(c_1842,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = X1 )
| ~ in(sK1(X0,X1,X1),X1)
| ~ in(sK1(X0,X1,X1),X0) ),
inference(superposition,[status(thm)],[c_1039,c_54]) ).
tcf(c_1843,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,set_intersection2(X1,X2),set_intersection2(X1,X2)),X2)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = set_intersection2(X1,X2) ) ),
inference(superposition,[status(thm)],[c_1039,c_59]) ).
tcf(c_1844,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,set_intersection2(X1,X2),set_intersection2(X1,X2)),X1)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = set_intersection2(X1,X2) ) ),
inference(superposition,[status(thm)],[c_1039,c_58]) ).
tcf(c_1845,plain,
! [X0: $i] :
( in(sK1(X0,sK5,sK5),iPr_def_10)
| ( set_intersection2(X0,sK5) = sK5 )
| ~ in(sK1(X0,sK5,sK5),sK6) ),
inference(superposition,[status(thm)],[c_1039,c_722]) ).
tcf(c_1846,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,iPr_def_10),sK6)
| ( set_intersection2(X0,iPr_def_10) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_1039,c_698]) ).
tcf(c_1847,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,iPr_def_10),sK5)
| ( set_intersection2(X0,iPr_def_10) = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_1039,c_636]) ).
tcf(c_1886,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,sK5),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_324,c_1461]) ).
tcf(c_1889,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X2,X0),X3)
| in(sK0(set_intersection2(X0,X2),X3),X1)
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_1461,c_53]) ).
tcf(c_1890,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| ~ in(X0,sK0(set_intersection2(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_1461,c_49]) ).
tcf(c_1893,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X2,set_intersection2(X0,X1)),X3)
| in(sK0(set_intersection2(set_intersection2(X0,X1),X2),X3),X1) ),
inference(superposition,[status(thm)],[c_1461,c_59]) ).
tcf(c_1894,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(set_intersection2(X2,set_intersection2(X0,X1)),X3)
| in(sK0(set_intersection2(set_intersection2(X0,X1),X2),X3),X0) ),
inference(superposition,[status(thm)],[c_1461,c_58]) ).
tcf(c_1895,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| in(sK0(set_intersection2(sK5,X0),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1461,c_722]) ).
tcf(c_1896,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1461,c_698]) ).
tcf(c_1897,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),sK5) ),
inference(superposition,[status(thm)],[c_1461,c_636]) ).
tcf(c_1898,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,empty_set),X1)
| in(sK0(set_intersection2(empty_set,X0),X1),X2) ),
inference(superposition,[status(thm)],[c_1461,c_637]) ).
tcf(c_1953,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_61,c_957]) ).
tcf(c_1954,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,empty_set),X0)
| in(sK0(empty_set,X0),sK5) ),
inference(superposition,[status(thm)],[c_68,c_957]) ).
tcf(c_1955,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(iPr_def_10,X1),X2)
| in(sK0(set_intersection2(iPr_def_10,X1),X2),X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_957,c_53]) ).
tcf(c_1956,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(sK5,sK0(set_intersection2(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_957,c_49]) ).
tcf(c_1958,plain,
! [X0: $i] : subset(set_intersection2(iPr_def_10,X0),sK5),
inference(superposition,[status(thm)],[c_957,c_51]) ).
tcf(c_1959,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_957,c_722]) ).
tcf(c_2057,plain,
! [X0: $i] : subset(set_intersection2(X0,iPr_def_10),sK5),
inference(superposition,[status(thm)],[c_50,c_1958]) ).
tcf(c_2060,plain,
subset(empty_set,sK5),
inference(superposition,[status(thm)],[c_68,c_1958]) ).
tcf(c_2069,plain,
! [X0: $i] :
( subset(empty_set,X0)
| in(sK0(empty_set,X0),sK5) ),
inference(demodulation,[status(thm)],[c_1954,c_68]) ).
tcf(c_2076,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| in(sK0(X0,X2),X1)
| ~ subset(sK6,X1)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1240,c_53]) ).
tcf(c_2077,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ in(sK6,sK0(X0,X1)) ),
inference(superposition,[status(thm)],[c_1240,c_49]) ).
tcf(c_2079,plain,
! [X0: $i] :
( subset(X0,sK6)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1240,c_51]) ).
tcf(c_2094,plain,
! [X0: $i] :
( subset(X0,sK6)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_2079]) ).
tcf(c_2096,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,X1),sK6)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_2079]) ).
tcf(c_2098,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,X0),sK6)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_2079]) ).
tcf(c_2135,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| in(sK0(X0,X2),X1)
| ~ subset(sK5,X1)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1241,c_53]) ).
tcf(c_2136,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ in(sK5,sK0(X0,X1)) ),
inference(superposition,[status(thm)],[c_1241,c_49]) ).
tcf(c_2138,plain,
! [X0: $i] :
( subset(X0,sK5)
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1241,c_51]) ).
tcf(c_2139,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| in(sK0(X0,X1),iPr_def_10)
| ~ subset(X0,iPr_def_10)
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_1241,c_722]) ).
tcf(c_2165,plain,
! [X0: $i] :
( subset(X0,sK5)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_2138]) ).
tcf(c_2167,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,X1),sK5)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_2138]) ).
tcf(c_2169,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,X0),sK5)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_2138]) ).
tcf(c_2189,plain,
! [X0: $i] :
( ~ empty(iPr_def_10)
| ~ in(X0,sK6)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_324,c_727]) ).
tcf(c_2190,plain,
! [X0: $i,X1: $i] :
( ~ empty(empty_set)
| ~ in(X0,empty_set)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_68,c_727]) ).
tcf(c_2192,plain,
! [X0: $i,X1: $i] :
( ~ in(X0,empty_set)
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2190,c_60]) ).
tcf(c_2202,plain,
! [X0: $i] : ~ in(X0,empty_set),
inference(global_subsumption_just,[status(thm)],[c_2192,c_637,c_2192]) ).
tcf(c_2205,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,empty_set,X1),X1)
| ( set_intersection2(X0,empty_set) = X1 ) ),
inference(superposition,[status(thm)],[c_56,c_2202]) ).
tcf(c_2206,plain,
! [X0: $i,X1: $i] :
( in(sK1(empty_set,X0,X1),X1)
| ( set_intersection2(empty_set,X0) = X1 ) ),
inference(superposition,[status(thm)],[c_55,c_2202]) ).
tcf(c_2207,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,empty_set),X1)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_56,c_2202]) ).
tcf(c_2208,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,empty_set),X0)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_55,c_2202]) ).
tcf(c_2211,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,empty_set) ),
inference(superposition,[status(thm)],[c_681,c_2202]) ).
tcf(c_2212,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK6,empty_set) ),
inference(superposition,[status(thm)],[c_874,c_2202]) ).
tcf(c_2213,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,empty_set) ),
inference(superposition,[status(thm)],[c_682,c_2202]) ).
tcf(c_2214,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(empty_set,X0),X1),
inference(superposition,[status(thm)],[c_943,c_2202]) ).
tcf(c_2215,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(X0,empty_set),X1),
inference(superposition,[status(thm)],[c_694,c_2202]) ).
tcf(c_2230,plain,
! [X0: $i,X1: $i] :
( in(sK1(empty_set,X1,X0),X0)
| ( X0 = empty_set ) ),
inference(light_normalisation,[status(thm)],[c_2206,c_587]) ).
tcf(c_2233,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,empty_set,X0),X0)
| ( X0 = empty_set ) ),
inference(light_normalisation,[status(thm)],[c_2205,c_68]) ).
tcf(c_2259,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(empty_set,X2,X0),X1)
| ( X0 = empty_set )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_2230,c_53]) ).
tcf(c_2260,plain,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ~ in(X0,sK1(empty_set,X1,X0)) ),
inference(superposition,[status(thm)],[c_2230,c_49]) ).
tcf(c_2262,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ( set_intersection2(empty_set,X0) = X0 )
| ~ in(sK1(empty_set,X0,X0),empty_set)
| ~ in(sK1(empty_set,X0,X0),X0) ),
inference(superposition,[status(thm)],[c_2230,c_54]) ).
tcf(c_2263,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(empty_set,X2,set_intersection2(X0,X1)),X1)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_2230,c_59]) ).
tcf(c_2264,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(empty_set,X2,set_intersection2(X0,X1)),X0)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_2230,c_58]) ).
tcf(c_2265,plain,
! [X0: $i] :
( in(sK1(empty_set,X0,sK5),iPr_def_10)
| ( empty_set = sK5 )
| ~ in(sK1(empty_set,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2230,c_722]) ).
tcf(c_2266,plain,
! [X0: $i] :
( in(sK1(empty_set,X0,iPr_def_10),sK6)
| ( empty_set = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_2230,c_698]) ).
tcf(c_2267,plain,
! [X0: $i] :
( in(sK1(empty_set,X0,iPr_def_10),sK5)
| ( empty_set = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_2230,c_636]) ).
tcf(c_2285,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ~ in(sK1(empty_set,X0,X0),empty_set)
| ~ in(sK1(empty_set,X0,X0),X0) ),
inference(light_normalisation,[status(thm)],[c_2262,c_587]) ).
tcf(c_2304,plain,
~ subset(sK6,empty_set),
inference(global_subsumption_just,[status(thm)],[c_2212,c_60,c_67,c_327,c_822,c_1006,c_1337,c_1657]) ).
tcf(c_2307,plain,
~ subset(sK5,empty_set),
inference(global_subsumption_just,[status(thm)],[c_2213,c_60,c_66,c_327,c_822,c_1005,c_1279,c_1657]) ).
tcf(c_2314,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X2,empty_set,X0),X1)
| ( X0 = empty_set )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_2233,c_53]) ).
tcf(c_2315,plain,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ~ in(X0,sK1(X1,empty_set,X0)) ),
inference(superposition,[status(thm)],[c_2233,c_49]) ).
tcf(c_2318,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X2,empty_set,set_intersection2(X0,X1)),X1)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_2233,c_59]) ).
tcf(c_2319,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X2,empty_set,set_intersection2(X0,X1)),X0)
| ( set_intersection2(X0,X1) = empty_set ) ),
inference(superposition,[status(thm)],[c_2233,c_58]) ).
tcf(c_2320,plain,
! [X0: $i] :
( in(sK1(X0,empty_set,sK5),iPr_def_10)
| ( empty_set = sK5 )
| ~ in(sK1(X0,empty_set,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2233,c_722]) ).
tcf(c_2321,plain,
! [X0: $i] :
( in(sK1(X0,empty_set,iPr_def_10),sK6)
| ( empty_set = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_2233,c_698]) ).
tcf(c_2322,plain,
! [X0: $i] :
( in(sK1(X0,empty_set,iPr_def_10),sK5)
| ( empty_set = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_2233,c_636]) ).
tcf(c_2350,plain,
! [X0: $i,X1: $i] :
( in(sK1(empty_set,X1,iPr_def_10),X0)
| ( empty_set = iPr_def_10 )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_2266,c_53]) ).
tcf(c_2351,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(sK6,sK1(empty_set,X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_2266,c_49]) ).
tcf(c_2353,plain,
( ( empty_set = iPr_def_10 )
| ( set_intersection2(empty_set,sK6) = iPr_def_10 )
| ~ in(sK1(empty_set,sK6,iPr_def_10),iPr_def_10)
| ~ in(sK1(empty_set,sK6,iPr_def_10),empty_set) ),
inference(superposition,[status(thm)],[c_2266,c_54]) ).
tcf(c_2364,plain,
! [X0: $i,X1: $i] :
( in(sK1(empty_set,X1,iPr_def_10),X0)
| ( empty_set = iPr_def_10 )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_2267,c_53]) ).
tcf(c_2365,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(sK5,sK1(empty_set,X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_2267,c_49]) ).
tcf(c_2367,plain,
( ( empty_set = iPr_def_10 )
| ( set_intersection2(empty_set,sK5) = iPr_def_10 )
| ~ in(sK1(empty_set,sK5,iPr_def_10),iPr_def_10)
| ~ in(sK1(empty_set,sK5,iPr_def_10),empty_set) ),
inference(superposition,[status(thm)],[c_2267,c_54]) ).
tcf(c_2368,plain,
! [X0: $i] :
( in(sK1(empty_set,X0,iPr_def_10),iPr_def_10)
| ( empty_set = iPr_def_10 )
| ~ in(sK1(empty_set,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2267,c_722]) ).
tcf(c_2387,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,empty_set,iPr_def_10),X0)
| ( empty_set = iPr_def_10 )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_2321,c_53]) ).
tcf(c_2388,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(sK6,sK1(X0,empty_set,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_2321,c_49]) ).
tcf(c_2399,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,empty_set,iPr_def_10),X0)
| ( empty_set = iPr_def_10 )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_2322,c_53]) ).
tcf(c_2400,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(sK5,sK1(X0,empty_set,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_2322,c_49]) ).
tcf(c_2402,plain,
! [X0: $i] :
( in(sK1(X0,empty_set,iPr_def_10),iPr_def_10)
| ( empty_set = iPr_def_10 )
| ~ in(sK1(X0,empty_set,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2322,c_722]) ).
tcf(c_2426,plain,
! [X0: $i] :
( subset(sK5,X0)
| ~ empty(iPr_def_10)
| ~ in(sK0(sK5,X0),sK6) ),
inference(superposition,[status(thm)],[c_52,c_2189]) ).
tcf(c_2427,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,sK5,X1),X1)
| ( set_intersection2(X0,sK5) = X1 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,sK5,X1),sK6) ),
inference(superposition,[status(thm)],[c_56,c_2189]) ).
tcf(c_2428,plain,
! [X0: $i,X1: $i] :
( in(sK1(sK5,X0,X1),X1)
| ( set_intersection2(sK5,X0) = X1 )
| ~ empty(iPr_def_10)
| ~ in(sK1(sK5,X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_55,c_2189]) ).
tcf(c_2429,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),X1)
| ( set_intersection2(X0,X1) = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_56,c_2189]) ).
tcf(c_2430,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),X0)
| ( set_intersection2(X0,X1) = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_55,c_2189]) ).
tcf(c_2431,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1461,c_2189]) ).
tcf(c_2432,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_632,c_2189]) ).
tcf(c_2433,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(iPr_def_10)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_651,c_2189]) ).
tcf(c_2434,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ empty(iPr_def_10)
| ~ subset(X0,sK5)
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_681,c_2189]) ).
tcf(c_2435,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(iPr_def_10)
| ~ subset(sK6,sK5)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_874,c_2189]) ).
tcf(c_2436,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(iPr_def_10)
| ~ subset(sK5,sK5)
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_682,c_2189]) ).
tcf(c_2437,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_943,c_2189]) ).
tcf(c_2438,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_694,c_2189]) ).
tcf(c_2439,plain,
! [X0: $i] :
( ( set_intersection2(sK5,X0) = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(sK5,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_769,c_2189]) ).
tcf(c_2440,plain,
! [X0: $i] :
( ( empty_set = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(empty_set,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2230,c_2189]) ).
tcf(c_2441,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_957,c_2189]) ).
tcf(c_2442,plain,
! [X0: $i] :
( ( set_intersection2(X0,sK5) = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,sK5,sK5),sK6) ),
inference(superposition,[status(thm)],[c_1039,c_2189]) ).
tcf(c_2443,plain,
! [X0: $i] :
( ( empty_set = sK5 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,empty_set,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2233,c_2189]) ).
tcf(c_2444,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ empty(iPr_def_10)
| ~ subset(X0,iPr_def_10)
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_1241,c_2189]) ).
tcf(c_2445,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ empty(iPr_def_10)
| ~ in(sK1(empty_set,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2267,c_2189]) ).
tcf(c_2446,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,empty_set,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2322,c_2189]) ).
tcf(c_2567,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_intersection2(X1,X2))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_64,c_725]) ).
tcf(c_2568,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X0,X3)
| ~ empty(X1)
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_951,c_725]) ).
tcf(c_2579,plain,
! [X0: $i,X1: $i] :
( in(X0,X1)
| ~ subset(iPr_def_10,X1)
| ~ in(X0,sK6)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_324,c_725]) ).
tcf(c_2600,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ( sK0(X0,X2) = empty_set )
| ~ subset(X0,sK1(empty_set,X1,sK0(X0,X2))) ),
inference(superposition,[status(thm)],[c_681,c_2260]) ).
tcf(c_2601,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( sK0(iPr_def_10,X1) = empty_set )
| ~ subset(sK6,sK1(empty_set,X0,sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_874,c_2260]) ).
tcf(c_2602,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( sK0(iPr_def_10,X1) = empty_set )
| ~ subset(sK5,sK1(empty_set,X0,sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_682,c_2260]) ).
tcf(c_2638,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ( sK0(X0,X2) = empty_set )
| ~ subset(X0,sK1(X1,empty_set,sK0(X0,X2))) ),
inference(superposition,[status(thm)],[c_681,c_2315]) ).
tcf(c_2639,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( sK0(iPr_def_10,X1) = empty_set )
| ~ subset(sK6,sK1(X0,empty_set,sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_874,c_2315]) ).
tcf(c_2640,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( sK0(iPr_def_10,X1) = empty_set )
| ~ subset(sK5,sK1(X0,empty_set,sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_682,c_2315]) ).
tcf(c_2680,plain,
! [X0: $i] :
( subset(set_intersection2(empty_set,iPr_def_10),X0)
| in(sK0(empty_set,X0),sK6) ),
inference(superposition,[status(thm)],[c_587,c_1474]) ).
tcf(c_2681,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,iPr_def_10),X2)
| in(sK0(set_intersection2(X1,iPr_def_10),X2),X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_1474,c_53]) ).
tcf(c_2682,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(sK6,sK0(set_intersection2(X0,iPr_def_10),X1)) ),
inference(superposition,[status(thm)],[c_1474,c_49]) ).
tcf(c_2702,plain,
! [X0: $i] :
( subset(set_intersection2(empty_set,iPr_def_10),X0)
| in(sK0(empty_set,X0),sK5) ),
inference(superposition,[status(thm)],[c_587,c_1475]) ).
tcf(c_2703,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,iPr_def_10),X2)
| in(sK0(set_intersection2(X1,iPr_def_10),X2),X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_1475,c_53]) ).
tcf(c_2704,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(sK5,sK0(set_intersection2(X0,iPr_def_10),X1)) ),
inference(superposition,[status(thm)],[c_1475,c_49]) ).
tcf(c_2707,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1475,c_2189]) ).
tcf(c_2708,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1475,c_722]) ).
tcf(c_2747,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X1,iPr_def_10),X0)
| ( set_intersection2(iPr_def_10,X1) = iPr_def_10 )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_1543,c_53]) ).
tcf(c_2748,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = iPr_def_10 )
| ~ in(sK6,sK1(iPr_def_10,X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_1543,c_49]) ).
tcf(c_2750,plain,
( ( set_intersection2(iPr_def_10,sK6) = iPr_def_10 )
| ~ in(sK1(iPr_def_10,sK6,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1543,c_54]) ).
tcf(c_2763,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X1,iPr_def_10),X0)
| ( set_intersection2(iPr_def_10,X1) = iPr_def_10 )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_1544,c_53]) ).
tcf(c_2764,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = iPr_def_10 )
| ~ in(sK5,sK1(iPr_def_10,X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_1544,c_49]) ).
tcf(c_2766,plain,
( ( set_intersection2(iPr_def_10,sK5) = iPr_def_10 )
| ~ in(sK1(iPr_def_10,sK5,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1544,c_54]) ).
tcf(c_2767,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = iPr_def_10 )
| ~ empty(iPr_def_10)
| ~ in(sK1(iPr_def_10,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1544,c_2189]) ).
tcf(c_2768,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,iPr_def_10),iPr_def_10)
| ( set_intersection2(iPr_def_10,X0) = iPr_def_10 )
| ~ in(sK1(iPr_def_10,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1544,c_722]) ).
tcf(c_2808,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(iPr_def_10,X1),X2)
| in(sK0(set_intersection2(X1,iPr_def_10),X2),X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_1699,c_53]) ).
tcf(c_2809,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(sK6,sK0(set_intersection2(X0,iPr_def_10),X1)) ),
inference(superposition,[status(thm)],[c_1699,c_49]) ).
tcf(c_2824,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ in(set_intersection2(X3,X2),X1)
| ~ in(set_intersection2(X3,X2),X0)
| ~ in(set_intersection2(X0,X1),X3)
| ~ in(set_intersection2(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_57,c_726]) ).
tcf(c_2828,plain,
! [X0: $i] :
( ~ in(iPr_def_10,X0)
| ~ in(X0,sK6)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_324,c_726]) ).
tcf(c_2844,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X2,X0,empty_set),X1)
| ( set_intersection2(X2,X0) = empty_set )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_2207,c_53]) ).
tcf(c_2845,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X1,X0) = empty_set )
| ~ in(X0,sK1(X1,X0,empty_set)) ),
inference(superposition,[status(thm)],[c_2207,c_49]) ).
tcf(c_2846,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X1,X0) = empty_set )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_2207,c_70]) ).
tcf(c_2847,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = empty_set )
| ~ in(sK1(X0,X1,empty_set),empty_set)
| ~ in(sK1(X0,X1,empty_set),X0) ),
inference(superposition,[status(thm)],[c_2207,c_54]) ).
tcf(c_2848,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,set_intersection2(X1,X2),empty_set),X2)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = empty_set ) ),
inference(superposition,[status(thm)],[c_2207,c_59]) ).
tcf(c_2849,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,set_intersection2(X1,X2),empty_set),X1)
| ( set_intersection2(X0,set_intersection2(X1,X2)) = empty_set ) ),
inference(superposition,[status(thm)],[c_2207,c_58]) ).
tcf(c_2850,plain,
! [X0: $i] :
( ( set_intersection2(X0,sK5) = empty_set )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,sK5,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2207,c_2189]) ).
tcf(c_2851,plain,
! [X0: $i] :
( in(sK1(X0,sK5,empty_set),iPr_def_10)
| ( set_intersection2(X0,sK5) = empty_set )
| ~ in(sK1(X0,sK5,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2207,c_722]) ).
tcf(c_2852,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,empty_set),sK6)
| ( set_intersection2(X0,iPr_def_10) = empty_set ) ),
inference(superposition,[status(thm)],[c_2207,c_698]) ).
tcf(c_2853,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,empty_set),sK5)
| ( set_intersection2(X0,iPr_def_10) = empty_set ) ),
inference(superposition,[status(thm)],[c_2207,c_636]) ).
tcf(c_2903,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(X0,X2,empty_set),X1)
| ( set_intersection2(X0,X2) = empty_set )
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_2208,c_53]) ).
tcf(c_2904,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = empty_set )
| ~ in(X0,sK1(X0,X1,empty_set)) ),
inference(superposition,[status(thm)],[c_2208,c_49]) ).
tcf(c_2905,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2(X0,X1) = empty_set )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_2208,c_70]) ).
tcf(c_2906,plain,
! [X0: $i] :
( ( set_intersection2(X0,X0) = empty_set )
| ~ in(sK1(X0,X0,empty_set),empty_set)
| ~ in(sK1(X0,X0,empty_set),X0) ),
inference(superposition,[status(thm)],[c_2208,c_54]) ).
tcf(c_2907,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(set_intersection2(X0,X1),X2,empty_set),X1)
| ( set_intersection2(set_intersection2(X0,X1),X2) = empty_set ) ),
inference(superposition,[status(thm)],[c_2208,c_59]) ).
tcf(c_2908,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(sK1(set_intersection2(X0,X1),X2,empty_set),X0)
| ( set_intersection2(set_intersection2(X0,X1),X2) = empty_set ) ),
inference(superposition,[status(thm)],[c_2208,c_58]) ).
tcf(c_2909,plain,
! [X0: $i] :
( ( set_intersection2(sK5,X0) = empty_set )
| ~ empty(iPr_def_10)
| ~ in(sK1(sK5,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2208,c_2189]) ).
tcf(c_2910,plain,
! [X0: $i] :
( in(sK1(sK5,X0,empty_set),iPr_def_10)
| ( set_intersection2(sK5,X0) = empty_set )
| ~ in(sK1(sK5,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2208,c_722]) ).
tcf(c_2911,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,empty_set),sK6)
| ( set_intersection2(iPr_def_10,X0) = empty_set ) ),
inference(superposition,[status(thm)],[c_2208,c_698]) ).
tcf(c_2912,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,empty_set),sK5)
| ( set_intersection2(iPr_def_10,X0) = empty_set ) ),
inference(superposition,[status(thm)],[c_2208,c_636]) ).
tcf(c_2935,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ~ in(sK1(X0,X0,empty_set),empty_set)
| ~ in(sK1(X0,X0,empty_set),X0) ),
inference(light_normalisation,[status(thm)],[c_2906,c_61]) ).
tcf(c_3020,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(iPr_def_10,X1),X2)
| in(sK0(set_intersection2(X1,iPr_def_10),X2),X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_1700,c_53]) ).
tcf(c_3021,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(sK5,sK0(set_intersection2(X0,iPr_def_10),X1)) ),
inference(superposition,[status(thm)],[c_1700,c_49]) ).
tcf(c_3024,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1700,c_2189]) ).
tcf(c_3025,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| in(sK0(set_intersection2(X0,iPr_def_10),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1700,c_722]) ).
tcf(c_3044,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,iPr_def_10,iPr_def_10),X0)
| ( set_intersection2(X1,iPr_def_10) = iPr_def_10 )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_1846,c_53]) ).
tcf(c_3045,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = iPr_def_10 )
| ~ in(sK6,sK1(X0,iPr_def_10,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_1846,c_49]) ).
tcf(c_3064,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,iPr_def_10,iPr_def_10),X0)
| ( set_intersection2(X1,iPr_def_10) = iPr_def_10 )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_1847,c_53]) ).
tcf(c_3065,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = iPr_def_10 )
| ~ in(sK5,sK1(X0,iPr_def_10,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_1847,c_49]) ).
tcf(c_3067,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = iPr_def_10 )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,iPr_def_10,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1847,c_2189]) ).
tcf(c_3068,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,iPr_def_10),iPr_def_10)
| ( set_intersection2(X0,iPr_def_10) = iPr_def_10 )
| ~ in(sK1(X0,iPr_def_10,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1847,c_722]) ).
tcf(c_3137,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,iPr_def_10),X2)
| in(sK0(set_intersection2(iPr_def_10,X1),X2),X0)
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_1896,c_53]) ).
tcf(c_3138,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(sK6,sK0(set_intersection2(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_1896,c_49]) ).
tcf(c_3157,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,iPr_def_10),X2)
| in(sK0(set_intersection2(iPr_def_10,X1),X2),X0)
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_1897,c_53]) ).
tcf(c_3158,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(sK5,sK0(set_intersection2(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_1897,c_49]) ).
tcf(c_3161,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ empty(iPr_def_10)
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1897,c_2189]) ).
tcf(c_3162,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| in(sK0(set_intersection2(iPr_def_10,X0),X1),iPr_def_10)
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1897,c_722]) ).
tcf(c_3217,plain,
! [X0: $i] :
( subset(sK5,X0)
| ~ empty(iPr_def_10)
| ~ subset(sK5,sK6) ),
inference(superposition,[status(thm)],[c_681,c_2426]) ).
tcf(c_3218,plain,
! [X0: $i] :
( subset(sK5,X0)
| ~ empty(iPr_def_10)
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1240,c_2426]) ).
tcf(c_3225,plain,
( subset(sK5,empty_set)
| ~ empty(iPr_def_10)
| ~ subset(sK5,iPr_def_10) ),
inference(instantiation,[status(thm)],[c_3218]) ).
tcf(c_3226,plain,
( subset(sK5,empty_set)
| ~ empty(iPr_def_10)
| ~ subset(sK5,sK6) ),
inference(instantiation,[status(thm)],[c_3217]) ).
tcf(c_3241,plain,
( ~ subset(sK5,sK6)
| ~ empty(iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_3217,c_60,c_66,c_327,c_822,c_1005,c_1279,c_1657,c_3226]) ).
tcf(c_3242,plain,
( ~ empty(iPr_def_10)
| ~ subset(sK5,sK6) ),
inference(renaming,[status(thm)],[c_3241]) ).
tcf(c_3248,plain,
( ~ subset(sK5,iPr_def_10)
| ~ empty(iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_3218,c_60,c_66,c_327,c_822,c_1005,c_1279,c_1657,c_3225]) ).
tcf(c_3249,plain,
( ~ empty(iPr_def_10)
| ~ subset(sK5,iPr_def_10) ),
inference(renaming,[status(thm)],[c_3248]) ).
tcf(c_3255,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ empty(iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_2433,c_843,c_2433]) ).
tcf(c_3264,plain,
! [X0: $i] :
( subset(sK5,X0)
| ~ in(iPr_def_10,sK0(sK5,X0))
| ~ in(sK0(sK5,X0),sK6) ),
inference(superposition,[status(thm)],[c_52,c_2828]) ).
tcf(c_3265,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,sK5,X1),X1)
| ( set_intersection2(X0,sK5) = X1 )
| ~ in(iPr_def_10,sK1(X0,sK5,X1))
| ~ in(sK1(X0,sK5,X1),sK6) ),
inference(superposition,[status(thm)],[c_56,c_2828]) ).
tcf(c_3266,plain,
! [X0: $i,X1: $i] :
( in(sK1(sK5,X0,X1),X1)
| ( set_intersection2(sK5,X0) = X1 )
| ~ in(iPr_def_10,sK1(sK5,X0,X1))
| ~ in(sK1(sK5,X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_55,c_2828]) ).
tcf(c_3267,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),X1)
| ( set_intersection2(X0,X1) = sK5 )
| ~ in(iPr_def_10,sK1(X0,X1,sK5))
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_56,c_2828]) ).
tcf(c_3268,plain,
! [X0: $i,X1: $i] :
( in(sK1(X0,X1,sK5),X0)
| ( set_intersection2(X0,X1) = sK5 )
| ~ in(iPr_def_10,sK1(X0,X1,sK5))
| ~ in(sK1(X0,X1,sK5),sK6) ),
inference(superposition,[status(thm)],[c_55,c_2828]) ).
tcf(c_3269,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(sK5,X0),X1))
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1461,c_2828]) ).
tcf(c_3270,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(sK5,X0),X1))
| ~ in(sK0(set_intersection2(sK5,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_632,c_2828]) ).
tcf(c_3271,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0))
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_651,c_2828]) ).
tcf(c_3272,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,sK5)
| ~ in(iPr_def_10,sK0(X0,X1))
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_681,c_2828]) ).
tcf(c_3273,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK6,sK5)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0))
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_874,c_2828]) ).
tcf(c_3274,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,sK5)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0))
| ~ in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_682,c_2828]) ).
tcf(c_3275,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(sK5,X0),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(X0,sK5),X1))
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_943,c_2828]) ).
tcf(c_3276,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,sK5),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(X0,sK5),X1))
| ~ in(sK0(set_intersection2(X0,sK5),X1),sK6) ),
inference(superposition,[status(thm)],[c_694,c_2828]) ).
tcf(c_3277,plain,
! [X0: $i] :
( ( set_intersection2(sK5,X0) = empty_set )
| ~ in(iPr_def_10,sK1(sK5,X0,empty_set))
| ~ in(sK1(sK5,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2208,c_2828]) ).
tcf(c_3278,plain,
! [X0: $i] :
( ( set_intersection2(sK5,X0) = sK5 )
| ~ in(iPr_def_10,sK1(sK5,X0,sK5))
| ~ in(sK1(sK5,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_769,c_2828]) ).
tcf(c_3279,plain,
! [X0: $i] :
( ( empty_set = sK5 )
| ~ in(iPr_def_10,sK1(empty_set,X0,sK5))
| ~ in(sK1(empty_set,X0,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2230,c_2828]) ).
tcf(c_3280,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(iPr_def_10,X0),X1))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_1897,c_2828]) ).
tcf(c_3281,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(iPr_def_10,X0),X1))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),X1),sK6) ),
inference(superposition,[status(thm)],[c_957,c_2828]) ).
tcf(c_3282,plain,
! [X0: $i] :
( ( set_intersection2(X0,sK5) = empty_set )
| ~ in(iPr_def_10,sK1(X0,sK5,empty_set))
| ~ in(sK1(X0,sK5,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2207,c_2828]) ).
tcf(c_3283,plain,
! [X0: $i] :
( ( set_intersection2(X0,sK5) = sK5 )
| ~ in(iPr_def_10,sK1(X0,sK5,sK5))
| ~ in(sK1(X0,sK5,sK5),sK6) ),
inference(superposition,[status(thm)],[c_1039,c_2828]) ).
tcf(c_3284,plain,
! [X0: $i] :
( ( empty_set = sK5 )
| ~ in(iPr_def_10,sK1(X0,empty_set,sK5))
| ~ in(sK1(X0,empty_set,sK5),sK6) ),
inference(superposition,[status(thm)],[c_2233,c_2828]) ).
tcf(c_3285,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ in(iPr_def_10,sK0(X0,X1))
| ~ in(sK0(X0,X1),sK6) ),
inference(superposition,[status(thm)],[c_1241,c_2828]) ).
tcf(c_3286,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(X0,iPr_def_10),X1))
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1700,c_2828]) ).
tcf(c_3287,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ in(iPr_def_10,sK0(set_intersection2(X0,iPr_def_10),X1))
| ~ in(sK0(set_intersection2(X0,iPr_def_10),X1),sK6) ),
inference(superposition,[status(thm)],[c_1475,c_2828]) ).
tcf(c_3288,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = iPr_def_10 )
| ~ in(iPr_def_10,sK1(iPr_def_10,X0,iPr_def_10))
| ~ in(sK1(iPr_def_10,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1544,c_2828]) ).
tcf(c_3289,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = iPr_def_10 )
| ~ in(iPr_def_10,sK1(X0,iPr_def_10,iPr_def_10))
| ~ in(sK1(X0,iPr_def_10,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_1847,c_2828]) ).
tcf(c_3290,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(iPr_def_10,sK1(empty_set,X0,iPr_def_10))
| ~ in(sK1(empty_set,X0,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2267,c_2828]) ).
tcf(c_3291,plain,
! [X0: $i] :
( ( empty_set = iPr_def_10 )
| ~ in(iPr_def_10,sK1(X0,empty_set,iPr_def_10))
| ~ in(sK1(X0,empty_set,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_2322,c_2828]) ).
tcf(c_3470,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,iPr_def_10,empty_set),X0)
| ( set_intersection2(X1,iPr_def_10) = empty_set )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_2852,c_53]) ).
tcf(c_3471,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = empty_set )
| ~ in(sK6,sK1(X0,iPr_def_10,empty_set)) ),
inference(superposition,[status(thm)],[c_2852,c_49]) ).
tcf(c_3489,plain,
! [X0: $i,X1: $i] :
( in(sK1(X1,iPr_def_10,empty_set),X0)
| ( set_intersection2(X1,iPr_def_10) = empty_set )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_2853,c_53]) ).
tcf(c_3490,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = empty_set )
| ~ in(sK5,sK1(X0,iPr_def_10,empty_set)) ),
inference(superposition,[status(thm)],[c_2853,c_49]) ).
tcf(c_3492,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = empty_set )
| ~ in(iPr_def_10,sK1(X0,iPr_def_10,empty_set))
| ~ in(sK1(X0,iPr_def_10,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2853,c_2828]) ).
tcf(c_3493,plain,
! [X0: $i] :
( ( set_intersection2(X0,iPr_def_10) = empty_set )
| ~ empty(iPr_def_10)
| ~ in(sK1(X0,iPr_def_10,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2853,c_2189]) ).
tcf(c_3494,plain,
! [X0: $i] :
( in(sK1(X0,iPr_def_10,empty_set),iPr_def_10)
| ( set_intersection2(X0,iPr_def_10) = empty_set )
| ~ in(sK1(X0,iPr_def_10,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2853,c_722]) ).
tcf(c_3531,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,X0))
| ~ in(sK0(X0,set_intersection2(X1,X0)),X1) ),
inference(superposition,[status(thm)],[c_52,c_728]) ).
tcf(c_3532,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,set_intersection2(X1,set_intersection2(X2,X3)))
| ~ in(sK0(X0,set_intersection2(X1,set_intersection2(X2,X3))),X3)
| ~ in(sK0(X0,set_intersection2(X1,set_intersection2(X2,X3))),X2)
| ~ in(sK0(X0,set_intersection2(X1,set_intersection2(X2,X3))),X1) ),
inference(superposition,[status(thm)],[c_57,c_728]) ).
tcf(c_3534,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),set_intersection2(X2,X0))
| ~ in(sK0(set_intersection2(X0,X1),set_intersection2(X2,X0)),X2) ),
inference(superposition,[status(thm)],[c_632,c_728]) ).
tcf(c_3535,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,sK5))
| ~ in(sK0(iPr_def_10,set_intersection2(X0,sK5)),X0) ),
inference(superposition,[status(thm)],[c_651,c_728]) ).
tcf(c_3536,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,set_intersection2(X1,X2))
| ~ subset(X0,X2)
| ~ in(sK0(X0,set_intersection2(X1,X2)),X1) ),
inference(superposition,[status(thm)],[c_681,c_728]) ).
tcf(c_3537,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,set_intersection2(X0,X1))
| ~ subset(sK6,X1)
| ~ in(sK0(iPr_def_10,set_intersection2(X0,X1)),X0) ),
inference(superposition,[status(thm)],[c_874,c_728]) ).
tcf(c_3538,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,set_intersection2(X0,X1))
| ~ subset(sK5,X1)
| ~ in(sK0(iPr_def_10,set_intersection2(X0,X1)),X0) ),
inference(superposition,[status(thm)],[c_682,c_728]) ).
tcf(c_3540,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),set_intersection2(X2,X1))
| ~ in(sK0(set_intersection2(X0,X1),set_intersection2(X2,X1)),X2) ),
inference(superposition,[status(thm)],[c_694,c_728]) ).
tcf(c_3541,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,sK6))
| ~ in(sK0(iPr_def_10,set_intersection2(X0,sK6)),X0) ),
inference(superposition,[status(thm)],[c_843,c_728]) ).
tcf(c_3542,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK6))
| subset(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK6))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK6)),X1) ),
inference(superposition,[status(thm)],[c_1896,c_728]) ).
tcf(c_3543,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK6))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK6)),X1) ),
inference(superposition,[status(thm)],[c_956,c_728]) ).
tcf(c_3544,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK5))
| subset(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK5))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK5)),X1) ),
inference(superposition,[status(thm)],[c_1897,c_728]) ).
tcf(c_3545,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK5))
| ~ in(sK0(set_intersection2(iPr_def_10,X0),set_intersection2(X1,sK5)),X1) ),
inference(superposition,[status(thm)],[c_957,c_728]) ).
tcf(c_3546,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,sK6))
| ~ subset(X0,iPr_def_10)
| ~ in(sK0(X0,set_intersection2(X1,sK6)),X1) ),
inference(superposition,[status(thm)],[c_1240,c_728]) ).
tcf(c_3547,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,sK5))
| ~ subset(X0,iPr_def_10)
| ~ in(sK0(X0,set_intersection2(X1,sK5)),X1) ),
inference(superposition,[status(thm)],[c_1241,c_728]) ).
tcf(c_3549,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK6))
| ~ in(sK0(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK6)),X1) ),
inference(superposition,[status(thm)],[c_1474,c_728]) ).
tcf(c_3551,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK5))
| ~ in(sK0(set_intersection2(X0,iPr_def_10),set_intersection2(X1,sK5)),X1) ),
inference(superposition,[status(thm)],[c_1475,c_728]) ).
tcf(c_3552,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,set_intersection2(X1,X2))
| ~ in(sK0(X0,set_intersection2(X2,X1)),X2)
| ~ in(sK0(X0,set_intersection2(X1,X2)),X1) ),
inference(superposition,[status(thm)],[c_50,c_728]) ).
tcf(c_3554,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,X1))
| ~ in(sK0(X0,X1),X1)
| ~ in(sK0(X0,set_intersection2(X1,X1)),X1) ),
inference(superposition,[status(thm)],[c_61,c_728]) ).
tcf(c_3555,plain,
! [X0: $i] :
( subset(X0,set_intersection2(sK5,sK6))
| ~ in(sK0(X0,iPr_def_10),sK6)
| ~ in(sK0(X0,set_intersection2(sK5,sK6)),sK5) ),
inference(superposition,[status(thm)],[c_324,c_728]) ).
tcf(c_3556,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,empty_set))
| ~ in(sK0(X0,empty_set),empty_set)
| ~ in(sK0(X0,set_intersection2(X1,empty_set)),X1) ),
inference(superposition,[status(thm)],[c_68,c_728]) ).
tcf(c_3557,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(empty_set,X1))
| ~ in(sK0(X0,empty_set),X1)
| ~ in(sK0(X0,set_intersection2(empty_set,X1)),empty_set) ),
inference(superposition,[status(thm)],[c_587,c_728]) ).
tcf(c_3591,plain,
! [X0: $i] :
( subset(X0,iPr_def_10)
| ~ in(sK0(X0,iPr_def_10),sK6)
| ~ in(sK0(X0,iPr_def_10),sK5) ),
inference(light_normalisation,[status(thm)],[c_3555,c_324]) ).
tcf(c_3735,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X1)
| subset(set_intersection2(sK0(X0,X1),X2),X3)
| ~ subset(X0,sK0(set_intersection2(sK0(X0,X1),X2),X3)) ),
inference(superposition,[status(thm)],[c_681,c_950]) ).
tcf(c_3736,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(sK0(iPr_def_10,X0),X1),X2)
| ~ subset(sK6,sK0(set_intersection2(sK0(iPr_def_10,X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_874,c_950]) ).
tcf(c_3737,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(sK0(iPr_def_10,X0),X1),X2)
| ~ subset(sK5,sK0(set_intersection2(sK0(iPr_def_10,X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_682,c_950]) ).
tcf(c_3740,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,X0),X1)
| ~ in(X0,sK0(X0,X1)) ),
inference(superposition,[status(thm)],[c_61,c_950]) ).
tcf(c_3741,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,sK6),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_324,c_950]) ).
tcf(c_3742,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,empty_set),X1)
| ~ in(X0,sK0(empty_set,X1)) ),
inference(superposition,[status(thm)],[c_68,c_950]) ).
tcf(c_3743,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(empty_set,X1),X0)
| ~ in(empty_set,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_587,c_950]) ).
tcf(c_3746,plain,
! [X0: $i,X1: $i] :
( subset(empty_set,X1)
| ~ in(X0,sK0(empty_set,X1)) ),
inference(light_normalisation,[status(thm)],[c_3742,c_68]) ).
tcf(c_3777,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X2)
| in(sK1(X1,sK0(X0,X2),X3),X3)
| ( set_intersection2(X1,sK0(X0,X2)) = X3 )
| ~ subset(X0,sK1(X1,sK0(X0,X2),X3)) ),
inference(superposition,[status(thm)],[c_56,c_1233]) ).
tcf(c_3778,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X1)
| in(sK1(sK0(X0,X1),X2,X3),X3)
| ( set_intersection2(sK0(X0,X1),X2) = X3 )
| ~ subset(X0,sK1(sK0(X0,X1),X2,X3)) ),
inference(superposition,[status(thm)],[c_55,c_1233]) ).
tcf(c_3779,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X3)
| in(sK1(X1,X2,sK0(X0,X3)),X2)
| ( set_intersection2(X1,X2) = sK0(X0,X3) )
| ~ subset(X0,sK1(X1,X2,sK0(X0,X3))) ),
inference(superposition,[status(thm)],[c_56,c_1233]) ).
tcf(c_3780,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X3)
| in(sK1(X1,X2,sK0(X0,X3)),X1)
| ( set_intersection2(X1,X2) = sK0(X0,X3) )
| ~ subset(X0,sK1(X1,X2,sK0(X0,X3))) ),
inference(superposition,[status(thm)],[c_55,c_1233]) ).
tcf(c_3781,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X1)
| subset(set_intersection2(X2,sK0(X0,X1)),X3)
| ~ subset(X0,sK0(set_intersection2(sK0(X0,X1),X2),X3)) ),
inference(superposition,[status(thm)],[c_1461,c_1233]) ).
tcf(c_3783,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X1,X2)
| subset(X0,X3)
| ~ subset(X1,sK0(X0,X3))
| ~ subset(X0,sK0(X1,X2)) ),
inference(superposition,[status(thm)],[c_681,c_1233]) ).
tcf(c_3784,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(X0,X2)
| ~ subset(sK6,sK0(X0,X2))
| ~ subset(X0,sK0(iPr_def_10,X1)) ),
inference(superposition,[status(thm)],[c_874,c_1233]) ).
tcf(c_3785,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(X0,X2)
| ~ subset(sK5,sK0(X0,X2))
| ~ subset(X0,sK0(iPr_def_10,X1)) ),
inference(superposition,[status(thm)],[c_682,c_1233]) ).
tcf(c_3786,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X2)
| subset(set_intersection2(sK0(X0,X2),X1),X3)
| ~ subset(X0,sK0(set_intersection2(X1,sK0(X0,X2)),X3)) ),
inference(superposition,[status(thm)],[c_943,c_1233]) ).
tcf(c_3787,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X2)
| subset(set_intersection2(X1,sK0(X0,X2)),X3)
| ~ subset(X0,sK0(set_intersection2(X1,sK0(X0,X2)),X3)) ),
inference(superposition,[status(thm)],[c_694,c_1233]) ).
tcf(c_3788,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| ( set_intersection2(sK0(X0,X1),X2) = empty_set )
| ~ subset(X0,sK1(sK0(X0,X1),X2,empty_set)) ),
inference(superposition,[status(thm)],[c_2208,c_1233]) ).
tcf(c_3789,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| ( set_intersection2(sK0(X0,X1),X2) = sK0(X0,X1) )
| ~ subset(X0,sK1(sK0(X0,X1),X2,sK0(X0,X1))) ),
inference(superposition,[status(thm)],[c_769,c_1233]) ).
tcf(c_3791,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ( set_intersection2(X1,sK0(X0,X2)) = empty_set )
| ~ subset(X0,sK1(X1,sK0(X0,X2),empty_set)) ),
inference(superposition,[status(thm)],[c_2207,c_1233]) ).
tcf(c_3792,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ( set_intersection2(X1,sK0(X0,X2)) = sK0(X0,X2) )
| ~ subset(X0,sK1(X1,sK0(X0,X2),sK0(X0,X2))) ),
inference(superposition,[status(thm)],[c_1039,c_1233]) ).
tcf(c_3858,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| in(sK1(X0,sK0(iPr_def_10,X1),X2),X2)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = X2 )
| ~ subset(sK5,sK1(X0,sK0(iPr_def_10,X1),X2)) ),
inference(superposition,[status(thm)],[c_56,c_1373]) ).
tcf(c_3859,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| in(sK1(sK0(iPr_def_10,X0),X1,X2),X2)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = X2 )
| ~ subset(sK5,sK1(sK0(iPr_def_10,X0),X1,X2)) ),
inference(superposition,[status(thm)],[c_55,c_1373]) ).
tcf(c_3860,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK1(X0,X1,sK0(iPr_def_10,X2)),X1)
| ( set_intersection2(X0,X1) = sK0(iPr_def_10,X2) )
| ~ subset(sK5,sK1(X0,X1,sK0(iPr_def_10,X2))) ),
inference(superposition,[status(thm)],[c_56,c_1373]) ).
tcf(c_3861,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK1(X0,X1,sK0(iPr_def_10,X2)),X0)
| ( set_intersection2(X0,X1) = sK0(iPr_def_10,X2) )
| ~ subset(sK5,sK1(X0,X1,sK0(iPr_def_10,X2))) ),
inference(superposition,[status(thm)],[c_55,c_1373]) ).
tcf(c_3862,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(X1,sK0(iPr_def_10,X0)),X2)
| ~ subset(sK5,sK0(set_intersection2(sK0(iPr_def_10,X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_1461,c_1373]) ).
tcf(c_3865,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| subset(iPr_def_10,X0)
| ~ subset(sK6,sK0(iPr_def_10,X1))
| ~ subset(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_874,c_1373]) ).
tcf(c_3866,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| subset(iPr_def_10,X0)
| ~ subset(sK5,sK0(iPr_def_10,X1))
| ~ subset(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_682,c_1373]) ).
tcf(c_3867,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(sK0(iPr_def_10,X1),X0),X2)
| ~ subset(sK5,sK0(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)) ),
inference(superposition,[status(thm)],[c_943,c_1373]) ).
tcf(c_3868,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)
| ~ subset(sK5,sK0(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)) ),
inference(superposition,[status(thm)],[c_694,c_1373]) ).
tcf(c_3869,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = empty_set )
| ~ subset(sK5,sK1(sK0(iPr_def_10,X0),X1,empty_set)) ),
inference(superposition,[status(thm)],[c_2208,c_1373]) ).
tcf(c_3870,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = sK0(iPr_def_10,X0) )
| ~ subset(sK5,sK1(sK0(iPr_def_10,X0),X1,sK0(iPr_def_10,X0))) ),
inference(superposition,[status(thm)],[c_769,c_1373]) ).
tcf(c_3872,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = empty_set )
| ~ subset(sK5,sK1(X0,sK0(iPr_def_10,X1),empty_set)) ),
inference(superposition,[status(thm)],[c_2207,c_1373]) ).
tcf(c_3873,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = sK0(iPr_def_10,X1) )
| ~ subset(sK5,sK1(X0,sK0(iPr_def_10,X1),sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_1039,c_1373]) ).
tcf(c_4001,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)
| ~ subset(sK6,sK0(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)) ),
inference(superposition,[status(thm)],[c_874,c_1468]) ).
tcf(c_4006,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,sK6),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_324,c_1468]) ).
tcf(c_4007,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,empty_set),X0)
| ~ in(empty_set,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_68,c_1468]) ).
tcf(c_4008,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(empty_set,X0),X1)
| ~ in(X0,sK0(empty_set,X1)) ),
inference(superposition,[status(thm)],[c_587,c_1468]) ).
tcf(c_4017,plain,
! [X0: $i] :
( subset(empty_set,X0)
| ~ in(empty_set,sK0(empty_set,X0)) ),
inference(demodulation,[status(thm)],[c_3743,c_587]) ).
tcf(c_4023,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X1,empty_set),X0)
| ( set_intersection2(iPr_def_10,X1) = empty_set )
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_2911,c_53]) ).
tcf(c_4024,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = empty_set )
| ~ in(sK6,sK1(iPr_def_10,X0,empty_set)) ),
inference(superposition,[status(thm)],[c_2911,c_49]) ).
tcf(c_4026,plain,
( ( set_intersection2(iPr_def_10,sK6) = empty_set )
| ~ in(sK1(iPr_def_10,sK6,empty_set),iPr_def_10)
| ~ in(sK1(iPr_def_10,sK6,empty_set),empty_set) ),
inference(superposition,[status(thm)],[c_2911,c_54]) ).
tcf(c_4037,plain,
! [X0: $i,X1: $i] :
( in(sK1(iPr_def_10,X1,empty_set),X0)
| ( set_intersection2(iPr_def_10,X1) = empty_set )
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_2912,c_53]) ).
tcf(c_4038,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = empty_set )
| ~ in(sK5,sK1(iPr_def_10,X0,empty_set)) ),
inference(superposition,[status(thm)],[c_2912,c_49]) ).
tcf(c_4040,plain,
( ( set_intersection2(iPr_def_10,sK5) = empty_set )
| ~ in(sK1(iPr_def_10,sK5,empty_set),iPr_def_10)
| ~ in(sK1(iPr_def_10,sK5,empty_set),empty_set) ),
inference(superposition,[status(thm)],[c_2912,c_54]) ).
tcf(c_4041,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = empty_set )
| ~ in(iPr_def_10,sK1(iPr_def_10,X0,empty_set))
| ~ in(sK1(iPr_def_10,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2912,c_2828]) ).
tcf(c_4042,plain,
! [X0: $i] :
( ( set_intersection2(iPr_def_10,X0) = empty_set )
| ~ empty(iPr_def_10)
| ~ in(sK1(iPr_def_10,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2912,c_2189]) ).
tcf(c_4043,plain,
! [X0: $i] :
( in(sK1(iPr_def_10,X0,empty_set),iPr_def_10)
| ( set_intersection2(iPr_def_10,X0) = empty_set )
| ~ in(sK1(iPr_def_10,X0,empty_set),sK6) ),
inference(superposition,[status(thm)],[c_2912,c_722]) ).
tcf(c_4067,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = sK0(iPr_def_10,X0) )
| ~ subset(sK6,sK1(sK0(iPr_def_10,X0),X1,sK0(iPr_def_10,X0))) ),
inference(superposition,[status(thm)],[c_874,c_1537]) ).
tcf(c_4080,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| in(sK1(X0,sK0(iPr_def_10,X1),X2),X2)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = X2 )
| ~ subset(sK6,sK1(X0,sK0(iPr_def_10,X1),X2)) ),
inference(superposition,[status(thm)],[c_56,c_1597]) ).
tcf(c_4081,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| in(sK1(sK0(iPr_def_10,X0),X1,X2),X2)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = X2 )
| ~ subset(sK6,sK1(sK0(iPr_def_10,X0),X1,X2)) ),
inference(superposition,[status(thm)],[c_55,c_1597]) ).
tcf(c_4082,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK1(X0,X1,sK0(iPr_def_10,X2)),X1)
| ( set_intersection2(X0,X1) = sK0(iPr_def_10,X2) )
| ~ subset(sK6,sK1(X0,X1,sK0(iPr_def_10,X2))) ),
inference(superposition,[status(thm)],[c_56,c_1597]) ).
tcf(c_4083,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X2)
| in(sK1(X0,X1,sK0(iPr_def_10,X2)),X0)
| ( set_intersection2(X0,X1) = sK0(iPr_def_10,X2) )
| ~ subset(sK6,sK1(X0,X1,sK0(iPr_def_10,X2))) ),
inference(superposition,[status(thm)],[c_55,c_1597]) ).
tcf(c_4084,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(X1,sK0(iPr_def_10,X0)),X2)
| ~ subset(sK6,sK0(set_intersection2(sK0(iPr_def_10,X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_1461,c_1597]) ).
tcf(c_4087,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| subset(iPr_def_10,X0)
| ~ subset(sK6,sK0(iPr_def_10,X1))
| ~ subset(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_874,c_1597]) ).
tcf(c_4089,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(sK0(iPr_def_10,X1),X0),X2)
| ~ subset(sK6,sK0(set_intersection2(X0,sK0(iPr_def_10,X1)),X2)) ),
inference(superposition,[status(thm)],[c_943,c_1597]) ).
tcf(c_4091,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| ( set_intersection2(sK0(iPr_def_10,X0),X1) = empty_set )
| ~ subset(sK6,sK1(sK0(iPr_def_10,X0),X1,empty_set)) ),
inference(superposition,[status(thm)],[c_2208,c_1597]) ).
tcf(c_4094,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = empty_set )
| ~ subset(sK6,sK1(X0,sK0(iPr_def_10,X1),empty_set)) ),
inference(superposition,[status(thm)],[c_2207,c_1597]) ).
tcf(c_4095,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ( set_intersection2(X0,sK0(iPr_def_10,X1)) = sK0(iPr_def_10,X1) )
| ~ subset(sK6,sK1(X0,sK0(iPr_def_10,X1),sK0(iPr_def_10,X1))) ),
inference(superposition,[status(thm)],[c_1039,c_1597]) ).
tcf(c_4174,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,sK5),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_324,c_1693]) ).
tcf(c_4187,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,iPr_def_10),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_61,c_1751]) ).
tcf(c_4188,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,empty_set),X0)
| ~ in(sK6,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_68,c_1751]) ).
tcf(c_4196,plain,
! [X0: $i] :
( subset(empty_set,X0)
| ~ in(sK6,sK0(empty_set,X0)) ),
inference(demodulation,[status(thm)],[c_4188,c_68]) ).
tcf(c_4210,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X1)
| subset(set_intersection2(sK0(X0,X1),X2),X3)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_3735]) ).
tcf(c_4211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(set_intersection2(X0,X1),X2)
| subset(set_intersection2(sK0(set_intersection2(X0,X1),X2),X3),X4)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_3735]) ).
tcf(c_4213,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(set_intersection2(X1,X0),X2)
| subset(set_intersection2(sK0(set_intersection2(X1,X0),X2),X3),X4)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_3735]) ).
tcf(c_4216,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X1)
| subset(set_intersection2(sK0(X0,X1),sK0(X0,X1)),X2)
| ~ subset(X0,sK0(sK0(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_61,c_3735]) ).
tcf(c_4217,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| subset(set_intersection2(sK0(X0,X2),empty_set),X1)
| ~ subset(X0,sK0(empty_set,X1)) ),
inference(superposition,[status(thm)],[c_68,c_3735]) ).
tcf(c_4243,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,sK5),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_324,c_1890]) ).
tcf(c_4256,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,iPr_def_10),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_61,c_1956]) ).
tcf(c_4257,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,empty_set),X0)
| ~ in(sK5,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_68,c_1956]) ).
tcf(c_4265,plain,
! [X0: $i] :
( subset(empty_set,X0)
| ~ in(sK5,sK0(empty_set,X0)) ),
inference(demodulation,[status(thm)],[c_4257,c_68]) ).
tcf(c_4285,plain,
! [X0: $i] :
( subset(set_intersection2(empty_set,iPr_def_10),X0)
| ~ in(sK6,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_587,c_2682]) ).
tcf(c_4297,plain,
! [X0: $i] :
( subset(set_intersection2(empty_set,iPr_def_10),X0)
| ~ in(sK5,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_587,c_2704]) ).
tcf(c_4308,plain,
set_intersection2(iPr_def_10,sK6) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_2750,c_769]) ).
tcf(c_4309,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_1693]) ).
tcf(c_4312,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_1890]) ).
tcf(c_4313,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_950]) ).
tcf(c_4314,plain,
! [X0: $i] :
( ~ in(iPr_def_10,X0)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_726]) ).
tcf(c_4315,plain,
! [X0: $i,X1: $i] :
( in(X0,X1)
| ~ subset(iPr_def_10,X1)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_725]) ).
tcf(c_4316,plain,
! [X0: $i] :
( ~ empty(iPr_def_10)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_727]) ).
tcf(c_4317,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4308,c_1461]) ).
tcf(c_4322,plain,
subset(iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_4308,c_952]) ).
tcf(c_4323,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| in(sK0(iPr_def_10,X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4308,c_632]) ).
tcf(c_4325,plain,
! [X0: $i] :
( subset(X0,set_intersection2(iPr_def_10,sK6))
| ~ in(sK0(X0,iPr_def_10),sK6)
| ~ in(sK0(X0,set_intersection2(iPr_def_10,sK6)),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4308,c_728]) ).
tcf(c_4328,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_1956]) ).
tcf(c_4329,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_1751]) ).
tcf(c_4330,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_4308,c_1897]) ).
tcf(c_4331,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_4308,c_1896]) ).
tcf(c_4333,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_4308,c_957]) ).
tcf(c_4335,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK6),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_4308,c_956]) ).
tcf(c_4342,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| in(sK0(iPr_def_10,X0),iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_4323,c_4308]) ).
tcf(c_4352,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0)) ),
inference(light_normalisation,[status(thm)],[c_4313,c_4308]) ).
tcf(c_4366,plain,
! [X0: $i] :
( subset(X0,iPr_def_10)
| ~ in(sK0(X0,iPr_def_10),iPr_def_10)
| ~ in(sK0(X0,iPr_def_10),sK6) ),
inference(light_normalisation,[status(thm)],[c_4325,c_4308]) ).
tcf(c_4453,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(sK0(iPr_def_10,X0),sK0(iPr_def_10,X0)),X1)
| ~ subset(sK6,sK0(sK0(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_61,c_3736]) ).
tcf(c_4454,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(sK0(iPr_def_10,X1),empty_set),X0)
| ~ subset(sK6,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_68,c_3736]) ).
tcf(c_4469,plain,
set_intersection2(iPr_def_10,sK5) = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_2766,c_769]) ).
tcf(c_4470,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_1693]) ).
tcf(c_4473,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_1890]) ).
tcf(c_4474,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| ~ in(iPr_def_10,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_950]) ).
tcf(c_4475,plain,
! [X0: $i] :
( ~ in(iPr_def_10,X0)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_726]) ).
tcf(c_4476,plain,
! [X0: $i,X1: $i] :
( in(X0,X1)
| ~ subset(iPr_def_10,X1)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_725]) ).
tcf(c_4477,plain,
! [X0: $i] :
( ~ empty(iPr_def_10)
| ~ in(X0,iPr_def_10)
| ~ in(X0,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_727]) ).
tcf(c_4478,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4469,c_1461]) ).
tcf(c_4484,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| in(sK0(iPr_def_10,X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4469,c_632]) ).
tcf(c_4486,plain,
! [X0: $i] :
( subset(X0,set_intersection2(iPr_def_10,sK5))
| ~ in(sK0(X0,iPr_def_10),sK5)
| ~ in(sK0(X0,set_intersection2(iPr_def_10,sK5)),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4469,c_728]) ).
tcf(c_4489,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_1956]) ).
tcf(c_4490,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_1751]) ).
tcf(c_4491,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_4469,c_1897]) ).
tcf(c_4492,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_4469,c_1896]) ).
tcf(c_4494,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| in(sK0(iPr_def_10,X0),sK5) ),
inference(superposition,[status(thm)],[c_4469,c_957]) ).
tcf(c_4496,plain,
! [X0: $i] :
( subset(set_intersection2(iPr_def_10,sK5),X0)
| in(sK0(iPr_def_10,X0),sK6) ),
inference(superposition,[status(thm)],[c_4469,c_956]) ).
tcf(c_4523,plain,
! [X0: $i] :
( subset(X0,iPr_def_10)
| ~ in(sK0(X0,iPr_def_10),iPr_def_10)
| ~ in(sK0(X0,iPr_def_10),sK5) ),
inference(light_normalisation,[status(thm)],[c_4486,c_4469]) ).
tcf(c_4609,plain,
! [X0: $i] :
( ~ empty(iPr_def_10)
| ~ in(X0,iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_4316,c_636,c_4477]) ).
tcf(c_4625,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X0)
| subset(set_intersection2(sK0(iPr_def_10,X0),sK0(iPr_def_10,X0)),X1)
| ~ subset(sK5,sK0(sK0(iPr_def_10,X0),X1)) ),
inference(superposition,[status(thm)],[c_61,c_3737]) ).
tcf(c_4626,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| subset(set_intersection2(sK0(iPr_def_10,X1),empty_set),X0)
| ~ subset(sK5,sK0(empty_set,X0)) ),
inference(superposition,[status(thm)],[c_68,c_3737]) ).
tcf(c_4658,plain,
! [X0: $i] :
( ~ in(iPr_def_10,X0)
| ~ in(X0,iPr_def_10) ),
inference(global_subsumption_just,[status(thm)],[c_4314,c_636,c_4475]) ).
tcf(c_4672,plain,
! [X0: $i] :
( subset(set_intersection2(sK5,iPr_def_10),X0)
| ~ in(sK6,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4469,c_3138]) ).
tcf(c_4685,plain,
! [X0: $i] :
( subset(set_intersection2(sK6,iPr_def_10),X0)
| ~ in(sK5,sK0(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_4308,c_3158]) ).
tcf(c_4703,plain,
! [X0: $i] : subset(X0,set_intersection2(X0,X0)),
inference(superposition,[status(thm)],[c_52,c_3531]) ).
tcf(c_4704,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,set_intersection2(set_intersection2(X1,X2),X0))
| ~ in(sK0(X0,set_intersection2(set_intersection2(X1,X2),X0)),X2)
| ~ in(sK0(X0,set_intersection2(set_intersection2(X1,X2),X0)),X1) ),
inference(superposition,[status(thm)],[c_57,c_3531]) ).
tcf(c_4706,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(X0,X1),set_intersection2(X0,set_intersection2(X0,X1))),
inference(superposition,[status(thm)],[c_632,c_3531]) ).
tcf(c_4707,plain,
subset(iPr_def_10,set_intersection2(sK5,iPr_def_10)),
inference(superposition,[status(thm)],[c_651,c_3531]) ).
tcf(c_4708,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,X0))
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_681,c_3531]) ).
tcf(c_4709,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,iPr_def_10))
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_874,c_3531]) ).
tcf(c_4710,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,iPr_def_10))
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_682,c_3531]) ).
tcf(c_4712,plain,
! [X0: $i,X1: $i] : subset(set_intersection2(X0,X1),set_intersection2(X1,set_intersection2(X0,X1))),
inference(superposition,[status(thm)],[c_694,c_3531]) ).
tcf(c_4713,plain,
subset(iPr_def_10,set_intersection2(sK6,iPr_def_10)),
inference(superposition,[status(thm)],[c_843,c_3531]) ).
tcf(c_4715,plain,
! [X0: $i] : subset(set_intersection2(iPr_def_10,X0),set_intersection2(sK6,set_intersection2(iPr_def_10,X0))),
inference(superposition,[status(thm)],[c_956,c_3531]) ).
tcf(c_4717,plain,
! [X0: $i] : subset(set_intersection2(iPr_def_10,X0),set_intersection2(sK5,set_intersection2(iPr_def_10,X0))),
inference(superposition,[status(thm)],[c_957,c_3531]) ).
tcf(c_4718,plain,
! [X0: $i] :
( subset(X0,set_intersection2(sK6,X0))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1240,c_3531]) ).
tcf(c_4719,plain,
! [X0: $i] :
( subset(X0,set_intersection2(sK5,X0))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1241,c_3531]) ).
tcf(c_4721,plain,
! [X0: $i] : subset(set_intersection2(X0,iPr_def_10),set_intersection2(sK6,set_intersection2(X0,iPr_def_10))),
inference(superposition,[status(thm)],[c_1474,c_3531]) ).
tcf(c_4723,plain,
! [X0: $i] : subset(set_intersection2(X0,iPr_def_10),set_intersection2(sK5,set_intersection2(X0,iPr_def_10))),
inference(superposition,[status(thm)],[c_1475,c_3531]) ).
tcf(c_4724,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,X0))
| ~ in(sK0(X0,set_intersection2(X0,X1)),X1) ),
inference(superposition,[status(thm)],[c_50,c_3531]) ).
tcf(c_4726,plain,
! [X0: $i] :
( subset(X0,set_intersection2(X0,X0))
| ~ in(sK0(X0,X0),X0) ),
inference(superposition,[status(thm)],[c_61,c_3531]) ).
tcf(c_4727,plain,
( subset(sK6,set_intersection2(sK5,sK6))
| ~ in(sK0(sK6,iPr_def_10),sK5) ),
inference(superposition,[status(thm)],[c_324,c_3531]) ).
tcf(c_4728,plain,
! [X0: $i] :
( subset(empty_set,set_intersection2(X0,empty_set))
| ~ in(sK0(empty_set,empty_set),X0) ),
inference(superposition,[status(thm)],[c_68,c_3531]) ).
tcf(c_4729,plain,
! [X0: $i] :
( subset(X0,set_intersection2(empty_set,X0))
| ~ in(sK0(X0,empty_set),empty_set) ),
inference(superposition,[status(thm)],[c_587,c_3531]) ).
tcf(c_4730,plain,
( subset(sK6,set_intersection2(iPr_def_10,sK6))
| ~ in(sK0(sK6,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4308,c_3531]) ).
tcf(c_4731,plain,
( subset(sK5,set_intersection2(iPr_def_10,sK5))
| ~ in(sK0(sK5,iPr_def_10),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4469,c_3531]) ).
tcf(c_4743,plain,
( subset(sK5,iPr_def_10)
| ~ in(sK0(sK5,iPr_def_10),iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_4731,c_4469]) ).
tcf(c_4746,plain,
( subset(sK6,iPr_def_10)
| ~ in(sK0(sK6,iPr_def_10),iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_4730,c_4308]) ).
tcf(c_4749,plain,
! [X0: $i] :
( subset(X0,empty_set)
| ~ in(sK0(X0,empty_set),empty_set) ),
inference(light_normalisation,[status(thm)],[c_4729,c_587]) ).
tcf(c_4750,plain,
! [X0: $i] :
( subset(empty_set,empty_set)
| ~ in(sK0(empty_set,empty_set),X0) ),
inference(light_normalisation,[status(thm)],[c_4728,c_68]) ).
tcf(c_4751,plain,
( subset(sK6,iPr_def_10)
| ~ in(sK0(sK6,iPr_def_10),sK5) ),
inference(light_normalisation,[status(thm)],[c_4727,c_324]) ).
tcf(c_4754,plain,
! [X0: $i] :
( subset(X0,X0)
| ~ in(sK0(X0,X0),X0) ),
inference(light_normalisation,[status(thm)],[c_4726,c_61]) ).
tcf(c_4804,plain,
! [X0: $i] : subset(set_intersection2(empty_set,X0),empty_set),
inference(superposition,[status(thm)],[c_587,c_4706]) ).
tcf(c_4810,plain,
subset(empty_set,set_intersection2(empty_set,empty_set)),
inference(superposition,[status(thm)],[c_587,c_4706]) ).
tcf(c_4811,plain,
subset(iPr_def_10,set_intersection2(iPr_def_10,iPr_def_10)),
inference(superposition,[status(thm)],[c_4308,c_4706]) ).
tcf(c_4813,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X0,X1),X2)
| ~ empty(set_intersection2(X0,set_intersection2(X0,X1))) ),
inference(superposition,[status(thm)],[c_4706,c_1234]) ).
tcf(c_4814,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_intersection2(X1,set_intersection2(X1,X2)))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4706,c_725]) ).
tcf(c_4827,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X0,X2)
| subset(set_intersection2(X1,sK0(X0,X2)),X3)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_613,c_3781]) ).
tcf(c_4828,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(set_intersection2(X0,X2),X3)
| subset(set_intersection2(X1,sK0(set_intersection2(X0,X2),X3)),X4)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_951,c_3781]) ).
tcf(c_4829,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(empty_set,X1)
| subset(set_intersection2(X0,sK0(empty_set,X1)),X2) ),
inference(superposition,[status(thm)],[c_864,c_3781]) ).
tcf(c_4830,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(set_intersection2(X2,X0),X3)
| subset(set_intersection2(X1,sK0(set_intersection2(X2,X0),X3)),X4)
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_1200,c_3781]) ).
tcf(c_4834,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| subset(set_intersection2(empty_set,sK0(X0,X2)),X1)
| ~ subset(X0,sK0(empty_set,X1)) ),
inference(superposition,[status(thm)],[c_68,c_3781]) ).
tcf(c_4851,plain,
( subset(sK6,iPr_def_10)
| ~ subset(sK6,sK5) ),
inference(superposition,[status(thm)],[c_681,c_4751]) ).
tcf(c_4868,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,set_intersection2(set_intersection2(X1,X2),X0))
| ~ in(sK0(X0,set_intersection2(X0,set_intersection2(X1,X2))),X2)
| ~ in(sK0(X0,set_intersection2(X0,set_intersection2(X1,X2))),X1) ),
inference(superposition,[status(thm)],[c_57,c_4724]) ).
tcf(c_4869,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,X0),set_intersection2(X1,set_intersection2(X1,X0)))
| subset(set_intersection2(X0,X1),set_intersection2(set_intersection2(X1,X0),X1)) ),
inference(superposition,[status(thm)],[c_1461,c_4724]) ).
tcf(c_4871,plain,
( subset(iPr_def_10,set_intersection2(iPr_def_10,sK5))
| subset(iPr_def_10,set_intersection2(sK5,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_651,c_4724]) ).
tcf(c_4872,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X1,X0))
| subset(X0,set_intersection2(X0,X1))
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_681,c_4724]) ).
tcf(c_4875,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X1,X0),set_intersection2(X0,set_intersection2(X1,X0)))
| subset(set_intersection2(X0,X1),set_intersection2(set_intersection2(X1,X0),X0)) ),
inference(superposition,[status(thm)],[c_943,c_4724]) ).
tcf(c_4877,plain,
( subset(iPr_def_10,set_intersection2(iPr_def_10,sK6))
| subset(iPr_def_10,set_intersection2(sK6,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_843,c_4724]) ).
tcf(c_4882,plain,
! [X0: $i] :
( subset(X0,set_intersection2(sK6,X0))
| subset(X0,set_intersection2(X0,sK6))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1240,c_4724]) ).
tcf(c_4883,plain,
! [X0: $i] :
( subset(X0,set_intersection2(sK5,X0))
| subset(X0,set_intersection2(X0,sK5))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_1241,c_4724]) ).
tcf(c_4891,plain,
( subset(sK5,set_intersection2(sK6,sK5))
| ~ in(sK0(sK5,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_324,c_4724]) ).
tcf(c_4894,plain,
( subset(iPr_def_10,set_intersection2(sK6,iPr_def_10))
| ~ in(sK0(iPr_def_10,iPr_def_10),sK6) ),
inference(superposition,[status(thm)],[c_4308,c_4724]) ).
tcf(c_4895,plain,
( subset(iPr_def_10,set_intersection2(sK5,iPr_def_10))
| ~ in(sK0(iPr_def_10,iPr_def_10),sK5) ),
inference(superposition,[status(thm)],[c_4469,c_4724]) ).
tcf(c_4896,plain,
( subset(iPr_def_10,iPr_def_10)
| subset(iPr_def_10,set_intersection2(sK6,iPr_def_10)) ),
inference(light_normalisation,[status(thm)],[c_4877,c_4308]) ).
tcf(c_4897,plain,
( subset(iPr_def_10,iPr_def_10)
| subset(iPr_def_10,set_intersection2(sK5,iPr_def_10)) ),
inference(light_normalisation,[status(thm)],[c_4871,c_4469]) ).
tcf(c_4931,plain,
! [X0: $i,X1: $i] :
( subset(X0,set_intersection2(X0,X1))
| ~ subset(X0,X1) ),
inference(superposition,[status(thm)],[c_50,c_4708]) ).
tcf(c_4935,plain,
! [X0: $i] :
( subset(empty_set,empty_set)
| ~ subset(empty_set,X0) ),
inference(superposition,[status(thm)],[c_68,c_4708]) ).
tcf(c_4939,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X1,X2)
| ~ subset(X1,X0)
| ~ empty(set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_4708,c_1234]) ).
tcf(c_4940,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X3,set_intersection2(X2,set_intersection2(X0,X1)))
| ~ in(X3,X1)
| ~ in(X3,X0)
| ~ subset(set_intersection2(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_4708,c_725]) ).
tcf(c_4941,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK5,X0)
| ~ empty(set_intersection2(X0,sK5)) ),
inference(superposition,[status(thm)],[c_4708,c_1374]) ).
tcf(c_4942,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,sK5))
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_4708,c_1375]) ).
tcf(c_4943,plain,
! [X0: $i] :
( ~ subset(sK6,X0)
| ~ empty(set_intersection2(X0,sK6)) ),
inference(superposition,[status(thm)],[c_4708,c_1674]) ).
tcf(c_4944,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(X0,sK6))
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_4708,c_1599]) ).
tcf(c_5018,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(iPr_def_10,X0))
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_50,c_4709]) ).
tcf(c_5020,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK6,iPr_def_10) ),
inference(superposition,[status(thm)],[c_61,c_4709]) ).
tcf(c_5022,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK6,X0)
| ~ empty(set_intersection2(X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_4709,c_1234]) ).
tcf(c_5032,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(iPr_def_10,X0))
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_50,c_4710]) ).
tcf(c_5034,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_61,c_4710]) ).
tcf(c_5036,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK5,X0)
| ~ empty(set_intersection2(X0,iPr_def_10)) ),
inference(superposition,[status(thm)],[c_4710,c_1234]) ).
tcf(c_5050,plain,
! [X0: $i] : subset(set_intersection2(X0,empty_set),empty_set),
inference(superposition,[status(thm)],[c_587,c_4712]) ).
tcf(c_5056,plain,
! [X0: $i] : subset(empty_set,set_intersection2(X0,empty_set)),
inference(superposition,[status(thm)],[c_587,c_4712]) ).
tcf(c_5059,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(set_intersection2(X1,X0),X2)
| ~ empty(set_intersection2(X0,set_intersection2(X1,X0))) ),
inference(superposition,[status(thm)],[c_4712,c_1234]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X0,set_intersection2(X2,set_intersection2(X1,X2)))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4712,c_725]) ).
tcf(c_5077,plain,
subset(empty_set,set_intersection2(sK6,empty_set)),
inference(superposition,[status(thm)],[c_68,c_4715]) ).
tcf(c_5080,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ empty(set_intersection2(sK6,set_intersection2(iPr_def_10,X0))) ),
inference(superposition,[status(thm)],[c_4715,c_1234]) ).
tcf(c_5081,plain,
! [X0: $i,X1: $i] :
( in(X0,set_intersection2(sK6,set_intersection2(iPr_def_10,X1)))
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4715,c_725]) ).
tcf(c_5097,plain,
subset(empty_set,set_intersection2(sK5,empty_set)),
inference(superposition,[status(thm)],[c_68,c_4717]) ).
tcf(c_5100,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(iPr_def_10,X0),X1)
| ~ empty(set_intersection2(sK5,set_intersection2(iPr_def_10,X0))) ),
inference(superposition,[status(thm)],[c_4717,c_1234]) ).
tcf(c_5101,plain,
! [X0: $i,X1: $i] :
( in(X0,set_intersection2(sK5,set_intersection2(iPr_def_10,X1)))
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4717,c_725]) ).
tcf(c_5112,plain,
! [X0: $i] :
( subset(X0,set_intersection2(X0,sK6))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_50,c_4718]) ).
tcf(c_5114,plain,
( subset(sK6,sK6)
| ~ subset(sK6,iPr_def_10) ),
inference(superposition,[status(thm)],[c_61,c_4718]) ).
tcf(c_5115,plain,
( subset(empty_set,empty_set)
| ~ subset(empty_set,iPr_def_10) ),
inference(superposition,[status(thm)],[c_68,c_4718]) ).
tcf(c_5116,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ empty(set_intersection2(sK6,X0)) ),
inference(superposition,[status(thm)],[c_4718,c_1234]) ).
tcf(c_5117,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,set_intersection2(sK6,set_intersection2(X0,X1)))
| ~ in(X2,X1)
| ~ in(X2,X0)
| ~ subset(set_intersection2(X0,X1),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4718,c_725]) ).
tcf(c_5118,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,iPr_def_10)
| ~ empty(set_intersection2(sK6,sK5)) ),
inference(superposition,[status(thm)],[c_4718,c_1374]) ).
tcf(c_5119,plain,
( subset(iPr_def_10,set_intersection2(sK6,sK5))
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_4718,c_1375]) ).
tcf(c_5120,plain,
( ~ subset(sK6,iPr_def_10)
| ~ empty(set_intersection2(sK6,sK6)) ),
inference(superposition,[status(thm)],[c_4718,c_1674]) ).
tcf(c_5121,plain,
( subset(iPr_def_10,set_intersection2(sK6,sK6))
| ~ subset(sK6,iPr_def_10) ),
inference(superposition,[status(thm)],[c_4718,c_1599]) ).
tcf(c_5188,plain,
! [X0: $i] :
( subset(X0,set_intersection2(X0,sK5))
| ~ subset(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_50,c_4719]) ).
tcf(c_5190,plain,
( subset(sK5,sK5)
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_61,c_4719]) ).
tcf(c_5193,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ empty(set_intersection2(sK5,X0)) ),
inference(superposition,[status(thm)],[c_4719,c_1234]) ).
tcf(c_5194,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,set_intersection2(sK5,set_intersection2(X0,X1)))
| ~ in(X2,X1)
| ~ in(X2,X0)
| ~ subset(set_intersection2(X0,X1),iPr_def_10) ),
inference(superposition,[status(thm)],[c_4719,c_725]) ).
tcf(c_5195,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,iPr_def_10)
| ~ empty(set_intersection2(sK5,sK5)) ),
inference(superposition,[status(thm)],[c_4719,c_1374]) ).
tcf(c_5196,plain,
( subset(iPr_def_10,set_intersection2(sK5,sK5))
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_4719,c_1375]) ).
tcf(c_5197,plain,
( ~ subset(sK6,iPr_def_10)
| ~ empty(set_intersection2(sK5,sK6)) ),
inference(superposition,[status(thm)],[c_4719,c_1674]) ).
tcf(c_5198,plain,
( subset(iPr_def_10,set_intersection2(sK5,sK6))
| ~ subset(sK6,iPr_def_10) ),
inference(superposition,[status(thm)],[c_4719,c_1599]) ).
tcf(c_5200,plain,
( ~ empty(iPr_def_10)
| ~ subset(sK6,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_5197,c_324]) ).
tcf(c_5250,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ empty(set_intersection2(sK6,set_intersection2(X0,iPr_def_10))) ),
inference(superposition,[status(thm)],[c_4721,c_1234]) ).
tcf(c_5251,plain,
! [X0: $i,X1: $i] :
( in(X0,set_intersection2(sK6,set_intersection2(X1,iPr_def_10)))
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4721,c_725]) ).
tcf(c_5266,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(X1,X2)
| subset(X0,X3)
| ~ empty(X1)
| ~ subset(X0,sK0(X1,X2)) ),
inference(superposition,[status(thm)],[c_613,c_3783]) ).
tcf(c_5268,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(X0,X4)
| subset(set_intersection2(X1,X2),X3)
| ~ empty(X1)
| ~ subset(X0,sK0(set_intersection2(X1,X2),X3)) ),
inference(superposition,[status(thm)],[c_951,c_3783]) ).
tcf(c_5269,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(empty_set,X1)
| subset(X0,X2)
| ~ subset(X0,sK0(empty_set,X1)) ),
inference(superposition,[status(thm)],[c_864,c_3783]) ).
tcf(c_5270,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( subset(X0,X4)
| subset(set_intersection2(X1,X2),X3)
| ~ empty(X2)
| ~ subset(X0,sK0(set_intersection2(X1,X2),X3)) ),
inference(superposition,[status(thm)],[c_1200,c_3783]) ).
tcf(c_5292,plain,
( subset(sK5,iPr_def_10)
| ~ subset(sK5,sK6) ),
inference(superposition,[status(thm)],[c_324,c_4931]) ).
tcf(c_5295,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(iPr_def_10,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_4931]) ).
tcf(c_5296,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(iPr_def_10,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_4931]) ).
tcf(c_5297,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ empty(set_intersection2(X0,X1)) ),
inference(superposition,[status(thm)],[c_4931,c_1234]) ).
tcf(c_5298,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X3,set_intersection2(set_intersection2(X0,X1),X2))
| ~ in(X3,X1)
| ~ in(X3,X0)
| ~ subset(set_intersection2(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_4931,c_725]) ).
tcf(c_5299,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK5,X0)
| ~ empty(set_intersection2(sK5,X0)) ),
inference(superposition,[status(thm)],[c_4931,c_1374]) ).
tcf(c_5300,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(sK5,X0))
| ~ subset(sK5,X0) ),
inference(superposition,[status(thm)],[c_4931,c_1375]) ).
tcf(c_5301,plain,
! [X0: $i] :
( ~ subset(sK6,X0)
| ~ empty(set_intersection2(sK6,X0)) ),
inference(superposition,[status(thm)],[c_4931,c_1674]) ).
tcf(c_5302,plain,
! [X0: $i] :
( subset(iPr_def_10,set_intersection2(sK6,X0))
| ~ subset(sK6,X0) ),
inference(superposition,[status(thm)],[c_4931,c_1599]) ).
tcf(c_5348,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK6,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_5018]) ).
tcf(c_5349,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK6,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_5018]) ).
tcf(c_5350,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK6,X0)
| ~ empty(set_intersection2(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_5018,c_1234]) ).
tcf(c_5405,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK5,sK6) ),
inference(superposition,[status(thm)],[c_4308,c_5032]) ).
tcf(c_5406,plain,
( subset(iPr_def_10,iPr_def_10)
| ~ subset(sK5,sK5) ),
inference(superposition,[status(thm)],[c_4469,c_5032]) ).
tcf(c_5407,plain,
! [X0: $i,X1: $i] :
( subset(iPr_def_10,X1)
| ~ subset(sK5,X0)
| ~ empty(set_intersection2(iPr_def_10,X0)) ),
inference(superposition,[status(thm)],[c_5032,c_1234]) ).
tcf(c_5419,plain,
! [X0: $i,X1: $i] :
( subset(set_intersection2(X0,iPr_def_10),X1)
| ~ empty(set_intersection2(sK5,set_intersection2(X0,iPr_def_10))) ),
inference(superposition,[status(thm)],[c_4723,c_1234]) ).
tcf(c_5420,plain,
! [X0: $i,X1: $i] :
( in(X0,set_intersection2(sK5,set_intersection2(X1,iPr_def_10)))
| ~ in(X0,iPr_def_10)
| ~ in(X0,X1) ),
inference(superposition,[status(thm)],[c_4723,c_725]) ).
tcf(c_5444,plain,
( ~ empty(iPr_def_10)
| ~ subset(sK6,sK5) ),
inference(superposition,[status(thm)],[c_324,c_4943]) ).
tcf(c_5475,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ empty(set_intersection2(X0,sK6)) ),
inference(superposition,[status(thm)],[c_5112,c_1234]) ).
tcf(c_5476,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,set_intersection2(set_intersection2(X0,X1),sK6))
| ~ in(X2,X1)
| ~ in(X2,X0)
| ~ subset(set_intersection2(X0,X1),iPr_def_10) ),
inference(superposition,[status(thm)],[c_5112,c_725]) ).
tcf(c_5477,plain,
! [X0: $i] :
( subset(iPr_def_10,X0)
| ~ subset(sK5,iPr_def_10)
| ~ empty(set_intersection2(sK5,sK6)) ),
inference(superposition,[status(thm)],[c_5112,c_1374]) ).
tcf(c_5478,plain,
( subset(iPr_def_10,set_intersection2(sK5,sK6))
| ~ subset(sK5,iPr_def_10) ),
inference(superposition,[status(thm)],[c_5112,c_1375]) ).
tcf(c_5491,plain,
( ~ empty(sK6)
| ~ subset(sK6,iPr_def_10) ),
inference(demodulation,[status(thm)],[c_5120,c_61]) ).
tcf(c_5492,plain,
( subset(iPr_def_10,sK6)
| ~ subset(sK6,iPr_def_10) ),
inference(demodulation,[status(thm)],[c_5121,c_61]) ).
tcf(c_5502,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ subset(X0,iPr_def_10)
| ~ empty(set_intersection2(X0,sK5)) ),
inference(superposition,[status(thm)],[c_5188,c_1234]) ).
tcf(c_5503,plain,
! [X0: $i,X1: $i,X2: $i] :
( in(X2,set_intersection2(set_intersection2(X0,X1),sK5))
| ~ in(X2,X1)
| ~ in(X2,X0)
| ~ subset(set_intersection2(X0,X1),iPr_def_10) ),
inference(superposition,[status(thm)],[c_5188,c_725]) ).
tcf(c_5506,plain,
( ~ subset(sK6,iPr_def_10)
| ~ empty(set_intersection2(sK6,sK5)) ),
inference(superposition,[status(thm)],[c_5188,c_1674]) ).
tcf(c_5507,plain,
( subset(iPr_def_10,set_intersection2(sK6,sK5))
| ~ subset(sK6,iPr_def_10) ),
inference(superposition,[status(thm)],[c_5188,c_1599]) ).
tcf(c_5531,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subset(iPr_def_10,X3)
| subset(set_intersection2(X0,X1),X2)
| ~ empty(X1)
| ~ subset(sK6,sK0(set_intersection2(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_1200,c_3784]) ).
tcf(c_5566,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5531,c_5507,c_5506,c_5503,c_5502,c_5492,c_5491,c_5478,c_5477,c_5476,c_5475,c_5444,c_5420,c_5419,c_5407,c_5406,c_5405,c_5350,c_5349,c_5348,c_5302,c_5301,c_5300,c_5299,c_5298,c_5297,c_5296,c_5295,c_5292,c_5270,c_5269,c_5268,c_5266,c_5251,c_5250,c_5200,c_5198,c_5197,c_5196,c_5195,c_5194,c_5193,c_5190,c_5188,c_5121,c_5120,c_5119,c_5118,c_5117,c_5116,c_5115,c_5114,c_5112,c_5101,c_5100,c_5097,c_5081,c_5080,c_5077,c_5060,c_5059,c_5050,c_5056,c_5036,c_5034,c_5032,c_5022,c_5020,c_5018,c_4944,c_4943,c_4942,c_4941,c_4940,c_4939,c_4935,c_4931,c_4897,c_4896,c_4895,c_4894,c_4891,c_4883,c_4882,c_4877,c_4875,c_4872,c_4871,c_4869,c_4868,c_4851,c_4834,c_4830,c_4829,c_4828,c_4827,c_4814,c_4813,c_4804,c_4811,c_4810,c_4754,c_4751,c_4750,c_4749,c_4746,c_4743,c_4731,c_4730,c_4729,c_4728,c_4727,c_4726,c_4724,c_4723,c_4721,c_4719,c_4718,c_4717,c_4715,c_4713,c_4712,c_4710,c_4709,c_4708,c_4707,c_4706,c_4704,c_4703,c_4685,c_4672,c_4658,c_4626,c_4625,c_4609,c_4523,c_4496,c_4492,c_4490,c_4486,c_4484,c_4494,c_4491,c_4478,c_4477,c_4476,c_4475,c_4474,c_4473,c_4489,c_4470,c_4469,c_4454,c_4453,c_4366,c_4352,c_4342,c_4333,c_4330,c_4328,c_4325,c_4323,c_4322,c_4335,c_4331,c_4317,c_4316,c_4315,c_4314,c_4313,c_4312,c_4329,c_4309,c_4308,c_4297,c_4285,c_4265,c_4257,c_4256,c_4243,c_4217,c_4216,c_4213,c_4211,c_4210,c_4196,c_4188,c_4187,c_4174,c_4095,c_4094,c_4091,c_4089,c_4087,c_4084,c_4083,c_4082,c_4081,c_4080,c_4067,c_4043,c_4042,c_4041,c_4040,c_4038,c_4037,c_4026,c_4024,c_4023,c_4017,c_4008,c_4007,c_4006,c_4001,c_3873,c_3872,c_3870,c_3869,c_3868,c_3867,c_3866,c_3865,c_3862,c_3861,c_3860,c_3859,c_3858,c_3792,c_3791,c_3789,c_3788,c_3787,c_3786,c_3785,c_3784,c_3783,c_3781,c_3780,c_3779,c_3778,c_3777,c_3746,c_3743,c_3742,c_3741,c_3740,c_3737,c_3736,c_3735,c_3591,c_3557,c_3556,c_3555,c_3554,c_3552,c_3551,c_3549,c_3547,c_3546,c_3545,c_3544,c_3543,c_3542,c_3541,c_3540,c_3538,c_3537,c_3536,c_3535,c_3534,c_3532,c_3531,c_3494,c_3493,c_3492,c_3490,c_3489,c_3471,c_3470,c_3291,c_3290,c_3289,c_3288,c_3287,c_3286,c_3285,c_3284,c_3283,c_3282,c_3281,c_3280,c_3279,c_3278,c_3277,c_3276,c_3275,c_3274,c_3273,c_3272,c_3271,c_3270,c_3269,c_3268,c_3267,c_3266,c_3265,c_3264,c_3255,c_3249,c_3242,c_3218,c_3217,c_3162,c_3161,c_3158,c_3157,c_3138,c_3137,c_3068,c_3067,c_3065,c_3064,c_3045,c_3044,c_3025,c_3024,c_3021,c_3020,c_2935,c_2912,c_2911,c_2910,c_2909,c_2908,c_2907,c_2906,c_2905,c_2904,c_2903,c_2853,c_2852,c_2851,c_2850,c_2849,c_2848,c_2847,c_2846,c_2845,c_2844,c_2828,c_2824,c_2809,c_2808,c_2768,c_2767,c_2766,c_2764,c_2763,c_2750,c_2748,c_2747,c_2708,c_2707,c_2704,c_2703,c_2702,c_2682,c_2681,c_2680,c_2640,c_2639,c_2638,c_2602,c_2601,c_2600,c_2579,c_2568,c_2567,c_2446,c_2445,c_2444,c_2443,c_2442,c_2441,c_2440,c_2439,c_2438,c_2437,c_2436,c_2435,c_2434,c_2433,c_2432,c_2431,c_2430,c_2429,c_2428,c_2427,c_2426,c_2402,c_2400,c_2399,c_2388,c_2387,c_2368,c_2367,c_2365,c_2364,c_2353,c_2351,c_2350,c_2322,c_2321,c_2320,c_2319,c_2318,c_2315,c_2314,c_2307,c_2304,c_2285,c_2267,c_2266,c_2265,c_2264,c_2263,c_2262,c_2260,c_2259,c_2233,c_2230,c_2213,c_2212,c_2211,c_2214,c_2215,c_2208,c_2207,c_2206,c_2205,c_2202,c_2192,c_2190,c_2189,c_2169,c_2167,c_2165,c_2139,c_2138,c_2136,c_2135,c_2098,c_2096,c_2094,c_2079,c_2077,c_2076,c_2069,c_2060,c_2057,c_1959,c_1958,c_1956,c_1955,c_1954,c_1953,c_1898,c_1897,c_1896,c_1895,c_1894,c_1893,c_1890,c_1889,c_1886,c_1847,c_1846,c_1845,c_1844,c_1843,c_1842,c_1841,c_1840,c_1839,c_1834,c_1812,c_1809,c_1753,c_1751,c_1750,c_1749,c_1748,c_1701,c_1700,c_1699,c_1698,c_1697,c_1696,c_1693,c_1692,c_1689,c_1674,c_1606,c_1603,c_1602,c_1601,c_1600,c_1599,c_1598,c_1597,c_1596,c_1544,c_1543,c_1542,c_1541,c_1540,c_1538,c_1537,c_1536,c_1476,c_1475,c_1474,c_1473,c_1472,c_1471,c_1468,c_1467,c_1466,c_1465,c_1464,c_1461,c_1420,c_1418,c_1417,c_1382,c_1379,c_1378,c_1377,c_1376,c_1375,c_1374,c_1373,c_1372,c_1360,c_1358,c_1304,c_1300,c_1299,c_1298,c_1297,c_1296,c_1294,c_1242,c_1241,c_1240,c_1239,c_1238,c_1237,c_1236,c_1234,c_1233,c_1232,c_1204,c_1200,c_1175,c_1049,c_1039,c_1038,c_1037,c_1036,c_1035,c_1034,c_1033,c_1032,c_1031,c_1030,c_1029,c_1028,c_1027,c_1026,c_1025,c_1024,c_1023,c_1022,c_1021,c_1009,c_961,c_958,c_957,c_956,c_955,c_954,c_953,c_952,c_951,c_950,c_949,c_948,c_947,c_946,c_945,c_943,c_920,c_919,c_918,c_917,c_877,c_876,c_875,c_874,c_864,c_845,c_844,c_843,c_779,c_769,c_768,c_767,c_766,c_765,c_764,c_763,c_762,c_761,c_760,c_759,c_758,c_757,c_756,c_755,c_728,c_727,c_726,c_725,c_722,c_698,c_694,c_682,c_681,c_668,c_667,c_666,c_659,c_651,c_637,c_636,c_632,c_622,c_613,c_612,c_594,c_587,c_327,c_324,c_1014,c_71,c_70,c_69,c_68,c_325,c_326,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_54,c_53,c_52,c_51,c_50,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU128+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.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/20.43 % CPULimit : 300
% 0.07/20.43 % WCLimit : 300
% 0.07/20.43 % DateTime : Thu Sep 24 12:51:12 UTC 2026
% 0.07/20.43 % CPUTime :
% 0.07/20.43 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.07/20.47 Running first-order theorem proving
% 0.07/20.47 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.07/20.48
% 0.07/20.48 % ======== iProver multi-core TPTP/SMT =========
% 0.07/20.48
% 0.07/20.48 % Detected problem language: tptp
% 0.07/20.49 % Proving...
% 3.81/21.34 % SZS status Started for theBenchmark.p
% 3.81/21.34 % SZS status Theorem for theBenchmark.p
% 3.81/21.34
% 3.81/21.34 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.81/21.34
% 3.81/21.34 % ------ iProver source info
% 3.81/21.34
% 3.81/21.34 % git: date: 2026-07-19 20:42:38 +0200
% 3.81/21.34 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.81/21.34 % git: non_committed_changes: false
% 3.81/21.34
% 3.81/21.34 % ------ Parsing...
% 3.81/21.34 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.81/21.34
% 3.81/21.34 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 3.81/21.34
% 3.81/21.34 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.81/21.34
% 3.81/21.34 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.81/21.34 % ------ Proving...
% 3.81/21.34 % ------ Problem Properties
% 3.81/21.34
% 3.81/21.34 %
% 3.81/21.34 % clauses 24
% 3.81/21.34 % conjectures 3
% 3.81/21.34 % EPR 12
% 3.81/21.34 % Horn 21
% 3.81/21.34 % unary 11
% 3.81/21.34 % binary 7
% 3.81/21.34 % lits 44
% 3.81/21.34 % lits eq 9
% 3.81/21.34 % fd_pure 0
% 3.81/21.34 % fd_pseudo 0
% 3.81/21.34 % fd_cond 1
% 3.81/21.34 % fd_pseudo_cond 4
% 3.81/21.34 % AC symbols 0
% 3.81/21.34
% 3.81/21.34 % ------ Schedule dynamic 5 is on
% 3.81/21.34
% 3.81/21.34 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.81/21.34
% 3.81/21.34
% 3.81/21.34 % ------
% 3.81/21.34 % Current options:
% 3.81/21.34 % ------
% 3.81/21.34
% 3.81/21.34
% 3.81/21.34 %
% 3.81/21.34
% 3.81/21.34 % ------ Proving...
% 3.81/21.34 %
% 3.81/21.34
% 3.81/21.34 % SZS status Theorem for theBenchmark.p
% 3.81/21.34
% 3.81/21.34 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.81/21.36
% 3.81/21.36
%------------------------------------------------------------------------------