%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU281+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 : Thu Sep 24 02:20:00 PM UTC 2026
% Result : Theorem 10.58s 6.90s
% Output : CNFRefutation 7.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 87
% Syntax : Number of formulae : 473 ( 5 unt; 84 def)
% Number of atoms : 1811 ( 412 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 2139 ( 801 ~;1151 |; 94 &)
% ( 89 <=>; 3 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 87 ( 85 usr; 84 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 2 con; 0-4 aty)
% Number of variables : 541 ( 473 !; 68 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f11,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,plain,
? [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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
? [A,B] :
! [C] :
? [D] :
( ( ! [E,F] :
( F != singleton(E)
| ~ in(E,A)
| ordered_pair(E,F) != D )
| ~ in(D,cartesian_product2(A,B))
| ~ in(D,C) )
& ( ( ? [E,F] :
( F = singleton(E)
& in(E,A)
& ordered_pair(E,F) = D )
& in(D,cartesian_product2(A,B)) )
| in(D,C) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f19,plain,
! [C] :
( ( ! [E,F] :
( F != singleton(E)
| ~ in(E,sK0_skl)
| ordered_pair(E,F) != sK2_skl(C) )
| ~ in(sK2_skl(C),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(C),C) )
& ( ( sK4_skl(C) = singleton(sK3_skl(C))
& in(sK3_skl(C),sK0_skl)
& ordered_pair(sK3_skl(C),sK4_skl(C)) = sK2_skl(C)
& in(sK2_skl(C),cartesian_product2(sK0_skl,sK1_skl)) )
| in(sK2_skl(C),C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C)),skolemize(E,sK3_skl(C)),skolemize(F,sK4_skl(C))],[f18]) ).
fof(f20,plain,
! [X0] :
( in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [X0] :
( ordered_pair(sK3_skl(X0),sK4_skl(X0)) = sK2_skl(X0)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f22,plain,
! [X0] :
( in(sK3_skl(X0),sK0_skl)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f23,plain,
! [X0] :
( sK4_skl(X0) = singleton(sK3_skl(X0))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f24,plain,
! [X0,X1,X2] :
( X2 != singleton(X1)
| ~ in(X1,sK0_skl)
| ordered_pair(X1,X2) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f49,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f50,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f52,plain,
! [A,B] :
( ? [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)) ) )
| ? [C,D,E] :
( 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 ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f53,definition,
! [A,C,D,E] :
( sP0_prd(E,D,C,A)
<=> ( 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 ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f54,plain,
! [A,B] :
( ? [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)) ) )
| ? [C,D,E] : sP0_prd(E,D,C,A) ),
inference(formula_renaming,[status(thm)],[f52,f53]) ).
fof(f55,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ! [J,K] :
( K != singleton(J)
| ~ in(J,A)
| ordered_pair(J,K) != D )
| E != D
| ~ in(E,cartesian_product2(A,B)) )
| 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)) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,A) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [A] :
( ! [B] :
? [C] :
( ! [D] :
( ! [J,K] :
( K != singleton(J)
| ~ in(J,A)
| ordered_pair(J,K) != D )
| ! [E] :
( E != D
| ~ in(E,cartesian_product2(A,B)) )
| in(D,C) )
& ! [D] :
( ( ? [J,K] :
( K = singleton(J)
& in(J,A)
& ordered_pair(J,K) = D )
& ? [E] :
( E = D
& in(E,cartesian_product2(A,B)) ) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,A) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
! [A] :
( ! [B] :
( ! [D] :
( ! [J,K] :
( K != singleton(J)
| ~ in(J,A)
| ordered_pair(J,K) != D )
| ! [E] :
( E != D
| ~ in(E,cartesian_product2(A,B)) )
| in(D,sK12_skl(B,A)) )
& ! [D] :
( ( sK15_skl(D,B,A) = singleton(sK14_skl(D,B,A))
& in(sK14_skl(D,B,A),A)
& ordered_pair(sK14_skl(D,B,A),sK15_skl(D,B,A)) = D
& sK13_skl(D,B,A) = D
& in(sK13_skl(D,B,A),cartesian_product2(A,B)) )
| ~ in(D,sK12_skl(B,A)) ) )
| sP0_prd(sK11_skl(A),sK10_skl(A),sK9_skl(A),A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(C,sK9_skl(A)),skolemize(D,sK10_skl(A)),skolemize(E,sK11_skl(A)),skolemize(C,sK12_skl(B,A)),skolemize(E,sK13_skl(D,B,A)),skolemize(J,sK14_skl(D,B,A)),skolemize(K,sK15_skl(D,B,A))],[f56]) ).
fof(f58,plain,
! [X0,X1,X2] :
( in(sK13_skl(X1,X2,X0),cartesian_product2(X0,X2))
| ~ in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( sK13_skl(X1,X2,X0) = X1
| ~ in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ordered_pair(sK14_skl(X1,X2,X0),sK15_skl(X1,X2,X0)) = X1
| ~ in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f61,plain,
! [X0,X1,X2] :
( in(sK14_skl(X1,X2,X0),X0)
| ~ in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f62,plain,
! [X0,X1,X2] :
( sK15_skl(X1,X2,X0) = singleton(sK14_skl(X1,X2,X0))
| ~ in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f63,plain,
! [X0,X1,X2,X3,X4,X5] :
( X5 != singleton(X4)
| ~ in(X4,X0)
| ordered_pair(X4,X5) != X1
| X3 != X1
| ~ in(X3,cartesian_product2(X0,X2))
| in(X1,sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f64,plain,
! [A,C,D,E] :
( ( 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
| sP0_prd(E,D,C,A) )
& ( ( 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 )
| ~ sP0_prd(E,D,C,A) ) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f65,plain,
( ! [A,C,D,E] :
( 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
| sP0_prd(E,D,C,A) )
& ! [A,C,D,E] :
( ( 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 )
| ~ sP0_prd(E,D,C,A) ) ),
inference(miniscoping,[status(thm)],[f64]) ).
fof(f66,plain,
( ! [A,C,D,E] :
( 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
| sP0_prd(E,D,C,A) )
& ! [A,C,D,E] :
( ( D != E
& sK19_skl(E,D,C,A) = singleton(sK18_skl(E,D,C,A))
& in(sK18_skl(E,D,C,A),A)
& ordered_pair(sK18_skl(E,D,C,A),sK19_skl(E,D,C,A)) = E
& C = E
& sK17_skl(E,D,C,A) = singleton(sK16_skl(E,D,C,A))
& in(sK16_skl(E,D,C,A),A)
& ordered_pair(sK16_skl(E,D,C,A),sK17_skl(E,D,C,A)) = D
& C = D )
| ~ sP0_prd(E,D,C,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(F,sK16_skl(E,D,C,A)),skolemize(G,sK17_skl(E,D,C,A)),skolemize(H,sK18_skl(E,D,C,A)),skolemize(I,sK19_skl(E,D,C,A))],[f65]) ).
fof(f67,plain,
! [X0,X1,X2,X3] :
( X2 = X1
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ordered_pair(sK16_skl(X0,X1,X2,X3),sK17_skl(X0,X1,X2,X3)) = X1
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( in(sK16_skl(X0,X1,X2,X3),X3)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f70,plain,
! [X0,X1,X2,X3] :
( sK17_skl(X0,X1,X2,X3) = singleton(sK16_skl(X0,X1,X2,X3))
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( X2 = X0
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ordered_pair(sK18_skl(X0,X1,X2,X3),sK19_skl(X0,X1,X2,X3)) = X0
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( in(sK18_skl(X0,X1,X2,X3),X3)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( sK19_skl(X0,X1,X2,X3) = singleton(sK18_skl(X0,X1,X2,X3))
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f75,plain,
! [X0,X1,X2,X3] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f77,plain,
! [X0,X1] :
( ~ in(X1,sK0_skl)
| ordered_pair(X1,singleton(X1)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(destructive_equality_resolution,[status(thm)],[f24]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f79,plain,
! [X0,X1,X2] : ~ sP0_prd(X0,X0,X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f75]) ).
fof(f80,plain,
! [X0] :
( ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)) = sK2_skl(sK0_skl)
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f77,f21]) ).
fof(f81,plain,
! [X0] :
( in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,sK1_skl))
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f77,f20]) ).
fof(f82,plain,
! [X0] :
( sK4_skl(sK0_skl) = singleton(sK3_skl(sK0_skl))
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f77,f23]) ).
fof(f83,plain,
! [X0] :
( in(sK3_skl(sK0_skl),sK0_skl)
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f77,f22]) ).
fof(f84,definition,
! [X0] :
( sQ0_spl
<=> ( ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f85,plain,
! [X0] :
( ~ sQ0_spl
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(component_clause,[status(thm)],[f84]) ).
fof(f87,definition,
( sQ1_spl
<=> ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)) = sK2_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f88,plain,
( ~ sQ1_spl
| ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)) = sK2_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f87]) ).
fof(f90,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f80,f84,f87]) ).
fof(f91,definition,
( sQ2_spl
<=> in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f94,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f81,f84,f91]) ).
fof(f95,definition,
( sQ3_spl
<=> sK4_skl(sK0_skl) = singleton(sK3_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( ~ sQ3_spl
| sK4_skl(sK0_skl) = singleton(sK3_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f95]) ).
fof(f98,plain,
( sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f82,f84,f95]) ).
fof(f99,definition,
( sQ4_spl
<=> in(sK3_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f100,plain,
( ~ sQ4_spl
| in(sK3_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f99]) ).
fof(f102,plain,
( sQ4_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f83,f84,f99]) ).
fof(f103,plain,
( ~ sQ0_spl
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f85,f20]) ).
fof(f110,definition,
( sQ5_spl
<=> in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f111,plain,
( ~ sQ5_spl
| in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f110]) ).
fof(f112,plain,
( sQ5_spl
| ~ in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f110]) ).
fof(f113,definition,
( sQ6_spl
<=> ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) = sK2_skl(cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f116,plain,
( ~ sQ0_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f103,f110,f113,f84]) ).
fof(f138,plain,
( sQ5_spl
| $false ),
inference(resolution,[status(thm)],[f112,f20]) ).
fof(f145,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f138]) ).
fof(f146,plain,
! [X0] :
( ~ sQ4_spl
| ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f100,f77]) ).
fof(f160,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f96,f146]) ).
fof(f161,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sK2_skl(sK0_skl) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f88,f160]) ).
fof(f162,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sK2_skl(sK0_skl) != sK2_skl(cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f161,f111]) ).
fof(f168,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sK4_skl(X0) = singleton(sK3_skl(X0))
| sK2_skl(sK0_skl) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f161,f23]) ).
fof(f169,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| in(sK3_skl(X0),sK0_skl)
| sK2_skl(sK0_skl) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f161,f22]) ).
fof(f170,definition,
( sQ10_spl
<=> sK2_skl(sK0_skl) = sK2_skl(cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f173,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f162,f110,f170,f87,f95,f99]) ).
fof(f234,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| sK9_skl(X0) = sK10_skl(X0) ),
inference(resolution,[status(thm)],[f67,f78]) ).
fof(f235,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X1,X0))
| sK9_skl(X0) = sK10_skl(X0) ),
inference(paramodulation,[status(thm)],[f96,f234]) ).
fof(f236,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X1,X0))
| sK9_skl(X0) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f96,f235]) ).
fof(f237,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK9_skl(X0) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f236]) ).
fof(f238,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK9_skl(X0) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f237]) ).
fof(f239,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| sK9_skl(sK0_skl) = sK10_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f238,f100]) ).
fof(f240,definition,
( sQ12_spl
<=> sK9_skl(sK0_skl) = sK10_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( ~ sQ12_spl
| sK9_skl(sK0_skl) = sK10_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
! [X0] :
( sQ13_spl
<=> ( ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f244,plain,
! [X0] :
( ~ sQ13_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f239,f240,f243,f87,f95,f99]) ).
fof(f247,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| sK9_skl(X0) = sK11_skl(X0) ),
inference(resolution,[status(thm)],[f71,f78]) ).
fof(f248,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ in(X0,sK0_skl)
| ~ in(ordered_pair(X0,singleton(X0)),cartesian_product2(sK0_skl,X1))
| in(ordered_pair(X0,singleton(X0)),sK12_skl(X1,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f78]) ).
fof(f249,definition,
( sQ14_spl
<=> sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ14_spl
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f252,definition,
! [X0,X1] :
( sQ15_spl
<=> ( ~ in(X0,sK0_skl)
| ~ in(ordered_pair(X0,singleton(X0)),cartesian_product2(sK0_skl,X1))
| in(ordered_pair(X0,singleton(X0)),sK12_skl(X1,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f253,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ in(X0,sK0_skl)
| ~ in(ordered_pair(X0,singleton(X0)),cartesian_product2(sK0_skl,X1))
| in(ordered_pair(X0,singleton(X0)),sK12_skl(X1,sK0_skl)) ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f255,plain,
( ~ sQ12_spl
| sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f248,f249,f252,f240]) ).
fof(f256,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| in(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(resolution,[status(thm)],[f69,f78]) ).
fof(f257,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| in(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(resolution,[status(thm)],[f73,f78]) ).
fof(f258,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(resolution,[status(thm)],[f70,f78]) ).
fof(f259,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(resolution,[status(thm)],[f74,f78]) ).
fof(f260,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| ordered_pair(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK10_skl(X0) ),
inference(resolution,[status(thm)],[f68,f78]) ).
fof(f261,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(ordered_pair(X1,singleton(X1)),cartesian_product2(X0,X2))
| in(ordered_pair(X1,singleton(X1)),sK12_skl(X2,X0))
| ordered_pair(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK11_skl(X0) ),
inference(resolution,[status(thm)],[f72,f78]) ).
fof(f263,plain,
( ~ sQ13_spl
| in(sK2_skl(sK0_skl),sK0_skl)
| in(sK2_skl(sK0_skl),sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f244,f20]) ).
fof(f264,definition,
( sQ16_spl
<=> in(sK2_skl(sK0_skl),sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( ~ sQ16_spl
| in(sK2_skl(sK0_skl),sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f264]) ).
fof(f267,definition,
( sQ17_spl
<=> in(sK2_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( ~ sQ17_spl
| in(sK2_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f267]) ).
fof(f270,plain,
( ~ sQ13_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f263,f264,f267,f243]) ).
fof(f272,plain,
! [X0] :
( ~ sQ17_spl
| ordered_pair(sK2_skl(sK0_skl),singleton(sK2_skl(sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f268,f77]) ).
fof(f275,plain,
( ~ sQ17_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f272,f84,f267]) ).
fof(f289,plain,
( ~ sQ14_spl
| sK9_skl(sK0_skl) = sK11_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f250,f71]) ).
fof(f291,plain,
( ~ sQ16_spl
| in(sK13_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),cartesian_product2(sK0_skl,sK1_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f58,f265]) ).
fof(f292,plain,
! [X0,X1] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f58,f21]) ).
fof(f293,plain,
! [X0,X1] :
( in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f58,f20]) ).
fof(f294,plain,
! [X0,X1] :
( sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f58,f23]) ).
fof(f295,plain,
! [X0,X1] :
( in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| in(sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),cartesian_product2(X0,X1))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f58,f22]) ).
fof(f296,definition,
( sQ18_spl
<=> sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f297,plain,
( ~ sQ18_spl
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f298,plain,
( sQ18_spl
| ~ sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f299,definition,
( sQ19_spl
<=> in(sK13_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( ~ sQ16_spl
| sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f291,f296,f299,f264]) ).
fof(f303,plain,
( ~ sQ18_spl
| ~ sQ12_spl
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f241,f297]) ).
fof(f304,plain,
( ~ sQ16_spl
| sK13_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl) = sK2_skl(sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f59,f265]) ).
fof(f305,plain,
! [X0,X1] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f59,f21]) ).
fof(f306,plain,
! [X0,X1] :
( in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f59,f20]) ).
fof(f307,plain,
! [X0,X1] :
( sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f59,f23]) ).
fof(f308,plain,
! [X0,X1] :
( in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f59,f22]) ).
fof(f309,definition,
( sQ20_spl
<=> sK13_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl) = sK2_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( ~ sQ16_spl
| sQ20_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f304,f296,f309,f264]) ).
fof(f313,plain,
( ~ sQ16_spl
| ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)) = sK2_skl(sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f60,f265]) ).
fof(f314,plain,
! [X0,X1] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f60,f21]) ).
fof(f315,plain,
! [X0,X1] :
( in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f60,f20]) ).
fof(f316,plain,
! [X0,X1] :
( sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f60,f23]) ).
fof(f317,plain,
! [X0,X1] :
( in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0)) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f60,f22]) ).
fof(f318,definition,
( sQ21_spl
<=> ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)) = sK2_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f319,plain,
( ~ sQ21_spl
| ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)) = sK2_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f321,plain,
( ~ sQ16_spl
| sQ21_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f313,f296,f318,f264]) ).
fof(f322,plain,
( ~ sQ14_spl
| sP0_prd(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f289,f250]) ).
fof(f324,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f322,f79]) ).
fof(f325,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f324]) ).
fof(f326,plain,
( ~ sQ18_spl
| ~ sQ12_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f303,f249,f240,f296]) ).
fof(f334,plain,
( ~ sQ18_spl
| sK9_skl(sK0_skl) = sK10_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f297,f67]) ).
fof(f335,plain,
( ~ sQ18_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f334,f240,f296]) ).
fof(f346,plain,
! [X0,X1] :
( ~ in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f292,f50]) ).
fof(f347,plain,
! [X0] :
( ~ sQ12_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f292]) ).
fof(f348,definition,
! [X0] :
( sQ22_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( ~ sQ12_spl
| sQ22_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f347,f249,f348,f240]) ).
fof(f355,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ15_spl
| ~ in(sK3_skl(sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f96,f253]) ).
fof(f356,definition,
! [X0] :
( sQ23_spl
<=> ( ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f357,plain,
! [X0] :
( ~ sQ23_spl
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,plain,
( ~ sQ3_spl
| ~ sQ15_spl
| ~ sQ4_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f355,f356,f99,f252,f95]) ).
fof(f360,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ3_spl
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f96,f357]) ).
fof(f361,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f88,f360]) ).
fof(f362,plain,
! [X0] :
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f88,f361]) ).
fof(f364,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| in(sK2_skl(sK0_skl),sK0_skl)
| in(sK2_skl(sK0_skl),sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f362,f20]) ).
fof(f365,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f364,f264,f267,f87,f95,f356]) ).
fof(f371,definition,
( sQ24_spl
<=> sK9_skl(sK0_skl) = sK11_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( ~ sQ24_spl
| sK9_skl(sK0_skl) = sK11_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f378,definition,
( sQ25_spl
<=> sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( ~ sQ25_spl
| sP0_prd(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f378]) ).
fof(f391,plain,
! [X0,X1] :
( ~ in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f295,f50]) ).
fof(f393,plain,
! [X0] :
( ~ sQ12_spl
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f295]) ).
fof(f394,definition,
! [X0] :
( sQ26_spl
<=> ( in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( ~ sQ12_spl
| sQ26_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f393,f249,f394,f240]) ).
fof(f407,plain,
( ~ sQ16_spl
| in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f61,f265]) ).
fof(f408,plain,
! [X0,X1] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f61,f21]) ).
fof(f409,plain,
! [X0,X1] :
( in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f61,f20]) ).
fof(f410,plain,
! [X0,X1] :
( sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f61,f23]) ).
fof(f411,plain,
! [X0,X1] :
( in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| in(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0),X0)
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f61,f22]) ).
fof(f412,definition,
( sQ27_spl
<=> in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ27_spl
| in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,plain,
( ~ sQ16_spl
| sQ27_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f407,f296,f412,f264]) ).
fof(f419,plain,
( ~ sQ16_spl
| sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f62,f265]) ).
fof(f420,plain,
! [X0,X1] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),sK4_skl(sK12_skl(X1,X0))) = sK2_skl(sK12_skl(X1,X0))
| sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f62,f21]) ).
fof(f421,plain,
! [X0,X1] :
( in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f62,f20]) ).
fof(f422,plain,
! [X0,X1] :
( sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f62,f23]) ).
fof(f423,plain,
! [X0,X1] :
( in(sK3_skl(sK12_skl(X1,X0)),sK0_skl)
| sK15_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = singleton(sK14_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f62,f22]) ).
fof(f424,definition,
( sQ28_spl
<=> sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( ~ sQ28_spl
| sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f427,plain,
( ~ sQ16_spl
| sQ28_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f419,f296,f424,f264]) ).
fof(f428,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X1,X0))
| in(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(paramodulation,[status(thm)],[f425,f257]) ).
fof(f429,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X1,X0))
| in(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(paramodulation,[status(thm)],[f425,f256]) ).
fof(f430,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X1,X0))
| sK9_skl(X0) = sK11_skl(X0) ),
inference(paramodulation,[status(thm)],[f425,f247]) ).
fof(f431,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ15_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f425,f253]) ).
fof(f433,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),sK12_skl(X1,X0))
| in(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f425,f428]) ).
fof(f434,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| in(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f319,f433]) ).
fof(f435,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| in(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f319,f434]) ).
fof(f436,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),sK12_skl(X1,X0))
| in(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f425,f429]) ).
fof(f437,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| in(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f319,f436]) ).
fof(f438,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| in(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),X0) ),
inference(forward_demodulation,[status(thm)],[f319,f437]) ).
fof(f439,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),sK12_skl(X1,X0))
| sK9_skl(X0) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f425,f430]) ).
fof(f440,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK9_skl(X0) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f319,f439]) ).
fof(f441,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK9_skl(X0) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f319,f440]) ).
fof(f442,definition,
! [X0] :
( sQ29_spl
<=> ( ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f445,plain,
( ~ sQ28_spl
| ~ sQ15_spl
| ~ sQ27_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f431,f442,f412,f252,f424]) ).
fof(f463,plain,
! [X0,X1,X2] :
( in(sK14_skl(sK14_skl(sK2_skl(sK12_skl(X2,sK12_skl(X0,X1))),X2,sK12_skl(X0,X1)),X0,X1),X1)
| sP0_prd(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1)
| in(sK3_skl(sK12_skl(X2,sK12_skl(X0,X1))),sK0_skl)
| sP0_prd(sK11_skl(sK12_skl(X0,X1)),sK10_skl(sK12_skl(X0,X1)),sK9_skl(sK12_skl(X0,X1)),sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f411,f61]) ).
fof(f467,plain,
! [X0,X1] :
( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f411,f77]) ).
fof(f470,plain,
! [X0] :
( ~ sQ12_spl
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f411]) ).
fof(f471,definition,
! [X0,X1] :
( sQ30_spl
<=> ( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sQ30_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f474,plain,
( sQ30_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f467,f296,f471]) ).
fof(f475,definition,
! [X0] :
( sQ31_spl
<=> ( in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ12_spl
| sQ31_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f470,f249,f475,f240]) ).
fof(f491,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X1,X0))
| sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(paramodulation,[status(thm)],[f96,f258]) ).
fof(f495,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X1,X0))
| sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f96,f491]) ).
fof(f496,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f88,f495]) ).
fof(f497,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f88,f496]) ).
fof(f499,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X1,X0))
| sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(paramodulation,[status(thm)],[f96,f259]) ).
fof(f503,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X1,X0))
| sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f96,f499]) ).
fof(f504,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f88,f503]) ).
fof(f505,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) = singleton(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f88,f504]) ).
fof(f507,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X1,X0))
| ordered_pair(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK10_skl(X0) ),
inference(paramodulation,[status(thm)],[f96,f260]) ).
fof(f511,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X1,X0))
| ordered_pair(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f96,f507]) ).
fof(f512,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| ordered_pair(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f511]) ).
fof(f513,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| ordered_pair(sK16_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK17_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK10_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f512]) ).
fof(f530,plain,
! [X0,X1,X2] :
( ordered_pair(sK3_skl(sK12_skl(X1,X0)),singleton(sK3_skl(sK12_skl(X1,X0)))) != sK2_skl(X2)
| ~ in(sK2_skl(X2),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X2),X2)
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f308,f77]) ).
fof(f533,plain,
! [X0] :
( ~ sQ12_spl
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f308]) ).
fof(f534,definition,
! [X0] :
( sQ32_spl
<=> ( in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( ~ sQ12_spl
| sQ32_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f533,f249,f534,f240]) ).
fof(f547,plain,
! [X0,X1] :
( ~ in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| in(sK2_skl(sK12_skl(X1,X0)),cartesian_product2(sK0_skl,sK1_skl))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f293,f50]) ).
fof(f549,plain,
! [X0] :
( ~ sQ12_spl
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f293]) ).
fof(f550,definition,
! [X0] :
( sQ33_spl
<=> ( in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ12_spl
| sQ33_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f549,f249,f550,f240]) ).
fof(f565,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X1,X0))
| ordered_pair(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK11_skl(X0) ),
inference(paramodulation,[status(thm)],[f96,f261]) ).
fof(f569,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),sK12_skl(X1,X0))
| ordered_pair(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f96,f565]) ).
fof(f570,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| ordered_pair(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f569]) ).
fof(f571,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK3_skl(sK0_skl),X0)
| ~ in(sK2_skl(sK0_skl),cartesian_product2(X0,X1))
| in(sK2_skl(sK0_skl),sK12_skl(X1,X0))
| ordered_pair(sK18_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0),sK19_skl(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0)) = sK11_skl(X0) ),
inference(forward_demodulation,[status(thm)],[f88,f570]) ).
fof(f580,plain,
! [X0,X1] :
( ~ in(cartesian_product2(X0,X1),sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0))
| sK4_skl(sK12_skl(X1,X0)) = singleton(sK3_skl(sK12_skl(X1,X0)))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f294,f50]) ).
fof(f582,plain,
! [X0] :
( ~ sQ12_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f294]) ).
fof(f583,definition,
! [X0] :
( sQ34_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f587,plain,
( ~ sQ12_spl
| sQ34_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f582,f249,f583,f240]) ).
fof(f607,definition,
( sQ35_spl
<=> in(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( ~ sQ35_spl
| in(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f639,definition,
( sQ39_spl
<=> in(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f640,plain,
( ~ sQ39_spl
| in(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f674,plain,
! [X0] :
( ~ sQ12_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f305]) ).
fof(f675,definition,
! [X0] :
( sQ45_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ12_spl
| sQ45_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f674,f249,f675,f240]) ).
fof(f693,plain,
! [X0] :
( ~ sQ12_spl
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f306]) ).
fof(f694,definition,
! [X0] :
( sQ46_spl
<=> ( in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( ~ sQ12_spl
| sQ46_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f693,f249,f694,f240]) ).
fof(f699,plain,
! [X0,X1] :
( ordered_pair(sK18_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1),sK19_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1)) = sK11_skl(X1)
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f72]) ).
fof(f700,plain,
! [X0,X1] :
( ordered_pair(sK16_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1),sK17_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1)) = sK10_skl(X1)
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f68]) ).
fof(f701,plain,
! [X0,X1] :
( sK19_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1) = singleton(sK18_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1))
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f74]) ).
fof(f702,plain,
! [X0,X1] :
( sK17_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1) = singleton(sK16_skl(sK11_skl(X1),sK10_skl(X1),sK9_skl(X1),X1))
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f70]) ).
fof(f705,plain,
! [X0,X1] :
( sK9_skl(X1) = sK11_skl(X1)
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f71]) ).
fof(f706,plain,
! [X0,X1] :
( sK9_skl(X1) = sK10_skl(X1)
| sK4_skl(sK12_skl(X0,X1)) = singleton(sK3_skl(sK12_skl(X0,X1)))
| sK13_skl(sK2_skl(sK12_skl(X0,X1)),X0,X1) = sK2_skl(sK12_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f307,f67]) ).
fof(f709,definition,
! [X0] :
( sQ47_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f710,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f724,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f391]) ).
fof(f731,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f294]) ).
fof(f734,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f293]) ).
fof(f739,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f295]) ).
fof(f740,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f292]) ).
fof(f743,definition,
! [X0] :
( sQ48_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f746,plain,
( ~ sQ47_spl
| sQ48_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f724,f296,f743,f709]) ).
fof(f747,definition,
! [X0] :
( sQ49_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f752,definition,
! [X0] :
( sQ50_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f753,plain,
! [X0] :
( ~ sQ50_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f757,definition,
! [X0] :
( sQ51_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( ~ sQ47_spl
| sQ50_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f731,f296,f752,f709]) ).
fof(f763,definition,
! [X0] :
( sQ52_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f768,plain,
( ~ sQ47_spl
| sQ52_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f734,f296,f763,f709]) ).
fof(f771,definition,
! [X0] :
( sQ53_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( ~ sQ47_spl
| sQ53_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f739,f296,f771,f709]) ).
fof(f777,definition,
! [X0] :
( sQ54_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( ~ sQ47_spl
| sQ54_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f740,f296,f777,f709]) ).
fof(f799,plain,
! [X0] :
( sQ18_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(resolution,[status(thm)],[f298,f307]) ).
fof(f801,plain,
! [X0] :
( sQ18_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sK13_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(resolution,[status(thm)],[f298,f305]) ).
fof(f808,plain,
! [X0,X1] :
( sQ18_spl
| ~ in(X0,sK0_skl)
| ~ in(ordered_pair(X0,singleton(X0)),cartesian_product2(sK0_skl,X1))
| in(ordered_pair(X0,singleton(X0)),sK12_skl(X1,sK0_skl)) ),
inference(resolution,[status(thm)],[f298,f78]) ).
fof(f809,plain,
( sQ18_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f799,f709,f296]) ).
fof(f810,plain,
! [X0] :
( ~ sQ50_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f753]) ).
fof(f826,definition,
! [X0] :
( sQ55_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f843,plain,
! [X0] :
( ~ sQ12_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f314]) ).
fof(f857,plain,
( ~ sQ12_spl
| sQ55_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f843,f249,f826,f240]) ).
fof(f877,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ50_spl
| sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))
| sK2_skl(sK0_skl) != sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl))) ),
inference(resolution,[status(thm)],[f810,f168]) ).
fof(f880,definition,
( sQ56_spl
<=> sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f881,plain,
( ~ sQ56_spl
| sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl))) ),
inference(component_clause,[status(thm)],[f880]) ).
fof(f883,definition,
( sQ57_spl
<=> sK2_skl(sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ50_spl
| ~ sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f877,f880,f883,f752,f87,f95,f99]) ).
fof(f891,definition,
( sQ59_spl
<=> in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f893,plain,
( sQ59_spl
| ~ in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl) ),
inference(component_clause,[status(thm)],[f891]) ).
fof(f924,plain,
! [X0] :
( ~ sQ12_spl
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f315]) ).
fof(f925,definition,
! [X0] :
( sQ60_spl
<=> ( in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f929,plain,
( ~ sQ12_spl
| sQ60_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f924,f249,f925,f240]) ).
fof(f939,plain,
! [X0] :
( ~ sQ12_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f316]) ).
fof(f940,definition,
! [X0] :
( sQ61_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f944,plain,
( ~ sQ12_spl
| sQ61_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f939,f249,f940,f240]) ).
fof(f945,plain,
! [X0] :
( ~ sQ28_spl
| sQ18_spl
| ~ in(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK0_skl),sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f425,f808]) ).
fof(f946,plain,
! [X0] :
( ~ sQ56_spl
| sQ18_spl
| ~ in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)
| ~ in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f881,f808]) ).
fof(f947,plain,
! [X0] :
( ~ sQ3_spl
| sQ18_spl
| ~ in(sK3_skl(sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK3_skl(sK0_skl),sK4_skl(sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK0_skl),singleton(sK3_skl(sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f96,f808]) ).
fof(f948,plain,
( ~ sQ28_spl
| sQ18_spl
| ~ sQ27_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f945,f442,f412,f296,f424]) ).
fof(f949,definition,
! [X0] :
( sQ62_spl
<=> ( ~ in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f950,plain,
! [X0] :
( ~ sQ62_spl
| ~ in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))),sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f952,plain,
( ~ sQ56_spl
| sQ18_spl
| ~ sQ59_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f946,f949,f891,f296,f880]) ).
fof(f953,plain,
( ~ sQ3_spl
| sQ18_spl
| ~ sQ4_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f947,f356,f99,f296,f95]) ).
fof(f958,plain,
( sQ59_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f893,f308]) ).
fof(f959,definition,
( sQ63_spl
<=> sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f960,plain,
( ~ sQ63_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f961,plain,
( sQ63_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) != sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f964,plain,
( sQ59_spl
| sQ63_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f958,f296,f959,f891]) ).
fof(f977,plain,
( ~ sQ63_spl
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f960,f293]) ).
fof(f988,definition,
( sQ65_spl
<=> in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f989,plain,
( ~ sQ65_spl
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f988]) ).
fof(f1002,plain,
( ~ sQ63_spl
| sQ65_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f977,f296,f988,f959]) ).
fof(f1018,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ65_spl
| in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)
| sK2_skl(sK0_skl) != sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f989,f169]) ).
fof(f1022,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ65_spl
| sQ59_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f1018,f883,f891,f988,f87,f95,f99]) ).
fof(f1031,plain,
( sQ59_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f317,f893]) ).
fof(f1035,plain,
! [X0] :
( ~ sQ12_spl
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f317]) ).
fof(f1036,definition,
( sQ66_spl
<=> ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( ~ sQ66_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1039,plain,
( sQ59_spl
| sQ66_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1031,f296,f1036,f891]) ).
fof(f1040,definition,
! [X0] :
( sQ67_spl
<=> ( in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1044,plain,
( ~ sQ12_spl
| sQ67_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1035,f249,f1040,f240]) ).
fof(f1058,plain,
! [X0,X1] :
( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f408,f77]) ).
fof(f1061,plain,
! [X0] :
( ~ sQ12_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f408]) ).
fof(f1062,definition,
! [X0,X1] :
( sQ68_spl
<=> ( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1065,plain,
( sQ68_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1058,f296,f1062]) ).
fof(f1066,definition,
! [X0] :
( sQ69_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1070,plain,
( ~ sQ12_spl
| sQ69_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1061,f249,f1066,f240]) ).
fof(f1084,plain,
! [X0,X1] :
( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f409,f77]) ).
fof(f1087,plain,
! [X0] :
( ~ sQ12_spl
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f409]) ).
fof(f1088,definition,
! [X0,X1] :
( sQ70_spl
<=> ( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1091,plain,
( sQ70_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1084,f296,f1088]) ).
fof(f1092,definition,
! [X0] :
( sQ71_spl
<=> ( in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1096,plain,
( ~ sQ12_spl
| sQ71_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1087,f249,f1092,f240]) ).
fof(f1128,plain,
! [X0,X1] :
( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f410,f77]) ).
fof(f1131,plain,
! [X0] :
( ~ sQ12_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f410]) ).
fof(f1132,definition,
! [X0,X1] :
( sQ72_spl
<=> ( ordered_pair(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X1)
| ~ in(sK2_skl(X1),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X1),X1)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1135,plain,
( sQ72_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1128,f296,f1132]) ).
fof(f1136,definition,
! [X0] :
( sQ73_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| in(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl),sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1140,plain,
( ~ sQ12_spl
| sQ73_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1131,f249,f1136,f240]) ).
fof(f1186,plain,
! [X0] :
( ~ sQ12_spl
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f420]) ).
fof(f1187,definition,
! [X0] :
( sQ74_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1191,plain,
( ~ sQ12_spl
| sQ74_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1186,f249,f1187,f240]) ).
fof(f1205,plain,
! [X0] :
( ~ sQ12_spl
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f421]) ).
fof(f1206,definition,
! [X0] :
( sQ75_spl
<=> ( in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1210,plain,
( ~ sQ12_spl
| sQ75_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1205,f249,f1206,f240]) ).
fof(f1250,definition,
( sQ76_spl
<=> sK2_skl(sK12_skl(sK1_skl,sK0_skl)) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1252,plain,
( sQ76_spl
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1250]) ).
fof(f1283,plain,
! [X0] :
( ~ sQ12_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f422]) ).
fof(f1284,definition,
! [X0] :
( sQ77_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1288,plain,
( ~ sQ12_spl
| sQ77_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1283,f249,f1284,f240]) ).
fof(f1297,plain,
( sQ59_spl
| sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f423,f893]) ).
fof(f1301,plain,
! [X0] :
( ~ sQ12_spl
| in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f241,f423]) ).
fof(f1302,definition,
( sQ78_spl
<=> sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ78_spl
| sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1305,plain,
( sQ59_spl
| sQ78_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1297,f296,f1302,f891]) ).
fof(f1306,definition,
! [X0] :
( sQ79_spl
<=> ( in(sK3_skl(sK12_skl(X0,sK0_skl)),sK0_skl)
| sK15_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(X0,sK0_skl)),X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
( ~ sQ12_spl
| sQ79_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f1301,f249,f1306,f240]) ).
fof(f1314,definition,
( sQ80_spl
<=> ordered_pair(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK11_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
! [X0] :
( ~ sQ78_spl
| sQ18_spl
| ~ in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1303,f808]) ).
fof(f1328,definition,
! [X0] :
( sQ81_spl
<=> ( ~ in(ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1331,definition,
( sQ82_spl
<=> in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1332,plain,
( ~ sQ82_spl
| in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f1331]) ).
fof(f1334,plain,
( ~ sQ78_spl
| sQ18_spl
| ~ sQ82_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f1319,f1328,f1331,f296,f1302]) ).
fof(f1353,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK9_skl(sK0_skl) = sK11_skl(sK0_skl)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f705]) ).
fof(f1381,definition,
! [X0] :
( sQ83_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( ~ sQ47_spl
| sQ24_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1353,f1381,f371,f709]) ).
fof(f1412,definition,
( sQ84_spl
<=> ordered_pair(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK10_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1474,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK9_skl(sK0_skl) = sK10_skl(sK0_skl)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f706]) ).
fof(f1505,plain,
( ~ sQ47_spl
| sQ12_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1474,f1381,f240,f709]) ).
fof(f1540,definition,
( sQ85_spl
<=> sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1541,plain,
( ~ sQ85_spl
| sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1540]) ).
fof(f1550,definition,
( sQ86_spl
<=> sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1551,plain,
( ~ sQ86_spl
| sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1550]) ).
fof(f1577,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| sK9_skl(sK0_skl) = sK11_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f441,f413]) ).
fof(f1578,plain,
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| sQ13_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1577,f371,f243,f318,f424,f412]) ).
fof(f1579,plain,
( ~ sQ25_spl
| ~ sQ12_spl
| sP0_prd(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f241,f379]) ).
fof(f1580,plain,
( ~ sQ25_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1579,f79]) ).
fof(f1581,plain,
( ~ sQ25_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f1580]) ).
fof(f1820,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f346]) ).
fof(f1824,definition,
! [X0] :
( sQ89_spl
<=> ( sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK3_skl(sK12_skl(X0,sK0_skl)),sK4_skl(sK12_skl(X0,sK0_skl))) = sK2_skl(sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1827,plain,
( ~ sQ47_spl
| sQ89_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1820,f296,f1824,f709]) ).
fof(f2090,plain,
( ~ sQ39_spl
| ~ sQ24_spl
| in(sK16_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f372,f640]) ).
fof(f2091,plain,
( ~ sQ39_spl
| ~ sQ24_spl
| ~ sQ12_spl
| in(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f241,f2090]) ).
fof(f2094,plain,
( ~ sQ35_spl
| ~ sQ24_spl
| in(sK18_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f372,f608]) ).
fof(f2095,plain,
( ~ sQ35_spl
| ~ sQ24_spl
| ~ sQ12_spl
| in(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f241,f2094]) ).
fof(f2178,plain,
! [X0,X1,X2] :
( ordered_pair(sK14_skl(sK14_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK14_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X2)
| ~ in(sK2_skl(X2),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X2),X2)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)
| in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)
| sP0_prd(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(resolution,[status(thm)],[f463,f77]) ).
fof(f2180,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( ordered_pair(sK14_skl(sK14_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),X0,sK0_skl),singleton(sK14_skl(sK14_skl(sK2_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),X1,sK12_skl(X0,sK0_skl)),X0,sK0_skl))) != sK2_skl(X2)
| ~ in(sK2_skl(X2),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X2),X2)
| in(sK3_skl(sK12_skl(X1,sK12_skl(X0,sK0_skl))),sK0_skl)
| sP0_prd(sK11_skl(sK12_skl(X0,sK0_skl)),sK10_skl(sK12_skl(X0,sK0_skl)),sK9_skl(sK12_skl(X0,sK0_skl)),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2183,plain,
( sQ18_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2178,f2180,f296]) ).
fof(f2201,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| in(sK2_skl(sK12_skl(X0,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f547]) ).
fof(f2205,plain,
( ~ sQ47_spl
| sQ51_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2201,f296,f757,f709]) ).
fof(f2207,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ~ in(cartesian_product2(sK0_skl,X0),sK2_skl(sK12_skl(X0,sK0_skl)))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(paramodulation,[status(thm)],[f710,f580]) ).
fof(f2211,plain,
( ~ sQ47_spl
| sQ49_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2207,f296,f747,f709]) ).
fof(f2299,plain,
! [X0] :
( sQ59_spl
| ~ sQ30_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f472,f893]) ).
fof(f2302,plain,
! [X0] :
( sQ59_spl
| ~ sQ30_spl
| ~ sQ78_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f1303,f2299]) ).
fof(f2303,plain,
! [X0] :
( sQ59_spl
| ~ sQ30_spl
| ~ sQ78_spl
| ~ sQ66_spl
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f1037,f2302]) ).
fof(f2311,plain,
! [X0] :
( sQ59_spl
| ~ sQ30_spl
| ~ sQ78_spl
| ~ sQ66_spl
| in(sK3_skl(X0),sK0_skl)
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f2303,f22]) ).
fof(f2319,plain,
( ~ sQ65_spl
| sQ59_spl
| ~ sQ30_spl
| ~ sQ78_spl
| ~ sQ66_spl
| in(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK0_skl)
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f2311,f989]) ).
fof(f2339,plain,
( ~ sQ65_spl
| ~ sQ30_spl
| ~ sQ78_spl
| ~ sQ66_spl
| sQ59_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f2319,f1250,f891,f1036,f1302,f471,f988]) ).
fof(f2351,plain,
( sQ76_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1252]) ).
fof(f2352,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f2351]) ).
fof(f2365,plain,
( ~ sQ86_spl
| ~ sQ24_spl
| sK17_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f372,f1551]) ).
fof(f2366,plain,
( ~ sQ86_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK17_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f241,f2365]) ).
fof(f2367,plain,
( ~ sQ86_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK17_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f372,f2366]) ).
fof(f2368,plain,
( ~ sQ86_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK17_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f241,f2367]) ).
fof(f2369,plain,
( ~ sQ85_spl
| ~ sQ24_spl
| sK19_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f372,f1541]) ).
fof(f2370,plain,
( ~ sQ85_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK19_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f241,f2369]) ).
fof(f2371,plain,
( ~ sQ85_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK19_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK9_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f372,f2370]) ).
fof(f2372,plain,
( ~ sQ85_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sK19_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f241,f2371]) ).
fof(f2387,plain,
! [X0] :
( ~ sQ62_spl
| ~ sQ56_spl
| ~ in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f881,f950]) ).
fof(f2396,plain,
( ~ sQ47_spl
| sQ63_spl
| sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl)))
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f961]) ).
fof(f2401,plain,
( ~ sQ47_spl
| sQ63_spl
| sQ56_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f2396,f1250,f880,f959,f709]) ).
fof(f2417,plain,
! [X0] :
( ~ sQ86_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sQ18_spl
| ~ in(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK17_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),singleton(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f2368,f808]) ).
fof(f2426,definition,
! [X0] :
( sQ93_spl
<=> ( ~ in(ordered_pair(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK17_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),singleton(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2429,definition,
( sQ94_spl
<=> in(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f2431,plain,
( sQ94_spl
| ~ in(sK16_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f2429]) ).
fof(f2432,plain,
( ~ sQ86_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sQ18_spl
| ~ sQ94_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f2417,f2426,f2429,f296,f240,f371,f1550]) ).
fof(f2441,plain,
( sQ94_spl
| ~ sQ39_spl
| ~ sQ24_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2431,f2091]) ).
fof(f2442,plain,
( sQ94_spl
| ~ sQ39_spl
| ~ sQ24_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f2441]) ).
fof(f2447,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f497,f100]) ).
fof(f2448,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ13_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f2447,f1550,f243,f87,f95,f99]) ).
fof(f2449,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) ),
inference(resolution,[status(thm)],[f505,f100]) ).
fof(f2450,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ13_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f2449,f1540,f243,f87,f95,f99]) ).
fof(f2451,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sQ18_spl
| ~ in(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl)
| ~ in(ordered_pair(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK19_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),singleton(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f2372,f808]) ).
fof(f2460,definition,
! [X0] :
( sQ95_spl
<=> ( ~ in(ordered_pair(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK19_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),singleton(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2463,definition,
( sQ96_spl
<=> in(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2465,plain,
( sQ96_spl
| ~ in(sK18_skl(sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f2463]) ).
fof(f2466,plain,
( ~ sQ85_spl
| ~ sQ24_spl
| ~ sQ12_spl
| sQ18_spl
| ~ sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2451,f2460,f2463,f296,f240,f371,f1540]) ).
fof(f2476,plain,
( sQ96_spl
| ~ sQ35_spl
| ~ sQ24_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2465,f2095]) ).
fof(f2477,plain,
( sQ96_spl
| ~ sQ35_spl
| ~ sQ24_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f2476]) ).
fof(f2712,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| ordered_pair(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK10_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f513,f100]) ).
fof(f2713,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ13_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f2712,f1412,f243,f87,f95,f99]) ).
fof(f2816,plain,
! [X0,X1] :
( ~ sQ5_spl
| ordered_pair(sK3_skl(sK12_skl(X1,X0)),singleton(sK3_skl(sK12_skl(X1,X0)))) != sK2_skl(cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(cartesian_product2(sK0_skl,sK1_skl)),cartesian_product2(sK0_skl,sK1_skl))
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ),
inference(resolution,[status(thm)],[f530,f111]) ).
fof(f2824,definition,
! [X0,X1] :
( sQ101_spl
<=> ( ordered_pair(sK3_skl(sK12_skl(X1,X0)),singleton(sK3_skl(sK12_skl(X1,X0)))) != sK2_skl(cartesian_product2(sK0_skl,sK1_skl))
| sK13_skl(sK2_skl(sK12_skl(X1,X0)),X1,X0) = sK2_skl(sK12_skl(X1,X0))
| sP0_prd(sK11_skl(X0),sK10_skl(X0),sK9_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2827,plain,
( ~ sQ5_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f2816,f2824,f110]) ).
fof(f3019,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| ordered_pair(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK11_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f571,f100]) ).
fof(f3020,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ13_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f3019,f1314,f243,f87,f95,f99]) ).
fof(f3271,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| in(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f435,f413]) ).
fof(f3272,plain,
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| sQ13_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f3271,f607,f243,f318,f424,f412]) ).
fof(f3273,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| ~ in(sK2_skl(sK0_skl),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK0_skl),sK12_skl(X0,sK0_skl))
| in(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f438,f413]) ).
fof(f3274,plain,
( ~ sQ27_spl
| ~ sQ28_spl
| ~ sQ21_spl
| sQ13_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f3273,f639,f243,f318,f424,f412]) ).
fof(f3503,plain,
! [X0] :
( sQ18_spl
| ~ sQ62_spl
| ~ sQ56_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f801,f2387]) ).
fof(f3512,definition,
! [X0] :
( sQ105_spl
<=> ( ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f3513,plain,
! [X0] :
( ~ sQ105_spl
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f3512]) ).
fof(f3516,plain,
( sQ18_spl
| ~ sQ62_spl
| ~ sQ56_spl
| sQ63_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f3503,f3512,f959,f880,f949,f296]) ).
fof(f3530,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK11_skl(sK0_skl)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f699]) ).
fof(f3600,plain,
( ~ sQ47_spl
| sQ80_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f3530,f1381,f1314,f709]) ).
fof(f3637,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| ordered_pair(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl),sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl)) = sK10_skl(sK0_skl)
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f700]) ).
fof(f3709,plain,
( ~ sQ47_spl
| sQ84_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f3637,f1381,f1412,f709]) ).
fof(f3752,plain,
! [X0] :
( sQ18_spl
| ~ sQ105_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f801,f3513]) ).
fof(f3781,definition,
! [X0] :
( sQ111_spl
<=> ( ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f3782,plain,
! [X0] :
( ~ sQ111_spl
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f3781]) ).
fof(f3785,plain,
( sQ18_spl
| ~ sQ105_spl
| sQ63_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f3752,f3781,f959,f3512,f296]) ).
fof(f3854,plain,
( ~ sQ111_spl
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f3782,f20]) ).
fof(f3855,definition,
( sQ112_spl
<=> in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f3856,plain,
( ~ sQ112_spl
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f3855]) ).
fof(f3857,plain,
( sQ112_spl
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f3855]) ).
fof(f3879,plain,
( ~ sQ111_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f3854,f3855,f3781]) ).
fof(f3901,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK19_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK18_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f701]) ).
fof(f3973,plain,
( ~ sQ47_spl
| sQ85_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f3901,f1381,f1540,f709]) ).
fof(f4009,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ112_spl
| sK2_skl(sK0_skl) != sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f3856,f161]) ).
fof(f4010,plain,
( ~ sQ112_spl
| sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f3856,f62]) ).
fof(f4011,plain,
( ~ sQ112_spl
| in(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK0_skl)
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f3856,f61]) ).
fof(f4012,plain,
( ~ sQ112_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f3856,f60]) ).
fof(f4013,plain,
( ~ sQ112_spl
| sK13_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| sP0_prd(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f3856,f59]) ).
fof(f4017,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ112_spl
| ~ sQ57_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f4009,f988,f883,f3855,f87,f95,f99]) ).
fof(f4018,plain,
( ~ sQ112_spl
| sQ78_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f4010,f296,f1302,f3855]) ).
fof(f4019,plain,
( ~ sQ112_spl
| sQ82_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f4011,f296,f1331,f3855]) ).
fof(f4020,plain,
( ~ sQ112_spl
| sQ66_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f4012,f296,f1036,f3855]) ).
fof(f4021,plain,
( ~ sQ112_spl
| sQ63_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f4013,f296,f959,f3855]) ).
fof(f4031,plain,
! [X0] :
( ~ sQ82_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),singleton(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl))) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f1332,f77]) ).
fof(f4197,plain,
! [X0] :
( ~ sQ47_spl
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK17_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl) = singleton(sK16_skl(sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK9_skl(sK0_skl),sK0_skl))
| sK4_skl(sK12_skl(X0,sK0_skl)) = singleton(sK3_skl(sK12_skl(X0,sK0_skl)))
| sK2_skl(sK12_skl(X0,sK0_skl)) = sK2_skl(sK12_skl(X0,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f710,f702]) ).
fof(f4273,plain,
( ~ sQ47_spl
| sQ86_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f4197,f1381,f1550,f709]) ).
fof(f4406,plain,
( sQ112_spl
| ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))) = sK2_skl(sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f3857,f21]) ).
fof(f4408,plain,
( sQ112_spl
| sK4_skl(sK12_skl(sK1_skl,sK0_skl)) = singleton(sK3_skl(sK12_skl(sK1_skl,sK0_skl))) ),
inference(resolution,[status(thm)],[f3857,f23]) ).
fof(f4823,plain,
! [X0] :
( ~ sQ62_spl
| ~ sQ56_spl
| sQ112_spl
| ~ in(ordered_pair(sK3_skl(sK12_skl(sK1_skl,sK0_skl)),sK4_skl(sK12_skl(sK1_skl,sK0_skl))),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4406,f2387]) ).
fof(f4824,plain,
! [X0] :
( ~ sQ62_spl
| ~ sQ56_spl
| sQ112_spl
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,X0))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(X0,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4406,f4823]) ).
fof(f4847,plain,
( ~ sQ62_spl
| ~ sQ56_spl
| sQ112_spl
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl))
| in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK12_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f4824,f20]) ).
fof(f4870,plain,
( ~ sQ62_spl
| ~ sQ56_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f4847,f3855,f880,f949]) ).
fof(f4871,plain,
! [X0] :
( ~ sQ82_spl
| ~ sQ78_spl
| ordered_pair(sK14_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),sK15_skl(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f1303,f4031]) ).
fof(f5188,plain,
! [X0] :
( ~ sQ82_spl
| ~ sQ78_spl
| ~ sQ66_spl
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(X0)
| ~ in(sK2_skl(X0),cartesian_product2(sK0_skl,sK1_skl))
| ~ in(sK2_skl(X0),X0) ),
inference(forward_demodulation,[status(thm)],[f1037,f4871]) ).
fof(f5189,plain,
( ~ sQ112_spl
| ~ sQ82_spl
| ~ sQ78_spl
| ~ sQ66_spl
| sK2_skl(sK12_skl(sK1_skl,sK0_skl)) != sK2_skl(sK12_skl(sK1_skl,sK0_skl))
| ~ in(sK2_skl(sK12_skl(sK1_skl,sK0_skl)),cartesian_product2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f5188,f3856]) ).
fof(f5198,plain,
( ~ sQ112_spl
| ~ sQ82_spl
| ~ sQ78_spl
| ~ sQ66_spl
| ~ sQ76_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f5189,f988,f1250,f1036,f1302,f1331,f3855]) ).
fof(f5203,plain,
( sQ112_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f4408,f880,f3855]) ).
fof(f5204,plain,
$false,
inference(sat_refutation,[status(thm)],[f90,f94,f98,f102,f116,f145,f173,f246,f255,f270,f275,f302,f312,f321,f325,f326,f335,f351,f359,f365,f398,f415,f427,f445,f474,f479,f538,f554,f587,f679,f698,f746,f762,f768,f776,f780,f809,f857,f890,f929,f944,f948,f952,f953,f964,f1002,f1022,f1039,f1044,f1065,f1070,f1091,f1096,f1135,f1140,f1191,f1210,f1288,f1305,f1310,f1334,f1384,f1505,f1578,f1581,f1827,f2183,f2205,f2211,f2339,f2352,f2401,f2432,f2442,f2448,f2450,f2466,f2477,f2713,f2827,f3020,f3272,f3274,f3516,f3600,f3709,f3785,f3879,f3973,f4017,f4018,f4019,f4020,f4021,f4273,f4870,f5198,f5203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU281+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n007.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 06:04:41 UTC 2026
% 0.16/5.44 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 10.58/6.90 % Refutation found
% 10.58/6.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.58/6.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.08/6.95 % Elapsed time: 1.492998 seconds
% 7.08/6.95 % CPU time: 11.415153 seconds
% 7.08/6.95 % Total memory used: 188.350 MB
% 7.08/6.95 % Net memory used: 177.850 MB
%------------------------------------------------------------------------------