%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO473+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 12:25:06 PM UTC 2026
% Result : Theorem 123.51s 17.83s
% Output : CNFRefutation 120.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 100
% Syntax : Number of formulae : 371 ( 57 unt; 56 def)
% Number of atoms : 1036 ( 193 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1109 ( 444 ~; 427 |; 140 &)
% ( 87 <=>; 9 =>; 0 <=; 2 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 59 ( 57 usr; 57 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 28 con; 0-3 aty)
% Number of variables : 770 ( 701 !; 69 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
( p(s(bool,f0))
<=> ! [P0] : p(s(bool,P0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( ~ p(s(bool,X))
<=> ( p(s(bool,X))
=> p(s(bool,f0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
s(bool,u_falsityu_) = s(bool,f0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,X] :
( s(A,X) = s(A,X)
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [T0] :
( ( s(bool,T0) = s(bool,f0)
<=> ~ p(s(bool,T0)) )
& ( s(bool,f0) = s(bool,T0)
<=> ~ p(s(bool,T0)) )
& ( s(bool,T0) = s(bool,t)
<=> p(s(bool,T0)) )
& ( s(bool,t) = s(bool,T0)
<=> p(s(bool,T0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
~ p(s(bool,f0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
( ~ p(s(bool,f0))
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A,P0,A5] :
( ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) )
<=> p(s(bool,i(s(fun(A,bool),P0),s(A,A5)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A,P0,A5] :
( ! [X] :
( s(A,X) = s(A,A5)
=> p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> p(s(bool,i(s(fun(A,bool),P0),s(A,A5)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [Q1020,P0,A5] :
( ! [X] :
( s(Q1020,A5) = s(Q1020,X)
=> p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X)))) )
<=> p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A,P0,Q0] :
( ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A,P0,Q0] :
( ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A,P0,Q0] :
( ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A,P0,Q0] :
( ( p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ? [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,P0,Q0] :
( ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
<=> ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A,P0,X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
=> p(s(bool,i(s(fun(A,bool),P0),s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [A,P0,X] :
( ! [Y] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,Y))))
<=> s(A,Y) = s(A,X) )
=> s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))) = s(A,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [A,P0,Q0] :
( ( p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
<=> ! [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [A,F0,G0] : s(fun(A,n10),F0) = s(fun(A,n10),G0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,axiom,
( s(num,u_0) = s(num,u_0)
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,axiom,
! [N0] : s(num,i(s(fun(num,num),numeral),s(num,N0))) = s(num,N0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f568,axiom,
! [N0] :
( s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0)
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f572,axiom,
! [M0,N0] :
( s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0)))
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1659,axiom,
! [A,X] : s(bool,i(s(fun(A,bool),empty),s(A,X))) = s(bool,f0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1661,axiom,
! [A,X] : s(bool,i(s(fun(A,bool),univ),s(A,X))) = s(bool,t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1710,axiom,
! [A,S0] : p(s(bool,i(s(fun(fun(A,bool),bool),i(s(fun(fun(A,bool),fun(fun(A,bool),bool)),subset),s(fun(A,bool),S0))),s(fun(A,bool),univ)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1983,axiom,
! [A,B] :
( ( p(s(bool,i(s(fun(fun(B,bool),bool),finite),s(fun(B,bool),univ))))
& p(s(bool,i(s(fun(fun(A,bool),bool),finite),s(fun(A,bool),univ)))) )
=> p(s(bool,i(s(fun(fun(fun(A,B),bool),bool),finite),s(fun(fun(A,B),bool),univ)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1986,axiom,
p(s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2001,axiom,
~ p(s(bool,i(s(fun(fun(num,bool),bool),finite),s(fun(num,bool),univ)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2041,axiom,
! [Q58981,P0] :
( ! [X] :
( p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty))))
=> p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X)))) )
<=> p(s(bool,t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2043,axiom,
! [Q59041,P0] :
( ? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) )
<=> p(s(bool,f0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2363,axiom,
! [A,S0] : s(num,i(s(fun(fun(A,bool),num),dimindex),s(fun(A,bool),S0))) != s(num,i(s(fun(num,num),numeral),s(num,u_0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2364,axiom,
! [A,S0] : p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,i(s(fun(fun(A,bool),num),dimindex),s(fun(A,bool),S0)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2377,axiom,
! [B,A,R0] :
( p(s(bool,t))
<=> s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2406,axiom,
s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))) = s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2413,axiom,
! [A,N] :
( p(s(bool,i(s(fun(fun(A,bool),bool),finite),s(fun(A,bool),univ))))
=> p(s(bool,i(s(fun(fun(cart(A,N),bool),bool),finite),s(fun(cart(A,N),bool),univ)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3331,axiom,
! [N] : s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),univ))) = s(fun(cart(real,N),bool),univ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3398,axiom,
! [N] : s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),univ))) = s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3400,axiom,
! [N,S0] : p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))))),s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3407,axiom,
! [N,S0] : s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))))) = s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3408,axiom,
! [N,S0] : s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),i(s(fun(cart(real,N),fun(fun(cart(real,N),bool),fun(cart(real,N),bool))),insert),s(cart(real,N),i(s(fun(num,cart(real,N)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,N),bool),S0))))) = s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3492,axiom,
! [N,S0,T0] :
( ( p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),T0))))),s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))))))
& p(s(bool,i(s(fun(fun(cart(real,N),bool),bool),i(s(fun(fun(cart(real,N),bool),fun(fun(cart(real,N),bool),bool)),subset),s(fun(cart(real,N),bool),S0))),s(fun(cart(real,N),bool),T0)))) )
=> s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),T0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3493,conjecture,
! [N,S0] :
( s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))) = s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ)))
<=> s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),univ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3494,negated_conjecture,
~ ! [N,S0] :
( s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))) = s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ)))
<=> s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),univ) ),
inference(negated_conjecture,[status(cth)],[f3493]) ).
fof(f3534,plain,
( ( ? [P0] : ~ p(s(bool,P0))
| p(s(bool,f0)) )
& ( ! [P0] : p(s(bool,P0))
| ~ p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f3535,plain,
( ( ~ p(s(bool,sK5_skl))
| p(s(bool,f0)) )
& ( ! [P0] : p(s(bool,P0))
| ~ p(s(bool,f0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P0,sK5_skl)],[f3534]) ).
fof(f3537,plain,
( ~ p(s(bool,sK5_skl))
| p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3535]) ).
fof(f3538,plain,
! [X] :
( ~ p(s(bool,X))
<=> ( p(s(bool,f0))
| ~ p(s(bool,X)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f3539,plain,
! [X] :
( ( ( ~ p(s(bool,f0))
& p(s(bool,X)) )
| ~ p(s(bool,X)) )
& ( p(s(bool,f0))
| ~ p(s(bool,X))
| p(s(bool,X)) ) ),
inference(NNF_transformation,[status(thm)],[f3538]) ).
fof(f3540,plain,
( ! [X] :
( ( ~ p(s(bool,f0))
& p(s(bool,X)) )
| ~ p(s(bool,X)) )
& ! [X] :
( p(s(bool,f0))
| ~ p(s(bool,X))
| p(s(bool,X)) ) ),
inference(miniscoping,[status(thm)],[f3539]) ).
fof(f3541,plain,
! [X0] :
( p(s(bool,f0))
| ~ p(s(bool,X0))
| p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3540]) ).
fof(f3545,plain,
s(bool,u_falsityu_) = s(bool,f0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f3555,plain,
! [A,X] :
( ( ~ p(s(bool,t))
| s(A,X) = s(A,X) )
& ( p(s(bool,t))
| s(A,X) != s(A,X) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f3556,plain,
( ( ~ p(s(bool,t))
| ! [A,X] : s(A,X) = s(A,X) )
& ( p(s(bool,t))
| ! [A,X] : s(A,X) != s(A,X) ) ),
inference(miniscoping,[status(thm)],[f3555]) ).
fof(f3557,plain,
! [X0,X1] :
( p(s(bool,t))
| s(X0,X1) != s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3556]) ).
fof(f3558,plain,
! [X0,X1] :
( ~ p(s(bool,t))
| s(X0,X1) = s(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3556]) ).
fof(f3703,plain,
! [T0] :
( ( p(s(bool,T0))
| s(bool,T0) = s(bool,f0) )
& ( ~ p(s(bool,T0))
| s(bool,T0) != s(bool,f0) )
& ( p(s(bool,T0))
| s(bool,f0) = s(bool,T0) )
& ( ~ p(s(bool,T0))
| s(bool,f0) != s(bool,T0) )
& ( ~ p(s(bool,T0))
| s(bool,T0) = s(bool,t) )
& ( p(s(bool,T0))
| s(bool,T0) != s(bool,t) )
& ( ~ p(s(bool,T0))
| s(bool,t) = s(bool,T0) )
& ( p(s(bool,T0))
| s(bool,t) != s(bool,T0) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f3704,plain,
( ! [T0] :
( p(s(bool,T0))
| s(bool,T0) = s(bool,f0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,T0) != s(bool,f0) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,f0) = s(bool,T0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,f0) != s(bool,T0) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,T0) = s(bool,t) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,T0) != s(bool,t) )
& ! [T0] :
( ~ p(s(bool,T0))
| s(bool,t) = s(bool,T0) )
& ! [T0] :
( p(s(bool,T0))
| s(bool,t) != s(bool,T0) ) ),
inference(miniscoping,[status(thm)],[f3703]) ).
fof(f3708,plain,
! [X0] :
( s(bool,X0) = s(bool,t)
| ~ p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3704]) ).
fof(f3709,plain,
! [X0] :
( s(bool,f0) != s(bool,X0)
| ~ p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3704]) ).
fof(f3713,plain,
~ p(s(bool,f0)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f3714,plain,
( ( ~ p(s(bool,t))
| ~ p(s(bool,f0)) )
& ( p(s(bool,t))
| p(s(bool,f0)) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f3716,plain,
( ~ p(s(bool,t))
| ~ p(s(bool,f0)) ),
inference(cnf_transformation,[status(thm)],[f3714]) ).
fof(f3796,plain,
! [A,P0,A5] :
( ( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) )
& ( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f3797,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(miniscoping,[status(thm)],[f3796]) ).
fof(f3798,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ( p(s(bool,i(s(fun(A,bool),P0),s(A,sK15_skl(A5,P0,A)))))
& s(A,sK15_skl(A5,P0,A)) = s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X,sK15_skl(A5,P0,A))],[f3797]) ).
fof(f3800,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| s(X0,X1) = s(X0,sK15_skl(X1,X2,X0)) ),
inference(cnf_transformation,[status(thm)],[f3798]) ).
fof(f3802,plain,
! [A,P0,A5] :
( ! [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) )
<=> p(s(bool,i(s(fun(A,bool),P0),s(A,A5)))) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f3803,plain,
! [A,P0,A5] :
( ( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) )
& ( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) ) ),
inference(NNF_transformation,[status(thm)],[f3802]) ).
fof(f3804,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ? [X] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
& s(A,X) = s(A,A5) ) ) ),
inference(miniscoping,[status(thm)],[f3803]) ).
fof(f3805,plain,
( ! [A,P0,A5] :
( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ! [X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| s(A,X) != s(A,A5) ) )
& ! [A,P0,A5] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,A5))))
| ( ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK16_skl(A5,P0,A)))))
& s(A,sK16_skl(A5,P0,A)) = s(A,A5) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(X,sK16_skl(A5,P0,A))],[f3804]) ).
fof(f3807,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK16_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3805]) ).
fof(f3809,plain,
! [Q1020,P0,A5] :
( ! [X] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
| s(Q1020,A5) != s(Q1020,X) )
<=> p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5)))) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f3810,plain,
! [Q1020,P0,A5] :
( ( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ! [X] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
| s(Q1020,A5) != s(Q1020,X) ) )
& ( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ? [X] :
( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
& s(Q1020,A5) = s(Q1020,X) ) ) ),
inference(NNF_transformation,[status(thm)],[f3809]) ).
fof(f3811,plain,
( ! [Q1020,P0,A5] :
( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ! [X] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
| s(Q1020,A5) != s(Q1020,X) ) )
& ! [Q1020,P0,A5] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ? [X] :
( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
& s(Q1020,A5) = s(Q1020,X) ) ) ),
inference(miniscoping,[status(thm)],[f3810]) ).
fof(f3812,plain,
( ! [Q1020,P0,A5] :
( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ! [X] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,X))))
| s(Q1020,A5) != s(Q1020,X) ) )
& ! [Q1020,P0,A5] :
( p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,A5))))
| ( ~ p(s(bool,i(s(fun(Q1020,bool),P0),s(Q1020,sK17_skl(A5,P0,Q1020)))))
& s(Q1020,A5) = s(Q1020,sK17_skl(A5,P0,Q1020)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X,sK17_skl(A5,P0,Q1020))],[f3811]) ).
fof(f3815,plain,
! [X0,X1,X2,X3] :
( s(X0,X2) != s(X0,X3)
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(cnf_transformation,[status(thm)],[f3812]) ).
fof(f3826,plain,
! [A,P0,Q0] :
( ( ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f3827,plain,
( ! [A,P0,Q0] :
( ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
inference(miniscoping,[status(thm)],[f3826]) ).
fof(f3828,plain,
( ! [A,P0,Q0] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK29_skl(Q0,P0,A)))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK28_skl(Q0,P0,A)))))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK27_skl(Q0,P0,A)))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK26_skl(Q0,P0,A))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl,sK29_skl]),skolemize(X,sK26_skl(Q0,P0,A)),skolemize(X,sK27_skl(Q0,P0,A)),skolemize(X,sK28_skl(Q0,P0,A)),skolemize(X,sK29_skl(Q0,P0,A))],[f3827]) ).
fof(f3829,plain,
! [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(X0,bool),X3),s(X0,sK27_skl(X3,X1,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK26_skl(X3,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(cnf_transformation,[status(thm)],[f3828]) ).
fof(f3830,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK26_skl(X1,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK27_skl(X1,X2,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3828]) ).
fof(f3831,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK29_skl(X2,X1,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK28_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3828]) ).
fof(f3833,plain,
! [A,P0,Q0] :
( ( ? [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ( ! [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
inference(NNF_transformation,[status(thm)],[f59]) ).
fof(f3834,plain,
( ! [A,P0,Q0] :
( ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ),
inference(miniscoping,[status(thm)],[f3833]) ).
fof(f3835,plain,
( ! [A,P0,Q0] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK33_skl(Q0,P0,A)))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK32_skl(Q0,P0,A)))))
| ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ! [A,P0,Q0] :
( ( ! [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,sK31_skl(Q0,P0,A)))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK30_skl(Q0,P0,A))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(X,sK30_skl(Q0,P0,A)),skolemize(X,sK31_skl(Q0,P0,A)),skolemize(X,sK32_skl(Q0,P0,A)),skolemize(X,sK33_skl(Q0,P0,A))],[f3834]) ).
fof(f3839,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK32_skl(X1,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK33_skl(X1,X2,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3835]) ).
fof(f3854,plain,
! [A,P0,Q0] :
( ( ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) )
& ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f3855,plain,
( ! [A,P0,Q0] :
( ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(miniscoping,[status(thm)],[f3854]) ).
fof(f3856,plain,
( ! [A,P0,Q0] :
( ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,i(s(fun(A,bool),Q0),s(A,sK41_skl(Q0,P0,A)))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK40_skl(Q0,P0,A))))) )
& ! [A,P0,Q0] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,sK39_skl(Q0,P0,A)))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK38_skl(Q0,P0,A)))))
| ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl,sK41_skl]),skolemize(X,sK38_skl(Q0,P0,A)),skolemize(X,sK39_skl(Q0,P0,A)),skolemize(X,sK40_skl(Q0,P0,A)),skolemize(X,sK41_skl(Q0,P0,A))],[f3855]) ).
fof(f3858,plain,
! [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X3))))
| p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK39_skl(X2,X1,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3856]) ).
fof(f3861,plain,
! [A,P0,Q0] :
( ( ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ( ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f63]) ).
fof(f3862,plain,
( ! [A,P0,Q0] :
( ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(miniscoping,[status(thm)],[f3861]) ).
fof(f3863,plain,
( ! [A,P0,Q0] :
( ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,i(s(fun(A,bool),Q0),s(A,sK45_skl(Q0,P0,A)))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK44_skl(Q0,P0,A))))) )
& ! [A,P0,Q0] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,sK43_skl(Q0,P0,A)))))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK42_skl(Q0,P0,A)))))
| ( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42_skl,sK43_skl,sK44_skl,sK45_skl]),skolemize(X,sK42_skl(Q0,P0,A)),skolemize(X,sK43_skl(Q0,P0,A)),skolemize(X,sK44_skl(Q0,P0,A)),skolemize(X,sK45_skl(Q0,P0,A))],[f3862]) ).
fof(f3867,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK45_skl(X2,X1,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X3))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK44_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f3863]) ).
fof(f3868,plain,
! [A,P0,Q0] :
( ( ! [X] :
( ~ p(s(bool,Q0))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ( ? [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f64]) ).
fof(f3869,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| ? [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(miniscoping,[status(thm)],[f3868]) ).
fof(f3870,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK47_skl(Q0,P0,A))))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK46_skl(Q0,P0,A)))))
| ( ~ p(s(bool,Q0))
& ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46_skl,sK47_skl]),skolemize(X,sK46_skl(Q0,P0,A)),skolemize(X,sK47_skl(Q0,P0,A))],[f3869]) ).
fof(f3873,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X1,bool),X2),s(X1,sK47_skl(X0,X2,X1)))))
| ~ p(s(bool,i(s(fun(X1,bool),X2),s(X1,X3))))
| p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3870]) ).
fof(f3909,plain,
! [A,P0,Q0] :
( ( ! [X] :
( ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) )
| ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) )
& ( ? [X] :
( p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
| ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) ) ),
inference(NNF_transformation,[status(thm)],[f70]) ).
fof(f3910,plain,
( ! [A,P0,Q0] :
( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0))
| ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) ) )
& ! [A,P0,Q0] :
( ( ? [X] : p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
& p(s(bool,P0)) )
| ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) ) ),
inference(miniscoping,[status(thm)],[f3909]) ).
fof(f3911,plain,
( ! [A,P0,Q0] :
( ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0))
| ( p(s(bool,i(s(fun(A,bool),Q0),s(A,sK57_skl(Q0,P0,A)))))
& p(s(bool,P0)) ) )
& ! [A,P0,Q0] :
( ( p(s(bool,i(s(fun(A,bool),Q0),s(A,sK56_skl(Q0,P0,A)))))
& p(s(bool,P0)) )
| ! [X] : ~ p(s(bool,i(s(fun(A,bool),Q0),s(A,X))))
| ~ p(s(bool,P0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl,sK57_skl]),skolemize(X,sK56_skl(Q0,P0,A)),skolemize(X,sK57_skl(Q0,P0,A))],[f3910]) ).
fof(f3915,plain,
! [X0,X1,X2,X3] :
( ~ p(s(bool,i(s(fun(X1,bool),X2),s(X1,X3))))
| p(s(bool,i(s(fun(X1,bool),X2),s(X1,sK57_skl(X2,X0,X1)))))
| ~ p(s(bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3911]) ).
fof(f4047,plain,
! [A,P0,X] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))))))
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f4048,plain,
! [A,P0] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))))))
| ! [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ),
inference(miniscoping,[status(thm)],[f4047]) ).
fof(f4049,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,i(s(fun(fun(X0,bool),X0),h_),s(fun(X0,bool),X1)))))) ),
inference(cnf_transformation,[status(thm)],[f4048]) ).
fof(f4056,plain,
! [A,P0,X] :
( s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))) = s(A,X)
| ? [Y] :
( p(s(bool,i(s(fun(A,bool),P0),s(A,Y))))
<~> s(A,Y) = s(A,X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f4057,plain,
! [A,P0,X] :
( s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))) = s(A,X)
| ? [Y] :
( ( s(A,Y) != s(A,X)
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,Y)))) )
& ( s(A,Y) = s(A,X)
| p(s(bool,i(s(fun(A,bool),P0),s(A,Y)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f4056]) ).
fof(f4058,plain,
! [A,P0,X] :
( s(A,i(s(fun(fun(A,bool),A),h_),s(fun(A,bool),P0))) = s(A,X)
| ( ( s(A,sK81_skl(X,P0,A)) != s(A,X)
| ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK81_skl(X,P0,A))))) )
& ( s(A,sK81_skl(X,P0,A)) = s(A,X)
| p(s(bool,i(s(fun(A,bool),P0),s(A,sK81_skl(X,P0,A))))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81_skl]),skolemize(Y,sK81_skl(X,P0,A))],[f4057]) ).
fof(f4060,plain,
! [X0,X1,X2] :
( s(X0,X2) = s(X0,i(s(fun(fun(X0,bool),X0),h_),s(fun(X0,bool),X1)))
| s(X0,sK81_skl(X2,X1,X0)) != s(X0,X2)
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK81_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f4058]) ).
fof(f4140,plain,
! [A,P0,Q0] :
( ( ? [X] :
( ~ p(s(bool,Q0))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ( ! [X] :
( p(s(bool,Q0))
| p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| ( ~ p(s(bool,Q0))
& ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f110]) ).
fof(f4141,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
| p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ~ p(s(bool,Q0))
& ? [X] : ~ p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) ) ) ),
inference(miniscoping,[status(thm)],[f4140]) ).
fof(f4142,plain,
( ! [A,P0,Q0] :
( ( ~ p(s(bool,Q0))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK97_skl(Q0,P0,A))))) )
| p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X)))) )
& ! [A,P0,Q0] :
( p(s(bool,Q0))
| ! [X] : p(s(bool,i(s(fun(A,bool),P0),s(A,X))))
| ( ~ p(s(bool,Q0))
& ~ p(s(bool,i(s(fun(A,bool),P0),s(A,sK96_skl(Q0,P0,A))))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96_skl,sK97_skl]),skolemize(X,sK96_skl(Q0,P0,A)),skolemize(X,sK97_skl(Q0,P0,A))],[f4141]) ).
fof(f4145,plain,
! [X0,X1,X2,X3] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X3))))
| p(s(bool,X2))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK97_skl(X2,X1,X0))))) ),
inference(cnf_transformation,[status(thm)],[f4142]) ).
fof(f4276,plain,
! [X0,X1,X2] : s(fun(X0,n10),X1) = s(fun(X0,n10),X2),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f4508,plain,
( ( ~ p(s(bool,t))
| s(num,u_0) = s(num,u_0) )
& ( p(s(bool,t))
| s(num,u_0) != s(num,u_0) ) ),
inference(NNF_transformation,[status(thm)],[f199]) ).
fof(f4510,plain,
( ~ p(s(bool,t))
| s(num,u_0) = s(num,u_0) ),
inference(cnf_transformation,[status(thm)],[f4508]) ).
fof(f4511,plain,
! [X0] : s(num,X0) = s(num,i(s(fun(num,num),numeral),s(num,X0))),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f5503,plain,
! [N0] :
( ( ~ p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0) )
& ( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,N0))) != s(num,u_0) ) ),
inference(NNF_transformation,[status(thm)],[f568]) ).
fof(f5504,plain,
( ( ~ p(s(bool,f0))
| ! [N0] : s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0) )
& ( p(s(bool,f0))
| ! [N0] : s(num,i(s(fun(num,num),bit1),s(num,N0))) != s(num,u_0) ) ),
inference(miniscoping,[status(thm)],[f5503]) ).
fof(f5505,plain,
! [X0] :
( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit1),s(num,X0))) != s(num,u_0) ),
inference(cnf_transformation,[status(thm)],[f5504]) ).
fof(f5519,plain,
! [M0,N0] :
( ( ~ p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0))) )
& ( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,M0))) != s(num,i(s(fun(num,num),bit1),s(num,N0))) ) ),
inference(NNF_transformation,[status(thm)],[f572]) ).
fof(f5520,plain,
( ( ~ p(s(bool,f0))
| ! [M0,N0] : s(num,i(s(fun(num,num),bit0),s(num,M0))) = s(num,i(s(fun(num,num),bit1),s(num,N0))) )
& ( p(s(bool,f0))
| ! [M0,N0] : s(num,i(s(fun(num,num),bit0),s(num,M0))) != s(num,i(s(fun(num,num),bit1),s(num,N0))) ) ),
inference(miniscoping,[status(thm)],[f5519]) ).
fof(f5521,plain,
! [X0,X1] :
( p(s(bool,f0))
| s(num,i(s(fun(num,num),bit0),s(num,X0))) != s(num,i(s(fun(num,num),bit1),s(num,X1))) ),
inference(cnf_transformation,[status(thm)],[f5520]) ).
fof(f8087,plain,
! [X0,X1] : s(bool,i(s(fun(X0,bool),empty),s(X0,X1))) = s(bool,f0),
inference(cnf_transformation,[status(thm)],[f1659]) ).
fof(f8093,plain,
! [X0,X1] : s(bool,t) = s(bool,i(s(fun(X0,bool),univ),s(X0,X1))),
inference(cnf_transformation,[status(thm)],[f1661]) ).
fof(f8357,plain,
! [X0,X1] : p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(fun(X0,bool),fun(fun(X0,bool),bool)),subset),s(fun(X0,bool),X1))),s(fun(X0,bool),univ)))),
inference(cnf_transformation,[status(thm)],[f1710]) ).
fof(f9571,plain,
! [A,B] :
( p(s(bool,i(s(fun(fun(fun(A,B),bool),bool),finite),s(fun(fun(A,B),bool),univ))))
| ~ p(s(bool,i(s(fun(fun(B,bool),bool),finite),s(fun(B,bool),univ))))
| ~ p(s(bool,i(s(fun(fun(A,bool),bool),finite),s(fun(A,bool),univ)))) ),
inference(pre_NNF_transformation,[status(thm)],[f1983]) ).
fof(f9572,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(fun(fun(X1,bool),bool),finite),s(fun(X1,bool),univ))))
| p(s(bool,i(s(fun(fun(fun(X1,X0),bool),bool),finite),s(fun(fun(X1,X0),bool),univ))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),univ)))) ),
inference(cnf_transformation,[status(thm)],[f9571]) ).
fof(f9575,plain,
p(s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ)))),
inference(cnf_transformation,[status(thm)],[f1986]) ).
fof(f9651,plain,
~ p(s(bool,i(s(fun(fun(num,bool),bool),finite),s(fun(num,bool),univ)))),
inference(cnf_transformation,[status(thm)],[f2001]) ).
fof(f9819,plain,
! [Q58981,P0] :
( ! [X] :
( p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) )
<=> p(s(bool,t)) ),
inference(pre_NNF_transformation,[status(thm)],[f2041]) ).
fof(f9820,plain,
! [Q58981,P0] :
( ( ~ p(s(bool,t))
| ! [X] :
( p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ? [X] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f9819]) ).
fof(f9821,plain,
( ( ~ p(s(bool,t))
| ! [Q58981,X] :
( ! [P0] : p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ! [Q58981,P0] :
? [X] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(miniscoping,[status(thm)],[f9820]) ).
fof(f9822,plain,
( ( ~ p(s(bool,t))
| ! [Q58981,X] :
( ! [P0] : p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X))))
| ~ p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,X))),s(fun(Q58981,bool),empty)))) ) )
& ( p(s(bool,t))
| ! [Q58981,P0] :
( ~ p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,sK1408_skl(P0,Q58981)))))
& p(s(bool,i(s(fun(fun(Q58981,bool),bool),i(s(fun(Q58981,fun(fun(Q58981,bool),bool)),in),s(Q58981,sK1408_skl(P0,Q58981)))),s(fun(Q58981,bool),empty)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1408_skl]),skolemize(X,sK1408_skl(P0,Q58981))],[f9821]) ).
fof(f9825,plain,
! [X0,X1,X2] :
( ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ),
inference(cnf_transformation,[status(thm)],[f9822]) ).
fof(f9835,plain,
! [Q59041,P0] :
( ( ~ p(s(bool,f0))
| ? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [X] :
( ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(NNF_transformation,[status(thm)],[f2043]) ).
fof(f9836,plain,
( ( ~ p(s(bool,f0))
| ! [Q59041,P0] :
? [X] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [Q59041,X] :
( ! [P0] : ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(miniscoping,[status(thm)],[f9835]) ).
fof(f9837,plain,
( ( ~ p(s(bool,f0))
| ! [Q59041,P0] :
( p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,sK1410_skl(P0,Q59041)))))
& p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,sK1410_skl(P0,Q59041)))),s(fun(Q59041,bool),empty)))) ) )
& ( p(s(bool,f0))
| ! [Q59041,X] :
( ! [P0] : ~ p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X))))
| ~ p(s(bool,i(s(fun(fun(Q59041,bool),bool),i(s(fun(Q59041,fun(fun(Q59041,bool),bool)),in),s(Q59041,X))),s(fun(Q59041,bool),empty)))) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1410_skl]),skolemize(X,sK1410_skl(P0,Q59041))],[f9836]) ).
fof(f9838,plain,
! [X0,X1,X2] :
( p(s(bool,f0))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ),
inference(cnf_transformation,[status(thm)],[f9837]) ).
fof(f11435,plain,
! [X0,X1] : s(num,i(s(fun(fun(X0,bool),num),dimindex),s(fun(X0,bool),X1))) != s(num,i(s(fun(num,num),numeral),s(num,u_0))),
inference(cnf_transformation,[status(thm)],[f2363]) ).
fof(f11436,plain,
! [X0,X1] : p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,i(s(fun(fun(X0,bool),num),dimindex),s(fun(X0,bool),X1)))))),
inference(cnf_transformation,[status(thm)],[f2364]) ).
fof(f11469,plain,
! [B,A,R0] :
( ( s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) != s(fun(finite_image(B),A),R0)
| p(s(bool,t)) )
& ( s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0)
| ~ p(s(bool,t)) ) ),
inference(NNF_transformation,[status(thm)],[f2377]) ).
fof(f11470,plain,
( ( ! [B,A,R0] : s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) != s(fun(finite_image(B),A),R0)
| p(s(bool,t)) )
& ( ! [B,A,R0] : s(fun(finite_image(B),A),i(s(fun(cart(A,B),fun(finite_image(B),A)),destu_cart),s(cart(A,B),i(s(fun(fun(finite_image(B),A),cart(A,B)),mku_cart),s(fun(finite_image(B),A),R0))))) = s(fun(finite_image(B),A),R0)
| ~ p(s(bool,t)) ) ),
inference(miniscoping,[status(thm)],[f11469]) ).
fof(f11471,plain,
! [X0,X1,X2] :
( s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) = s(fun(finite_image(X0),X1),X2)
| ~ p(s(bool,t)) ),
inference(cnf_transformation,[status(thm)],[f11470]) ).
fof(f11561,plain,
s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))) = s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))),
inference(cnf_transformation,[status(thm)],[f2406]) ).
fof(f11579,plain,
! [A,N] :
( p(s(bool,i(s(fun(fun(cart(A,N),bool),bool),finite),s(fun(cart(A,N),bool),univ))))
| ~ p(s(bool,i(s(fun(fun(A,bool),bool),finite),s(fun(A,bool),univ)))) ),
inference(pre_NNF_transformation,[status(thm)],[f2413]) ).
fof(f11580,plain,
! [A] :
( ! [N] : p(s(bool,i(s(fun(fun(cart(A,N),bool),bool),finite),s(fun(cart(A,N),bool),univ))))
| ~ p(s(bool,i(s(fun(fun(A,bool),bool),finite),s(fun(A,bool),univ)))) ),
inference(miniscoping,[status(thm)],[f11579]) ).
fof(f11581,plain,
! [X0,X1] :
( p(s(bool,i(s(fun(fun(cart(X0,X1),bool),bool),finite),s(fun(cart(X0,X1),bool),univ))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),univ)))) ),
inference(cnf_transformation,[status(thm)],[f11580]) ).
fof(f14680,plain,
! [X0] : s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),univ))) = s(fun(cart(real,X0),bool),univ),
inference(cnf_transformation,[status(thm)],[f3331]) ).
fof(f15024,plain,
! [X0] : s(num,i(s(fun(fun(X0,bool),num),dimindex),s(fun(X0,bool),univ))) = s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),univ))),
inference(cnf_transformation,[status(thm)],[f3398]) ).
fof(f15027,plain,
! [X0,X1] : p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),X1))))),s(num,i(s(fun(fun(X0,bool),num),dimindex),s(fun(X0,bool),univ)))))),
inference(cnf_transformation,[status(thm)],[f3400]) ).
fof(f15043,plain,
! [X0,X1] : s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X1))))) = s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),X1))),
inference(cnf_transformation,[status(thm)],[f3407]) ).
fof(f15044,plain,
! [X0,X1] : s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),i(s(fun(cart(real,X0),fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool))),insert),s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X0),bool),X1))))) = s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),X1))),
inference(cnf_transformation,[status(thm)],[f3408]) ).
fof(f15415,plain,
! [N,S0,T0] :
( s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),T0)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),T0))))),s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))))))
| ~ p(s(bool,i(s(fun(fun(cart(real,N),bool),bool),i(s(fun(fun(cart(real,N),bool),fun(fun(cart(real,N),bool),bool)),subset),s(fun(cart(real,N),bool),S0))),s(fun(cart(real,N),bool),T0)))) ),
inference(pre_NNF_transformation,[status(thm)],[f3492]) ).
fof(f15416,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),X2))))),s(num,i(s(fun(fun(cart(real,X0),bool),num),dim),s(fun(cart(real,X0),bool),X1))))))
| s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X2))) = s(fun(cart(real,X0),bool),i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),X1)))
| ~ p(s(bool,i(s(fun(fun(cart(real,X0),bool),bool),i(s(fun(fun(cart(real,X0),bool),fun(fun(cart(real,X0),bool),bool)),subset),s(fun(cart(real,X0),bool),X1))),s(fun(cart(real,X0),bool),X2)))) ),
inference(cnf_transformation,[status(thm)],[f15415]) ).
fof(f15417,plain,
? [N,S0] :
( s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))) = s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ)))
<~> s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),univ) ),
inference(pre_NNF_transformation,[status(thm)],[f3494]) ).
fof(f15418,plain,
? [N,S0] :
( ( s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) != s(fun(cart(real,N),bool),univ)
| s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))) != s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))) )
& ( s(fun(cart(real,N),bool),i(s(fun(fun(cart(real,N),bool),fun(cart(real,N),bool)),span),s(fun(cart(real,N),bool),S0))) = s(fun(cart(real,N),bool),univ)
| s(num,i(s(fun(fun(cart(real,N),bool),num),dim),s(fun(cart(real,N),bool),S0))) = s(num,i(s(fun(fun(N,bool),num),dimindex),s(fun(N,bool),univ))) ) ),
inference(NNF_transformation,[status(thm)],[f15417]) ).
fof(f15419,plain,
( ( s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(fun(cart(real,sK3697_skl),bool),univ)
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) )
& ( s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),univ)
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3697_skl,sK3698_skl]),skolemize(N,sK3697_skl),skolemize(S0,sK3698_skl)],[f15418]) ).
fof(f15420,plain,
( s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),univ)
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(cnf_transformation,[status(thm)],[f15419]) ).
fof(f15421,plain,
( s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(fun(cart(real,sK3697_skl),bool),univ)
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(cnf_transformation,[status(thm)],[f15419]) ).
fof(f17987,definition,
! [X2] :
( sQ1_spl
<=> ( p(s(bool,X2))
| ~ p(s(bool,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f17991,definition,
( sQ2_spl
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f17994,definition,
! [X0] :
( sQ3_spl
<=> p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f17995,plain,
! [X0] :
( ~ sQ3_spl
| p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f17994]) ).
fof(f17998,definition,
( sQ4_spl
<=> p(s(bool,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f18001,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f3537,f17991,f17998]) ).
fof(f18002,plain,
( sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3541,f17987,f17991]) ).
fof(f18003,definition,
! [X0] :
( sQ5_spl
<=> ~ p(s(bool,X0)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f18004,plain,
! [X0] :
( ~ sQ5_spl
| ~ p(s(bool,X0)) ),
inference(component_clause,[status(thm)],[f18003]) ).
fof(f18022,definition,
! [X0,X1] :
( sQ9_spl
<=> s(X0,X1) != s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f18023,plain,
! [X0,X1] :
( ~ sQ9_spl
| s(X0,X1) != s(X0,X1) ),
inference(component_clause,[status(thm)],[f18022]) ).
fof(f18025,definition,
( sQ10_spl
<=> p(s(bool,t)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f18028,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f3557,f18022,f18025]) ).
fof(f18029,definition,
! [X0,X1] :
( sQ11_spl
<=> s(X0,X1) = s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f18032,plain,
( ~ sQ10_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f3558,f18029,f18025]) ).
fof(f18124,plain,
( ~ sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3716,f17991,f18025]) ).
fof(f18325,definition,
( sQ39_spl
<=> s(num,u_0) = s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f18329,plain,
( ~ sQ10_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f4510,f18325,f18025]) ).
fof(f18503,definition,
! [X0] :
( sQ86_spl
<=> s(num,i(s(fun(num,num),bit1),s(num,X0))) != s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f18506,plain,
( sQ2_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f5505,f18503,f17991]) ).
fof(f18513,definition,
! [X0,X1] :
( sQ88_spl
<=> s(num,i(s(fun(num,num),bit0),s(num,X0))) != s(num,i(s(fun(num,num),bit1),s(num,X1))) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f18516,plain,
( sQ2_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f5521,f18513,f17991]) ).
fof(f18675,definition,
! [X0,X1] :
( sQ131_spl
<=> ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK1408_skl(X1,X0))))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f18676,plain,
! [X0,X1] :
( ~ sQ131_spl
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK1408_skl(X1,X0))))) ),
inference(component_clause,[status(thm)],[f18675]) ).
fof(f18679,definition,
! [X0,X1,X2] :
( sQ132_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f18682,plain,
( ~ sQ10_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f9825,f18679,f18025]) ).
fof(f18683,definition,
! [X0,X1,X2] :
( sQ133_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))
| ~ p(s(bool,i(s(fun(fun(X0,bool),bool),i(s(fun(X0,fun(fun(X0,bool),bool)),in),s(X0,X1))),s(fun(X0,bool),empty)))) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f18686,plain,
( sQ2_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f9838,f18683,f17991]) ).
fof(f18714,definition,
! [X0,X1,X2] :
( sQ141_spl
<=> s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) = s(fun(finite_image(X0),X1),X2) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f18717,plain,
( sQ141_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f11471,f18025,f18714]) ).
fof(f18718,definition,
! [X0,X1,X2] :
( sQ142_spl
<=> s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) != s(fun(finite_image(X0),X1),X2) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f18719,plain,
! [X0,X1,X2] :
( ~ sQ142_spl
| s(fun(finite_image(X0),X1),X2) != s(fun(finite_image(X0),X1),i(s(fun(cart(X1,X0),fun(finite_image(X0),X1)),destu_cart),s(cart(X1,X0),i(s(fun(fun(finite_image(X0),X1),cart(X1,X0)),mku_cart),s(fun(finite_image(X0),X1),X2))))) ),
inference(component_clause,[status(thm)],[f18718]) ).
fof(f18903,definition,
( sQ192_spl
<=> s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f18904,plain,
( ~ sQ192_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(component_clause,[status(thm)],[f18903]) ).
fof(f18905,plain,
( sQ192_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(component_clause,[status(thm)],[f18903]) ).
fof(f18906,definition,
( sQ193_spl
<=> s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),univ) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f18907,plain,
( ~ sQ193_spl
| s(fun(cart(real,sK3697_skl),bool),univ) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
inference(component_clause,[status(thm)],[f18906]) ).
fof(f18909,plain,
( sQ193_spl
| sQ192_spl ),
inference(split_clause,[status(thm)],[f15420,f18903,f18906]) ).
fof(f18910,plain,
( ~ sQ193_spl
| ~ sQ192_spl ),
inference(split_clause,[status(thm)],[f15421,f18903,f18906]) ).
fof(f18945,plain,
( ~ sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18023]) ).
fof(f18946,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f18945]) ).
fof(f19095,definition,
! [X2,X3] :
( sQ208_spl
<=> s(num,i(s(fun(num,num),bit1),s(num,X2))) != s(num,i(s(fun(num,num),bit1),s(num,X3))) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f19096,plain,
! [X0,X1] :
( ~ sQ208_spl
| s(num,i(s(fun(num,num),bit1),s(num,X0))) != s(num,i(s(fun(num,num),bit1),s(num,X1))) ),
inference(component_clause,[status(thm)],[f19095]) ).
fof(f19239,plain,
( ~ sQ208_spl
| $false ),
inference(equality_resolution,[status(thm)],[f19096]) ).
fof(f19240,plain,
~ sQ208_spl,
inference(contradiction_clause,[status(thm)],[f19239]) ).
fof(f19399,plain,
s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ))) = s(bool,t),
inference(resolution,[status(thm)],[f3708,f9575]) ).
fof(f19451,plain,
p(s(bool,t)),
inference(backward_demodulation,[status(thm)],[f19399,f9575]) ).
fof(f19463,plain,
! [X0] :
( ~ p(s(bool,t))
| s(fun(bool,bool),X0) != s(fun(bool,bool),univ)
| p(s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),X0)))) ),
inference(paramodulation,[status(thm)],[f19399,f3815]) ).
fof(f19477,definition,
! [X0] :
( sQ215_spl
<=> ( s(fun(bool,bool),X0) != s(fun(bool,bool),univ)
| p(s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),X0)))) ) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f19480,plain,
( ~ sQ10_spl
| sQ215_spl ),
inference(split_clause,[status(thm)],[f19463,f19477,f18025]) ).
fof(f19623,plain,
( s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ))) != s(bool,f0)
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f19399,f3709]) ).
fof(f19624,definition,
( sQ216_spl
<=> s(bool,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ))) = s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f19627,plain,
( ~ sQ216_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f19623,f18025,f19624]) ).
fof(f19764,plain,
! [X0,X1,X2] :
( ~ sQ142_spl
| s(fun(finite_image(X0),n10),X1) != s(fun(finite_image(X0),n10),i(s(fun(cart(n10,X0),fun(finite_image(X0),n10)),destu_cart),s(cart(n10,X0),i(s(fun(fun(finite_image(X0),n10),cart(n10,X0)),mku_cart),s(fun(finite_image(X0),n10),X2))))) ),
inference(paramodulation,[status(thm)],[f4276,f18719]) ).
fof(f19765,plain,
( ~ sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19764,f4276]) ).
fof(f19766,plain,
~ sQ142_spl,
inference(contradiction_clause,[status(thm)],[f19765]) ).
fof(f19782,definition,
( sQ221_spl
<=> s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),univ))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f19783,plain,
( ~ sQ221_spl
| s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),univ))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
inference(component_clause,[status(thm)],[f19782]) ).
fof(f19789,definition,
( sQ223_spl
<=> s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f19791,plain,
( sQ223_spl
| s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) != s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
inference(component_clause,[status(thm)],[f19789]) ).
fof(f19796,definition,
( sQ225_spl
<=> s(num,i(s(fun(num,num),numeral),s(num,u_0))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f19797,plain,
( ~ sQ225_spl
| s(num,i(s(fun(num,num),numeral),s(num,u_0))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(component_clause,[status(thm)],[f19796]) ).
fof(f19801,plain,
( sQ223_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f19791]) ).
fof(f19802,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f19801]) ).
fof(f19806,plain,
( ~ sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19797,f11435]) ).
fof(f19807,plain,
~ sQ225_spl,
inference(contradiction_clause,[status(thm)],[f19806]) ).
fof(f19808,plain,
( ~ sQ221_spl
| s(fun(cart(real,sK3697_skl),bool),univ) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) ),
inference(forward_demodulation,[status(thm)],[f14680,f19783]) ).
fof(f20160,plain,
( ~ sQ193_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))) = s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),i(s(fun(cart(real,sK3697_skl),fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool))),insert),s(cart(real,sK3697_skl),i(s(fun(num,cart(real,sK3697_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3697_skl),bool),univ))))) ),
inference(paramodulation,[status(thm)],[f18907,f15044]) ).
fof(f20221,plain,
( ~ sQ193_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),i(s(fun(cart(real,sK3697_skl),fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool))),insert),s(cart(real,sK3697_skl),i(s(fun(num,cart(real,sK3697_skl)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,sK3697_skl),bool),univ))))) ),
inference(forward_demodulation,[status(thm)],[f15043,f20160]) ).
fof(f20222,plain,
( ~ sQ193_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),univ))) ),
inference(forward_demodulation,[status(thm)],[f15044,f20221]) ).
fof(f20223,plain,
( ~ sQ193_spl
| s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
inference(forward_demodulation,[status(thm)],[f15024,f20222]) ).
fof(f20224,plain,
( ~ sQ193_spl
| sQ192_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20223,f18905]) ).
fof(f20225,plain,
( ~ sQ193_spl
| sQ192_spl ),
inference(contradiction_clause,[status(thm)],[f20224]) ).
fof(f20244,plain,
! [X0,X1,X2,X3,X4] :
( p(s(bool,X4))
| ~ p(s(bool,i(s(fun(fun(X0,n10),bool),X1),s(fun(X0,n10),X3))))
| p(s(bool,i(s(fun(fun(X0,n10),bool),X1),s(fun(X0,n10),X2)))) ),
inference(paramodulation,[status(thm)],[f4276,f3873]) ).
fof(f20254,definition,
! [X0,X1,X2,X3] :
( sQ237_spl
<=> ( ~ p(s(bool,i(s(fun(fun(X0,n10),bool),X1),s(fun(X0,n10),X3))))
| p(s(bool,i(s(fun(fun(X0,n10),bool),X1),s(fun(X0,n10),X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f20257,plain,
( sQ3_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f20244,f20254,f17994]) ).
fof(f20302,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK57_skl(X1,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ)),X0)))))
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f19399,f3915]) ).
fof(f20304,definition,
! [X0,X1,X2] :
( sQ239_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK57_skl(X1,i(s(fun(fun(bool,bool),bool),finite),s(fun(bool,bool),univ)),X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f20307,plain,
( ~ sQ10_spl
| sQ239_spl ),
inference(split_clause,[status(thm)],[f20302,f20304,f18025]) ).
fof(f20457,definition,
( sQ245_spl
<=> s(fun(bool,bool),univ) = s(fun(bool,bool),univ) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f20459,plain,
( sQ245_spl
| s(fun(bool,bool),univ) != s(fun(bool,bool),univ) ),
inference(component_clause,[status(thm)],[f20457]) ).
fof(f20462,plain,
( sQ245_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f20459]) ).
fof(f20463,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f20462]) ).
fof(f20594,plain,
! [X0] :
( ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),univ))))
| ~ p(s(bool,t))
| p(s(bool,i(s(fun(fun(fun(X0,bool),bool),bool),finite),s(fun(fun(X0,bool),bool),univ)))) ),
inference(paramodulation,[status(thm)],[f19399,f9572]) ).
fof(f20595,definition,
! [X0] :
( sQ253_spl
<=> ( ~ p(s(bool,i(s(fun(fun(X0,bool),bool),finite),s(fun(X0,bool),univ))))
| p(s(bool,i(s(fun(fun(fun(X0,bool),bool),bool),finite),s(fun(fun(X0,bool),bool),univ)))) ) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f20598,plain,
( ~ sQ10_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f20594,f20595,f18025]) ).
fof(f20600,plain,
! [X0] :
( p(s(bool,i(s(fun(fun(cart(bool,X0),bool),bool),finite),s(fun(cart(bool,X0),bool),univ))))
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f19399,f11581]) ).
fof(f20601,definition,
! [X0] :
( sQ254_spl
<=> p(s(bool,i(s(fun(fun(cart(bool,X0),bool),bool),finite),s(fun(cart(bool,X0),bool),univ)))) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f20604,plain,
( sQ254_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f20600,f18025,f20601]) ).
fof(f20629,definition,
( sQ256_spl
<=> p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),univ)))))) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f20631,plain,
( sQ256_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),univ)))))) ),
inference(component_clause,[status(thm)],[f20629]) ).
fof(f20639,definition,
( sQ259_spl
<=> p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))),s(fun(cart(real,sK3697_skl),bool),univ)))) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f20641,plain,
( sQ259_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))),s(fun(cart(real,sK3697_skl),bool),univ)))) ),
inference(component_clause,[status(thm)],[f20639]) ).
fof(f20657,plain,
( sQ259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20641,f8357]) ).
fof(f20658,plain,
sQ259_spl,
inference(contradiction_clause,[status(thm)],[f20657]) ).
fof(f20660,plain,
( sQ256_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))))),s(fun(cart(real,sK3697_skl),bool),univ)))) ),
inference(forward_demodulation,[status(thm)],[f14680,f20631]) ).
fof(f20661,plain,
( sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20660,f8357]) ).
fof(f20662,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f20661]) ).
fof(f20834,definition,
( sQ263_spl
<=> s(bool,u_falsityu_) = s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f20836,plain,
( sQ263_spl
| s(bool,u_falsityu_) != s(bool,f0) ),
inference(component_clause,[status(thm)],[f20834]) ).
fof(f20845,plain,
( sQ263_spl
| s(bool,f0) != s(bool,f0) ),
inference(forward_demodulation,[status(thm)],[f3545,f20836]) ).
fof(f20846,plain,
( sQ263_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f20845]) ).
fof(f20847,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f20846]) ).
fof(f20891,plain,
! [X0,X1,X2] :
( ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK29_skl(X2,univ,X0)))))
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f8093,f3831]) ).
fof(f20892,plain,
! [X0,X1,X2] :
( ~ p(s(bool,t))
| s(X0,X1) != s(X0,X2)
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f8093,f3815]) ).
fof(f20893,plain,
! [X0,X1,X2,X3,X4] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK57_skl(X1,i(s(fun(X3,bool),univ),s(X3,X4)),X0)))))
| ~ p(s(bool,t))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ),
inference(paramodulation,[status(thm)],[f8093,f3915]) ).
fof(f20894,plain,
! [X0,X1] :
( s(bool,i(s(fun(X0,bool),univ),s(X0,X1))) != s(bool,f0)
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f8093,f3709]) ).
fof(f20899,definition,
! [X0,X1] :
( sQ265_spl
<=> s(bool,i(s(fun(X0,bool),univ),s(X0,X1))) != s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f20902,plain,
( sQ265_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f20894,f18025,f20899]) ).
fof(f20904,definition,
! [X0,X1,X2] :
( sQ266_spl
<=> ( s(X0,X1) != s(X0,X2)
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f20907,plain,
( ~ sQ10_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f20892,f20904,f18025]) ).
fof(f20909,definition,
! [X0,X1,X2] :
( sQ267_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK29_skl(X2,univ,X0)))))
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f20912,plain,
( ~ sQ10_spl
| sQ267_spl ),
inference(split_clause,[status(thm)],[f20891,f20909,f18025]) ).
fof(f20913,definition,
! [X0,X1,X2,X3,X4] :
( sQ268_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK57_skl(X1,i(s(fun(X3,bool),univ),s(X3,X4)),X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f20916,plain,
( ~ sQ10_spl
| sQ268_spl ),
inference(split_clause,[status(thm)],[f20893,f20913,f18025]) ).
fof(f20918,definition,
! [X0,X1] :
( sQ269_spl
<=> ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f20919,plain,
! [X0,X1] :
( ~ sQ269_spl
| ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(component_clause,[status(thm)],[f20918]) ).
fof(f21066,plain,
! [X0,X1] : p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),s(num,i(s(fun(fun(X0,bool),num),dimindex),s(fun(X0,bool),X1)))))),
inference(forward_demodulation,[status(thm)],[f11561,f11436]) ).
fof(f21103,definition,
( sQ278_spl
<=> p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0)))))))) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f21105,plain,
( sQ278_spl
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0)))))))) ),
inference(component_clause,[status(thm)],[f21103]) ).
fof(f21106,definition,
( sQ279_spl
<=> p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ)))))) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f21108,plain,
( sQ279_spl
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ)))))) ),
inference(component_clause,[status(thm)],[f21106]) ).
fof(f21119,plain,
( sQ279_spl
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ)))))) ),
inference(forward_demodulation,[status(thm)],[f11561,f21108]) ).
fof(f21120,plain,
( sQ279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21119,f21066]) ).
fof(f21121,plain,
sQ279_spl,
inference(contradiction_clause,[status(thm)],[f21120]) ).
fof(f21126,plain,
( sQ278_spl
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ)))))) ),
inference(forward_demodulation,[status(thm)],[f11561,f21105]) ).
fof(f21127,plain,
( sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21126,f21066]) ).
fof(f21128,plain,
sQ278_spl,
inference(contradiction_clause,[status(thm)],[f21127]) ).
fof(f21154,definition,
! [X0,X1,X2] :
( sQ281_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK44_skl(univ,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition]) ).
fof(f21155,plain,
! [X0,X1,X2] :
( ~ sQ281_spl
| p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK44_skl(univ,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(component_clause,[status(thm)],[f21154]) ).
fof(f21161,plain,
! [X0,X1] :
( ~ sQ281_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK44_skl(univ,X1,X0)))))
| ~ p(s(bool,t)) ),
inference(forward_demodulation,[status(thm)],[f8093,f21155]) ).
fof(f21162,plain,
! [X0,X1] :
( ~ sQ281_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK44_skl(univ,X1,X0))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f21161,f19451]) ).
fof(f21203,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK44_skl(empty,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),empty),s(X0,X1))))
| p(s(bool,f0)) ),
inference(paramodulation,[status(thm)],[f8087,f3867]) ).
fof(f21216,definition,
! [X1,X2] :
( sQ282_spl
<=> ~ p(s(bool,i(s(fun(X1,bool),empty),s(X1,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f21220,definition,
! [X0,X1] :
( sQ283_spl
<=> s(bool,i(s(fun(X0,bool),empty),s(X0,X1))) != s(bool,f0) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f21221,plain,
! [X0,X1] :
( ~ sQ283_spl
| s(bool,i(s(fun(X0,bool),empty),s(X0,X1))) != s(bool,f0) ),
inference(component_clause,[status(thm)],[f21220]) ).
fof(f21230,definition,
! [X0,X1,X2] :
( sQ285_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK44_skl(empty,X2,X0)))))
| ~ p(s(bool,i(s(fun(X0,bool),empty),s(X0,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f21233,plain,
( sQ285_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f21203,f17991,f21230]) ).
fof(f21249,plain,
( ~ sQ283_spl
| s(bool,f0) != s(bool,f0) ),
inference(forward_demodulation,[status(thm)],[f8087,f21221]) ).
fof(f21250,plain,
( ~ sQ283_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21249]) ).
fof(f21251,plain,
~ sQ283_spl,
inference(contradiction_clause,[status(thm)],[f21250]) ).
fof(f21283,plain,
( ~ sQ269_spl
| ~ p(s(bool,t)) ),
inference(forward_demodulation,[status(thm)],[f8093,f20919]) ).
fof(f21284,plain,
( ~ sQ269_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21283,f19451]) ).
fof(f21285,plain,
~ sQ269_spl,
inference(contradiction_clause,[status(thm)],[f21284]) ).
fof(f21403,plain,
( ~ sQ281_spl
| p(s(bool,f0)) ),
inference(paramodulation,[status(thm)],[f8087,f21162]) ).
fof(f21477,plain,
! [X0,X1] :
( ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f8093,f3807]) ).
fof(f21486,definition,
! [X0,X1] :
( sQ288_spl
<=> p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition]) ).
fof(f21489,plain,
( ~ sQ10_spl
| sQ288_spl ),
inference(split_clause,[status(thm)],[f21477,f21486,f18025]) ).
fof(f21510,plain,
! [X0] :
( ~ sQ192_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))),s(fun(cart(real,sK3697_skl),bool),X0))))
| s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),X0)))
| ~ p(s(bool,i(s(fun(num,bool),i(s(fun(num,fun(num,bool)),l_a_),s(num,i(s(fun(fun(cart(real,sK3697_skl),bool),num),dim),s(fun(cart(real,sK3697_skl),bool),X0))))),s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ)))))) ),
inference(paramodulation,[status(thm)],[f18904,f15416]) ).
fof(f21595,plain,
( ~ sQ281_spl
| s(bool,f0) != s(bool,f0) ),
inference(resolution,[status(thm)],[f21403,f3709]) ).
fof(f21596,plain,
( ~ sQ281_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21595]) ).
fof(f21597,plain,
~ sQ281_spl,
inference(contradiction_clause,[status(thm)],[f21596]) ).
fof(f21779,plain,
( ~ sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f9651,f17995]) ).
fof(f21796,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f21779]) ).
fof(f21804,plain,
! [X0] :
( ~ sQ131_spl
| ~ p(s(bool,i(s(fun(cart(real,X0),bool),univ),s(cart(real,X0),sK1408_skl(i(s(fun(fun(cart(real,X0),bool),fun(cart(real,X0),bool)),span),s(fun(cart(real,X0),bool),univ)),cart(real,X0)))))) ),
inference(paramodulation,[status(thm)],[f14680,f18676]) ).
fof(f21808,plain,
( ~ sQ131_spl
| ~ p(s(bool,t)) ),
inference(forward_demodulation,[status(thm)],[f8093,f21804]) ).
fof(f21832,plain,
! [X0,X1] :
( s(X0,X1) != s(X0,sK81_skl(X1,univ,X0))
| ~ p(s(bool,t))
| s(X0,X1) = s(X0,i(s(fun(fun(X0,bool),X0),h_),s(fun(X0,bool),univ))) ),
inference(paramodulation,[status(thm)],[f8093,f4060]) ).
fof(f21840,definition,
! [X0,X1] :
( sQ290_spl
<=> ( s(X0,X1) != s(X0,sK81_skl(X1,univ,X0))
| s(X0,X1) = s(X0,i(s(fun(fun(X0,bool),X0),h_),s(fun(X0,bool),univ))) ) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f21843,plain,
( ~ sQ10_spl
| sQ290_spl ),
inference(split_clause,[status(thm)],[f21832,f21840,f18025]) ).
fof(f21879,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK33_skl(X1,univ,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f8093,f3839]) ).
fof(f21886,definition,
! [X0,X1,X2] :
( sQ292_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK33_skl(X1,univ,X0)))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f21889,plain,
( sQ292_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f21879,f18025,f21886]) ).
fof(f22074,plain,
( ~ sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21808,f19451]) ).
fof(f22075,plain,
~ sQ131_spl,
inference(contradiction_clause,[status(thm)],[f22074]) ).
fof(f22123,plain,
! [X0,X1] :
( p(s(bool,f0))
| ~ p(s(bool,i(s(fun(X0,bool),empty),s(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f8087,f4049]) ).
fof(f22153,plain,
( sQ2_spl
| sQ282_spl ),
inference(split_clause,[status(thm)],[f22123,f21216,f17991]) ).
fof(f22162,plain,
! [X0,X1,X2] :
( ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK27_skl(X1,univ,X0))))) ),
inference(paramodulation,[status(thm)],[f8093,f3830]) ).
fof(f22169,definition,
! [X0,X1,X2] :
( sQ299_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK27_skl(X1,univ,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f22172,plain,
( ~ sQ10_spl
| sQ299_spl ),
inference(split_clause,[status(thm)],[f22162,f22169,f18025]) ).
fof(f22711,plain,
( s(fun(bool,bool),sK15_skl(univ,finite,fun(bool,bool))) = s(fun(bool,bool),univ)
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f19399,f3800]) ).
fof(f22713,plain,
! [X0,X1] :
( s(X0,sK15_skl(X1,univ,X0)) = s(X0,X1)
| ~ p(s(bool,t)) ),
inference(paramodulation,[status(thm)],[f8093,f3800]) ).
fof(f22742,definition,
! [X0,X1] :
( sQ304_spl
<=> s(X0,sK15_skl(X1,univ,X0)) = s(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f22745,plain,
( sQ304_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f22713,f18025,f22742]) ).
fof(f22746,definition,
( sQ305_spl
<=> s(fun(bool,bool),sK15_skl(univ,finite,fun(bool,bool))) = s(fun(bool,bool),univ) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f22749,plain,
( sQ305_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f22711,f18025,f22746]) ).
fof(f23087,plain,
( ~ sQ5_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19451,f18004]) ).
fof(f23108,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f23087]) ).
fof(f23288,plain,
! [X0,X1,X2] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| p(s(bool,f0))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK97_skl(u_falsityu_,X1,X0))))) ),
inference(paramodulation,[status(thm)],[f3545,f4145]) ).
fof(f23290,plain,
! [X0,X1,X2,X3,X4] :
( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X4))))
| p(s(bool,f0))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK97_skl(i(s(fun(X2,bool),empty),s(X2,X3)),X1,X0))))) ),
inference(paramodulation,[status(thm)],[f8087,f4145]) ).
fof(f23309,definition,
! [X0,X1,X2,X3,X4] :
( sQ312_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X4))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK97_skl(i(s(fun(X2,bool),empty),s(X2,X3)),X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f23312,plain,
( sQ2_spl
| sQ312_spl ),
inference(split_clause,[status(thm)],[f23290,f23309,f17991]) ).
fof(f23313,definition,
! [X0,X1,X2] :
( sQ313_spl
<=> ( p(s(bool,i(s(fun(X0,bool),X1),s(X0,X2))))
| ~ p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK97_skl(u_falsityu_,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f23316,plain,
( sQ2_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f23288,f23313,f17991]) ).
fof(f23323,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),empty),s(X0,X2))))
| p(s(bool,f0))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(empty,X1,X0))))) ),
inference(paramodulation,[status(thm)],[f8087,f3858]) ).
fof(f23333,definition,
! [X0,X1,X2] :
( sQ314_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X2))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(univ,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f23334,plain,
! [X0,X1,X2] :
( ~ sQ314_spl
| ~ p(s(bool,i(s(fun(X0,bool),univ),s(X0,X2))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(univ,X1,X0))))) ),
inference(component_clause,[status(thm)],[f23333]) ).
fof(f23340,definition,
! [X0,X1,X2] :
( sQ315_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),empty),s(X0,X2))))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(empty,X1,X0))))) ) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f23343,plain,
( sQ2_spl
| sQ315_spl ),
inference(split_clause,[status(thm)],[f23323,f23340,f17991]) ).
fof(f23348,plain,
! [X0,X1] :
( ~ sQ314_spl
| ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(univ,X1,X0))))) ),
inference(forward_demodulation,[status(thm)],[f8093,f23334]) ).
fof(f23349,plain,
! [X0,X1] :
( ~ sQ314_spl
| p(s(bool,i(s(fun(X0,bool),X1),s(X0,sK38_skl(univ,X1,X0))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f23348,f19451]) ).
fof(f23459,definition,
( sQ316_spl
<=> s(num,u_0) = s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f23460,plain,
( ~ sQ316_spl
| s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) = s(num,u_0) ),
inference(component_clause,[status(thm)],[f23459]) ).
fof(f23694,definition,
! [X3] :
( sQ319_spl
<=> s(num,X3) != s(num,u_0) ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f23695,plain,
! [X0] :
( ~ sQ319_spl
| s(num,u_0) != s(num,X0) ),
inference(component_clause,[status(thm)],[f23694]) ).
fof(f23908,plain,
( ~ sQ319_spl
| $false ),
inference(resolution,[status(thm)],[f23695,f4511]) ).
fof(f23926,plain,
~ sQ319_spl,
inference(contradiction_clause,[status(thm)],[f23908]) ).
fof(f23985,plain,
( ~ sQ316_spl
| s(num,i(s(fun(fun(sK3697_skl,bool),num),dimindex),s(fun(sK3697_skl,bool),univ))) = s(num,i(s(fun(num,num),numeral),s(num,u_0))) ),
inference(paramodulation,[status(thm)],[f23460,f4511]) ).
fof(f23999,plain,
( ~ sQ316_spl
| sQ225_spl ),
inference(split_clause,[status(thm)],[f23985,f19796,f23459]) ).
fof(f24008,plain,
! [X0,X1,X2] :
( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK27_skl(X2,univ,X0)))))
| ~ p(s(bool,t))
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f8093,f3829]) ).
fof(f24022,definition,
! [X0,X1,X2] :
( sQ332_spl
<=> ( ~ p(s(bool,i(s(fun(X0,bool),X2),s(X0,sK27_skl(X2,univ,X0)))))
| p(s(bool,i(s(fun(X0,bool),univ),s(X0,X1)))) ) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f24025,plain,
( ~ sQ10_spl
| sQ332_spl ),
inference(split_clause,[status(thm)],[f24008,f24022,f18025]) ).
fof(f24479,plain,
( ~ sQ314_spl
| p(s(bool,f0)) ),
inference(paramodulation,[status(thm)],[f8087,f23349]) ).
fof(f24489,plain,
( ~ sQ314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24479,f3713]) ).
fof(f24490,plain,
~ sQ314_spl,
inference(contradiction_clause,[status(thm)],[f24489]) ).
fof(f24616,plain,
( ~ sQ221_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f19808,f18906,f19782]) ).
fof(f24724,plain,
! [X0] :
( ~ sQ192_spl
| ~ p(s(bool,i(s(fun(fun(cart(real,sK3697_skl),bool),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(fun(cart(real,sK3697_skl),bool),bool)),subset),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))),s(fun(cart(real,sK3697_skl),bool),X0))))
| s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f21510,f15027]) ).
fof(f24728,plain,
( ~ sQ192_spl
| s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),sK3698_skl))) = s(fun(cart(real,sK3697_skl),bool),i(s(fun(fun(cart(real,sK3697_skl),bool),fun(cart(real,sK3697_skl),bool)),span),s(fun(cart(real,sK3697_skl),bool),univ))) ),
inference(resolution,[status(thm)],[f24724,f8357]) ).
fof(f24759,plain,
( ~ sQ192_spl
| sQ221_spl ),
inference(split_clause,[status(thm)],[f24728,f19782,f18903]) ).
fof(f24779,plain,
$false,
inference(sat_refutation,[status(thm)],[f18001,f18002,f18028,f18032,f18124,f18329,f18506,f18516,f18682,f18686,f18717,f18909,f18910,f18946,f19240,f19480,f19627,f19766,f19802,f19807,f20225,f20257,f20307,f20463,f20598,f20604,f20658,f20662,f20847,f20902,f20907,f20912,f20916,f21121,f21128,f21233,f21251,f21285,f21489,f21597,f21796,f21843,f21889,f22075,f22153,f22172,f22745,f22749,f23108,f23312,f23316,f23343,f23926,f23999,f24025,f24490,f24616,f24759]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO473+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 16:40:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 2.25/2.50 % Drodi V4.1.1
% 123.51/17.83 % Refutation found
% 123.51/17.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 123.51/17.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.80/18.15 % Elapsed time: 17.749450 seconds
% 21.80/18.15 % CPU time: 124.697926 seconds
% 21.80/18.15 % Total memory used: 2.439 GB
% 21.80/18.15 % Net memory used: 2.424 GB
%------------------------------------------------------------------------------