%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW473+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:27:12 PM UTC 2026
% Result : Theorem 113.86s 15.15s
% Output : Proof 113.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 62
% Syntax : Number of formulae : 268 ( 147 unt; 0 def)
% Number of atoms : 585 ( 220 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 697 ( 380 ~; 194 |; 80 &)
% ( 23 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 66 ( 66 usr; 22 con; 0-4 aty)
% Number of variables : 421 ( 38 sgn 282 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f427,axiom,
! [X_3,A_1,B_6] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X_3,A_1)),B_6))
<=> ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_3),B_6)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_324_insert__subset) ).
fof(f427_nnf,plain,
! [X_3,A_1,B_6] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_3),B_6))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X_3,A_1)),B_6)) )
& ( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_3),B_6)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X_3,A_1)),B_6)) ) ),
inference(nnf_transformation,[status(thm)],[f427]) ).
fof(f427_sk,plain,
! [X_3,A_1,B_6] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_3),B_6))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X_3,A_1)),B_6)) )
& ( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_3),B_6)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X_3,A_1)),B_6)) ) ),
inference(skolemisation,[status(esa)],[f427_nnf]) ).
cnf(c616,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),X2))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X0,X1)),X2)) ),
inference(cnf_transformation,[status(esa)],[f427_sk]) ).
cnf(t217,plain,
ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X1),X2)),true,ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),X2)),true,hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X1,X3)),X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c616]) ).
cnf(t349,plain,
ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X1),X2)),true,ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),X2)),true,hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X1,X3)),X2)),true),true) = true,
inference(orient,[status(thm)],[t217]) ).
fof(f916,conjecture,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_6) ).
fof(f916_neg,negated_conjecture,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(negated_conjecture,[status(cth)],[f916]) ).
fof(f916_nnf,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(nnf_transformation,[status(thm)],[f916_neg]) ).
fof(f916_sk,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(skolemisation,[status(esa)],[f916_nnf]) ).
cnf(c1380,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(esa)],[f916_sk]) ).
cnf(t83,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))) = false,
inference(equality_encoding,[status(esa)],[c1380]) ).
cnf(t986,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))) = false,
inference(orient,[status(thm)],[t83]) ).
cnf(t1014,plain,
true = ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u))),true,ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),true,false,true),true),
inference(cp,[status(thm)],[t349,t986]) ).
fof(f410,axiom,
! [F,X_3,A_1] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_3)),image_pname_a(F,A_1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_307_imageI) ).
fof(f410_nnf,plain,
! [F,X_3,A_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_3)),image_pname_a(F,A_1)))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1)) ),
inference(nnf_transformation,[status(thm)],[f410]) ).
fof(f410_sk,plain,
! [X_3,A_1,F] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_3)),image_pname_a(F,A_1)))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1)) ),
inference(skolemisation,[status(esa)],[f410_nnf]) ).
cnf(c593,plain,
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X0,X1)),image_pname_a(X0,X2)))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f410_sk]) ).
cnf(t150,plain,
ifeq(hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X1),X2)),true,hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X3,X1)),image_pname_a(X3,X2))),true) = true,
inference(equality_encoding,[status(esa)],[c593]) ).
cnf(t395,plain,
ifeq(hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X1),X2)),true,hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X3,X1)),image_pname_a(X3,X2))),true) = true,
inference(orient,[status(thm)],[t150]) ).
fof(f914,hypothesis,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_4) ).
fof(f914_nnf,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(nnf_transformation,[status(thm)],[f914]) ).
cnf(c1378,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(cnf_transformation,[status(esa)],[f914_nnf]) ).
cnf(t33,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)) = true,
inference(equality_encoding,[status(esa)],[c1378]) ).
cnf(t741,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)) = true,
inference(orient,[status(thm)],[t33]) ).
cnf(t743,plain,
true = ifeq(true,true,hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X1,pn)),image_pname_a(X1,u))),true),
inference(cp,[status(thm)],[t395,t741]) ).
cnf(t25,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t3340,plain,
true = hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X1,pn)),image_pname_a(X1,u))),
inference(step,[status(thm)],[t743,t256]) ).
cnf(t2037,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(X1,pn)),image_pname_a(X1,u))) = true,
inference(orient,[status(thm)],[t3340]) ).
cnf(t3409,plain,
true = ifeq(true,true,ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),true,false,true),true),
inference(step,[status(thm)],[t1014,t2037]) ).
cnf(t3410,plain,
true = ifeq(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),true,false,true),
inference(step,[status(thm)],[t3409,t256]) ).
fof(f911,hypothesis,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f911_nnf,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
inference(nnf_transformation,[status(thm)],[f911]) ).
cnf(c1375,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(esa)],[f911_nnf]) ).
cnf(t56,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))) = true,
inference(equality_encoding,[status(esa)],[c1375]) ).
cnf(t579,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t3411,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t3410,t579]) ).
cnf(t3412,plain,
true = false,
inference(step,[status(thm)],[t3411,t256]) ).
cnf(t3205,plain,
false = true,
inference(orient,[status(thm)],[t3412]) ).
fof(f186,axiom,
! [N] : hAPP_nat_nat(suc,N) != N,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_Suc__n__not__n) ).
fof(f186_nnf,plain,
! [N] : hAPP_nat_nat(suc,N) != N,
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [N] : hAPP_nat_nat(suc,N) != N,
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c199,plain,
hAPP_nat_nat(suc,X0) != X0,
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
fof(f187,axiom,
! [N] : N != hAPP_nat_nat(suc,N),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_n__not__Suc__n) ).
fof(f187_nnf,plain,
! [N] : N != hAPP_nat_nat(suc,N),
inference(nnf_transformation,[status(thm)],[f187]) ).
fof(f187_sk,plain,
! [N] : N != hAPP_nat_nat(suc,N),
inference(skolemisation,[status(esa)],[f187_nnf]) ).
cnf(c200,plain,
X0 != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f187_sk]) ).
fof(f223,axiom,
! [M_1,Na] :
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na))
<=> hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_not__less__eq__eq) ).
fof(f223_nnf,plain,
! [M_1,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M_1))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M_1))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [M_1,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M_1))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M_1))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) ) ),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c258,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,X1)),X0))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
fof(f224,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,N)),N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_Suc__n__not__le__n) ).
fof(f224_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,N)),N)),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,N)),N)),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c259,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,X0)),X0)),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
fof(f486,axiom,
! [A_3] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),bot_bot_fun_nat_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_383_emptyE) ).
fof(f486_nnf,plain,
! [A_3] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),bot_bot_fun_nat_bool)),
inference(nnf_transformation,[status(thm)],[f486]) ).
fof(f486_sk,plain,
! [A_3] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),bot_bot_fun_nat_bool)),
inference(skolemisation,[status(esa)],[f486_nnf]) ).
cnf(c723,plain,
~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),bot_bot_fun_nat_bool)),
inference(cnf_transformation,[status(esa)],[f486_sk]) ).
fof(f487,axiom,
! [A_3] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),bot_bo844097828e_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_384_emptyE) ).
fof(f487_nnf,plain,
! [A_3] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),bot_bo844097828e_bool)),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [A_3] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),bot_bo844097828e_bool)),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c724,plain,
~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool)),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f488,axiom,
! [A_3] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),bot_bot_fun_a_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_385_emptyE) ).
fof(f488_nnf,plain,
! [A_3] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),bot_bot_fun_a_bool)),
inference(nnf_transformation,[status(thm)],[f488]) ).
fof(f488_sk,plain,
! [A_3] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),bot_bot_fun_a_bool)),
inference(skolemisation,[status(esa)],[f488_nnf]) ).
cnf(c725,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),bot_bot_fun_a_bool)),
inference(cnf_transformation,[status(esa)],[f488_sk]) ).
fof(f498,axiom,
! [A_3,A_1] :
( A_1 = bot_bot_fun_nat_bool
=> ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_395_equals0D) ).
fof(f498_nnf,plain,
! [A_3,A_1] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),A_1))
| A_1 != bot_bot_fun_nat_bool ),
inference(nnf_transformation,[status(thm)],[f498]) ).
fof(f498_sk,plain,
! [A_1,A_3] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_3),A_1))
| A_1 != bot_bot_fun_nat_bool ),
inference(skolemisation,[status(esa)],[f498_nnf]) ).
cnf(c735,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),X1))
| X1 != bot_bot_fun_nat_bool ),
inference(cnf_transformation,[status(esa)],[f498_sk]) ).
fof(f499,axiom,
! [A_3,A_1] :
( A_1 = bot_bo844097828e_bool
=> ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_396_equals0D) ).
fof(f499_nnf,plain,
! [A_3,A_1] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),A_1))
| A_1 != bot_bo844097828e_bool ),
inference(nnf_transformation,[status(thm)],[f499]) ).
fof(f499_sk,plain,
! [A_1,A_3] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_3),A_1))
| A_1 != bot_bo844097828e_bool ),
inference(skolemisation,[status(esa)],[f499_nnf]) ).
cnf(c736,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1))
| X1 != bot_bo844097828e_bool ),
inference(cnf_transformation,[status(esa)],[f499_sk]) ).
fof(f500,axiom,
! [A_3,A_1] :
( A_1 = bot_bot_fun_a_bool
=> ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),A_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_397_equals0D) ).
fof(f500_nnf,plain,
! [A_3,A_1] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),A_1))
| A_1 != bot_bot_fun_a_bool ),
inference(nnf_transformation,[status(thm)],[f500]) ).
fof(f500_sk,plain,
! [A_1,A_3] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_3),A_1))
| A_1 != bot_bot_fun_a_bool ),
inference(skolemisation,[status(esa)],[f500_nnf]) ).
cnf(c737,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),X1))
| X1 != bot_bot_fun_a_bool ),
inference(cnf_transformation,[status(esa)],[f500_sk]) ).
fof(f501,axiom,
! [Pa] :
( collect_pname(Pa) = bot_bo844097828e_bool
<=> ! [X_1] :
( is_pname(X_1)
=> ~ hBOOL(hAPP_pname_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_398_Collect__empty__eq) ).
fof(f501_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_pname_bool(Pa,X_1))
& is_pname(X_1) )
| collect_pname(Pa) = bot_bo844097828e_bool )
& ( ! [X_1] :
( ~ hBOOL(hAPP_pname_bool(Pa,X_1))
| ~ is_pname(X_1) )
| collect_pname(Pa) != bot_bo844097828e_bool ) ),
inference(nnf_transformation,[status(thm)],[f501]) ).
fof(f501_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_pname_bool(Pa,sk84(Pa)))
& is_pname(sk84(Pa)) )
| collect_pname(Pa) = bot_bo844097828e_bool )
& ( ~ hBOOL(hAPP_pname_bool(Pa,X_1))
| ~ is_pname(X_1)
| collect_pname(Pa) != bot_bo844097828e_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk84])],[f501_nnf]) ).
cnf(c738,plain,
( ~ hBOOL(hAPP_pname_bool(X0,X1))
| ~ is_pname(X1)
| collect_pname(X0) != bot_bo844097828e_bool ),
inference(cnf_transformation,[status(esa)],[f501_sk]) ).
fof(f502,axiom,
! [Pa] :
( collect_fun_nat_bool(Pa) = bot_bo1701429464l_bool
<=> ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_399_Collect__empty__eq) ).
fof(f502_nnf,plain,
! [Pa] :
( ( ? [X_1] : hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| collect_fun_nat_bool(Pa) = bot_bo1701429464l_bool )
& ( ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| collect_fun_nat_bool(Pa) != bot_bo1701429464l_bool ) ),
inference(nnf_transformation,[status(thm)],[f502]) ).
fof(f502_sk,plain,
! [Pa,X_1] :
( ( hBOOL(hAPP_f54304608l_bool(Pa,sk85(Pa)))
| collect_fun_nat_bool(Pa) = bot_bo1701429464l_bool )
& ( ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| collect_fun_nat_bool(Pa) != bot_bo1701429464l_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk85])],[f502_nnf]) ).
cnf(c741,plain,
( ~ hBOOL(hAPP_f54304608l_bool(X0,X1))
| collect_fun_nat_bool(X0) != bot_bo1701429464l_bool ),
inference(cnf_transformation,[status(esa)],[f502_sk]) ).
fof(f503,axiom,
! [Pa] :
( collec1974731493e_bool(Pa) = bot_bo1649642514l_bool
<=> ! [X_1] :
( is_fun_pname_bool(X_1)
=> ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_400_Collect__empty__eq) ).
fof(f503_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
& is_fun_pname_bool(X_1) )
| collec1974731493e_bool(Pa) = bot_bo1649642514l_bool )
& ( ! [X_1] :
( ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
| ~ is_fun_pname_bool(X_1) )
| collec1974731493e_bool(Pa) != bot_bo1649642514l_bool ) ),
inference(nnf_transformation,[status(thm)],[f503]) ).
fof(f503_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_f1664156314l_bool(Pa,sk86(Pa)))
& is_fun_pname_bool(sk86(Pa)) )
| collec1974731493e_bool(Pa) = bot_bo1649642514l_bool )
& ( ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
| ~ is_fun_pname_bool(X_1)
| collec1974731493e_bool(Pa) != bot_bo1649642514l_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk86])],[f503_nnf]) ).
cnf(c743,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(X0,X1))
| ~ is_fun_pname_bool(X1)
| collec1974731493e_bool(X0) != bot_bo1649642514l_bool ),
inference(cnf_transformation,[status(esa)],[f503_sk]) ).
fof(f504,axiom,
! [Pa] :
( collect_fun_a_bool(Pa) = bot_bo1389914601l_bool
<=> ! [X_1] :
( is_fun_a_bool(X_1)
=> ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_401_Collect__empty__eq) ).
fof(f504_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
& is_fun_a_bool(X_1) )
| collect_fun_a_bool(Pa) = bot_bo1389914601l_bool )
& ( ! [X_1] :
( ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
| ~ is_fun_a_bool(X_1) )
| collect_fun_a_bool(Pa) != bot_bo1389914601l_bool ) ),
inference(nnf_transformation,[status(thm)],[f504]) ).
fof(f504_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_fun_a_bool_bool(Pa,sk87(Pa)))
& is_fun_a_bool(sk87(Pa)) )
| collect_fun_a_bool(Pa) = bot_bo1389914601l_bool )
& ( ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
| ~ is_fun_a_bool(X_1)
| collect_fun_a_bool(Pa) != bot_bo1389914601l_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk87])],[f504_nnf]) ).
cnf(c746,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(X0,X1))
| ~ is_fun_a_bool(X1)
| collect_fun_a_bool(X0) != bot_bo1389914601l_bool ),
inference(cnf_transformation,[status(esa)],[f504_sk]) ).
fof(f505,axiom,
! [Pa] :
( collect_a(Pa) = bot_bot_fun_a_bool
<=> ! [X_1] :
( is_a(X_1)
=> ~ hBOOL(hAPP_a_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_402_Collect__empty__eq) ).
fof(f505_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_a_bool(Pa,X_1))
& is_a(X_1) )
| collect_a(Pa) = bot_bot_fun_a_bool )
& ( ! [X_1] :
( ~ hBOOL(hAPP_a_bool(Pa,X_1))
| ~ is_a(X_1) )
| collect_a(Pa) != bot_bot_fun_a_bool ) ),
inference(nnf_transformation,[status(thm)],[f505]) ).
fof(f505_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_a_bool(Pa,sk88(Pa)))
& is_a(sk88(Pa)) )
| collect_a(Pa) = bot_bot_fun_a_bool )
& ( ~ hBOOL(hAPP_a_bool(Pa,X_1))
| ~ is_a(X_1)
| collect_a(Pa) != bot_bot_fun_a_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk88])],[f505_nnf]) ).
cnf(c749,plain,
( ~ hBOOL(hAPP_a_bool(X0,X1))
| ~ is_a(X1)
| collect_a(X0) != bot_bot_fun_a_bool ),
inference(cnf_transformation,[status(esa)],[f505_sk]) ).
fof(f506,axiom,
! [Pa] :
( collect_nat(Pa) = bot_bot_fun_nat_bool
<=> ! [X_1] : ~ hBOOL(hAPP_nat_bool(Pa,X_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_403_Collect__empty__eq) ).
fof(f506_nnf,plain,
! [Pa] :
( ( ? [X_1] : hBOOL(hAPP_nat_bool(Pa,X_1))
| collect_nat(Pa) = bot_bot_fun_nat_bool )
& ( ! [X_1] : ~ hBOOL(hAPP_nat_bool(Pa,X_1))
| collect_nat(Pa) != bot_bot_fun_nat_bool ) ),
inference(nnf_transformation,[status(thm)],[f506]) ).
fof(f506_sk,plain,
! [Pa,X_1] :
( ( hBOOL(hAPP_nat_bool(Pa,sk89(Pa)))
| collect_nat(Pa) = bot_bot_fun_nat_bool )
& ( ~ hBOOL(hAPP_nat_bool(Pa,X_1))
| collect_nat(Pa) != bot_bot_fun_nat_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk89])],[f506_nnf]) ).
cnf(c752,plain,
( ~ hBOOL(hAPP_nat_bool(X0,X1))
| collect_nat(X0) != bot_bot_fun_nat_bool ),
inference(cnf_transformation,[status(esa)],[f506_sk]) ).
fof(f507,axiom,
! [C_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_1),bot_bot_fun_nat_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_404_empty__iff) ).
fof(f507_nnf,plain,
! [C_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_1),bot_bot_fun_nat_bool)),
inference(nnf_transformation,[status(thm)],[f507]) ).
fof(f507_sk,plain,
! [C_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_1),bot_bot_fun_nat_bool)),
inference(skolemisation,[status(esa)],[f507_nnf]) ).
cnf(c754,plain,
~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),bot_bot_fun_nat_bool)),
inference(cnf_transformation,[status(esa)],[f507_sk]) ).
fof(f508,axiom,
! [C_1] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_1),bot_bo844097828e_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_405_empty__iff) ).
fof(f508_nnf,plain,
! [C_1] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_1),bot_bo844097828e_bool)),
inference(nnf_transformation,[status(thm)],[f508]) ).
fof(f508_sk,plain,
! [C_1] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_1),bot_bo844097828e_bool)),
inference(skolemisation,[status(esa)],[f508_nnf]) ).
cnf(c755,plain,
~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool)),
inference(cnf_transformation,[status(esa)],[f508_sk]) ).
fof(f509,axiom,
! [C_1] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_1),bot_bot_fun_a_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_406_empty__iff) ).
fof(f509_nnf,plain,
! [C_1] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_1),bot_bot_fun_a_bool)),
inference(nnf_transformation,[status(thm)],[f509]) ).
fof(f509_sk,plain,
! [C_1] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_1),bot_bot_fun_a_bool)),
inference(skolemisation,[status(esa)],[f509_nnf]) ).
cnf(c756,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),bot_bot_fun_a_bool)),
inference(cnf_transformation,[status(esa)],[f509_sk]) ).
fof(f510,axiom,
! [Pa] :
( bot_bo844097828e_bool = collect_pname(Pa)
<=> ! [X_1] :
( is_pname(X_1)
=> ~ hBOOL(hAPP_pname_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_407_empty__Collect__eq) ).
fof(f510_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_pname_bool(Pa,X_1))
& is_pname(X_1) )
| bot_bo844097828e_bool = collect_pname(Pa) )
& ( ! [X_1] :
( ~ hBOOL(hAPP_pname_bool(Pa,X_1))
| ~ is_pname(X_1) )
| bot_bo844097828e_bool != collect_pname(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f510]) ).
fof(f510_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_pname_bool(Pa,sk90(Pa)))
& is_pname(sk90(Pa)) )
| bot_bo844097828e_bool = collect_pname(Pa) )
& ( ~ hBOOL(hAPP_pname_bool(Pa,X_1))
| ~ is_pname(X_1)
| bot_bo844097828e_bool != collect_pname(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk90])],[f510_nnf]) ).
cnf(c757,plain,
( ~ hBOOL(hAPP_pname_bool(X0,X1))
| ~ is_pname(X1)
| bot_bo844097828e_bool != collect_pname(X0) ),
inference(cnf_transformation,[status(esa)],[f510_sk]) ).
fof(f511,axiom,
! [Pa] :
( bot_bo1701429464l_bool = collect_fun_nat_bool(Pa)
<=> ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_408_empty__Collect__eq) ).
fof(f511_nnf,plain,
! [Pa] :
( ( ? [X_1] : hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| bot_bo1701429464l_bool = collect_fun_nat_bool(Pa) )
& ( ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| bot_bo1701429464l_bool != collect_fun_nat_bool(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f511]) ).
fof(f511_sk,plain,
! [Pa,X_1] :
( ( hBOOL(hAPP_f54304608l_bool(Pa,sk91(Pa)))
| bot_bo1701429464l_bool = collect_fun_nat_bool(Pa) )
& ( ~ hBOOL(hAPP_f54304608l_bool(Pa,X_1))
| bot_bo1701429464l_bool != collect_fun_nat_bool(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk91])],[f511_nnf]) ).
cnf(c760,plain,
( ~ hBOOL(hAPP_f54304608l_bool(X0,X1))
| bot_bo1701429464l_bool != collect_fun_nat_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f511_sk]) ).
fof(f512,axiom,
! [Pa] :
( bot_bo1649642514l_bool = collec1974731493e_bool(Pa)
<=> ! [X_1] :
( is_fun_pname_bool(X_1)
=> ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_409_empty__Collect__eq) ).
fof(f512_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
& is_fun_pname_bool(X_1) )
| bot_bo1649642514l_bool = collec1974731493e_bool(Pa) )
& ( ! [X_1] :
( ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
| ~ is_fun_pname_bool(X_1) )
| bot_bo1649642514l_bool != collec1974731493e_bool(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f512]) ).
fof(f512_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_f1664156314l_bool(Pa,sk92(Pa)))
& is_fun_pname_bool(sk92(Pa)) )
| bot_bo1649642514l_bool = collec1974731493e_bool(Pa) )
& ( ~ hBOOL(hAPP_f1664156314l_bool(Pa,X_1))
| ~ is_fun_pname_bool(X_1)
| bot_bo1649642514l_bool != collec1974731493e_bool(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk92])],[f512_nnf]) ).
cnf(c762,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(X0,X1))
| ~ is_fun_pname_bool(X1)
| bot_bo1649642514l_bool != collec1974731493e_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
fof(f513,axiom,
! [Pa] :
( bot_bo1389914601l_bool = collect_fun_a_bool(Pa)
<=> ! [X_1] :
( is_fun_a_bool(X_1)
=> ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_410_empty__Collect__eq) ).
fof(f513_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
& is_fun_a_bool(X_1) )
| bot_bo1389914601l_bool = collect_fun_a_bool(Pa) )
& ( ! [X_1] :
( ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
| ~ is_fun_a_bool(X_1) )
| bot_bo1389914601l_bool != collect_fun_a_bool(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f513]) ).
fof(f513_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_fun_a_bool_bool(Pa,sk93(Pa)))
& is_fun_a_bool(sk93(Pa)) )
| bot_bo1389914601l_bool = collect_fun_a_bool(Pa) )
& ( ~ hBOOL(hAPP_fun_a_bool_bool(Pa,X_1))
| ~ is_fun_a_bool(X_1)
| bot_bo1389914601l_bool != collect_fun_a_bool(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk93])],[f513_nnf]) ).
cnf(c765,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(X0,X1))
| ~ is_fun_a_bool(X1)
| bot_bo1389914601l_bool != collect_fun_a_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f513_sk]) ).
fof(f514,axiom,
! [Pa] :
( bot_bot_fun_a_bool = collect_a(Pa)
<=> ! [X_1] :
( is_a(X_1)
=> ~ hBOOL(hAPP_a_bool(Pa,X_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_411_empty__Collect__eq) ).
fof(f514_nnf,plain,
! [Pa] :
( ( ? [X_1] :
( hBOOL(hAPP_a_bool(Pa,X_1))
& is_a(X_1) )
| bot_bot_fun_a_bool = collect_a(Pa) )
& ( ! [X_1] :
( ~ hBOOL(hAPP_a_bool(Pa,X_1))
| ~ is_a(X_1) )
| bot_bot_fun_a_bool != collect_a(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f514]) ).
fof(f514_sk,plain,
! [Pa,X_1] :
( ( ( hBOOL(hAPP_a_bool(Pa,sk94(Pa)))
& is_a(sk94(Pa)) )
| bot_bot_fun_a_bool = collect_a(Pa) )
& ( ~ hBOOL(hAPP_a_bool(Pa,X_1))
| ~ is_a(X_1)
| bot_bot_fun_a_bool != collect_a(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk94])],[f514_nnf]) ).
cnf(c768,plain,
( ~ hBOOL(hAPP_a_bool(X0,X1))
| ~ is_a(X1)
| bot_bot_fun_a_bool != collect_a(X0) ),
inference(cnf_transformation,[status(esa)],[f514_sk]) ).
fof(f515,axiom,
! [Pa] :
( bot_bot_fun_nat_bool = collect_nat(Pa)
<=> ! [X_1] : ~ hBOOL(hAPP_nat_bool(Pa,X_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_412_empty__Collect__eq) ).
fof(f515_nnf,plain,
! [Pa] :
( ( ? [X_1] : hBOOL(hAPP_nat_bool(Pa,X_1))
| bot_bot_fun_nat_bool = collect_nat(Pa) )
& ( ! [X_1] : ~ hBOOL(hAPP_nat_bool(Pa,X_1))
| bot_bot_fun_nat_bool != collect_nat(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f515]) ).
fof(f515_sk,plain,
! [Pa,X_1] :
( ( hBOOL(hAPP_nat_bool(Pa,sk95(Pa)))
| bot_bot_fun_nat_bool = collect_nat(Pa) )
& ( ~ hBOOL(hAPP_nat_bool(Pa,X_1))
| bot_bot_fun_nat_bool != collect_nat(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95])],[f515_nnf]) ).
cnf(c771,plain,
( ~ hBOOL(hAPP_nat_bool(X0,X1))
| bot_bot_fun_nat_bool != collect_nat(X0) ),
inference(cnf_transformation,[status(esa)],[f515_sk]) ).
fof(f516,axiom,
! [A_1] :
( ? [X_1] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1))
<=> A_1 != bot_bot_fun_nat_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_413_ex__in__conv) ).
fof(f516_nnf,plain,
! [A_1] :
( ( A_1 = bot_bot_fun_nat_bool
| ? [X_1] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) )
& ( A_1 != bot_bot_fun_nat_bool
| ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) ) ),
inference(nnf_transformation,[status(thm)],[f516]) ).
fof(f516_sk,plain,
! [X_1,A_1] :
( ( A_1 = bot_bot_fun_nat_bool
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,sk96(A_1)),A_1)) )
& ( A_1 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk96])],[f516_nnf]) ).
cnf(c773,plain,
( X0 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f516_sk]) ).
fof(f517,axiom,
! [A_1] :
( is_fun_pname_bool(A_1)
=> ( ? [X_1] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
& is_pname(X_1) )
<=> A_1 != bot_bo844097828e_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_414_ex__in__conv) ).
fof(f517_nnf,plain,
! [A_1] :
( ( ( A_1 = bot_bo844097828e_bool
| ? [X_1] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
& is_pname(X_1) ) )
& ( A_1 != bot_bo844097828e_bool
| ! [X_1] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
| ~ is_pname(X_1) ) ) )
| ~ is_fun_pname_bool(A_1) ),
inference(nnf_transformation,[status(thm)],[f517]) ).
fof(f517_sk,plain,
! [A_1,X_1] :
( ( ( A_1 = bot_bo844097828e_bool
| ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,sk97(A_1)),A_1))
& is_pname(sk97(A_1)) ) )
& ( A_1 != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
| ~ is_pname(X_1) ) )
| ~ is_fun_pname_bool(A_1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk97])],[f517_nnf]) ).
cnf(c775,plain,
( X0 != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X1),X0))
| ~ is_pname(X1)
| ~ is_fun_pname_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f517_sk]) ).
fof(f518,axiom,
! [A_1] :
( is_fun_a_bool(A_1)
=> ( ? [X_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
& is_a(X_1) )
<=> A_1 != bot_bot_fun_a_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_415_ex__in__conv) ).
fof(f518_nnf,plain,
! [A_1] :
( ( ( A_1 = bot_bot_fun_a_bool
| ? [X_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
& is_a(X_1) ) )
& ( A_1 != bot_bot_fun_a_bool
| ! [X_1] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
| ~ is_a(X_1) ) ) )
| ~ is_fun_a_bool(A_1) ),
inference(nnf_transformation,[status(thm)],[f518]) ).
fof(f518_sk,plain,
! [A_1,X_1] :
( ( ( A_1 = bot_bot_fun_a_bool
| ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,sk98(A_1)),A_1))
& is_a(sk98(A_1)) ) )
& ( A_1 != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
| ~ is_a(X_1) ) )
| ~ is_fun_a_bool(A_1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk98])],[f518_nnf]) ).
cnf(c778,plain,
( X0 != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X1),X0))
| ~ is_a(X1)
| ~ is_fun_a_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f518_sk]) ).
fof(f519,axiom,
! [A_1] :
( ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1))
<=> A_1 = bot_bot_fun_nat_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_416_all__not__in__conv) ).
fof(f519_nnf,plain,
! [A_1] :
( ( A_1 != bot_bot_fun_nat_bool
| ! [X_1] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) )
& ( A_1 = bot_bot_fun_nat_bool
| ? [X_1] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) ) ),
inference(nnf_transformation,[status(thm)],[f519]) ).
fof(f519_sk,plain,
! [A_1,X_1] :
( ( A_1 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_1),A_1)) )
& ( A_1 = bot_bot_fun_nat_bool
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,sk99(A_1)),A_1)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk99])],[f519_nnf]) ).
cnf(c782,plain,
( X0 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f519_sk]) ).
fof(f520,axiom,
! [A_1] :
( is_fun_pname_bool(A_1)
=> ( ! [X_1] :
( is_pname(X_1)
=> ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1)) )
<=> A_1 = bot_bo844097828e_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_417_all__not__in__conv) ).
fof(f520_nnf,plain,
! [A_1] :
( ( ( A_1 != bot_bo844097828e_bool
| ! [X_1] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
| ~ is_pname(X_1) ) )
& ( A_1 = bot_bo844097828e_bool
| ? [X_1] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
& is_pname(X_1) ) ) )
| ~ is_fun_pname_bool(A_1) ),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [A_1,X_1] :
( ( ( A_1 != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A_1))
| ~ is_pname(X_1) )
& ( A_1 = bot_bo844097828e_bool
| ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,sk100(A_1)),A_1))
& is_pname(sk100(A_1)) ) ) )
| ~ is_fun_pname_bool(A_1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk100])],[f520_nnf]) ).
cnf(c785,plain,
( X0 != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X1),X0))
| ~ is_pname(X1)
| ~ is_fun_pname_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
fof(f521,axiom,
! [A_1] :
( is_fun_a_bool(A_1)
=> ( ! [X_1] :
( is_a(X_1)
=> ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1)) )
<=> A_1 = bot_bot_fun_a_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_418_all__not__in__conv) ).
fof(f521_nnf,plain,
! [A_1] :
( ( ( A_1 != bot_bot_fun_a_bool
| ! [X_1] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
| ~ is_a(X_1) ) )
& ( A_1 = bot_bot_fun_a_bool
| ? [X_1] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
& is_a(X_1) ) ) )
| ~ is_fun_a_bool(A_1) ),
inference(nnf_transformation,[status(thm)],[f521]) ).
fof(f521_sk,plain,
! [A_1,X_1] :
( ( ( A_1 != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),A_1))
| ~ is_a(X_1) )
& ( A_1 = bot_bot_fun_a_bool
| ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,sk101(A_1)),A_1))
& is_a(sk101(A_1)) ) ) )
| ~ is_fun_a_bool(A_1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk101])],[f521_nnf]) ).
cnf(c788,plain,
( X0 != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X1),X0))
| ~ is_a(X1)
| ~ is_fun_a_bool(X0) ),
inference(cnf_transformation,[status(esa)],[f521_sk]) ).
fof(f561,axiom,
! [A_3,A_1] : insert_pname(A_3,A_1) != bot_bo844097828e_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_458_insert__not__empty) ).
fof(f561_nnf,plain,
! [A_3,A_1] : insert_pname(A_3,A_1) != bot_bo844097828e_bool,
inference(nnf_transformation,[status(thm)],[f561]) ).
fof(f561_sk,plain,
! [A_3,A_1] : insert_pname(A_3,A_1) != bot_bo844097828e_bool,
inference(skolemisation,[status(esa)],[f561_nnf]) ).
cnf(c862,plain,
insert_pname(X0,X1) != bot_bo844097828e_bool,
inference(cnf_transformation,[status(esa)],[f561_sk]) ).
fof(f562,axiom,
! [A_3,A_1] : insert_nat(A_3,A_1) != bot_bot_fun_nat_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_459_insert__not__empty) ).
fof(f562_nnf,plain,
! [A_3,A_1] : insert_nat(A_3,A_1) != bot_bot_fun_nat_bool,
inference(nnf_transformation,[status(thm)],[f562]) ).
fof(f562_sk,plain,
! [A_3,A_1] : insert_nat(A_3,A_1) != bot_bot_fun_nat_bool,
inference(skolemisation,[status(esa)],[f562_nnf]) ).
cnf(c863,plain,
insert_nat(X0,X1) != bot_bot_fun_nat_bool,
inference(cnf_transformation,[status(esa)],[f562_sk]) ).
fof(f563,axiom,
! [A_3,A_1] : insert_a(A_3,A_1) != bot_bot_fun_a_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_460_insert__not__empty) ).
fof(f563_nnf,plain,
! [A_3,A_1] : insert_a(A_3,A_1) != bot_bot_fun_a_bool,
inference(nnf_transformation,[status(thm)],[f563]) ).
fof(f563_sk,plain,
! [A_3,A_1] : insert_a(A_3,A_1) != bot_bot_fun_a_bool,
inference(skolemisation,[status(esa)],[f563_nnf]) ).
cnf(c864,plain,
insert_a(X0,X1) != bot_bot_fun_a_bool,
inference(cnf_transformation,[status(esa)],[f563_sk]) ).
fof(f564,axiom,
! [A_3,A_1] : bot_bo844097828e_bool != insert_pname(A_3,A_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_461_empty__not__insert) ).
fof(f564_nnf,plain,
! [A_3,A_1] : bot_bo844097828e_bool != insert_pname(A_3,A_1),
inference(nnf_transformation,[status(thm)],[f564]) ).
fof(f564_sk,plain,
! [A_3,A_1] : bot_bo844097828e_bool != insert_pname(A_3,A_1),
inference(skolemisation,[status(esa)],[f564_nnf]) ).
cnf(c865,plain,
bot_bo844097828e_bool != insert_pname(X0,X1),
inference(cnf_transformation,[status(esa)],[f564_sk]) ).
fof(f565,axiom,
! [A_3,A_1] : bot_bot_fun_nat_bool != insert_nat(A_3,A_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_462_empty__not__insert) ).
fof(f565_nnf,plain,
! [A_3,A_1] : bot_bot_fun_nat_bool != insert_nat(A_3,A_1),
inference(nnf_transformation,[status(thm)],[f565]) ).
fof(f565_sk,plain,
! [A_3,A_1] : bot_bot_fun_nat_bool != insert_nat(A_3,A_1),
inference(skolemisation,[status(esa)],[f565_nnf]) ).
cnf(c866,plain,
bot_bot_fun_nat_bool != insert_nat(X0,X1),
inference(cnf_transformation,[status(esa)],[f565_sk]) ).
fof(f566,axiom,
! [A_3,A_1] : bot_bot_fun_a_bool != insert_a(A_3,A_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_463_empty__not__insert) ).
fof(f566_nnf,plain,
! [A_3,A_1] : bot_bot_fun_a_bool != insert_a(A_3,A_1),
inference(nnf_transformation,[status(thm)],[f566]) ).
fof(f566_sk,plain,
! [A_3,A_1] : bot_bot_fun_a_bool != insert_a(A_3,A_1),
inference(skolemisation,[status(esa)],[f566_nnf]) ).
cnf(c867,plain,
bot_bot_fun_a_bool != insert_a(X0,X1),
inference(cnf_transformation,[status(esa)],[f566_sk]) ).
fof(f727,axiom,
! [J_2,I] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(J_2),I)),I)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_624_not__add__less2) ).
fof(f727_nnf,plain,
! [J_2,I] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(J_2),I)),I)),
inference(nnf_transformation,[status(thm)],[f727]) ).
fof(f727_sk,plain,
! [J_2,I] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(J_2),I)),I)),
inference(skolemisation,[status(esa)],[f727_nnf]) ).
cnf(c1144,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(X0),X1)),X1)),
inference(cnf_transformation,[status(esa)],[f727_sk]) ).
fof(f728,axiom,
! [I,J_2] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(I),J_2)),I)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_625_not__add__less1) ).
fof(f728_nnf,plain,
! [I,J_2] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(I),J_2)),I)),
inference(nnf_transformation,[status(thm)],[f728]) ).
fof(f728_sk,plain,
! [I,J_2] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(I),J_2)),I)),
inference(skolemisation,[status(esa)],[f728_nnf]) ).
cnf(c1145,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(plus_plus_nat(X0),X1)),X0)),
inference(cnf_transformation,[status(esa)],[f728_sk]) ).
fof(f739,axiom,
! [M_1,Na] :
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na))
<=> hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M_1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_636_not__less__eq) ).
fof(f739_nnf,plain,
! [M_1,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M_1)))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M_1)))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f739]) ).
fof(f739_sk,plain,
! [M_1,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M_1)))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M_1)))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) ) ),
inference(skolemisation,[status(esa)],[f739_nnf]) ).
cnf(c1161,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X1),hAPP_nat_nat(suc,X0)))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f739_sk]) ).
fof(f744,axiom,
! [M_1,Na] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na))
<=> ( M_1 != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_641_nat__less__le) ).
fof(f744_nnf,plain,
! [M_1,Na] :
( ( M_1 = Na
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
& ( ( M_1 != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) )
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f744]) ).
fof(f744_sk,plain,
! [M_1,Na] :
( ( M_1 = Na
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
& ( ( M_1 != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M_1),Na)) )
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) ) ),
inference(skolemisation,[status(esa)],[f744_nnf]) ).
cnf(c1170,plain,
( X0 != X1
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f744_sk]) ).
fof(f748,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_645_less__not__refl) ).
fof(f748_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(nnf_transformation,[status(thm)],[f748]) ).
fof(f748_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(skolemisation,[status(esa)],[f748_nnf]) ).
cnf(c1175,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X0)),
inference(cnf_transformation,[status(esa)],[f748_sk]) ).
fof(f749,axiom,
! [M_1,Na] :
( M_1 != Na
<=> ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M_1))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_646_nat__neq__iff) ).
fof(f749_nnf,plain,
! [M_1,Na] :
( ( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M_1))
& ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
| M_1 != Na )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M_1))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na))
| M_1 = Na ) ),
inference(nnf_transformation,[status(thm)],[f749]) ).
fof(f749_sk,plain,
! [M_1,Na] :
( ( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M_1))
& ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na)) )
| M_1 != Na )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M_1))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),Na))
| M_1 = Na ) ),
inference(skolemisation,[status(esa)],[f749_nnf]) ).
cnf(c1177,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1))
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f749_sk]) ).
cnf(c1178,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X1),X0))
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f749_sk]) ).
fof(f751,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_648_less__irrefl__nat) ).
fof(f751_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(nnf_transformation,[status(thm)],[f751]) ).
fof(f751_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(skolemisation,[status(esa)],[f751_nnf]) ).
cnf(c1180,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X0)),
inference(cnf_transformation,[status(esa)],[f751_sk]) ).
fof(f752,axiom,
! [N,M] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M))
=> M != N ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_649_less__not__refl2) ).
fof(f752_nnf,plain,
! [N,M] :
( M != N
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M)) ),
inference(nnf_transformation,[status(thm)],[f752]) ).
fof(f752_sk,plain,
! [N,M] :
( M != N
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M)) ),
inference(skolemisation,[status(esa)],[f752_nnf]) ).
cnf(c1181,plain,
( X1 != X0
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f752_sk]) ).
fof(f753,axiom,
! [S,T] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,S),T))
=> S != T ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_650_less__not__refl3) ).
fof(f753_nnf,plain,
! [S,T] :
( S != T
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,S),T)) ),
inference(nnf_transformation,[status(thm)],[f753]) ).
fof(f753_sk,plain,
! [S,T] :
( S != T
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,S),T)) ),
inference(skolemisation,[status(esa)],[f753_nnf]) ).
cnf(c1182,plain,
( X0 != X1
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f753_sk]) ).
fof(f781,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_678_less__zeroE) ).
fof(f781_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(nnf_transformation,[status(thm)],[f781]) ).
fof(f781_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(skolemisation,[status(esa)],[f781_nnf]) ).
cnf(c1233,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),zero_zero_nat)),
inference(cnf_transformation,[status(esa)],[f781_sk]) ).
fof(f794,axiom,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_691_Suc__neq__Zero) ).
fof(f794_nnf,plain,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f794]) ).
fof(f794_sk,plain,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f794_nnf]) ).
cnf(c1257,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f794_sk]) ).
fof(f795,axiom,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_692_Zero__neq__Suc) ).
fof(f795_nnf,plain,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
inference(nnf_transformation,[status(thm)],[f795]) ).
fof(f795_sk,plain,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
inference(skolemisation,[status(esa)],[f795_nnf]) ).
cnf(c1258,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f795_sk]) ).
fof(f796,axiom,
! [Nat_1] : hAPP_nat_nat(suc,Nat_1) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_693_nat_Osimps_I3_J) ).
fof(f796_nnf,plain,
! [Nat_1] : hAPP_nat_nat(suc,Nat_1) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f796]) ).
fof(f796_sk,plain,
! [Nat_1] : hAPP_nat_nat(suc,Nat_1) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f796_nnf]) ).
cnf(c1259,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f796_sk]) ).
fof(f797,axiom,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_694_Suc__not__Zero) ).
fof(f797_nnf,plain,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f797]) ).
fof(f797_sk,plain,
! [M] : hAPP_nat_nat(suc,M) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f797_nnf]) ).
cnf(c1260,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f797_sk]) ).
fof(f798,axiom,
! [Nat] : zero_zero_nat != hAPP_nat_nat(suc,Nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_695_nat_Osimps_I2_J) ).
fof(f798_nnf,plain,
! [Nat] : zero_zero_nat != hAPP_nat_nat(suc,Nat),
inference(nnf_transformation,[status(thm)],[f798]) ).
fof(f798_sk,plain,
! [Nat] : zero_zero_nat != hAPP_nat_nat(suc,Nat),
inference(skolemisation,[status(esa)],[f798_nnf]) ).
cnf(c1261,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f798_sk]) ).
fof(f799,axiom,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_696_Zero__not__Suc) ).
fof(f799_nnf,plain,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
inference(nnf_transformation,[status(thm)],[f799]) ).
fof(f799_sk,plain,
! [M] : zero_zero_nat != hAPP_nat_nat(suc,M),
inference(skolemisation,[status(esa)],[f799_nnf]) ).
cnf(c1262,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f799_sk]) ).
fof(f803,axiom,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fNot_1_1_U) ).
fof(f803_nnf,plain,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
inference(nnf_transformation,[status(thm)],[f803]) ).
fof(f803_sk,plain,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
inference(skolemisation,[status(esa)],[f803_nnf]) ).
cnf(c1267,plain,
( ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(fNot,X0)) ),
inference(cnf_transformation,[status(esa)],[f803_sk]) ).
fof(f811,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f811_nnf,plain,
~ hBOOL(fFalse),
inference(nnf_transformation,[status(thm)],[f811]) ).
fof(f811_sk,plain,
~ hBOOL(fFalse),
inference(skolemisation,[status(esa)],[f811_nnf]) ).
cnf(c1275,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(esa)],[f811_sk]) ).
fof(f915,hypothesis,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_5) ).
fof(f915_nnf,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
inference(nnf_transformation,[status(thm)],[f915]) ).
fof(f915_sk,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
inference(skolemisation,[status(esa)],[f915_nnf]) ).
cnf(c1379,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
inference(cnf_transformation,[status(esa)],[f915_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c199,c200,c258,c259,c723,c724,c725,c735,c736,c737,c738,c741,c743,c746,c749,c752,c754,c755,c756,c757,c760,c762,c765,c768,c771,c773,c775,c778,c782,c785,c788,c862,c863,c864,c865,c866,c867,c1144,c1145,c1161,c1170,c1175,c1177,c1178,c1180,c1181,c1182,c1233,c1257,c1258,c1259,c1260,c1261,c1262,c1267,c1275,c1379,c1380]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3205]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW473+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n013.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Thu Sep 24 22:33:07 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 113.86/15.15 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.86/15.15 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------