%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU281+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Sun Sep 27 08:45:40 AM UTC 2026
% Result : Theorem 119.75s 16.78s
% Output : CNFRefutation 119.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 2
% Syntax : Number of formulae : 306 ( 13 unt; 0 def)
% Number of atoms : 1303 ( 936 equ)
% Maximal formula atoms : 198 ( 4 avg)
% Number of connectives : 1442 ( 445 ~; 884 |; 108 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 67 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 2 con; 0-3 aty)
% Number of variables : 599 ( 0 sgn 226 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(s1_tarski__e16_22__wellord2__2,axiom,
! [A,B] :
( ! [C,D,E] :
( ( ? [H,I] :
( I = singleton(H)
& in(H,A)
& ordered_pair(H,I) = E )
& C = E
& ? [F,G] :
( G = singleton(F)
& in(F,A)
& ordered_pair(F,G) = D )
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( ? [J,K] :
( K = singleton(J)
& in(J,A)
& ordered_pair(J,K) = D )
& E = D
& in(E,cartesian_product2(A,B)) ) ) ),
file('theBenchmark.p',s1_tarski__e16_22__wellord2__2) ).
fof(s1_xboole_0__e16_22__wellord2__1,conjecture,
! [A,B] :
? [C] :
! [D] :
( in(D,C)
<=> ( ? [E,F] :
( F = singleton(E)
& in(E,A)
& ordered_pair(E,F) = D )
& in(D,cartesian_product2(A,B)) ) ),
file('theBenchmark.p',s1_xboole_0__e16_22__wellord2__1) ).
fof(s1_xboole_0__e16_22__wellord2__1_neg,negated_conjecture,
~ ! [A,B] :
? [C] :
! [D] :
( in(D,C)
<=> ( ? [E,F] :
( F = singleton(E)
& in(E,A)
& ordered_pair(E,F) = D )
& in(D,cartesian_product2(A,B)) ) ),
inference(assume_negation,[status(cth)],[s1_xboole_0__e16_22__wellord2__1]) ).
fof(nnf_14,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ! [J,K] :
( singleton(J) != K
| ~ in(J,A)
| ordered_pair(J,K) != D )
| E != D
| ~ in(E,cartesian_product2(A,B)) )
| in(D,C) )
& ( ? [X3] :
( ? [X4,X5] :
( singleton(X4) = X5
& in(X4,A)
& ordered_pair(X4,X5) = D )
& X3 = D
& in(X3,cartesian_product2(A,B)) )
| ~ in(D,C) ) )
| ? [X0,X1,X2] :
( X2 != X1
& ? [H,I] :
( singleton(H) = I
& in(H,A)
& ordered_pair(H,I) = X2 )
& X2 = X0
& ? [F,G] :
( singleton(F) = G
& in(F,A)
& ordered_pair(F,G) = X1 )
& X0 = X1 ) ),
inference(fof_nnf,[status(thm)],[s1_tarski__e16_22__wellord2__2]) ).
fof(sk_s1_tarski__e16_22__wellord2__2_sk,plain,
! [A,B] :
( ! [D] :
( ( ! [E] :
( ! [J,K] :
( singleton(J) != K
| ~ in(J,A)
| ordered_pair(J,K) != D )
| E != D
| ~ in(E,cartesian_product2(A,B)) )
| in(D,sK2(A,B)) )
& ( ( singleton(sK4(A,B,D)) = sK5(A,B,D)
& in(sK4(A,B,D),A)
& ordered_pair(sK4(A,B,D),sK5(A,B,D)) = D
& sK3(A,B,D) = D
& in(sK3(A,B,D),cartesian_product2(A,B)) )
| ~ in(D,sK2(A,B)) ) )
| ( sK6(A,B) != sK1(A,B)
& singleton(sK14(A,B)) = sK15(A,B)
& in(sK14(A,B),A)
& ordered_pair(sK14(A,B),sK15(A,B)) = sK6(A,B)
& sK6(A,B) = sK0(A,B)
& singleton(sK12(A,B)) = sK13(A,B)
& in(sK12(A,B),A)
& ordered_pair(sK12(A,B),sK13(A,B)) = sK1(A,B)
& sK0(A,B) = sK1(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK12,sK13,sK6,sK14,sK15,sK2,sK3,sK4,sK5]),skolemize(X0,sK0(A,B)),skolemize(X1,sK1(A,B)),skolemize(X2,sK6(A,B)),skolemize(F,sK12(A,B)),skolemize(G,sK13(A,B)),skolemize(H,sK14(A,B)),skolemize(I,sK15(A,B)),skolemize(C,sK2(A,B)),skolemize(X3,sK3(A,B,D)),skolemize(X4,sK4(A,B,D)),skolemize(X5,sK5(A,B,D))],[nnf_14]) ).
fof(sk_s1_tarski__e16_22__wellord2__2,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) != sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK14(VAR_0,VAR_1)) = sK15(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK14(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK14(VAR_0,VAR_1),sK15(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK6(VAR_0,VAR_1) = sK0(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| singleton(sK12(VAR_0,VAR_1)) = sK13(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| in(sK12(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| ordered_pair(sK12(VAR_0,VAR_1),sK13(VAR_0,VAR_1)) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( singleton(VAR_4) != VAR_5
| ~ in(VAR_4,VAR_0)
| ordered_pair(VAR_4,VAR_5) != VAR_2
| VAR_3 != VAR_2
| ~ in(VAR_3,cartesian_product2(VAR_0,VAR_1))
| in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( singleton(sK4(VAR_0,VAR_1,VAR_2)) = sK5(VAR_0,VAR_1,VAR_2)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK4(VAR_0,VAR_1,VAR_2),VAR_0)
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_pair(sK4(VAR_0,VAR_1,VAR_2),sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK3(VAR_0,VAR_1,VAR_2) = VAR_2
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK3(VAR_0,VAR_1,VAR_2),cartesian_product2(VAR_0,VAR_1))
| ~ in(VAR_2,sK2(VAR_0,VAR_1))
| sK0(VAR_0,VAR_1) = sK1(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2_sk]) ).
cnf(c_27,plain,
( in(sK3(A,B,C),cartesian_product2(A,B))
| ~ in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_28,plain,
( in(sK3(A,B,C),cartesian_product2(A,B))
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_29,plain,
( sK3(A,B,C) = C
| ~ in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_30,plain,
( sK3(A,B,C) = C
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_29]) ).
cnf(c_31,plain,
( ordered_pair(sK4(A,B,C),sK5(A,B,C)) = C
| ~ in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_32,plain,
( ordered_pair(sK4(A,B,C),sK5(A,B,C)) = C
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_31]) ).
cnf(c_33,plain,
( in(sK4(A,B,C),A)
| ~ in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_34,plain,
( in(sK4(A,B,C),A)
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_33]) ).
cnf(c_35,plain,
( singleton(sK4(A,B,C)) = sK5(A,B,C)
| ~ in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_23797,plain,
( singleton(sK4(A,B,C)) = sK5(A,B,C)
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_35]) ).
cnf(c_36,plain,
( sK5(A,B,C) = singleton(sK4(A,B,C))
| ~ in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_23797]) ).
cnf(c_37,plain,
( singleton(E) != F
| ~ in(E,A)
| ordered_pair(E,F) != C
| D != C
| ~ in(D,cartesian_product2(A,B))
| in(C,sK2(A,B))
| sK0(A,B) = sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_38,plain,
( singleton(E) != F
| ~ in(E,A)
| ordered_pair(E,F) != C
| D != C
| ~ in(D,cartesian_product2(A,B))
| in(C,sK2(A,B))
| sK1(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_37]) ).
cnf(c_60,plain,
( in(sK3(A,B,C),cartesian_product2(A,B))
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_61,plain,
( sK3(A,B,C) = C
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_62,plain,
( ordered_pair(sK4(A,B,C),sK5(A,B,C)) = C
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_63,plain,
( in(sK4(A,B,C),A)
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_64,plain,
( singleton(sK4(A,B,C)) = sK5(A,B,C)
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_65,plain,
( sK5(A,B,C) = singleton(sK4(A,B,C))
| ~ in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(copy,[status(thm)],[c_64]) ).
cnf(c_66,plain,
( singleton(E) != F
| ~ in(E,A)
| ordered_pair(E,F) != C
| D != C
| ~ in(D,cartesian_product2(A,B))
| in(C,sK2(A,B))
| sK6(A,B) = sK0(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_88,plain,
( in(sK3(A,B,C),cartesian_product2(A,B))
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_89,plain,
( sK3(A,B,C) = C
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_90,plain,
( ordered_pair(sK4(A,B,C),sK5(A,B,C)) = C
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_91,plain,
( in(sK4(A,B,C),A)
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_92,plain,
( singleton(sK4(A,B,C)) = sK5(A,B,C)
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
cnf(c_93,plain,
( sK5(A,B,C) = singleton(sK4(A,B,C))
| ~ in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(copy,[status(thm)],[c_92]) ).
cnf(c_94,plain,
( singleton(E) != F
| ~ in(E,A)
| ordered_pair(E,F) != C
| D != C
| ~ in(D,cartesian_product2(A,B))
| in(C,sK2(A,B))
| sK6(A,B) != sK1(A,B) ),
inference(split_conjunct,[status(thm)],[sk_s1_tarski__e16_22__wellord2__2]) ).
fof(nnf_15,plain,
? [A,B] :
! [C] :
? [D] :
( ( ! [E,F] :
( singleton(E) != F
| ~ in(E,A)
| ordered_pair(E,F) != D )
| ~ in(D,cartesian_product2(A,B))
| ~ in(D,C) )
& ( ( ? [X3,X4] :
( singleton(X3) = X4
& in(X3,A)
& ordered_pair(X3,X4) = D )
& in(D,cartesian_product2(A,B)) )
| in(D,C) ) ),
inference(fof_nnf,[status(thm)],[s1_xboole_0__e16_22__wellord2__1_neg]) ).
fof(sk_s1_xboole_0__e16_22__wellord2__1_neg_sk,plain,
! [C] :
( ( ! [E,F] :
( singleton(E) != F
| ~ in(E,sK8)
| ordered_pair(E,F) != sK7(C) )
| ~ in(sK7(C),cartesian_product2(sK8,sK9))
| ~ in(sK7(C),C) )
& ( ( singleton(sK10(C)) = sK11(C)
& in(sK10(C),sK8)
& ordered_pair(sK10(C),sK11(C)) = sK7(C)
& in(sK7(C),cartesian_product2(sK8,sK9)) )
| in(sK7(C),C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11]),skolemize(A,sK8),skolemize(B,sK9),skolemize(D,sK7(C)),skolemize(X3,sK10(C)),skolemize(X4,sK11(C))],[nnf_15]) ).
fof(sk_s1_xboole_0__e16_22__wellord2__1_neg,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( singleton(VAR_1) != VAR_2
| ~ in(VAR_1,sK8)
| ordered_pair(VAR_1,VAR_2) != sK7(VAR_0)
| ~ in(sK7(VAR_0),cartesian_product2(sK8,sK9))
| ~ in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( singleton(sK10(VAR_0)) = sK11(VAR_0)
| in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( in(sK10(VAR_0),sK8)
| in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( ordered_pair(sK10(VAR_0),sK11(VAR_0)) = sK7(VAR_0)
| in(sK7(VAR_0),VAR_0) )
& ! [VAR_0] :
( in(sK7(VAR_0),cartesian_product2(sK8,sK9))
| in(sK7(VAR_0),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg_sk]) ).
cnf(c_95,negated_conjecture,
( in(sK7(A),cartesian_product2(sK8,sK9))
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg]) ).
cnf(c_96,negated_conjecture,
( ordered_pair(sK10(A),sK11(A)) = sK7(A)
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg]) ).
cnf(c_97,negated_conjecture,
( in(sK10(A),sK8)
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg]) ).
cnf(c_98,negated_conjecture,
( singleton(sK10(A)) = sK11(A)
| in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg]) ).
cnf(c_99,negated_conjecture,
( sK11(A) = singleton(sK10(A))
| in(sK7(A),A) ),
inference(copy,[status(thm)],[c_98]) ).
cnf(c_100,negated_conjecture,
( singleton(B) != C
| ~ in(B,sK8)
| ordered_pair(B,C) != sK7(A)
| ~ in(sK7(A),cartesian_product2(sK8,sK9))
| ~ in(sK7(A),A) ),
inference(split_conjunct,[status(thm)],[sk_s1_xboole_0__e16_22__wellord2__1_neg]) ).
cnf(c_101,negated_conjecture,
( singleton(B) != C
| ~ in(B,sK8)
| sK7(A) != ordered_pair(B,C)
| ~ in(sK7(A),cartesian_product2(sK8,sK9))
| ~ in(sK7(A),A) ),
inference(copy,[status(thm)],[c_100]) ).
cnf(c_131,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK6(A,B) != sK1(A,B)
| in(sK7(sK2(A,B)),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_95,c_88]) ).
cnf(c_159,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| in(sK7(sK2(A,B)),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_95,c_60]) ).
cnf(c_187,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| in(sK7(sK2(A,B)),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_95,c_28]) ).
cnf(c_190,plain,
( singleton(C) != D
| ~ in(C,sK8)
| ordered_pair(C,D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_95,c_94]) ).
cnf(c_198,plain,
( singleton(C) != D
| ~ in(C,sK8)
| ordered_pair(C,D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_95,c_66]) ).
cnf(c_206,plain,
( singleton(C) != D
| ~ in(C,sK8)
| ordered_pair(C,D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_95,c_38]) ).
cnf(c_284,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK6(A,B) != sK1(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_93]) ).
cnf(c_285,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK6(A,B) != sK1(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_91]) ).
cnf(c_286,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK6(A,B) != sK1(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_90]) ).
cnf(c_287,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) != sK1(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_89]) ).
cnf(c_312,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_65]) ).
cnf(c_313,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_63]) ).
cnf(c_314,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_62]) ).
cnf(c_315,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_61]) ).
cnf(c_316,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_60]) ).
cnf(c_340,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_36]) ).
cnf(c_341,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_34]) ).
cnf(c_342,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_32]) ).
cnf(c_343,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_30]) ).
cnf(c_344,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(resolve,[status(thm)],[c_96,c_28]) ).
cnf(c_423,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK6(A,B) != sK1(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_93]) ).
cnf(c_424,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK6(A,B) != sK1(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_91]) ).
cnf(c_425,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK6(A,B) != sK1(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_90]) ).
cnf(c_426,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) != sK1(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_89]) ).
cnf(c_451,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_65]) ).
cnf(c_452,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_63]) ).
cnf(c_453,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_62]) ).
cnf(c_454,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_61]) ).
cnf(c_455,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_60]) ).
cnf(c_479,plain,
( sK5(A,B,sK7(sK2(A,B))) = singleton(sK4(A,B,sK7(sK2(A,B))))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_36]) ).
cnf(c_480,plain,
( in(sK4(A,B,sK7(sK2(A,B))),A)
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_34]) ).
cnf(c_481,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),sK5(A,B,sK7(sK2(A,B)))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_32]) ).
cnf(c_482,plain,
( sK3(A,B,sK7(sK2(A,B))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_30]) ).
cnf(c_483,plain,
( in(sK3(A,B,sK7(sK2(A,B))),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(resolve,[status(thm)],[c_99,c_28]) ).
cnf(c_504,plain,
( sK11(A) = singleton(sK10(A))
| singleton(B) != C
| ~ in(B,sK8)
| sK7(A) != ordered_pair(B,C)
| ~ in(sK7(A),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_101,c_99]) ).
cnf(c_505,plain,
( ordered_pair(sK10(A),sK11(A)) = sK7(A)
| singleton(B) != C
| ~ in(B,sK8)
| sK7(A) != ordered_pair(B,C)
| ~ in(sK7(A),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_101,c_96]) ).
cnf(c_23798,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B)))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(paramod,[status(thm)],[c_454,c_455]) ).
cnf(c_23799,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23798]) ).
cnf(c_3851,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23799]) ).
cnf(c_23800,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_3851,c_504]) ).
cnf(c_3857,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23800]) ).
cnf(c_23801,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B)))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(paramod,[status(thm)],[c_482,c_483]) ).
cnf(c_23802,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23801]) ).
cnf(c_4000,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23802]) ).
cnf(c_23803,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_4000,c_504]) ).
cnf(c_4006,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23803]) ).
cnf(c_7005,plain,
( in(sK7(C),C)
| singleton(sK10(C)) != D
| ordered_pair(sK10(C),D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_190,c_97]) ).
cnf(c_7007,plain,
( singleton(sK10(A)) != C
| ordered_pair(sK10(A),C) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(A),A) ),
inference(factor,[status(thm)],[c_7005]) ).
cnf(c_7160,plain,
( ordered_pair(sK10(A),singleton(sK10(A))) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(A),A) ),
inference(xxres,[status(thm)],[c_7007]) ).
cnf(c_23804,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| sK7(sK2(sK8,sK9)) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(factor,[status(thm)],[c_7160]) ).
cnf(c_7161,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23804]) ).
cnf(c_7240,plain,
( in(sK7(C),C)
| singleton(sK10(C)) != D
| ordered_pair(sK10(C),D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_198,c_97]) ).
cnf(c_7245,plain,
( singleton(sK10(A)) != C
| ordered_pair(sK10(A),C) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(factor,[status(thm)],[c_7240]) ).
cnf(c_7345,plain,
( in(sK7(C),C)
| singleton(sK10(C)) != D
| ordered_pair(sK10(C),D) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(resolve,[status(thm)],[c_206,c_97]) ).
cnf(c_7350,plain,
( singleton(sK10(A)) != C
| ordered_pair(sK10(A),C) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(factor,[status(thm)],[c_7345]) ).
cnf(c_23805,plain,
( sK6(sK8,A) = sK0(sK8,A)
| sK11(sK2(sK8,A)) = singleton(sK10(sK2(sK8,A)))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_3857,c_452]) ).
cnf(c_7773,plain,
( sK6(sK8,A) = sK0(sK8,A)
| sK11(sK2(sK8,A)) = singleton(sK10(sK2(sK8,A)))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23805]) ).
cnf(c_23806,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(factor,[status(thm)],[c_7773]) ).
cnf(c_7799,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23806]) ).
cnf(c_23807,plain,
( sK1(sK8,A) = sK0(sK8,A)
| sK11(sK2(sK8,A)) = singleton(sK10(sK2(sK8,A)))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_4006,c_480]) ).
cnf(c_7800,plain,
( sK1(sK8,A) = sK0(sK8,A)
| sK11(sK2(sK8,A)) = singleton(sK10(sK2(sK8,A)))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23807]) ).
cnf(c_23808,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(factor,[status(thm)],[c_7800]) ).
cnf(c_7828,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23808]) ).
cnf(c_23809,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(paramod,[status(thm)],[c_315,c_316]) ).
cnf(c_23810,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23809]) ).
cnf(c_8005,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23810]) ).
cnf(c_23811,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_8005,c_505]) ).
cnf(c_8011,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23811]) ).
cnf(c_23812,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(paramod,[status(thm)],[c_343,c_344]) ).
cnf(c_23813,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23812]) ).
cnf(c_8119,plain,
( in(sK7(sK2(A,B)),cartesian_product2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23813]) ).
cnf(c_23814,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_8119,c_505]) ).
cnf(c_8125,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23814]) ).
cnf(c_23815,plain,
( sK6(sK8,A) = sK0(sK8,A)
| ordered_pair(sK10(sK2(sK8,A)),sK11(sK2(sK8,A))) = sK7(sK2(sK8,A))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_8011,c_313]) ).
cnf(c_11117,plain,
( sK6(sK8,A) = sK0(sK8,A)
| ordered_pair(sK10(sK2(sK8,A)),sK11(sK2(sK8,A))) = sK7(sK2(sK8,A))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23815]) ).
cnf(c_23816,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(factor,[status(thm)],[c_11117]) ).
cnf(c_11135,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23816]) ).
cnf(c_23817,plain,
( sK1(sK8,A) = sK0(sK8,A)
| ordered_pair(sK10(sK2(sK8,A)),sK11(sK2(sK8,A))) = sK7(sK2(sK8,A))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_8125,c_341]) ).
cnf(c_11150,plain,
( sK1(sK8,A) = sK0(sK8,A)
| ordered_pair(sK10(sK2(sK8,A)),sK11(sK2(sK8,A))) = sK7(sK2(sK8,A))
| singleton(sK4(sK8,A,sK7(sK2(sK8,A)))) != B
| ordered_pair(sK4(sK8,A,sK7(sK2(sK8,A))),B) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23817]) ).
cnf(c_23818,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(factor,[status(thm)],[c_11150]) ).
cnf(c_11170,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23818]) ).
cnf(c_23819,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B)))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(paramod,[status(thm)],[c_451,c_453]) ).
cnf(c_23820,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23819]) ).
cnf(c_12243,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23820]) ).
cnf(c_23821,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B)))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(paramod,[status(thm)],[c_479,c_481]) ).
cnf(c_23822,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23821]) ).
cnf(c_12338,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK11(sK2(A,B)) = singleton(sK10(sK2(A,B))) ),
inference(copy,[status(thm)],[c_23822]) ).
cnf(c_23823,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(paramod,[status(thm)],[c_312,c_314]) ).
cnf(c_23824,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23823]) ).
cnf(c_12559,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK6(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23824]) ).
cnf(c_23825,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(paramod,[status(thm)],[c_340,c_342]) ).
cnf(c_23826,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23825]) ).
cnf(c_13268,plain,
( ordered_pair(sK4(A,B,sK7(sK2(A,B))),singleton(sK4(A,B,sK7(sK2(A,B))))) = sK7(sK2(A,B))
| sK1(A,B) = sK0(A,B)
| ordered_pair(sK10(sK2(A,B)),sK11(sK2(A,B))) = sK7(sK2(A,B)) ),
inference(copy,[status(thm)],[c_23826]) ).
cnf(c_23827,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_7799,c_12243]) ).
cnf(c_23828,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23827]) ).
cnf(c_23829,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23828]) ).
cnf(c_15574,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23829]) ).
cnf(c_23830,plain,
( C != singleton(sK10(A))
| ordered_pair(sK10(A),C) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(copy,[status(thm)],[c_7245]) ).
cnf(c_23831,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) != A
| sK7(sK2(sK8,sK9)) != A
| in(A,sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_15574,c_23830]) ).
cnf(c_15607,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) != A
| sK7(sK2(sK8,sK9)) != A
| in(A,sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23831]) ).
cnf(c_23832,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_7828,c_12338]) ).
cnf(c_23833,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23832]) ).
cnf(c_23834,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23833]) ).
cnf(c_15621,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23834]) ).
cnf(c_23835,plain,
( C != singleton(sK10(A))
| ordered_pair(sK10(A),C) != B
| sK7(A) != B
| in(B,sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(A),A) ),
inference(copy,[status(thm)],[c_7350]) ).
cnf(c_23836,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) != A
| sK7(sK2(sK8,sK9)) != A
| in(A,sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_15621,c_23835]) ).
cnf(c_15647,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) != A
| sK7(sK2(sK8,sK9)) != A
| in(A,sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23836]) ).
cnf(c_23837,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_11135,c_12559]) ).
cnf(c_23838,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23837]) ).
cnf(c_23839,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23838]) ).
cnf(c_18630,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23839]) ).
cnf(c_23840,plain,
( sK7(sK2(sK8,sK9)) != sK7(sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18630,c_15607]) ).
cnf(c_23841,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23840]) ).
cnf(c_23842,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23841]) ).
cnf(c_18645,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23842]) ).
cnf(c_18724,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| ~ in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18645,c_101]) ).
cnf(c_23843,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18645,c_65]) ).
cnf(c_18750,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23843]) ).
cnf(c_23844,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18645,c_63]) ).
cnf(c_18751,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23844]) ).
cnf(c_23845,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18645,c_62]) ).
cnf(c_18752,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23845]) ).
cnf(c_23846,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18645,c_61]) ).
cnf(c_18753,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23846]) ).
cnf(c_23847,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_18753,c_159]) ).
cnf(c_23848,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23847]) ).
cnf(c_18984,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23848]) ).
cnf(c_23849,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_18750,c_18752]) ).
cnf(c_19124,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23849]) ).
cnf(c_23850,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_18724,c_18984]) ).
cnf(c_19136,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23850]) ).
cnf(c_23851,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_19136,c_18751]) ).
cnf(c_23852,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23851]) ).
cnf(c_19172,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23852]) ).
cnf(c_23853,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_19172,c_19124]) ).
cnf(c_23854,plain,
( sK6(sK8,sK9) = sK0(sK8,sK9)
| sK6(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23853]) ).
cnf(c_19260,plain,
sK6(sK8,sK9) = sK0(sK8,sK9),
inference(copy,[status(thm)],[c_23854]) ).
cnf(c_23855,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_7161]) ).
cnf(c_19734,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23855]) ).
cnf(c_23856,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_131]) ).
cnf(c_19974,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23856]) ).
cnf(c_23857,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK1(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_19260,c_424]) ).
cnf(c_19975,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK1(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23857]) ).
cnf(c_23858,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_19260,c_426]) ).
cnf(c_19977,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23858]) ).
cnf(c_23859,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK1(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_285]) ).
cnf(c_19978,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK1(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23859]) ).
cnf(c_23860,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_287]) ).
cnf(c_19981,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23860]) ).
cnf(c_23861,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_19260,c_423]) ).
cnf(c_19982,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23861]) ).
cnf(c_23862,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_284]) ).
cnf(c_19983,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23862]) ).
cnf(c_23863,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_19260,c_286]) ).
cnf(c_19984,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23863]) ).
cnf(c_23864,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_19260,c_425]) ).
cnf(c_19985,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23864]) ).
cnf(c_23865,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_11170,c_13268]) ).
cnf(c_23866,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23865]) ).
cnf(c_23867,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23866]) ).
cnf(c_20121,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23867]) ).
cnf(c_23868,plain,
( sK7(sK2(sK8,sK9)) != sK7(sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20121,c_15647]) ).
cnf(c_23869,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23868]) ).
cnf(c_23870,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23869]) ).
cnf(c_20134,plain,
( in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23870]) ).
cnf(c_20213,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| ~ in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20134,c_101]) ).
cnf(c_23871,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20134,c_36]) ).
cnf(c_20253,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23871]) ).
cnf(c_23872,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20134,c_34]) ).
cnf(c_20254,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23872]) ).
cnf(c_23873,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20134,c_32]) ).
cnf(c_20255,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23873]) ).
cnf(c_23874,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20134,c_30]) ).
cnf(c_20256,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23874]) ).
cnf(c_23875,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20256,c_187]) ).
cnf(c_23876,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23875]) ).
cnf(c_20450,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23876]) ).
cnf(c_23877,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20253,c_20255]) ).
cnf(c_20568,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23877]) ).
cnf(c_23878,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20213,c_20450]) ).
cnf(c_20580,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23878]) ).
cnf(c_23879,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20580,c_20254]) ).
cnf(c_23880,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23879]) ).
cnf(c_20616,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23880]) ).
cnf(c_23881,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(resolve,[status(thm)],[c_20616,c_20568]) ).
cnf(c_23882,plain,
( sK1(sK8,sK9) = sK0(sK8,sK9)
| sK1(sK8,sK9) = sK0(sK8,sK9) ),
inference(copy,[status(thm)],[c_23881]) ).
cnf(c_20711,plain,
sK1(sK8,sK9) = sK0(sK8,sK9),
inference(copy,[status(thm)],[c_23882]) ).
cnf(c_23883,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20711,c_19985]) ).
cnf(c_20765,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23883]) ).
cnf(c_23884,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19984]) ).
cnf(c_20766,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23884]) ).
cnf(c_23885,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19983]) ).
cnf(c_20767,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23885]) ).
cnf(c_23886,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20711,c_19982]) ).
cnf(c_20768,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23886]) ).
cnf(c_23887,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19981]) ).
cnf(c_20769,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23887]) ).
cnf(c_23888,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK0(sK8,sK9)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19978]) ).
cnf(c_20772,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23888]) ).
cnf(c_23889,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20711,c_19977]) ).
cnf(c_20773,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23889]) ).
cnf(c_23890,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK0(sK8,sK9)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20711,c_19975]) ).
cnf(c_20775,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23890]) ).
cnf(c_23891,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19974]) ).
cnf(c_20776,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23891]) ).
cnf(c_23892,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9)
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20711,c_19734]) ).
cnf(c_20939,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) != sK7(sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23892]) ).
cnf(c_23893,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20773,c_20776]) ).
cnf(c_21691,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23893]) ).
cnf(c_23894,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_21691,c_504]) ).
cnf(c_21740,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23894]) ).
cnf(c_23895,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A)
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_21740,c_20775]) ).
cnf(c_23896,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23895]) ).
cnf(c_22116,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23896]) ).
cnf(c_23897,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20769,c_20776]) ).
cnf(c_22183,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23897]) ).
cnf(c_23898,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_22183,c_505]) ).
cnf(c_22215,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23898]) ).
cnf(c_23899,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A)
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_22215,c_20772]) ).
cnf(c_23900,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23899]) ).
cnf(c_22373,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23900]) ).
cnf(c_23901,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(paramod,[status(thm)],[c_20768,c_20765]) ).
cnf(c_22452,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23901]) ).
cnf(c_23902,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_20767,c_20766]) ).
cnf(c_22514,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),sK11(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23902]) ).
cnf(c_23903,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(resolve,[status(thm)],[c_22116,c_22452]) ).
cnf(c_23904,plain,
( sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9)))
| sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))) ),
inference(copy,[status(thm)],[c_23903]) ).
cnf(c_22556,plain,
sK11(sK2(sK8,sK9)) = singleton(sK10(sK2(sK8,sK9))),
inference(copy,[status(thm)],[c_23904]) ).
cnf(c_22557,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_22556,c_22514]) ).
cnf(c_22604,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) != sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_22556,c_22373]) ).
cnf(c_23905,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_22604,c_22557]) ).
cnf(c_23906,plain,
( ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9)) ),
inference(copy,[status(thm)],[c_23905]) ).
cnf(c_23272,plain,
ordered_pair(sK10(sK2(sK8,sK9)),singleton(sK10(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9)),
inference(copy,[status(thm)],[c_23906]) ).
cnf(c_23907,plain,
( sK7(sK2(sK8,sK9)) != sK7(sK2(sK8,sK9))
| in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)) ),
inference(paramod,[status(thm)],[c_23272,c_20939]) ).
cnf(c_23273,plain,
in(sK7(sK2(sK8,sK9)),sK2(sK8,sK9)),
inference(copy,[status(thm)],[c_23907]) ).
cnf(c_23440,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B)
| ~ in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)) ),
inference(resolve,[status(thm)],[c_23273,c_101]) ).
cnf(c_23908,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK6(sK8,sK9) != sK1(sK8,sK9) ),
inference(resolve,[status(thm)],[c_23273,c_93]) ).
cnf(c_23909,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK1(sK8,sK9) ),
inference(paramod,[status(thm)],[c_19260,c_23908]) ).
cnf(c_23910,plain,
( sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20711,c_23909]) ).
cnf(c_23442,plain,
sK5(sK8,sK9,sK7(sK2(sK8,sK9))) = singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))),
inference(copy,[status(thm)],[c_23910]) ).
cnf(c_23911,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK6(sK8,sK9) != sK1(sK8,sK9) ),
inference(resolve,[status(thm)],[c_23273,c_91]) ).
cnf(c_23912,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK1(sK8,sK9) ),
inference(paramod,[status(thm)],[c_19260,c_23911]) ).
cnf(c_23913,plain,
( in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8)
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20711,c_23912]) ).
cnf(c_23443,plain,
in(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK8),
inference(copy,[status(thm)],[c_23913]) ).
cnf(c_23914,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9) ),
inference(resolve,[status(thm)],[c_23273,c_90]) ).
cnf(c_23915,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9) ),
inference(paramod,[status(thm)],[c_19260,c_23914]) ).
cnf(c_23916,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),sK5(sK8,sK9,sK7(sK2(sK8,sK9)))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20711,c_23915]) ).
cnf(c_23917,plain,
( ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_23442,c_23916]) ).
cnf(c_23444,plain,
ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))) = sK7(sK2(sK8,sK9)),
inference(copy,[status(thm)],[c_23917]) ).
cnf(c_23918,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9) ),
inference(resolve,[status(thm)],[c_23273,c_89]) ).
cnf(c_23919,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9) ),
inference(paramod,[status(thm)],[c_19260,c_23918]) ).
cnf(c_23920,plain,
( sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20711,c_23919]) ).
cnf(c_23445,plain,
sK3(sK8,sK9,sK7(sK2(sK8,sK9))) = sK7(sK2(sK8,sK9)),
inference(copy,[status(thm)],[c_23920]) ).
cnf(c_23921,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK6(sK8,sK9) != sK1(sK8,sK9) ),
inference(resolve,[status(thm)],[c_23273,c_88]) ).
cnf(c_23922,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK0(sK8,sK9) != sK1(sK8,sK9) ),
inference(paramod,[status(thm)],[c_19260,c_23921]) ).
cnf(c_23923,plain,
( in(sK3(sK8,sK9,sK7(sK2(sK8,sK9))),cartesian_product2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_20711,c_23922]) ).
cnf(c_23924,plain,
( in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9))
| sK0(sK8,sK9) != sK0(sK8,sK9) ),
inference(paramod,[status(thm)],[c_23445,c_23923]) ).
cnf(c_23446,plain,
in(sK7(sK2(sK8,sK9)),cartesian_product2(sK8,sK9)),
inference(copy,[status(thm)],[c_23924]) ).
cnf(c_23458,plain,
( singleton(A) != B
| ~ in(A,sK8)
| sK7(sK2(sK8,sK9)) != ordered_pair(A,B) ),
inference(resolve,[status(thm)],[c_23446,c_23440]) ).
cnf(c_23925,plain,
( singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9)))) != A
| sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),A) ),
inference(resolve,[status(thm)],[c_23458,c_23443]) ).
cnf(c_23926,plain,
sK7(sK2(sK8,sK9)) != ordered_pair(sK4(sK8,sK9,sK7(sK2(sK8,sK9))),singleton(sK4(sK8,sK9,sK7(sK2(sK8,sK9))))),
inference(xxres,[status(thm)],[c_23925]) ).
cnf(c_23927,plain,
sK7(sK2(sK8,sK9)) != sK7(sK2(sK8,sK9)),
inference(paramod,[status(thm)],[c_23444,c_23926]) ).
cnf(c_23796,plain,
$false,
inference(copy,[status(thm)],[c_23927]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU281+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n018.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 26 09:06:37 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 61096 was started by sandbox on n018,
% 0.09/0.38 % Sat Sep 26 09:06:37 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 119.75/16.78
% 119.75/16.78 % given #500 (T,wt=34): 6846 singleton(f4(c5,c6)) = f5(c5,c6) | in(A,f8(c5,c6)) | f12(cartesian_product2(c5,c6)) != A | ordered_pair(f13(B),C) != A | singleton(f13(B)) != C | in(f12(B),B). [resolve(526,e,97,b)].
% 119.75/16.78
% 119.75/16.78 % given #1000 (T,wt=36): 14168 in(f12(A),A) | f3(c5,c6) != f2(c5,c6) | in(B,f8(c5,c6)) | f12(A) != B | ordered_pair(f12(c5),singleton(f12(c5))) != B | ordered_pair(f13(c5),f14(c5)) = f12(c5). [xx_res(7006,f)].
% 119.75/16.78
% 119.75/16.78 % given #1500 (T,wt=38): 17106 in(f12(A),A) | ordered_pair(f4(c5,c6),f5(c5,c6)) = f2(c5,c6) | in(f12(A),f8(c5,c6)) | f12(A) != ordered_pair(f12(c5),singleton(f12(c5))) | ordered_pair(f13(c5),f14(c5)) = f12(c5). [xx_res(17104,d),flip(d)].
% 119.75/16.78
% 119.75/16.78 % given #2000 (T,wt=35): 19739 in(f12(A),A) | f2(c5,c6) != f1(c5,c6) | in(B,f8(c5,c6)) | f12(A) != B | ordered_pair(f13(C),D) != B | singleton(f13(C)) != D | in(f12(C),C). [back_rewrite(7005),rewrite([19260(5)]),flip(b)].
% 119.75/16.78
% 119.75/16.78 % SZS status Theorem for theBenchmark
% 119.75/16.78
% 119.75/16.78 % Proof 1 at 14.23 (+ 1.49) seconds.
% 119.75/16.78 % Length of proof is 168.
% 119.75/16.78 % Level of proof is 28.
% 119.75/16.78 % Maximum clause weight is 66.000.
% 119.75/16.78 % Given clauses 2358.
% 119.75/16.78
% 119.75/16.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------