%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO445+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:26:30 PM UTC 2026
% Result : Theorem 2.25s 3.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO445+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n004.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 20 16:15:49 UTC 2026
% 0.13/0.40 % CPUTime :
% 2.06/2.30 % Drodi V4.1.1
% 2.25/3.14 % Refutation found
% 2.25/3.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.25/3.14 % SZS output start CNFRefutation for theBenchmark
% 2.25/3.14 fof(f9,axiom,(
% 2.25/3.14 ( p(s(bool,f0))<=> (! [P0] : p(s(bool,P0)) )) ),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f10,axiom,(
% 2.25/3.14 (! [X] :( ~ p(s(bool,X))<=> ( p(s(bool,X))=> p(s(bool,f0)) ) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f12,axiom,(
% 2.25/3.14 s(bool,u_falsityu_) = s(bool,f0) ),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f15,axiom,(
% 2.25/3.14 (! [A,X] :( s(A,X) = s(A,X)<=> p(s(bool,t)) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f42,axiom,(
% 2.25/3.14 (! [T0] :( ( s(bool,t) = s(bool,T0)<=> p(s(bool,T0)) )& ( s(bool,T0) = s(bool,t)<=> p(s(bool,T0)) )& ( s(bool,f0) = s(bool,T0)<=> ~ p(s(bool,T0)) )& ( s(bool,T0) = s(bool,f0)<=> ~ p(s(bool,T0)) ) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f43,axiom,(
% 2.25/3.14 ~ p(s(bool,f0)) ),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f44,axiom,(
% 2.25/3.14 ( ~ p(s(bool,f0))<=> p(s(bool,t)) ) ),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f199,axiom,(
% 2.25/3.14 ( s(num,u_0) = s(num,u_0)<=> p(s(bool,t)) ) ),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f568,axiom,(
% 2.25/3.14 (! [N0] :( s(num,i(s(fun(num,num),bit1),s(num,N0))) = s(num,u_0)<=> p(s(bool,f0)) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f572,axiom,(
% 2.25/3.14 (! [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)) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2041,axiom,(
% 2.25/3.14 (! [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)) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2043,axiom,(
% 2.25/3.14 (! [Q59041,P0] :( (? [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,i(s(fun(Q59041,bool),P0),s(Q59041,X)))) ))<=> p(s(bool,f0)) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2377,axiom,(
% 2.25/3.14 (! [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) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2796,axiom,(
% 2.25/3.14 (! [Q100205,X,Y] : s(real,i(s(fun(cart(real,Q100205),real),i(s(fun(cart(real,Q100205),fun(cart(real,Q100205),real)),dot),s(cart(real,Q100205),X))),s(cart(real,Q100205),Y))) = s(real,i(s(fun(cart(real,Q100205),real),i(s(fun(cart(real,Q100205),fun(cart(real,Q100205),real)),dot),s(cart(real,Q100205),Y))),s(cart(real,Q100205),X))) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2807,axiom,(
% 2.25/3.14 (! [Q100487,X] : p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,Q100487),real),i(s(fun(cart(real,Q100487),fun(cart(real,Q100487),real)),dot),s(cart(real,Q100487),X))),s(cart(real,Q100487),X)))))) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f2889,axiom,(
% 2.25/3.14 (! [Q104636,X,Y] :( s(cart(real,Q104636),X) = s(cart(real,Q104636),Y)<=> ( s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))& s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y))) = s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))) ) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f3003,conjecture,(
% 2.25/3.14 (! [Q110616,X,Y] :( (! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))))<=> s(cart(real,Q110616),X) = s(cart(real,Q110616),Y) ) )),
% 2.25/3.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.25/3.14 fof(f3004,negated_conjecture,(
% 2.25/3.14 ~((! [Q110616,X,Y] :( (! [Z0] : s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0))) = s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))))<=> s(cart(real,Q110616),X) = s(cart(real,Q110616),Y) ) ))),
% 2.25/3.14 inference(negated_conjecture,[status(cth)],[f3003])).
% 2.25/3.14 fof(f3044,plain,(
% 2.25/3.14 (~p(s(bool,f0))|(![P0]: p(s(bool,P0))))&(p(s(bool,f0))|(?[P0]: ~p(s(bool,P0))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f9])).
% 2.25/3.14 fof(f3045,plain,(
% 2.25/3.14 (~p(s(bool,f0))|(![P0]: p(s(bool,P0))))&(p(s(bool,f0))|~p(s(bool,sK5_skl)))),
% 2.25/3.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P0,sK5_skl)],[f3044])).
% 2.25/3.14 fof(f3047,plain,(
% 2.25/3.14 p(s(bool,f0))|~p(s(bool,sK5_skl))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3045])).
% 2.25/3.14 fof(f3048,plain,(
% 2.25/3.14 ![X]: (~p(s(bool,X))<=>(~p(s(bool,X))|p(s(bool,f0))))),
% 2.25/3.14 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 2.25/3.14 fof(f3049,plain,(
% 2.25/3.14 ![X]: ((p(s(bool,X))|(~p(s(bool,X))|p(s(bool,f0))))&(~p(s(bool,X))|(p(s(bool,X))&~p(s(bool,f0)))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f3048])).
% 2.25/3.14 fof(f3050,plain,(
% 2.25/3.14 (![X]: (p(s(bool,X))|(~p(s(bool,X))|p(s(bool,f0)))))&(![X]: (~p(s(bool,X))|(p(s(bool,X))&~p(s(bool,f0)))))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f3049])).
% 2.25/3.14 fof(f3051,plain,(
% 2.25/3.14 ![X0]: (p(s(bool,X0))|~p(s(bool,X0))|p(s(bool,f0)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3050])).
% 2.25/3.14 fof(f3055,plain,(
% 2.25/3.14 s(bool,u_falsityu_)=s(bool,f0)),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f12])).
% 2.25/3.14 fof(f3065,plain,(
% 2.25/3.14 ![A,X]: ((~s(A,X)=s(A,X)|p(s(bool,t)))&(s(A,X)=s(A,X)|~p(s(bool,t))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f15])).
% 2.25/3.14 fof(f3066,plain,(
% 2.25/3.14 ((![A,X]: ~s(A,X)=s(A,X))|p(s(bool,t)))&((![A,X]: s(A,X)=s(A,X))|~p(s(bool,t)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f3065])).
% 2.25/3.14 fof(f3067,plain,(
% 2.25/3.14 ![X0,X1]: (~s(X0,X1)=s(X0,X1)|p(s(bool,t)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3066])).
% 2.25/3.14 fof(f3068,plain,(
% 2.25/3.14 ![X0,X1]: (s(X0,X1)=s(X0,X1)|~p(s(bool,t)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3066])).
% 2.25/3.14 fof(f3213,plain,(
% 2.25/3.14 ![T0]: (((((~s(bool,t)=s(bool,T0)|p(s(bool,T0)))&(s(bool,t)=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,f0)=s(bool,T0)|~p(s(bool,T0)))&(s(bool,f0)=s(bool,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)))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f42])).
% 2.25/3.14 fof(f3214,plain,(
% 2.25/3.14 ((((![T0]: (~s(bool,t)=s(bool,T0)|p(s(bool,T0))))&(![T0]: (s(bool,t)=s(bool,T0)|~p(s(bool,T0)))))&((![T0]: (~s(bool,T0)=s(bool,t)|p(s(bool,T0))))&(![T0]: (s(bool,T0)=s(bool,t)|~p(s(bool,T0))))))&((![T0]: (~s(bool,f0)=s(bool,T0)|~p(s(bool,T0))))&(![T0]: (s(bool,f0)=s(bool,T0)|p(s(bool,T0))))))&((![T0]: (~s(bool,T0)=s(bool,f0)|~p(s(bool,T0))))&(![T0]: (s(bool,T0)=s(bool,f0)|p(s(bool,T0)))))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f3213])).
% 2.25/3.14 fof(f3215,plain,(
% 2.25/3.14 ![X0]: (~s(bool,t)=s(bool,X0)|p(s(bool,X0)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3214])).
% 2.25/3.14 fof(f3223,plain,(
% 2.25/3.14 ~p(s(bool,f0))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f43])).
% 2.25/3.14 fof(f3224,plain,(
% 2.25/3.14 (p(s(bool,f0))|p(s(bool,t)))&(~p(s(bool,f0))|~p(s(bool,t)))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f44])).
% 2.25/3.14 fof(f3226,plain,(
% 2.25/3.14 ~p(s(bool,f0))|~p(s(bool,t))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f3224])).
% 2.25/3.14 fof(f4018,plain,(
% 2.25/3.14 (~s(num,u_0)=s(num,u_0)|p(s(bool,t)))&(s(num,u_0)=s(num,u_0)|~p(s(bool,t)))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f199])).
% 2.25/3.14 fof(f4020,plain,(
% 2.25/3.14 s(num,u_0)=s(num,u_0)|~p(s(bool,t))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f4018])).
% 2.25/3.14 fof(f5013,plain,(
% 2.25/3.14 ![N0]: ((~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)|~p(s(bool,f0))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f568])).
% 2.25/3.14 fof(f5014,plain,(
% 2.25/3.14 ((![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))|~p(s(bool,f0)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f5013])).
% 2.25/3.14 fof(f5015,plain,(
% 2.25/3.14 ![X0]: (~s(num,i(s(fun(num,num),bit1),s(num,X0)))=s(num,u_0)|p(s(bool,f0)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f5014])).
% 2.25/3.14 fof(f5029,plain,(
% 2.25/3.14 ![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)))&(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))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f572])).
% 2.25/3.14 fof(f5030,plain,(
% 2.25/3.14 ((![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))))|~p(s(bool,f0)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f5029])).
% 2.25/3.14 fof(f5031,plain,(
% 2.25/3.14 ![X0,X1]: (~s(num,i(s(fun(num,num),bit0),s(num,X0)))=s(num,i(s(fun(num,num),bit1),s(num,X1)))|p(s(bool,f0)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f5030])).
% 2.25/3.14 fof(f9329,plain,(
% 2.25/3.14 ![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)))),
% 2.25/3.14 inference(pre_NNF_transformation,[status(thm)],[f2041])).
% 2.25/3.14 fof(f9330,plain,(
% 2.25/3.14 ![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)))&((![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))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f9329])).
% 2.25/3.14 fof(f9331,plain,(
% 2.25/3.14 ((![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)))&((![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))))|(![P0]: p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X)))))))|~p(s(bool,t)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f9330])).
% 2.25/3.14 fof(f9332,plain,(
% 2.25/3.14 ((![Q58981,P0]: (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))))&~p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,sK1408_skl(P0,Q58981)))))))|p(s(bool,t)))&((![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))))|(![P0]: p(s(bool,i(s(fun(Q58981,bool),P0),s(Q58981,X)))))))|~p(s(bool,t)))),
% 2.25/3.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK1408_skl]),skolemize(X,sK1408_skl(P0,Q58981))],[f9331])).
% 2.25/3.14 fof(f9335,plain,(
% 2.25/3.14 ![X0,X1,X2]: (~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))))|p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))|~p(s(bool,t)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f9332])).
% 2.25/3.14 fof(f9345,plain,(
% 2.25/3.14 ![Q59041,P0]: (((![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,i(s(fun(Q59041,bool),P0),s(Q59041,X))))))|p(s(bool,f0)))&((?[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,i(s(fun(Q59041,bool),P0),s(Q59041,X))))))|~p(s(bool,f0))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f2043])).
% 2.25/3.14 fof(f9346,plain,(
% 2.25/3.14 ((![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))))|(![P0]: ~p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X)))))))|p(s(bool,f0)))&((![Q59041,P0]: ?[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,i(s(fun(Q59041,bool),P0),s(Q59041,X))))))|~p(s(bool,f0)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f9345])).
% 2.25/3.14 fof(f9347,plain,(
% 2.25/3.14 ((![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))))|(![P0]: ~p(s(bool,i(s(fun(Q59041,bool),P0),s(Q59041,X)))))))|p(s(bool,f0)))&((![Q59041,P0]: (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,i(s(fun(Q59041,bool),P0),s(Q59041,sK1410_skl(P0,Q59041)))))))|~p(s(bool,f0)))),
% 2.25/3.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK1410_skl]),skolemize(X,sK1410_skl(P0,Q59041))],[f9346])).
% 2.25/3.14 fof(f9348,plain,(
% 2.25/3.14 ![X0,X1,X2]: (~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))))|~p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))|p(s(bool,f0)))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f9347])).
% 2.25/3.14 fof(f10979,plain,(
% 2.25/3.14 ![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))|~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)))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f2377])).
% 2.25/3.14 fof(f10980,plain,(
% 2.25/3.14 (~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))|(![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)))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f10979])).
% 2.25/3.14 fof(f10981,plain,(
% 2.25/3.14 ![X0,X1,X2]: (~p(s(bool,t))|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))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f10980])).
% 2.25/3.14 fof(f12682,plain,(
% 2.25/3.14 ![X0,X1,X2]: (s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X2)))=s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X2))),s(cart(real,X0),X1))))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f2796])).
% 2.25/3.14 fof(f12693,plain,(
% 2.25/3.14 ![X0,X1]: (p(s(bool,i(s(fun(real,bool),i(s(fun(real,fun(real,bool)),realu_le),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1)))))))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f2807])).
% 2.25/3.14 fof(f12916,plain,(
% 2.25/3.14 ![Q104636,X,Y]: ((~s(cart(real,Q104636),X)=s(cart(real,Q104636),Y)|(s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))&s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))))&(s(cart(real,Q104636),X)=s(cart(real,Q104636),Y)|(~s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))|~s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))))))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f2889])).
% 2.25/3.14 fof(f12917,plain,(
% 2.25/3.14 (![Q104636,X,Y]: (~s(cart(real,Q104636),X)=s(cart(real,Q104636),Y)|(s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))&s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))))))&(![Q104636,X,Y]: (s(cart(real,Q104636),X)=s(cart(real,Q104636),Y)|(~s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),Y)))|~s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),Y))),s(cart(real,Q104636),Y)))=s(real,i(s(fun(cart(real,Q104636),real),i(s(fun(cart(real,Q104636),fun(cart(real,Q104636),real)),dot),s(cart(real,Q104636),X))),s(cart(real,Q104636),X))))))),
% 2.25/3.14 inference(miniscoping,[status(thm)],[f12916])).
% 2.25/3.14 fof(f12920,plain,(
% 2.25/3.14 ![X0,X1,X2]: (s(cart(real,X0),X1)=s(cart(real,X0),X2)|~s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1)))=s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X2)))|~s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X2))),s(cart(real,X0),X2)))=s(real,i(s(fun(cart(real,X0),real),i(s(fun(cart(real,X0),fun(cart(real,X0),real)),dot),s(cart(real,X0),X1))),s(cart(real,X0),X1))))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f12917])).
% 2.25/3.14 fof(f13369,plain,(
% 2.25/3.14 (?[Q110616,X,Y]: ((![Z0]: s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0)))=s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))))<~>s(cart(real,Q110616),X)=s(cart(real,Q110616),Y)))),
% 2.25/3.14 inference(pre_NNF_transformation,[status(thm)],[f3004])).
% 2.25/3.14 fof(f13370,plain,(
% 2.25/3.14 ?[Q110616,X,Y]: (((![Z0]: s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0)))=s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))))|s(cart(real,Q110616),X)=s(cart(real,Q110616),Y))&((?[Z0]: ~s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),X))),s(cart(real,Q110616),Z0)))=s(real,i(s(fun(cart(real,Q110616),real),i(s(fun(cart(real,Q110616),fun(cart(real,Q110616),real)),dot),s(cart(real,Q110616),Y))),s(cart(real,Q110616),Z0))))|~s(cart(real,Q110616),X)=s(cart(real,Q110616),Y)))),
% 2.25/3.14 inference(NNF_transformation,[status(thm)],[f13369])).
% 2.25/3.14 fof(f13371,plain,(
% 2.25/3.14 (((![Z0]: s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),Z0)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),Z0))))|s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl))&(~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl)))|~s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl)))),
% 2.25/3.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK3163_skl,sK3164_skl,sK3165_skl,sK3166_skl]),skolemize(Q110616,sK3163_skl),skolemize(X,sK3164_skl),skolemize(Y,sK3165_skl),skolemize(Z0,sK3166_skl)],[f13370])).
% 2.25/3.14 fof(f13372,plain,(
% 2.25/3.14 ![X0]: (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0)))|s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl))),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f13371])).
% 2.25/3.14 fof(f13373,plain,(
% 2.25/3.14 ~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl)))|~s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl)),
% 2.25/3.14 inference(cnf_transformation,[status(thm)],[f13371])).
% 2.25/3.14 fof(f15901,definition,(
% 2.25/3.14 ![X2]: (sQ1_spl <=> (~p(s(bool,X2))|p(s(bool,X2))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15905,definition,(
% 2.25/3.14 sQ2_spl <=> (p(s(bool,f0)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15907,plain,(
% 2.25/3.14 ~p(s(bool,f0))|sQ2_spl),
% 2.25/3.14 inference(component_clause,[status(thm)],[f15905])).
% 2.25/3.14 fof(f15908,definition,(
% 2.25/3.14 ![X0]: (sQ3_spl <=> (p(s(bool,X0))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15909,plain,(
% 2.25/3.14 ![X0]: (p(s(bool,X0))|~sQ3_spl)),
% 2.25/3.14 inference(component_clause,[status(thm)],[f15908])).
% 2.25/3.14 fof(f15912,definition,(
% 2.25/3.14 sQ4_spl <=> (p(s(bool,sK5_skl)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15915,plain,(
% 2.25/3.14 sQ2_spl|~sQ4_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f3047,f15905,f15912])).
% 2.25/3.14 fof(f15916,plain,(
% 2.25/3.14 sQ1_spl|sQ2_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f3051,f15901,f15905])).
% 2.25/3.14 fof(f15917,definition,(
% 2.25/3.14 ![X0]: (sQ5_spl <=> (~p(s(bool,X0))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15918,plain,(
% 2.25/3.14 ![X0]: (~p(s(bool,X0))|~sQ5_spl)),
% 2.25/3.14 inference(component_clause,[status(thm)],[f15917])).
% 2.25/3.14 fof(f15936,definition,(
% 2.25/3.14 ![X0,X1]: (sQ9_spl <=> (~s(X0,X1)=s(X0,X1)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15937,plain,(
% 2.25/3.14 ![X0,X1]: (~s(X0,X1)=s(X0,X1)|~sQ9_spl)),
% 2.25/3.14 inference(component_clause,[status(thm)],[f15936])).
% 2.25/3.14 fof(f15939,definition,(
% 2.25/3.14 sQ10_spl <=> (p(s(bool,t)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15942,plain,(
% 2.25/3.14 sQ9_spl|sQ10_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f3067,f15936,f15939])).
% 2.25/3.14 fof(f15943,definition,(
% 2.25/3.14 ![X0,X1]: (sQ11_spl <=> (s(X0,X1)=s(X0,X1)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f15946,plain,(
% 2.25/3.14 sQ11_spl|~sQ10_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f3068,f15943,f15939])).
% 2.25/3.14 fof(f16038,plain,(
% 2.25/3.14 ~sQ2_spl|~sQ10_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f3226,f15905,f15939])).
% 2.25/3.14 fof(f16239,definition,(
% 2.25/3.14 sQ39_spl <=> (s(num,u_0)=s(num,u_0))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16243,plain,(
% 2.25/3.14 sQ39_spl|~sQ10_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f4020,f16239,f15939])).
% 2.25/3.14 fof(f16417,definition,(
% 2.25/3.14 ![X0]: (sQ86_spl <=> (~s(num,i(s(fun(num,num),bit1),s(num,X0)))=s(num,u_0)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16420,plain,(
% 2.25/3.14 sQ86_spl|sQ2_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f5015,f16417,f15905])).
% 2.25/3.14 fof(f16427,definition,(
% 2.25/3.14 ![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)))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16430,plain,(
% 2.25/3.14 sQ88_spl|sQ2_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f5031,f16427,f15905])).
% 2.25/3.14 fof(f16593,definition,(
% 2.25/3.14 ![X0,X1,X2]: (sQ132_spl <=> (~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))))|p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16596,plain,(
% 2.25/3.14 sQ132_spl|~sQ10_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f9335,f16593,f15939])).
% 2.25/3.14 fof(f16597,definition,(
% 2.25/3.14 ![X0,X1,X2]: (sQ133_spl <=> (~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))))|~p(s(bool,i(s(fun(X0,bool),X2),s(X0,X1))))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16600,plain,(
% 2.25/3.14 sQ133_spl|sQ2_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f9348,f16597,f15905])).
% 2.25/3.14 fof(f16628,definition,(
% 2.25/3.14 ![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)))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16631,plain,(
% 2.25/3.14 ~sQ10_spl|sQ141_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f10981,f15939,f16628])).
% 2.25/3.14 fof(f16750,definition,(
% 2.25/3.14 ![X0]: (sQ173_spl <=> (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0)))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16751,plain,(
% 2.25/3.14 ![X0]: (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),X0)))|~sQ173_spl)),
% 2.25/3.14 inference(component_clause,[status(thm)],[f16750])).
% 2.25/3.14 fof(f16753,definition,(
% 2.25/3.14 sQ174_spl <=> (s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16754,plain,(
% 2.25/3.14 s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl)|~sQ174_spl),
% 2.25/3.14 inference(component_clause,[status(thm)],[f16753])).
% 2.25/3.14 fof(f16756,plain,(
% 2.25/3.14 sQ173_spl|sQ174_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f13372,f16750,f16753])).
% 2.25/3.14 fof(f16757,definition,(
% 2.25/3.14 sQ175_spl <=> (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f16759,plain,(
% 2.25/3.14 ~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3166_skl)))|sQ175_spl),
% 2.25/3.14 inference(component_clause,[status(thm)],[f16757])).
% 2.25/3.14 fof(f16760,plain,(
% 2.25/3.14 ~sQ175_spl|~sQ174_spl),
% 2.25/3.14 inference(split_clause,[status(thm)],[f13373,f16757,f16753])).
% 2.25/3.14 fof(f16800,plain,(
% 2.25/3.14 $false|~sQ9_spl),
% 2.25/3.14 inference(trivial_equality_resolution,[status(thm)],[f15937])).
% 2.25/3.14 fof(f16801,plain,(
% 2.25/3.14 ~sQ9_spl),
% 2.25/3.14 inference(contradiction_clause,[status(thm)],[f16800])).
% 2.25/3.14 fof(f16802,plain,(
% 2.25/3.14 ~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3166_skl)))|~sQ174_spl|sQ175_spl),
% 2.25/3.14 inference(forward_demodulation,[status(thm)],[f16754,f16759])).
% 2.25/3.14 fof(f16803,plain,(
% 2.25/3.14 $false|~sQ174_spl|sQ175_spl),
% 2.25/3.14 inference(trivial_equality_resolution,[status(thm)],[f16802])).
% 2.25/3.14 fof(f16804,plain,(
% 2.25/3.14 ~sQ174_spl|sQ175_spl),
% 2.25/3.14 inference(contradiction_clause,[status(thm)],[f16803])).
% 2.25/3.14 fof(f16817,plain,(
% 2.25/3.14 ![X0]: (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),X0)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),X0))),s(cart(real,sK3163_skl),sK3165_skl)))|~sQ173_spl)),
% 2.25/3.14 inference(paramodulation,[status(thm)],[f16751,f12682])).
% 2.25/3.14 fof(f17012,plain,(
% 2.25/3.14 $false|~sQ5_spl),
% 2.25/3.14 inference(forward_subsumption_resolution,[status(thm)],[f12693,f15918])).
% 2.25/3.14 fof(f17013,plain,(
% 2.25/3.14 ~sQ5_spl),
% 2.25/3.14 inference(contradiction_clause,[status(thm)],[f17012])).
% 2.25/3.14 fof(f17117,plain,(
% 2.25/3.14 $false|~sQ3_spl),
% 2.25/3.14 inference(forward_subsumption_resolution,[status(thm)],[f3223,f15909])).
% 2.25/3.14 fof(f17118,plain,(
% 2.25/3.14 ~sQ3_spl),
% 2.25/3.14 inference(contradiction_clause,[status(thm)],[f17117])).
% 2.25/3.14 fof(f17139,definition,(
% 2.25/3.14 sQ188_spl <=> (s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl))))),
% 2.25/3.14 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 2.25/3.14 fof(f17141,plain,(
% 2.25/3.14 ~s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),vectoru_norm),s(cart(real,sK3163_skl),sK3164_skl)))|sQ188_spl),
% 2.25/3.14 inference(component_clause,[status(thm)],[f17139])).
% 2.25/3.14 fof(f17146,plain,(
% 2.25/3.14 $false|sQ188_spl),
% 2.25/3.14 inference(trivial_equality_resolution,[status(thm)],[f17141])).
% 2.25/3.14 fof(f17147,plain,(
% 2.25/3.14 sQ188_spl),
% 2.25/3.14 inference(contradiction_clause,[status(thm)],[f17146])).
% 2.25/3.14 fof(f17278,plain,(
% 2.25/3.14 ~s(bool,t)=s(bool,f0)|p(s(bool,u_falsityu_))),
% 2.25/3.14 inference(paramodulation,[status(thm)],[f3055,f3215])).
% 5.52/3.28 fof(f17282,definition,(
% 5.52/3.28 sQ200_spl <=> (s(bool,t)=s(bool,f0))),
% 5.52/3.28 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 5.52/3.28 fof(f17285,definition,(
% 5.52/3.28 sQ201_spl <=> (p(s(bool,u_falsityu_)))),
% 5.52/3.28 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 5.52/3.28 fof(f17286,plain,(
% 5.52/3.28 p(s(bool,u_falsityu_))|~sQ201_spl),
% 5.52/3.28 inference(component_clause,[status(thm)],[f17285])).
% 5.52/3.28 fof(f17288,plain,(
% 5.52/3.28 ~sQ200_spl|sQ201_spl),
% 5.52/3.28 inference(split_clause,[status(thm)],[f17278,f17282,f17285])).
% 5.52/3.28 fof(f17291,plain,(
% 5.52/3.28 p(s(bool,f0))|~sQ201_spl),
% 5.52/3.28 inference(forward_demodulation,[status(thm)],[f3055,f17286])).
% 5.52/3.28 fof(f17292,plain,(
% 5.52/3.28 $false|sQ2_spl|~sQ201_spl),
% 5.52/3.28 inference(forward_subsumption_resolution,[status(thm)],[f17291,f15907])).
% 5.52/3.28 fof(f17293,plain,(
% 5.52/3.28 sQ2_spl|~sQ201_spl),
% 5.52/3.28 inference(contradiction_clause,[status(thm)],[f17292])).
% 5.52/3.28 fof(f17311,plain,(
% 5.52/3.28 s(cart(real,sK3163_skl),sK3164_skl)=s(cart(real,sK3163_skl),sK3165_skl)|~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl)))|~sQ173_spl),
% 5.52/3.28 inference(resolution,[status(thm)],[f12920,f16817])).
% 5.52/3.28 fof(f17325,definition,(
% 5.52/3.28 sQ203_spl <=> (s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl))))),
% 5.52/3.28 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 5.52/3.28 fof(f17327,plain,(
% 5.52/3.28 ~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3165_skl))),s(cart(real,sK3163_skl),sK3165_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl)))|sQ203_spl),
% 5.52/3.28 inference(component_clause,[status(thm)],[f17325])).
% 5.52/3.28 fof(f17328,plain,(
% 5.52/3.28 sQ174_spl|~sQ203_spl|~sQ173_spl),
% 5.52/3.28 inference(split_clause,[status(thm)],[f17311,f16753,f17325,f16750])).
% 5.52/3.28 fof(f17350,plain,(
% 5.52/3.28 ~s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3165_skl)))=s(real,i(s(fun(cart(real,sK3163_skl),real),i(s(fun(cart(real,sK3163_skl),fun(cart(real,sK3163_skl),real)),dot),s(cart(real,sK3163_skl),sK3164_skl))),s(cart(real,sK3163_skl),sK3164_skl)))|~sQ173_spl|sQ203_spl),
% 5.52/3.28 inference(forward_demodulation,[status(thm)],[f16751,f17327])).
% 5.52/3.28 fof(f17355,plain,(
% 5.52/3.28 $false|~sQ173_spl|sQ203_spl),
% 5.52/3.28 inference(forward_subsumption_resolution,[status(thm)],[f17350,f16817])).
% 5.52/3.28 fof(f17356,plain,(
% 5.52/3.28 ~sQ173_spl|sQ203_spl),
% 5.52/3.28 inference(contradiction_clause,[status(thm)],[f17355])).
% 5.52/3.28 fof(f17357,plain,(
% 5.52/3.28 $false),
% 5.52/3.28 inference(sat_refutation,[status(thm)],[f15915,f15916,f15942,f15946,f16038,f16243,f16420,f16430,f16596,f16600,f16631,f16756,f16760,f16801,f16804,f17013,f17118,f17147,f17288,f17293,f17328,f17356])).
% 5.52/3.28 % SZS output end CNFRefutation for theBenchmark.p
% 2.31/3.32 % Elapsed time: 2.898650 seconds
% 2.31/3.32 % CPU time: 8.556436 seconds
% 2.31/3.32 % Total memory used: 1.400 GB
% 2.31/3.32 % Net memory used: 1.397 GB
%------------------------------------------------------------------------------