%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU277+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:56:27 PM UTC 2026
% Result : Theorem 24.07s 9.54s
% Output : CNFRefutation 24.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 7
% Syntax : Number of formulae : 148 ( 16 unt; 1 def)
% Number of atoms : 705 ( 169 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 873 ( 340 ~; 396 |; 119 &)
% ( 7 <=>; 9 =>; 0 <=; 2 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 4 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-4 aty)
% Number of variables : 456 ( 0 sgn 349 !; 107 ?; 220 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1,X2] :
( ( function(X2)
& relation(X2)
& relation(X1) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e6_21__wellord2__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1,X2] :
( ( function(X2)
& relation(X2)
& relation(X1) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ( function(X2)
& relation(X2)
& relation(X1) )
=> ( ! [X3,X4,X5] :
( ( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4 )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( ? [X10,X11] :
( in(ordered_pair(apply(X2,X10),apply(X2,X11)),X1)
& X4 = ordered_pair(X10,X11) )
& X5 = X4
& in(X5,cartesian_product2(X0,X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e6_21__wellord2__1) ).
fof(f22,plain,
! [X0,X1,X2] :
( ( function(X2)
& relation(X2)
& relation(X1) )
=> ( ! [X3,X4,X5] :
( ( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4 )
=> X4 = X5 )
=> ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( ? [X13,X14] :
( in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
& ordered_pair(X13,X14) = X11 )
& X11 = X12
& in(X12,cartesian_product2(X0,X0)) ) ) ) ),
inference(rectify,[],[f21]) ).
fof(f26,plain,
? [X0,X1,X2] :
( function(X2)
& relation(X2)
& relation(X1)
& ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f27,plain,
? [X0,X1,X2] :
( function(X2)
& relation(X2)
& relation(X1)
& ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(flattening,[],[f26]) ).
fof(f35,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ? [X3,X4,X5] :
( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4
& X4 != X5 )
| ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( ? [X13,X14] :
( in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
& ordered_pair(X13,X14) = X11 )
& X11 = X12
& in(X12,cartesian_product2(X0,X0)) ) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ? [X3,X4,X5] :
( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4
& X4 != X5 )
| ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( ? [X13,X14] :
( in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
& ordered_pair(X13,X14) = X11 )
& X11 = X12
& in(X12,cartesian_product2(X0,X0)) ) ) ),
inference(flattening,[],[f36]) ).
fof(f40,plain,
? [X0,X1,X2] :
( function(X2)
& relation(X2)
& relation(X1)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) )
& ( ~ in(X4,X3)
| ! [X5,X6] :
( ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
| ordered_pair(X5,X6) != X4 )
| ~ in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f41,plain,
? [X0,X1,X2] :
( function(X2)
& relation(X2)
& relation(X1)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X5,X6] :
( in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
& X4 = ordered_pair(X5,X6) )
& in(X4,cartesian_product2(X0,X0)) ) )
& ( ~ in(X4,X3)
| ! [X5,X6] :
( ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
| ordered_pair(X5,X6) != X4 )
| ~ in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
? [X0,X1,X2] :
( function(X2)
& relation(X2)
& relation(X1)
& ! [X3] :
? [X4] :
( ( in(X4,X3)
| ( ? [X7,X8] :
( in(ordered_pair(apply(X2,X7),apply(X2,X8)),X1)
& ordered_pair(X7,X8) = X4 )
& in(X4,cartesian_product2(X0,X0)) ) )
& ( ~ in(X4,X3)
| ! [X5,X6] :
( ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1)
| ordered_pair(X5,X6) != X4 )
| ~ in(X4,cartesian_product2(X0,X0)) ) ) ),
inference(rectify,[],[f41]) ).
fof(f43,plain,
( function(sK3)
& relation(sK3)
& relation(sK2)
& ! [X3] :
( ( in(sK4(X3),X3)
| ( in(ordered_pair(apply(sK3,sK5(X3)),apply(sK3,sK6(X3))),sK2)
& sK4(X3) = ordered_pair(sK5(X3),sK6(X3))
& in(sK4(X3),cartesian_product2(sK1,sK1)) ) )
& ( ~ in(sK4(X3),X3)
| ! [X5,X6] :
( ~ in(ordered_pair(apply(sK3,X5),apply(sK3,X6)),sK2)
| ordered_pair(X5,X6) != sK4(X3) )
| ~ in(sK4(X3),cartesian_product2(sK1,sK1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X4,sK4(X3)),skolemize(X7,sK5(X3)),skolemize(X8,sK6(X3))],[f42]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ? [X10] :
! [X11] :
( ( ~ in(X11,X10)
| ? [X12] :
( ? [X13,X14] :
( in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
& ordered_pair(X13,X14) = X11 )
& X11 = X12
& in(X12,cartesian_product2(X0,X0)) ) )
& ( ! [X12] :
( ! [X13,X14] :
( ~ in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
| ordered_pair(X13,X14) != X11 )
| X11 != X12
| ~ in(X12,cartesian_product2(X0,X0)) )
| in(X11,X10) ) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ? [X3] :
! [X4] :
( ( ~ in(X4,X3)
| ? [X8] :
( ? [X9,X10] :
( in(ordered_pair(apply(X2,X9),apply(X2,X10)),X1)
& ordered_pair(X9,X10) = X4 )
& X4 = X8
& in(X8,cartesian_product2(X0,X0)) ) )
& ( ! [X5] :
( ! [X6,X7] :
( ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ordered_pair(X6,X7) != X4 )
| X4 != X5
| ~ in(X5,cartesian_product2(X0,X0)) )
| in(X4,X3) ) ) ),
inference(rectify,[],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ! [X4] :
( ( ~ in(X4,sK22(X0,X1,X2))
| ( in(ordered_pair(apply(X2,sK24(X1,X2,X4)),apply(X2,sK25(X1,X2,X4))),X1)
& ordered_pair(sK24(X1,X2,X4),sK25(X1,X2,X4)) = X4
& sK23(X0,X1,X2,X4) = X4
& in(sK23(X0,X1,X2,X4),cartesian_product2(X0,X0)) ) )
& ( ! [X5] :
( ! [X6,X7] :
( ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ordered_pair(X6,X7) != X4 )
| X4 != X5
| ~ in(X5,cartesian_product2(X0,X0)) )
| in(X4,sK22(X0,X1,X2)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25]),skolemize(X3,sK22(X0,X1,X2)),skolemize(X8,sK23(X0,X1,X2,X4)),skolemize(X9,sK24(X1,X2,X4)),skolemize(X10,sK25(X1,X2,X4))],[f56]) ).
fof(f58,plain,
function(sK3),
inference(cnf_transformation,[],[f43]) ).
fof(f59,plain,
relation(sK3),
inference(cnf_transformation,[],[f43]) ).
fof(f60,plain,
relation(sK2),
inference(cnf_transformation,[],[f43]) ).
fof(f61,plain,
! [X3] :
( in(sK4(X3),X3)
| in(ordered_pair(apply(sK3,sK5(X3)),apply(sK3,sK6(X3))),sK2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f62,plain,
! [X3] :
( in(sK4(X3),X3)
| sK4(X3) = ordered_pair(sK5(X3),sK6(X3)) ),
inference(cnf_transformation,[],[f43]) ).
fof(f63,plain,
! [X3] :
( in(sK4(X3),X3)
| in(sK4(X3),cartesian_product2(sK1,sK1)) ),
inference(cnf_transformation,[],[f43]) ).
fof(f64,plain,
! [X3,X6,X5] :
( ~ in(sK4(X3),X3)
| ~ in(ordered_pair(apply(sK3,X5),apply(sK3,X6)),sK2)
| ordered_pair(X5,X6) != sK4(X3)
| ~ in(sK4(X3),cartesian_product2(sK1,sK1)) ),
inference(cnf_transformation,[],[f43]) ).
fof(f94,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f35]) ).
fof(f105,plain,
! [X2,X0,X1,X4] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(X4,sK22(X0,X1,X2))
| in(ordered_pair(apply(X2,sK24(X1,X2,X4)),apply(X2,sK25(X1,X2,X4))),X1) ),
inference(cnf_transformation,[],[f57]) ).
fof(f106,plain,
! [X2,X0,X1,X4] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(X4,sK22(X0,X1,X2))
| ordered_pair(sK24(X1,X2,X4),sK25(X1,X2,X4)) = X4 ),
inference(cnf_transformation,[],[f57]) ).
fof(f107,plain,
! [X2,X0,X1,X4] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(X4,sK22(X0,X1,X2))
| sK23(X0,X1,X2,X4) = X4 ),
inference(cnf_transformation,[],[f57]) ).
fof(f108,plain,
! [X2,X0,X1,X4] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(X4,sK22(X0,X1,X2))
| in(sK23(X0,X1,X2,X4),cartesian_product2(X0,X0)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f109,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ordered_pair(X6,X7) != X4
| X4 != X5
| ~ in(X5,cartesian_product2(X0,X0))
| in(X4,sK22(X0,X1,X2)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f110,plain,
! [X2,X0,X1,X6,X7,X5] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ordered_pair(X6,X7) != X5
| ~ in(X5,cartesian_product2(X0,X0))
| in(X5,sK22(X0,X1,X2)) ),
inference(equality_resolution,[],[f109]) ).
fof(f111,plain,
! [X2,X0,X1,X6,X7] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| ~ in(ordered_pair(X6,X7),cartesian_product2(X0,X0))
| in(ordered_pair(X6,X7),sK22(X0,X1,X2)) ),
inference(equality_resolution,[],[f110]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ~ in(sK4(X2),X2)
| ~ in(sK4(X2),cartesian_product2(sK1,sK1))
| ~ in(ordered_pair(apply(sK3,X0),apply(sK3,X1)),sK2)
| ( ordered_pair(X0,X1) != sK4(X2) ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_50,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| in(sK4(X0),cartesian_product2(sK1,sK1)) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_51,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| ( ordered_pair(sK5(X0),sK6(X0)) = sK4(X0) ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_52,negated_conjecture,
! [X0: $i] :
( in(sK4(X0),X0)
| in(ordered_pair(apply(sK3,sK5(X0)),apply(sK3,sK6(X0))),sK2) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_53,negated_conjecture,
relation(sK2),
inference(cnf_transformation,[],[f60]) ).
tcf(c_54,negated_conjecture,
relation(sK3),
inference(cnf_transformation,[],[f59]) ).
tcf(c_55,negated_conjecture,
function(sK3),
inference(cnf_transformation,[],[f58]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(X3,X0)
| in(ordered_pair(X1,X2),sK22(X4,X3,X0))
| ~ function(X0)
| ~ relation(X3)
| ~ relation(X0)
| ~ in(ordered_pair(X1,X2),cartesian_product2(X4,X4))
| ~ in(ordered_pair(apply(X0,X1),apply(X0,X2)),X3) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X2,X3)
| in(sK23(X1,X2,X3,X0),cartesian_product2(X1,X1))
| ~ function(X3)
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X0,sK22(X1,X2,X3)) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X2,X3)
| ( sK23(X1,X2,X3,X0) = X0 )
| ~ function(X3)
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X0,sK22(X1,X2,X3)) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X2,X3)
| ( ordered_pair(sK24(X2,X3,X0),sK25(X2,X3,X0)) = X0 )
| ~ function(X3)
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X0,sK22(X1,X2,X3)) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X2,X3)
| in(ordered_pair(apply(X3,sK24(X2,X3,X0)),apply(X3,sK25(X2,X3,X0))),X2)
| ~ function(X3)
| ~ relation(X3)
| ~ relation(X2)
| ~ in(X0,sK22(X1,X2,X3)) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_176,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( sP0(X1_iProver_in_2,X2_iProver_in_2)
| in(ordered_pair(apply(X2_iProver_in_2,sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)),apply(X2_iProver_in_2,sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2))),X1_iProver_in_2)
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(subtyping,[status(esa)],[c_98]) ).
tcf(c_177,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( sP0(X1_iProver_in_2,X2_iProver_in_2)
| ( ordered_pair(sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(subtyping,[status(esa)],[c_97]) ).
tcf(c_178,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( sP0(X1_iProver_in_2,X2_iProver_in_2)
| ( sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(subtyping,[status(esa)],[c_96]) ).
tcf(c_179,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( sP0(X1_iProver_in_2,X2_iProver_in_2)
| in(sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(subtyping,[status(esa)],[c_95]) ).
tcf(c_180,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X0_iProver_ordered_pair_2: iProver_ordered_pair_2,X1_iProver_in_2: iProver_in_2,X1_iProver_ordered_pair_2: iProver_ordered_pair_2] :
( sP0(X1_iProver_in_2,X0_iProver_in_2)
| in(ordered_pair(X0_iProver_ordered_pair_2,X1_iProver_ordered_pair_2),sK22(X0_iProver_sK23_1,X1_iProver_in_2,X0_iProver_in_2))
| ~ function(X0_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2)
| ~ in(ordered_pair(X0_iProver_ordered_pair_2,X1_iProver_ordered_pair_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| ~ in(ordered_pair(apply(X0_iProver_in_2,X0_iProver_ordered_pair_2),apply(X0_iProver_in_2,X1_iProver_ordered_pair_2)),X1_iProver_in_2) ),
inference(subtyping,[status(esa)],[c_94]) ).
tcf(c_191,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ~ in(X1_iProver_in_2,X0_iProver_in_2)
| ~ in(X0_iProver_in_2,X1_iProver_in_2) ),
inference(subtyping,[status(esa)],[c_83]) ).
tcf(c_204,negated_conjecture,
function(sK3),
inference(subtyping,[status(esa)],[c_55]) ).
tcf(c_206,negated_conjecture,
relation(sK2),
inference(subtyping,[status(esa)],[c_53]) ).
tcf(c_207,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(apply(sK3,sK5(X0_iProver_in_2)),apply(sK3,sK6(X0_iProver_in_2))),sK2) ),
inference(subtyping,[status(esa)],[c_52]) ).
tcf(c_208,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ( ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)) = sK4(X0_iProver_in_2) ) ),
inference(subtyping,[status(esa)],[c_51]) ).
tcf(c_209,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(sK4(X0_iProver_in_2),cartesian_product2(sK1,sK1)) ),
inference(subtyping,[status(esa)],[c_50]) ).
tcf(c_210,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_ordered_pair_2: iProver_ordered_pair_2,X1_iProver_ordered_pair_2: iProver_ordered_pair_2] :
( ~ in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ~ in(sK4(X0_iProver_in_2),cartesian_product2(sK1,sK1))
| ~ in(ordered_pair(apply(sK3,X0_iProver_ordered_pair_2),apply(sK3,X1_iProver_ordered_pair_2)),sK2)
| ( ordered_pair(X0_iProver_ordered_pair_2,X1_iProver_ordered_pair_2) != sK4(X0_iProver_in_2) ) ),
inference(subtyping,[status(esa)],[c_49]) ).
tcf(c_212,plain,
! [X0_iProver_in_2: iProver_in_2] : X0_iProver_in_2 = X0_iProver_in_2,
theory(equality) ).
tcf(c_214,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( X2_iProver_in_2 = X0_iProver_in_2 )
| ( X2_iProver_in_2 != X1_iProver_in_2 )
| ( X0_iProver_in_2 != X1_iProver_in_2 ) ),
theory(equality) ).
tcf(c_216,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2,X3_iProver_in_2: iProver_in_2] :
( in(X0_iProver_in_2,X2_iProver_in_2)
| ~ in(X1_iProver_in_2,X3_iProver_in_2)
| ( X2_iProver_in_2 != X3_iProver_in_2 )
| ( X0_iProver_in_2 != X1_iProver_in_2 ) ),
theory(equality) ).
tcf(c_286,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( sP0(X0_iProver_in_2,X1_iProver_in_2)
| ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2)
| ~ in(sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) ),
inference(instantiation,[status(thm)],[c_178]) ).
tcf(c_287,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( in(sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) ) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_322,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( sP0(X0_iProver_in_2,X1_iProver_in_2)
| in(ordered_pair(apply(X1_iProver_in_2,sK24(X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)))),apply(X1_iProver_in_2,sK25(X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))))),X0_iProver_in_2)
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2)
| ~ in(sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) ),
inference(instantiation,[status(thm)],[c_176]) ).
tcf(c_323,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( sP0(X0_iProver_in_2,X1_iProver_in_2)
| ( ordered_pair(sK24(X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))),sK25(X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2)
| ~ in(sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_335,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( sP0(X0_iProver_in_2,X1_iProver_in_2)
| ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2) ),
inference(superposition,[status(thm)],[c_208,c_178]) ).
tcf(c_353,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( sK16(X0_iProver_in_2,X1_iProver_in_2) = sK17(X0_iProver_in_2,X1_iProver_in_2) )
| ( sK17(X0_iProver_in_2,X1_iProver_in_2) != X2_iProver_in_2 )
| ( sK16(X0_iProver_in_2,X1_iProver_in_2) != X2_iProver_in_2 ) ),
inference(instantiation,[status(thm)],[c_214]) ).
tcf(c_403,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( sP0(sK2,sK3)
| in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(superposition,[status(thm)],[c_207,c_180]) ).
tcf(c_426,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( sP0(sK2,sK3)
| in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(global_subsumption_just,[status(thm)],[c_403,c_55,c_54,c_53,c_403]) ).
tcf(c_458,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ( sK16(X0_iProver_in_2,X1_iProver_in_2) = sK17(X0_iProver_in_2,X1_iProver_in_2) )
| ( sK17(X0_iProver_in_2,X1_iProver_in_2) != sK15(X0_iProver_in_2,X1_iProver_in_2) )
| ( sK16(X0_iProver_in_2,X1_iProver_in_2) != sK15(X0_iProver_in_2,X1_iProver_in_2) ) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_1388,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ( X1_iProver_in_2 = X0_iProver_in_2 )
| ( X0_iProver_in_2 != X1_iProver_in_2 ) ),
inference(resolution,[status(thm)],[c_214,c_212]) ).
tcf(c_1417,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( in(X0_iProver_in_2,X2_iProver_in_2)
| ~ in(X1_iProver_in_2,X2_iProver_in_2)
| ( X0_iProver_in_2 != X1_iProver_in_2 ) ),
inference(resolution,[status(thm)],[c_216,c_212]) ).
tcf(c_3272,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( sP0(sK2,sK3)
| in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))))),sK2)
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_3273,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ~ in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ~ in(sK4(X0_iProver_in_2),cartesian_product2(sK1,sK1))
| ~ in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))))),sK2)
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))) != sK4(X0_iProver_in_2) ) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_3274,plain,
( sP0(sK2,sK3)
| in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(sK1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(sK1,sK2,sK3))))),sK2)
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_3272]) ).
tcf(c_7748,plain,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ( sK4(X0_iProver_in_2) = ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)) ) ),
inference(resolution,[status(thm)],[c_1388,c_208]) ).
tcf(c_9585,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( sP0(sK2,sK3)
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_323]) ).
tcf(c_9586,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))))),sK2)
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))) != sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(instantiation,[status(thm)],[c_3273]) ).
tcf(c_9587,plain,
( sP0(sK2,sK3)
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(sK1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(sK1,sK2,sK3)))) = sK4(sK22(sK1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3)) ),
inference(instantiation,[status(thm)],[c_9585]) ).
tcf(c_9588,plain,
( ~ in(sK4(sK22(sK1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3))
| ~ in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(sK1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(sK1,sK2,sK3))))),sK2)
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(sK1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(sK1,sK2,sK3)))) != sK4(sK22(sK1,sK2,sK3)) ) ),
inference(instantiation,[status(thm)],[c_9586]) ).
tcf(c_10236,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),X1_iProver_in_2)
| ~ in(sK4(X0_iProver_in_2),X1_iProver_in_2) ),
inference(resolution,[status(thm)],[c_1417,c_208]) ).
tcf(c_10255,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X1_iProver_in_2)
| in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),X1_iProver_in_2) ),
inference(resolution,[status(thm)],[c_1417,c_7748]) ).
fof(f38,definition,
! [X1,X2] :
( ~ sP0(X1,X2)
| ? [X3,X4,X5] :
( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4
& X4 != X5 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f39,plain,
! [X0,X1,X2] :
( ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| sP0(X1,X2)
| ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( ? [X13,X14] :
( in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1)
& ordered_pair(X13,X14) = X11 )
& X11 = X12
& in(X12,cartesian_product2(X0,X0)) ) ) ),
inference(definition_folding,[],[f37,f38]) ).
fof(f52,plain,
! [X1,X2] :
( ~ sP0(X1,X2)
| ? [X3,X4,X5] :
( ? [X8,X9] :
( in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1)
& X5 = ordered_pair(X8,X9) )
& X3 = X5
& ? [X6,X7] :
( in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
& X4 = ordered_pair(X6,X7) )
& X3 = X4
& X4 != X5 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f53,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ? [X2,X3,X4] :
( ? [X7,X8] :
( in(ordered_pair(apply(X1,X7),apply(X1,X8)),X0)
& ordered_pair(X7,X8) = X4 )
& X2 = X4
& ? [X5,X6] :
( in(ordered_pair(apply(X1,X5),apply(X1,X6)),X0)
& ordered_pair(X5,X6) = X3 )
& X2 = X3
& X3 != X4 ) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( in(ordered_pair(apply(X1,sK20(X0,X1)),apply(X1,sK21(X0,X1))),X0)
& sK17(X0,X1) = ordered_pair(sK20(X0,X1),sK21(X0,X1))
& sK15(X0,X1) = sK17(X0,X1)
& in(ordered_pair(apply(X1,sK18(X0,X1)),apply(X1,sK19(X0,X1))),X0)
& sK16(X0,X1) = ordered_pair(sK18(X0,X1),sK19(X0,X1))
& sK15(X0,X1) = sK16(X0,X1)
& sK16(X0,X1) != sK17(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17,sK18,sK19,sK20,sK21]),skolemize(X2,sK15(X0,X1)),skolemize(X3,sK16(X0,X1)),skolemize(X4,sK17(X0,X1)),skolemize(X5,sK18(X0,X1)),skolemize(X6,sK19(X0,X1)),skolemize(X7,sK20(X0,X1)),skolemize(X8,sK21(X0,X1))],[f53]) ).
fof(f100,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK15(X0,X1) = sK17(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f103,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK15(X0,X1) = sK16(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f104,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| sK16(X0,X1) != sK17(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_87,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ sP0(X0,X1)
| ( sK16(X0,X1) != sK17(X0,X1) ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( ( sK16(X0,X1) = sK15(X0,X1) )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( ( sK17(X0,X1) = sK15(X0,X1) )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_183,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ( sK17(X0_iProver_in_2,X1_iProver_in_2) = sK15(X0_iProver_in_2,X1_iProver_in_2) )
| ~ sP0(X0_iProver_in_2,X1_iProver_in_2) ),
inference(subtyping,[status(esa)],[c_91]) ).
tcf(c_186,plain,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ( sK16(X0_iProver_in_2,X1_iProver_in_2) = sK15(X0_iProver_in_2,X1_iProver_in_2) )
| ~ sP0(X0_iProver_in_2,X1_iProver_in_2) ),
inference(subtyping,[status(esa)],[c_88]) ).
tcf(c_187,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] :
( ~ sP0(X0_iProver_in_2,X1_iProver_in_2)
| ( sK16(X0_iProver_in_2,X1_iProver_in_2) != sK17(X0_iProver_in_2,X1_iProver_in_2) ) ),
inference(subtyping,[status(esa)],[c_87]) ).
tcf(c_442,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( ( sK16(X0_iProver_in_2,X1_iProver_in_2) = sK15(X0_iProver_in_2,X1_iProver_in_2) )
| ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2) ),
inference(superposition,[status(thm)],[c_335,c_186]) ).
tcf(c_536,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] : ~ sP0(X0_iProver_in_2,X1_iProver_in_2),
inference(global_subsumption_just,[status(thm)],[c_187,c_183,c_186,c_187,c_458]) ).
tcf(c_890,negated_conjecture,
! [X0_iProver_in_2: iProver_in_2,X1_iProver_in_2: iProver_in_2] : ~ sP0(X0_iProver_in_2,X1_iProver_in_2),
inference(global_subsumption_just,[status(thm)],[c_187,c_183,c_186,c_187,c_458]) ).
tcf(c_900,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_178,c_890]) ).
tcf(c_901,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( in(sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_179,c_890]) ).
tcf(c_902,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( in(ordered_pair(apply(X2_iProver_in_2,sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)),apply(X2_iProver_in_2,sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2))),X1_iProver_in_2)
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_176,c_890]) ).
tcf(c_903,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X0_iProver_ordered_pair_2: iProver_ordered_pair_2,X1_iProver_in_2: iProver_in_2,X1_iProver_ordered_pair_2: iProver_ordered_pair_2] :
( in(ordered_pair(X0_iProver_ordered_pair_2,X1_iProver_ordered_pair_2),sK22(X0_iProver_sK23_1,X1_iProver_in_2,X0_iProver_in_2))
| ~ function(X0_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2)
| ~ in(ordered_pair(X0_iProver_ordered_pair_2,X1_iProver_ordered_pair_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| ~ in(ordered_pair(apply(X0_iProver_in_2,X0_iProver_ordered_pair_2),apply(X0_iProver_in_2,X1_iProver_ordered_pair_2)),X1_iProver_in_2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_180,c_890]) ).
tcf(c_904,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( ordered_pair(sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_177,c_890]) ).
tcf(c_999,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( ~ relation(X0_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ function(X1_iProver_in_2)
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) ) ),
inference(global_subsumption_just,[status(thm)],[c_442,c_286,c_287,c_536]) ).
tcf(c_1000,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2] :
( ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,X1_iProver_in_2)) )
| ~ function(X1_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ relation(X0_iProver_in_2) ),
inference(renaming,[status(thm)],[c_999]) ).
tcf(c_1002,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,sK3,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ~ relation(sK3)
| ~ relation(X0_iProver_in_2) ),
inference(superposition,[status(thm)],[c_204,c_1000]) ).
tcf(c_1055,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,sK3,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ~ relation(X0_iProver_in_2) ),
inference(global_subsumption_just,[status(thm)],[c_1002,c_54,c_1002]) ).
tcf(c_1057,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,sK2,sK3)),sK6(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_206,c_1055]) ).
tcf(c_1145,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| ~ in(sK4(X0_iProver_in_2),cartesian_product2(sK1,sK1))
| ~ in(ordered_pair(apply(sK3,sK5(sK22(X0_iProver_sK23_1,sK2,sK3))),apply(sK3,sK6(sK22(X0_iProver_sK23_1,sK2,sK3)))),sK2)
| ( sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) != sK4(X0_iProver_in_2) ) ),
inference(superposition,[status(thm)],[c_1057,c_210]) ).
tcf(c_1219,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(resolution,[status(thm)],[c_903,c_207]) ).
tcf(c_1230,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| in(sK4(X0_iProver_in_2),X0_iProver_in_2) ),
inference(global_subsumption_just,[status(thm)],[c_426,c_55,c_54,c_53,c_1219]) ).
tcf(c_1231,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(renaming,[status(thm)],[c_1230]) ).
tcf(c_1265,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,sK3,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ~ relation(X0_iProver_in_2) ),
inference(global_subsumption_just,[status(thm)],[c_1002,c_54,c_1002]) ).
tcf(c_1267,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,sK2,sK3)),sK6(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_206,c_1265]) ).
tcf(c_1275,plain,
! [X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3))
| in(ordered_pair(sK5(sK22(X0_iProver_sK23_1,sK2,sK3)),sK6(sK22(X0_iProver_sK23_1,sK2,sK3))),sK22(X1_iProver_sK23_1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),cartesian_product2(X1_iProver_sK23_1,X1_iProver_sK23_1)) ),
inference(superposition,[status(thm)],[c_1267,c_1231]) ).
tcf(c_1694,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(global_subsumption_just,[status(thm)],[c_1219,c_55,c_54,c_53,c_1219]) ).
tcf(c_3135,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,X0_iProver_in_2,sK3,sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)),sK6(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3))) = sK4(sK22(X0_iProver_sK23_1,X0_iProver_in_2,sK3)) )
| ~ relation(X0_iProver_in_2) ),
inference(global_subsumption_just,[status(thm)],[c_1002,c_1055]) ).
tcf(c_3137,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ( ordered_pair(sK5(sK22(X0_iProver_sK23_1,sK2,sK3)),sK6(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_206,c_3135]) ).
tcf(c_3482,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3))
| in(ordered_pair(sK5(sK22(X0_iProver_sK23_1,sK2,sK3)),sK6(sK22(X0_iProver_sK23_1,sK2,sK3))),sK22(sK1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_209,c_1275]) ).
tcf(c_3724,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(sK1,sK2,sK3))
| in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(superposition,[status(thm)],[c_3137,c_3482]) ).
tcf(c_6169,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(ordered_pair(apply(sK3,sK5(sK22(X0_iProver_sK23_1,sK2,sK3))),apply(sK3,sK6(sK22(X0_iProver_sK23_1,sK2,sK3)))),sK2) ),
inference(equality_resolution,[status(thm)],[c_1145]) ).
tcf(c_7359,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2))
| ~ relation(X1_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ function(X2_iProver_in_2)
| ( sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2) = X0_iProver_in_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_178,c_900]) ).
tcf(c_7360,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(renaming,[status(thm)],[c_7359]) ).
tcf(c_7363,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2))
| ~ relation(X1_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ function(X2_iProver_in_2)
| in(sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(global_subsumption_just,[status(thm)],[c_179,c_901]) ).
tcf(c_7364,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( in(sK23(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1))
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(renaming,[status(thm)],[c_7363]) ).
tcf(c_7366,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2))
| ~ relation(X1_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ function(X2_iProver_in_2)
| ( ordered_pair(sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)) = X0_iProver_in_2 ) ),
inference(global_subsumption_just,[status(thm)],[c_177,c_904]) ).
tcf(c_7367,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ( ordered_pair(sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2),sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)) = X0_iProver_in_2 )
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(renaming,[status(thm)],[c_7366]) ).
tcf(c_7370,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2))
| ~ relation(X1_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ function(X2_iProver_in_2)
| in(ordered_pair(apply(X2_iProver_in_2,sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)),apply(X2_iProver_in_2,sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2))),X1_iProver_in_2) ),
inference(global_subsumption_just,[status(thm)],[c_176,c_902]) ).
tcf(c_7371,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1,X1_iProver_in_2: iProver_in_2,X2_iProver_in_2: iProver_in_2] :
( in(ordered_pair(apply(X2_iProver_in_2,sK24(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2)),apply(X2_iProver_in_2,sK25(X1_iProver_in_2,X2_iProver_in_2,X0_iProver_in_2))),X1_iProver_in_2)
| ~ function(X2_iProver_in_2)
| ~ relation(X2_iProver_in_2)
| ~ relation(X1_iProver_in_2)
| ~ in(X0_iProver_in_2,sK22(X0_iProver_sK23_1,X1_iProver_in_2,X2_iProver_in_2)) ),
inference(renaming,[status(thm)],[c_7370]) ).
tcf(c_7512,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(sK1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3) ),
inference(superposition,[status(thm)],[c_3724,c_7360]) ).
tcf(c_7513,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(sK1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ in(sK22(X0_iProver_sK23_1,sK2,sK3),sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) ),
inference(superposition,[status(thm)],[c_3724,c_191]) ).
tcf(c_7559,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(sK1,sK2,sK3))
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) ) ),
inference(global_subsumption_just,[status(thm)],[c_7513,c_55,c_54,c_53,c_7512]) ).
tcf(c_7561,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( in(ordered_pair(apply(sK3,sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))),apply(sK3,sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))))),sK2)
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3) ),
inference(superposition,[status(thm)],[c_7559,c_7371]) ).
tcf(c_7562,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ( ordered_pair(sK24(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))),sK25(sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3)))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3) ),
inference(superposition,[status(thm)],[c_7559,c_7367]) ).
tcf(c_7563,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(sK1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3) ),
inference(superposition,[status(thm)],[c_7559,c_7360]) ).
tcf(c_7566,plain,
( ( sK23(sK1,sK2,sK3,sK4(sK22(sK1,sK2,sK3))) = sK4(sK22(sK1,sK2,sK3)) )
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3) ),
inference(instantiation,[status(thm)],[c_7563]) ).
tcf(c_10207,plain,
! [X0_iProver_sK23_1: iProver_sK23_1] :
( ( sK23(X0_iProver_sK23_1,sK2,sK3,sK4(sK22(X0_iProver_sK23_1,sK2,sK3))) = sK4(sK22(X0_iProver_sK23_1,sK2,sK3)) )
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ in(sK4(sK22(X0_iProver_sK23_1,sK2,sK3)),sK22(X0_iProver_sK23_1,sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_6169,c_55,c_54,c_53,c_7561,c_7562,c_9586]) ).
tcf(c_10213,plain,
( ( sK23(sK1,sK2,sK3,sK4(sK22(sK1,sK2,sK3))) = sK4(sK22(sK1,sK2,sK3)) )
| ~ in(sK4(sK22(sK1,sK2,sK3)),cartesian_product2(sK1,sK1)) ),
inference(superposition,[status(thm)],[c_7559,c_10207]) ).
tcf(c_10398,plain,
sK23(sK1,sK2,sK3,sK4(sK22(sK1,sK2,sK3))) = sK4(sK22(sK1,sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_10213,c_55,c_54,c_53,c_7566]) ).
tcf(c_10401,plain,
( in(sK4(sK22(sK1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ function(sK3)
| ~ relation(sK2)
| ~ relation(sK3)
| ~ in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3)) ),
inference(superposition,[status(thm)],[c_10398,c_7364]) ).
tcf(c_10810,plain,
( in(sK4(sK22(sK1,sK2,sK3)),cartesian_product2(sK1,sK1))
| ~ in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3)) ),
inference(global_subsumption_just,[status(thm)],[c_10401,c_55,c_54,c_53,c_10401]) ).
tcf(c_10813,plain,
in(sK4(sK22(sK1,sK2,sK3)),cartesian_product2(sK1,sK1)),
inference(superposition,[status(thm)],[c_209,c_10810]) ).
tcf(c_10872,plain,
! [X0_iProver_in_2: iProver_in_2,X0_iProver_sK23_1: iProver_sK23_1] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(X0_iProver_sK23_1,sK2,sK3))
| ~ in(sK4(X0_iProver_in_2),cartesian_product2(X0_iProver_sK23_1,X0_iProver_sK23_1)) ),
inference(resolution,[status(thm)],[c_1694,c_10236]) ).
tcf(c_11035,plain,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(ordered_pair(sK5(X0_iProver_in_2),sK6(X0_iProver_in_2)),sK22(sK1,sK2,sK3)) ),
inference(resolution,[status(thm)],[c_10872,c_209]) ).
tcf(c_11137,plain,
! [X0_iProver_in_2: iProver_in_2] :
( in(sK4(X0_iProver_in_2),X0_iProver_in_2)
| in(sK4(X0_iProver_in_2),sK22(sK1,sK2,sK3)) ),
inference(resolution,[status(thm)],[c_11035,c_10255]) ).
tcf(c_11259,plain,
in(sK4(sK22(sK1,sK2,sK3)),sK22(sK1,sK2,sK3)),
inference(factoring,[status(thm)],[c_11137]) ).
tcf(c_13773,plain,
sP0(sK2,sK3),
inference(global_subsumption_just,[status(thm)],[c_426,c_55,c_54,c_53,c_3274,c_9587,c_9588,c_10813,c_11259]) ).
tcf(c_13775,plain,
$false,
inference(superposition,[status(thm)],[c_13773,c_536]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU277+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.42 % Computer : n017.cluster.edu
% 0.16/5.42 % Model : x86_64 x86_64
% 0.16/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.42 % Memory : 8046.5625MB
% 0.16/5.42 % OS : Linux 6.8.0-71-generic
% 0.16/5.42 % CPULimit : 300
% 0.16/5.42 % WCLimit : 300
% 0.16/5.42 % DateTime : Thu Sep 24 13:26:08 UTC 2026
% 0.16/5.42 % CPUTime :
% 0.16/5.42 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.48 Running first-order theorem proving
% 0.16/5.48 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.49
% 0.16/5.49 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.49
% 0.16/5.49 % Detected problem language: tptp
% 0.20/5.51 % Proving...
% 24.07/9.54 % SZS status Started for theBenchmark.p
% 24.07/9.54 % SZS status Theorem for theBenchmark.p
% 24.07/9.54
% 24.07/9.54 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 24.07/9.54
% 24.07/9.54 % ------ iProver source info
% 24.07/9.54
% 24.07/9.54 % git: date: 2026-07-19 20:42:38 +0200
% 24.07/9.54 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 24.07/9.54 % git: non_committed_changes: false
% 24.07/9.54
% 24.07/9.54 % ------ Parsing...
% 24.07/9.54 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 24.07/9.54
% 24.07/9.54 % ------ Preprocessing... sup_sim: 0 sf_s rm: 19 0s sf_e sup_sim: 0 sf_s rm: 4 0s sf_e %
% 24.07/9.54
% 24.07/9.54 % ------ Preprocessing...%
% 24.07/9.54
% 24.07/9.54 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 24.07/9.54 % ------ Proving...
% 24.07/9.54 % ------ Problem Properties
% 24.07/9.54
% 24.07/9.54 %
% 24.07/9.54 % clauses 35
% 24.07/9.54 % conjectures 12
% 24.07/9.54 % EPR 18
% 24.07/9.54 % Horn 27
% 24.07/9.54 % unary 17
% 24.07/9.54 % binary 12
% 24.07/9.54 % lits 76
% 24.07/9.54 % lits eq 9
% 24.07/9.54 % fd_pure 0
% 24.07/9.54 % fd_pseudo 0
% 24.07/9.54 % fd_cond 0
% 24.07/9.54 % fd_pseudo_cond 0
% 24.07/9.54 % AC symbols 0
% 24.07/9.54
% 24.07/9.54 % ------ Input Options Time Limit: Unbounded
% 24.07/9.54
% 24.07/9.54
% 24.07/9.54 % ------
% 24.07/9.54 % Current options:
% 24.07/9.54 % ------
% 24.07/9.54
% 24.07/9.54
% 24.07/9.54 %
% 24.07/9.54
% 24.07/9.54 % ------ Proving...
% 24.07/9.54 %
% 24.07/9.54
% 24.07/9.54 % SZS status Theorem for theBenchmark.p
% 24.07/9.54
% 24.07/9.54 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 24.07/9.54
% 24.07/9.54
%------------------------------------------------------------------------------