%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW473+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:13 PM UTC 2026
% Result : Theorem 182.78s 24.57s
% Output : Proof 182.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 90
% Syntax : Number of formulae : 380 ( 203 unt; 0 def)
% Number of atoms : 766 ( 236 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 912 ( 526 ~; 234 |; 97 &)
% ( 26 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 97 ( 97 usr; 39 con; 0-4 aty)
% Number of variables : 605 ( 63 sgn 422 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f559,axiom,
! [X_1,A,B] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X_1),A)),B))
<=> ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_453_insert__subset) ).
fof(f559_nnf,plain,
! [X_1,A,B] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),B))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X_1),A)),B)) )
& ( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),B)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X_1),A)),B)) ) ),
inference(nnf_transformation,[status(thm)],[f559]) ).
fof(f559_sk,plain,
! [X_1,A,B] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),B))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X_1),A)),B)) )
& ( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_1),B)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X_1),A)),B)) ) ),
inference(skolemisation,[status(esa)],[f559_nnf]) ).
cnf(c790,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,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X0),X1)),X2)) ),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(t176,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,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X1),X3)),X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c790]) ).
cnf(t236,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,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X1),X3)),X2)),true),true) = true,
inference(orient,[status(thm)],[t176]) ).
fof(f1414,conjecture,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_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(f1414_neg,negated_conjecture,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(negated_conjecture,[status(cth)],[f1414]) ).
fof(f1414_nnf,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(nnf_transformation,[status(thm)],[f1414_neg]) ).
fof(f1414_sk,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(skolemisation,[status(esa)],[f1414_nnf]) ).
cnf(c2238,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))),
inference(cnf_transformation,[status(esa)],[f1414_sk]) ).
cnf(t83,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))) = false,
inference(equality_encoding,[status(esa)],[c2238]) ).
cnf(t836,plain,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,hAPP_pname_a(mgt_call,pn)),g)),image_pname_a(mgt_call,u))) = false,
inference(orient,[status(thm)],[t83]) ).
cnf(t865,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)],[t236,t836]) ).
fof(f540,axiom,
! [F,X_1,A] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_434_imageI) ).
fof(f540_nnf,plain,
! [F,X_1,A] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A)))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A)) ),
inference(nnf_transformation,[status(thm)],[f540]) ).
fof(f540_sk,plain,
! [X_1,A,F] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(F,X_1)),image_pname_a(F,A)))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_1),A)) ),
inference(skolemisation,[status(esa)],[f540_nnf]) ).
cnf(c765,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)],[f540_sk]) ).
cnf(t101,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)],[c765]) ).
cnf(t286,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)],[t101]) ).
fof(f1412,hypothesis,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_4) ).
fof(f1412_nnf,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(nnf_transformation,[status(thm)],[f1412]) ).
cnf(c2236,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)),
inference(cnf_transformation,[status(esa)],[f1412_nnf]) ).
cnf(t30,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)) = true,
inference(equality_encoding,[status(esa)],[c2236]) ).
cnf(t545,plain,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)) = true,
inference(orient,[status(thm)],[t30]) ).
cnf(t549,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)],[t286,t545]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t205,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t2105,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)],[t549,t205]) ).
cnf(t1395,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)],[t2105]) ).
cnf(t2188,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)],[t865,t1395]) ).
cnf(t2189,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)],[t2188,t205]) ).
fof(f1409,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(f1409_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)],[f1409]) ).
cnf(c2233,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)],[f1409_nnf]) ).
cnf(t46,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)],[c2233]) ).
cnf(t490,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)],[t46]) ).
cnf(t2190,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t2189,t490]) ).
cnf(t2191,plain,
true = false,
inference(step,[status(thm)],[t2190,t205]) ).
cnf(t2011,plain,
false = true,
inference(orient,[status(thm)],[t2191]) ).
fof(f230,axiom,
! [N] : hAPP_nat_nat(suc,N) != N,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_Suc__n__not__n) ).
fof(f230_nnf,plain,
! [N] : hAPP_nat_nat(suc,N) != N,
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [N] : hAPP_nat_nat(suc,N) != N,
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c247,plain,
hAPP_nat_nat(suc,X0) != X0,
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
fof(f231,axiom,
! [N] : N != hAPP_nat_nat(suc,N),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_n__not__Suc__n) ).
fof(f231_nnf,plain,
! [N] : N != hAPP_nat_nat(suc,N),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
! [N] : N != hAPP_nat_nat(suc,N),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c248,plain,
X0 != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
fof(f275,axiom,
! [M,Na] :
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na))
<=> hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_not__less__eq__eq) ).
fof(f275_nnf,plain,
! [M,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [M,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,Na)),M))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) ) ),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c320,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)],[f275_sk]) ).
fof(f276,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_170_Suc__n__not__le__n) ).
fof(f276_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)],[f276]) ).
fof(f276_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,N)),N)),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c321,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,hAPP_nat_nat(suc,X0)),X0)),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
fof(f596,axiom,
! [A_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),bot_bot_fun_int_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_490_emptyE) ).
fof(f596_nnf,plain,
! [A_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),bot_bot_fun_int_bool)),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
! [A_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),bot_bot_fun_int_bool)),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c861,plain,
~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),bot_bot_fun_int_bool)),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
fof(f597,axiom,
! [A_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),bot_bot_fun_nat_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_491_emptyE) ).
fof(f597_nnf,plain,
! [A_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),bot_bot_fun_nat_bool)),
inference(nnf_transformation,[status(thm)],[f597]) ).
fof(f597_sk,plain,
! [A_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),bot_bot_fun_nat_bool)),
inference(skolemisation,[status(esa)],[f597_nnf]) ).
cnf(c862,plain,
~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),bot_bot_fun_nat_bool)),
inference(cnf_transformation,[status(esa)],[f597_sk]) ).
fof(f598,axiom,
! [A_2] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),bot_bot_fun_a_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_492_emptyE) ).
fof(f598_nnf,plain,
! [A_2] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),bot_bot_fun_a_bool)),
inference(nnf_transformation,[status(thm)],[f598]) ).
fof(f598_sk,plain,
! [A_2] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),bot_bot_fun_a_bool)),
inference(skolemisation,[status(esa)],[f598_nnf]) ).
cnf(c863,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),bot_bot_fun_a_bool)),
inference(cnf_transformation,[status(esa)],[f598_sk]) ).
fof(f599,axiom,
! [A_2] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),bot_bo844097828e_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_493_emptyE) ).
fof(f599_nnf,plain,
! [A_2] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),bot_bo844097828e_bool)),
inference(nnf_transformation,[status(thm)],[f599]) ).
fof(f599_sk,plain,
! [A_2] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),bot_bo844097828e_bool)),
inference(skolemisation,[status(esa)],[f599_nnf]) ).
cnf(c864,plain,
~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool)),
inference(cnf_transformation,[status(esa)],[f599_sk]) ).
fof(f610,axiom,
! [A_2,A] :
( A = bot_bot_fun_int_bool
=> ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_504_equals0D) ).
fof(f610_nnf,plain,
! [A_2,A] :
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),A))
| A != bot_bot_fun_int_bool ),
inference(nnf_transformation,[status(thm)],[f610]) ).
fof(f610_sk,plain,
! [A,A_2] :
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,A_2),A))
| A != bot_bot_fun_int_bool ),
inference(skolemisation,[status(esa)],[f610_nnf]) ).
cnf(c875,plain,
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),X1))
| X1 != bot_bot_fun_int_bool ),
inference(cnf_transformation,[status(esa)],[f610_sk]) ).
fof(f611,axiom,
! [A_2,A] :
( A = bot_bot_fun_nat_bool
=> ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_505_equals0D) ).
fof(f611_nnf,plain,
! [A_2,A] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),A))
| A != bot_bot_fun_nat_bool ),
inference(nnf_transformation,[status(thm)],[f611]) ).
fof(f611_sk,plain,
! [A,A_2] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,A_2),A))
| A != bot_bot_fun_nat_bool ),
inference(skolemisation,[status(esa)],[f611_nnf]) ).
cnf(c876,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),X1))
| X1 != bot_bot_fun_nat_bool ),
inference(cnf_transformation,[status(esa)],[f611_sk]) ).
fof(f612,axiom,
! [A_2,A] :
( A = bot_bot_fun_a_bool
=> ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_506_equals0D) ).
fof(f612_nnf,plain,
! [A_2,A] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),A))
| A != bot_bot_fun_a_bool ),
inference(nnf_transformation,[status(thm)],[f612]) ).
fof(f612_sk,plain,
! [A,A_2] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,A_2),A))
| A != bot_bot_fun_a_bool ),
inference(skolemisation,[status(esa)],[f612_nnf]) ).
cnf(c877,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)],[f612_sk]) ).
fof(f613,axiom,
! [A_2,A] :
( A = bot_bo844097828e_bool
=> ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_507_equals0D) ).
fof(f613_nnf,plain,
! [A_2,A] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),A))
| A != bot_bo844097828e_bool ),
inference(nnf_transformation,[status(thm)],[f613]) ).
fof(f613_sk,plain,
! [A,A_2] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,A_2),A))
| A != bot_bo844097828e_bool ),
inference(skolemisation,[status(esa)],[f613_nnf]) ).
cnf(c878,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1))
| X1 != bot_bo844097828e_bool ),
inference(cnf_transformation,[status(esa)],[f613_sk]) ).
fof(f614,axiom,
! [Pa] :
( collect_int(Pa) = bot_bot_fun_int_bool
<=> ! [X_2] : ~ hBOOL(hAPP_int_bool(Pa,X_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_508_Collect__empty__eq) ).
fof(f614_nnf,plain,
! [Pa] :
( ( ? [X_2] : hBOOL(hAPP_int_bool(Pa,X_2))
| collect_int(Pa) = bot_bot_fun_int_bool )
& ( ! [X_2] : ~ hBOOL(hAPP_int_bool(Pa,X_2))
| collect_int(Pa) != bot_bot_fun_int_bool ) ),
inference(nnf_transformation,[status(thm)],[f614]) ).
fof(f614_sk,plain,
! [Pa,X_2] :
( ( hBOOL(hAPP_int_bool(Pa,sk86(Pa)))
| collect_int(Pa) = bot_bot_fun_int_bool )
& ( ~ hBOOL(hAPP_int_bool(Pa,X_2))
| collect_int(Pa) != bot_bot_fun_int_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk86])],[f614_nnf]) ).
cnf(c879,plain,
( ~ hBOOL(hAPP_int_bool(X0,X1))
| collect_int(X0) != bot_bot_fun_int_bool ),
inference(cnf_transformation,[status(esa)],[f614_sk]) ).
fof(f615,axiom,
! [Pa] :
( collect_nat(Pa) = bot_bot_fun_nat_bool
<=> ! [X_2] : ~ hBOOL(hAPP_nat_bool(Pa,X_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_509_Collect__empty__eq) ).
fof(f615_nnf,plain,
! [Pa] :
( ( ? [X_2] : hBOOL(hAPP_nat_bool(Pa,X_2))
| collect_nat(Pa) = bot_bot_fun_nat_bool )
& ( ! [X_2] : ~ hBOOL(hAPP_nat_bool(Pa,X_2))
| collect_nat(Pa) != bot_bot_fun_nat_bool ) ),
inference(nnf_transformation,[status(thm)],[f615]) ).
fof(f615_sk,plain,
! [Pa,X_2] :
( ( hBOOL(hAPP_nat_bool(Pa,sk87(Pa)))
| collect_nat(Pa) = bot_bot_fun_nat_bool )
& ( ~ hBOOL(hAPP_nat_bool(Pa,X_2))
| collect_nat(Pa) != bot_bot_fun_nat_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk87])],[f615_nnf]) ).
cnf(c881,plain,
( ~ hBOOL(hAPP_nat_bool(X0,X1))
| collect_nat(X0) != bot_bot_fun_nat_bool ),
inference(cnf_transformation,[status(esa)],[f615_sk]) ).
fof(f616,axiom,
! [Pa] :
( collect_a(Pa) = bot_bot_fun_a_bool
<=> ! [X_2] :
( is_a(X_2)
=> ~ hBOOL(hAPP_a_bool(Pa,X_2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_510_Collect__empty__eq) ).
fof(f616_nnf,plain,
! [Pa] :
( ( ? [X_2] :
( hBOOL(hAPP_a_bool(Pa,X_2))
& is_a(X_2) )
| collect_a(Pa) = bot_bot_fun_a_bool )
& ( ! [X_2] :
( ~ hBOOL(hAPP_a_bool(Pa,X_2))
| ~ is_a(X_2) )
| collect_a(Pa) != bot_bot_fun_a_bool ) ),
inference(nnf_transformation,[status(thm)],[f616]) ).
fof(f616_sk,plain,
! [Pa,X_2] :
( ( ( 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_2))
| ~ is_a(X_2)
| collect_a(Pa) != bot_bot_fun_a_bool ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk88])],[f616_nnf]) ).
cnf(c883,plain,
( ~ hBOOL(hAPP_a_bool(X0,X1))
| ~ is_a(X1)
| collect_a(X0) != bot_bot_fun_a_bool ),
inference(cnf_transformation,[status(esa)],[f616_sk]) ).
fof(f623,axiom,
! [C_6] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),bot_bot_fun_int_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_517_empty__iff) ).
fof(f623_nnf,plain,
! [C_6] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),bot_bot_fun_int_bool)),
inference(nnf_transformation,[status(thm)],[f623]) ).
fof(f623_sk,plain,
! [C_6] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),bot_bot_fun_int_bool)),
inference(skolemisation,[status(esa)],[f623_nnf]) ).
cnf(c892,plain,
~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),bot_bot_fun_int_bool)),
inference(cnf_transformation,[status(esa)],[f623_sk]) ).
fof(f624,axiom,
! [C_6] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),bot_bot_fun_nat_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_518_empty__iff) ).
fof(f624_nnf,plain,
! [C_6] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),bot_bot_fun_nat_bool)),
inference(nnf_transformation,[status(thm)],[f624]) ).
fof(f624_sk,plain,
! [C_6] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),bot_bot_fun_nat_bool)),
inference(skolemisation,[status(esa)],[f624_nnf]) ).
cnf(c893,plain,
~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),bot_bot_fun_nat_bool)),
inference(cnf_transformation,[status(esa)],[f624_sk]) ).
fof(f625,axiom,
! [C_6] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),bot_bot_fun_a_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_519_empty__iff) ).
fof(f625_nnf,plain,
! [C_6] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),bot_bot_fun_a_bool)),
inference(nnf_transformation,[status(thm)],[f625]) ).
fof(f625_sk,plain,
! [C_6] : ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),bot_bot_fun_a_bool)),
inference(skolemisation,[status(esa)],[f625_nnf]) ).
cnf(c894,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),bot_bot_fun_a_bool)),
inference(cnf_transformation,[status(esa)],[f625_sk]) ).
fof(f626,axiom,
! [C_6] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),bot_bo844097828e_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_520_empty__iff) ).
fof(f626_nnf,plain,
! [C_6] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),bot_bo844097828e_bool)),
inference(nnf_transformation,[status(thm)],[f626]) ).
fof(f626_sk,plain,
! [C_6] : ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),bot_bo844097828e_bool)),
inference(skolemisation,[status(esa)],[f626_nnf]) ).
cnf(c895,plain,
~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),bot_bo844097828e_bool)),
inference(cnf_transformation,[status(esa)],[f626_sk]) ).
fof(f627,axiom,
! [Pa] :
( bot_bot_fun_int_bool = collect_int(Pa)
<=> ! [X_2] : ~ hBOOL(hAPP_int_bool(Pa,X_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_521_empty__Collect__eq) ).
fof(f627_nnf,plain,
! [Pa] :
( ( ? [X_2] : hBOOL(hAPP_int_bool(Pa,X_2))
| bot_bot_fun_int_bool = collect_int(Pa) )
& ( ! [X_2] : ~ hBOOL(hAPP_int_bool(Pa,X_2))
| bot_bot_fun_int_bool != collect_int(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f627]) ).
fof(f627_sk,plain,
! [Pa,X_2] :
( ( hBOOL(hAPP_int_bool(Pa,sk89(Pa)))
| bot_bot_fun_int_bool = collect_int(Pa) )
& ( ~ hBOOL(hAPP_int_bool(Pa,X_2))
| bot_bot_fun_int_bool != collect_int(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk89])],[f627_nnf]) ).
cnf(c896,plain,
( ~ hBOOL(hAPP_int_bool(X0,X1))
| bot_bot_fun_int_bool != collect_int(X0) ),
inference(cnf_transformation,[status(esa)],[f627_sk]) ).
fof(f628,axiom,
! [Pa] :
( bot_bot_fun_nat_bool = collect_nat(Pa)
<=> ! [X_2] : ~ hBOOL(hAPP_nat_bool(Pa,X_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_522_empty__Collect__eq) ).
fof(f628_nnf,plain,
! [Pa] :
( ( ? [X_2] : hBOOL(hAPP_nat_bool(Pa,X_2))
| bot_bot_fun_nat_bool = collect_nat(Pa) )
& ( ! [X_2] : ~ hBOOL(hAPP_nat_bool(Pa,X_2))
| bot_bot_fun_nat_bool != collect_nat(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f628]) ).
fof(f628_sk,plain,
! [Pa,X_2] :
( ( hBOOL(hAPP_nat_bool(Pa,sk90(Pa)))
| bot_bot_fun_nat_bool = collect_nat(Pa) )
& ( ~ hBOOL(hAPP_nat_bool(Pa,X_2))
| bot_bot_fun_nat_bool != collect_nat(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk90])],[f628_nnf]) ).
cnf(c898,plain,
( ~ hBOOL(hAPP_nat_bool(X0,X1))
| bot_bot_fun_nat_bool != collect_nat(X0) ),
inference(cnf_transformation,[status(esa)],[f628_sk]) ).
fof(f629,axiom,
! [Pa] :
( bot_bot_fun_a_bool = collect_a(Pa)
<=> ! [X_2] :
( is_a(X_2)
=> ~ hBOOL(hAPP_a_bool(Pa,X_2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_523_empty__Collect__eq) ).
fof(f629_nnf,plain,
! [Pa] :
( ( ? [X_2] :
( hBOOL(hAPP_a_bool(Pa,X_2))
& is_a(X_2) )
| bot_bot_fun_a_bool = collect_a(Pa) )
& ( ! [X_2] :
( ~ hBOOL(hAPP_a_bool(Pa,X_2))
| ~ is_a(X_2) )
| bot_bot_fun_a_bool != collect_a(Pa) ) ),
inference(nnf_transformation,[status(thm)],[f629]) ).
fof(f629_sk,plain,
! [Pa,X_2] :
( ( ( hBOOL(hAPP_a_bool(Pa,sk91(Pa)))
& is_a(sk91(Pa)) )
| bot_bot_fun_a_bool = collect_a(Pa) )
& ( ~ hBOOL(hAPP_a_bool(Pa,X_2))
| ~ is_a(X_2)
| bot_bot_fun_a_bool != collect_a(Pa) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk91])],[f629_nnf]) ).
cnf(c900,plain,
( ~ hBOOL(hAPP_a_bool(X0,X1))
| ~ is_a(X1)
| bot_bot_fun_a_bool != collect_a(X0) ),
inference(cnf_transformation,[status(esa)],[f629_sk]) ).
fof(f633,axiom,
! [A] :
( ? [X_2] : hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A))
<=> A != bot_bot_fun_int_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_527_ex__in__conv) ).
fof(f633_nnf,plain,
! [A] :
( ( A = bot_bot_fun_int_bool
| ? [X_2] : hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) )
& ( A != bot_bot_fun_int_bool
| ! [X_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) ) ),
inference(nnf_transformation,[status(thm)],[f633]) ).
fof(f633_sk,plain,
! [X_2,A] :
( ( A = bot_bot_fun_int_bool
| hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,sk92(A)),A)) )
& ( A != bot_bot_fun_int_bool
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk92])],[f633_nnf]) ).
cnf(c906,plain,
( X0 != bot_bot_fun_int_bool
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f633_sk]) ).
fof(f634,axiom,
! [A] :
( ? [X_2] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A))
<=> A != bot_bot_fun_nat_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_528_ex__in__conv) ).
fof(f634_nnf,plain,
! [A] :
( ( A = bot_bot_fun_nat_bool
| ? [X_2] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) )
& ( A != bot_bot_fun_nat_bool
| ! [X_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) ) ),
inference(nnf_transformation,[status(thm)],[f634]) ).
fof(f634_sk,plain,
! [X_2,A] :
( ( A = bot_bot_fun_nat_bool
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,sk93(A)),A)) )
& ( A != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk93])],[f634_nnf]) ).
cnf(c908,plain,
( X0 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
fof(f635,axiom,
! [A] :
( is_fun_a_bool(A)
=> ( ? [X_2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
& is_a(X_2) )
<=> A != bot_bot_fun_a_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_529_ex__in__conv) ).
fof(f635_nnf,plain,
! [A] :
( ( ( A = bot_bot_fun_a_bool
| ? [X_2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
& is_a(X_2) ) )
& ( A != bot_bot_fun_a_bool
| ! [X_2] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
| ~ is_a(X_2) ) ) )
| ~ is_fun_a_bool(A) ),
inference(nnf_transformation,[status(thm)],[f635]) ).
fof(f635_sk,plain,
! [A,X_2] :
( ( ( A = bot_bot_fun_a_bool
| ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,sk94(A)),A))
& is_a(sk94(A)) ) )
& ( A != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
| ~ is_a(X_2) ) )
| ~ is_fun_a_bool(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk94])],[f635_nnf]) ).
cnf(c910,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)],[f635_sk]) ).
fof(f636,axiom,
! [A] :
( is_fun_pname_bool(A)
=> ( ? [X_2] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
& is_pname(X_2) )
<=> A != bot_bo844097828e_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_530_ex__in__conv) ).
fof(f636_nnf,plain,
! [A] :
( ( ( A = bot_bo844097828e_bool
| ? [X_2] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
& is_pname(X_2) ) )
& ( A != bot_bo844097828e_bool
| ! [X_2] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
| ~ is_pname(X_2) ) ) )
| ~ is_fun_pname_bool(A) ),
inference(nnf_transformation,[status(thm)],[f636]) ).
fof(f636_sk,plain,
! [A,X_2] :
( ( ( A = bot_bo844097828e_bool
| ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,sk95(A)),A))
& is_pname(sk95(A)) ) )
& ( A != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
| ~ is_pname(X_2) ) )
| ~ is_fun_pname_bool(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95])],[f636_nnf]) ).
cnf(c913,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)],[f636_sk]) ).
fof(f637,axiom,
! [A] :
( ! [X_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A))
<=> A = bot_bot_fun_int_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_531_all__not__in__conv) ).
fof(f637_nnf,plain,
! [A] :
( ( A != bot_bot_fun_int_bool
| ! [X_2] : ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) )
& ( A = bot_bot_fun_int_bool
| ? [X_2] : hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) ) ),
inference(nnf_transformation,[status(thm)],[f637]) ).
fof(f637_sk,plain,
! [A,X_2] :
( ( A != bot_bot_fun_int_bool
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X_2),A)) )
& ( A = bot_bot_fun_int_bool
| hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,sk96(A)),A)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk96])],[f637_nnf]) ).
cnf(c917,plain,
( X0 != bot_bot_fun_int_bool
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f637_sk]) ).
fof(f638,axiom,
! [A] :
( ! [X_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A))
<=> A = bot_bot_fun_nat_bool ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_532_all__not__in__conv) ).
fof(f638_nnf,plain,
! [A] :
( ( A != bot_bot_fun_nat_bool
| ! [X_2] : ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) )
& ( A = bot_bot_fun_nat_bool
| ? [X_2] : hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) ) ),
inference(nnf_transformation,[status(thm)],[f638]) ).
fof(f638_sk,plain,
! [A,X_2] :
( ( A != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X_2),A)) )
& ( A = bot_bot_fun_nat_bool
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,sk97(A)),A)) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk97])],[f638_nnf]) ).
cnf(c919,plain,
( X0 != bot_bot_fun_nat_bool
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X1),X0)) ),
inference(cnf_transformation,[status(esa)],[f638_sk]) ).
fof(f639,axiom,
! [A] :
( is_fun_a_bool(A)
=> ( ! [X_2] :
( is_a(X_2)
=> ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A)) )
<=> A = bot_bot_fun_a_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_533_all__not__in__conv) ).
fof(f639_nnf,plain,
! [A] :
( ( ( A != bot_bot_fun_a_bool
| ! [X_2] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
| ~ is_a(X_2) ) )
& ( A = bot_bot_fun_a_bool
| ? [X_2] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
& is_a(X_2) ) ) )
| ~ is_fun_a_bool(A) ),
inference(nnf_transformation,[status(thm)],[f639]) ).
fof(f639_sk,plain,
! [A,X_2] :
( ( ( A != bot_bot_fun_a_bool
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X_2),A))
| ~ is_a(X_2) )
& ( A = bot_bot_fun_a_bool
| ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,sk98(A)),A))
& is_a(sk98(A)) ) ) )
| ~ is_fun_a_bool(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk98])],[f639_nnf]) ).
cnf(c922,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)],[f639_sk]) ).
fof(f640,axiom,
! [A] :
( is_fun_pname_bool(A)
=> ( ! [X_2] :
( is_pname(X_2)
=> ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A)) )
<=> A = bot_bo844097828e_bool ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_534_all__not__in__conv) ).
fof(f640_nnf,plain,
! [A] :
( ( ( A != bot_bo844097828e_bool
| ! [X_2] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
| ~ is_pname(X_2) ) )
& ( A = bot_bo844097828e_bool
| ? [X_2] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
& is_pname(X_2) ) ) )
| ~ is_fun_pname_bool(A) ),
inference(nnf_transformation,[status(thm)],[f640]) ).
fof(f640_sk,plain,
! [A,X_2] :
( ( ( A != bot_bo844097828e_bool
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_2),A))
| ~ is_pname(X_2) )
& ( A = bot_bo844097828e_bool
| ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,sk99(A)),A))
& is_pname(sk99(A)) ) ) )
| ~ is_fun_pname_bool(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk99])],[f640_nnf]) ).
cnf(c925,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)],[f640_sk]) ).
fof(f709,axiom,
! [A_2,A] : hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A) != bot_bot_fun_a_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_603_insert__not__empty) ).
fof(f709_nnf,plain,
! [A_2,A] : hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A) != bot_bot_fun_a_bool,
inference(nnf_transformation,[status(thm)],[f709]) ).
fof(f709_sk,plain,
! [A_2,A] : hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A) != bot_bot_fun_a_bool,
inference(skolemisation,[status(esa)],[f709_nnf]) ).
cnf(c1046,plain,
hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X0),X1) != bot_bot_fun_a_bool,
inference(cnf_transformation,[status(esa)],[f709_sk]) ).
fof(f710,axiom,
! [A_2,A] : hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A) != bot_bot_fun_nat_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_604_insert__not__empty) ).
fof(f710_nnf,plain,
! [A_2,A] : hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A) != bot_bot_fun_nat_bool,
inference(nnf_transformation,[status(thm)],[f710]) ).
fof(f710_sk,plain,
! [A_2,A] : hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A) != bot_bot_fun_nat_bool,
inference(skolemisation,[status(esa)],[f710_nnf]) ).
cnf(c1047,plain,
hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,X0),X1) != bot_bot_fun_nat_bool,
inference(cnf_transformation,[status(esa)],[f710_sk]) ).
fof(f711,axiom,
! [A_2,A] : hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A) != bot_bot_fun_int_bool,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_605_insert__not__empty) ).
fof(f711_nnf,plain,
! [A_2,A] : hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A) != bot_bot_fun_int_bool,
inference(nnf_transformation,[status(thm)],[f711]) ).
fof(f711_sk,plain,
! [A_2,A] : hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A) != bot_bot_fun_int_bool,
inference(skolemisation,[status(esa)],[f711_nnf]) ).
cnf(c1048,plain,
hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,X0),X1) != bot_bot_fun_int_bool,
inference(cnf_transformation,[status(esa)],[f711_sk]) ).
fof(f712,axiom,
! [A_2,A] : bot_bot_fun_a_bool != hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_606_empty__not__insert) ).
fof(f712_nnf,plain,
! [A_2,A] : bot_bot_fun_a_bool != hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A),
inference(nnf_transformation,[status(thm)],[f712]) ).
fof(f712_sk,plain,
! [A_2,A] : bot_bot_fun_a_bool != hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,A_2),A),
inference(skolemisation,[status(esa)],[f712_nnf]) ).
cnf(c1049,plain,
bot_bot_fun_a_bool != hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,X0),X1),
inference(cnf_transformation,[status(esa)],[f712_sk]) ).
fof(f713,axiom,
! [A_2,A] : bot_bot_fun_nat_bool != hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_607_empty__not__insert) ).
fof(f713_nnf,plain,
! [A_2,A] : bot_bot_fun_nat_bool != hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A),
inference(nnf_transformation,[status(thm)],[f713]) ).
fof(f713_sk,plain,
! [A_2,A] : bot_bot_fun_nat_bool != hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,A_2),A),
inference(skolemisation,[status(esa)],[f713_nnf]) ).
cnf(c1050,plain,
bot_bot_fun_nat_bool != hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,X0),X1),
inference(cnf_transformation,[status(esa)],[f713_sk]) ).
fof(f714,axiom,
! [A_2,A] : bot_bot_fun_int_bool != hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_608_empty__not__insert) ).
fof(f714_nnf,plain,
! [A_2,A] : bot_bot_fun_int_bool != hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A),
inference(nnf_transformation,[status(thm)],[f714]) ).
fof(f714_sk,plain,
! [A_2,A] : bot_bot_fun_int_bool != hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,A_2),A),
inference(skolemisation,[status(esa)],[f714_nnf]) ).
cnf(c1051,plain,
bot_bot_fun_int_bool != hAPP_f1805168059t_bool(hAPP_i1529485324t_bool(insert_int,X0),X1),
inference(cnf_transformation,[status(esa)],[f714_sk]) ).
fof(f810,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B)))
=> ~ ( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A))
=> hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_704_DiffE) ).
fof(f810_nnf,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
& hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A)) )
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f810]) ).
fof(f810_sk,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
& hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A)) )
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f810_nnf]) ).
cnf(c1253,plain,
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),X2))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f810_sk]) ).
fof(f811,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B)))
=> ~ ( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A))
=> hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_705_DiffE) ).
fof(f811_nnf,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
& hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A)) )
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f811]) ).
fof(f811_sk,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
& hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A)) )
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f811_nnf]) ).
cnf(c1255,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),X2))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f811_sk]) ).
fof(f812,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B)))
=> ~ ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A))
=> hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_706_DiffE) ).
fof(f812_nnf,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f812]) ).
fof(f812_sk,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f812_nnf]) ).
cnf(c1257,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f812_sk]) ).
fof(f813,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B)))
=> ~ ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A))
=> hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_707_DiffE) ).
fof(f813_nnf,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
& hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A)) )
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f813]) ).
fof(f813_sk,plain,
! [C_6,A,B] :
( ( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
& hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A)) )
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f813_nnf]) ).
cnf(c1259,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X2))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f813_sk]) ).
fof(f818,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B)))
=> ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_712_DiffD2) ).
fof(f818_nnf,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f818]) ).
fof(f818_sk,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f818_nnf]) ).
cnf(c1264,plain,
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),X2))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f818_sk]) ).
fof(f819,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B)))
=> ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_713_DiffD2) ).
fof(f819_nnf,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f819]) ).
fof(f819_sk,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f819_nnf]) ).
cnf(c1265,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),X2))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f819_sk]) ).
fof(f820,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B)))
=> ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_714_DiffD2) ).
fof(f820_nnf,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f820]) ).
fof(f820_sk,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f820_nnf]) ).
cnf(c1266,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f820_sk]) ).
fof(f821,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B)))
=> ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_715_DiffD2) ).
fof(f821_nnf,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ),
inference(nnf_transformation,[status(thm)],[f821]) ).
fof(f821_sk,plain,
! [C_6,A,B] :
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ),
inference(skolemisation,[status(esa)],[f821_nnf]) ).
cnf(c1267,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X2))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f821_sk]) ).
fof(f826,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B)))
<=> ( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
& hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_720_Diff__iff) ).
fof(f826_nnf,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A))
| hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
& hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A)) )
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ) ),
inference(nnf_transformation,[status(thm)],[f826]) ).
fof(f826_sk,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A))
| hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),B))
& hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),A)) )
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,C_6),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,A),B))) ) ),
inference(skolemisation,[status(esa)],[f826_nnf]) ).
cnf(c1273,plain,
( ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),X2))
| ~ hBOOL(hAPP_f448129468l_bool(hAPP_i2112223885l_bool(member_int,X0),hAPP_f1805168059t_bool(hAPP_f1223193598t_bool(minus_1449998731t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f826_sk]) ).
fof(f827,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B)))
<=> ( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
& hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_721_Diff__iff) ).
fof(f827_nnf,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A))
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
& hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A)) )
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ) ),
inference(nnf_transformation,[status(thm)],[f827]) ).
fof(f827_sk,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A))
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),B))
& hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),A)) )
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,C_6),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,A),B))) ) ),
inference(skolemisation,[status(esa)],[f827_nnf]) ).
cnf(c1276,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),X2))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,X0),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f827_sk]) ).
fof(f828,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B)))
<=> ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_722_Diff__iff) ).
fof(f828_nnf,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ) ),
inference(nnf_transformation,[status(thm)],[f828]) ).
fof(f828_sk,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),B))
& hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),A)) )
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,C_6),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,A),B))) ) ),
inference(skolemisation,[status(esa)],[f828_nnf]) ).
cnf(c1279,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),X2))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,X0),hAPP_f2050579477a_bool(hAPP_f1791771145a_bool(minus_1762468890a_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f828_sk]) ).
fof(f829,axiom,
! [C_6,A,B] :
( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B)))
<=> ( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
& hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_723_Diff__iff) ).
fof(f829_nnf,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A))
| hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
& hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A)) )
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ) ),
inference(nnf_transformation,[status(thm)],[f829]) ).
fof(f829_sk,plain,
! [C_6,A,B] :
( ( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A))
| hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) )
& ( ( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),B))
& hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),A)) )
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,C_6),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,A),B))) ) ),
inference(skolemisation,[status(esa)],[f829_nnf]) ).
cnf(c1282,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X2))
| ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),hAPP_f759274231e_bool(hAPP_f1388330588e_bool(minus_1015773161e_bool,X1),X2))) ),
inference(cnf_transformation,[status(esa)],[f829_sk]) ).
fof(f964,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_858_less__not__refl) ).
fof(f964_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(nnf_transformation,[status(thm)],[f964]) ).
fof(f964_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(skolemisation,[status(esa)],[f964_nnf]) ).
cnf(c1486,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X0)),
inference(cnf_transformation,[status(esa)],[f964_sk]) ).
fof(f965,axiom,
! [M,Na] :
( M != Na
<=> ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_859_nat__neq__iff) ).
fof(f965_nnf,plain,
! [M,Na] :
( ( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M))
& ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
| M != Na )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na))
| M = Na ) ),
inference(nnf_transformation,[status(thm)],[f965]) ).
fof(f965_sk,plain,
! [M,Na] :
( ( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M))
& ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
| M != Na )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),M))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na))
| M = Na ) ),
inference(skolemisation,[status(esa)],[f965_nnf]) ).
cnf(c1488,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1))
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f965_sk]) ).
cnf(c1489,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X1),X0))
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f965_sk]) ).
fof(f967,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_861_less__irrefl__nat) ).
fof(f967_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(nnf_transformation,[status(thm)],[f967]) ).
fof(f967_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),N)),
inference(skolemisation,[status(esa)],[f967_nnf]) ).
cnf(c1491,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X0)),
inference(cnf_transformation,[status(esa)],[f967_sk]) ).
fof(f968,axiom,
! [N,M_1] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M_1))
=> M_1 != N ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_862_less__not__refl2) ).
fof(f968_nnf,plain,
! [N,M_1] :
( M_1 != N
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M_1)) ),
inference(nnf_transformation,[status(thm)],[f968]) ).
fof(f968_sk,plain,
! [N,M_1] :
( M_1 != N
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),M_1)) ),
inference(skolemisation,[status(esa)],[f968_nnf]) ).
cnf(c1492,plain,
( X1 != X0
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f968_sk]) ).
fof(f969,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_863_less__not__refl3) ).
fof(f969_nnf,plain,
! [S,T] :
( S != T
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,S),T)) ),
inference(nnf_transformation,[status(thm)],[f969]) ).
fof(f969_sk,plain,
! [S,T] :
( S != T
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,S),T)) ),
inference(skolemisation,[status(esa)],[f969_nnf]) ).
cnf(c1493,plain,
( X0 != X1
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f969_sk]) ).
fof(f971,axiom,
! [M,Na] :
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na))
<=> hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_865_not__less__eq) ).
fof(f971_nnf,plain,
! [M,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M)))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M)))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f971]) ).
fof(f971_sk,plain,
! [M,Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M)))
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,Na),hAPP_nat_nat(suc,M)))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) ) ),
inference(skolemisation,[status(esa)],[f971_nnf]) ).
cnf(c1503,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)],[f971_sk]) ).
fof(f982,axiom,
! [I_1,J] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,I_1),J)),I_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_876_not__add__less1) ).
fof(f982_nnf,plain,
! [I_1,J] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,I_1),J)),I_1)),
inference(nnf_transformation,[status(thm)],[f982]) ).
fof(f982_sk,plain,
! [I_1,J] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,I_1),J)),I_1)),
inference(skolemisation,[status(esa)],[f982_nnf]) ).
cnf(c1518,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,X0),X1)),X0)),
inference(cnf_transformation,[status(esa)],[f982_sk]) ).
fof(f983,axiom,
! [J,I_1] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,J),I_1)),I_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_877_not__add__less2) ).
fof(f983_nnf,plain,
! [J,I_1] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,J),I_1)),I_1)),
inference(nnf_transformation,[status(thm)],[f983]) ).
fof(f983_sk,plain,
! [J,I_1] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,J),I_1)),I_1)),
inference(skolemisation,[status(esa)],[f983_nnf]) ).
cnf(c1519,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,hAPP_nat_nat(hAPP_nat_fun_nat_nat(plus_plus_nat,X0),X1)),X1)),
inference(cnf_transformation,[status(esa)],[f983_sk]) ).
fof(f993,axiom,
! [M,Na] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na))
<=> ( M != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_887_nat__less__le) ).
fof(f993_nnf,plain,
! [M,Na] :
( ( M = Na
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
& ( ( M != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) )
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) ) ),
inference(nnf_transformation,[status(thm)],[f993]) ).
fof(f993_sk,plain,
! [M,Na] :
( ( M = Na
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na))
| hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) )
& ( ( M != Na
& hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_eq_nat,M),Na)) )
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M),Na)) ) ),
inference(skolemisation,[status(esa)],[f993_nnf]) ).
cnf(c1531,plain,
( X0 != X1
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f993_sk]) ).
fof(f1027,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_921_less__zeroE) ).
fof(f1027_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(nnf_transformation,[status(thm)],[f1027]) ).
fof(f1027_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(skolemisation,[status(esa)],[f1027_nnf]) ).
cnf(c1585,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),zero_zero_nat)),
inference(cnf_transformation,[status(esa)],[f1027_sk]) ).
fof(f1042,axiom,
! [M_1,N] :
( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),N))
=> N != zero_zero_nat ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_936_gr__implies__not0) ).
fof(f1042_nnf,plain,
! [M_1,N] :
( N != zero_zero_nat
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),N)) ),
inference(nnf_transformation,[status(thm)],[f1042]) ).
fof(f1042_sk,plain,
! [M_1,N] :
( N != zero_zero_nat
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,M_1),N)) ),
inference(skolemisation,[status(esa)],[f1042_nnf]) ).
cnf(c1603,plain,
( X1 != zero_zero_nat
| ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f1042_sk]) ).
fof(f1043,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_937_less__nat__zero__code) ).
fof(f1043_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(nnf_transformation,[status(thm)],[f1043]) ).
fof(f1043_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(skolemisation,[status(esa)],[f1043_nnf]) ).
cnf(c1604,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),zero_zero_nat)),
inference(cnf_transformation,[status(esa)],[f1043_sk]) ).
fof(f1044,axiom,
! [Na] :
( Na != zero_zero_nat
<=> hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),Na)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_938_neq0__conv) ).
fof(f1044_nnf,plain,
! [Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),Na))
| Na != zero_zero_nat )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),Na))
| Na = zero_zero_nat ) ),
inference(nnf_transformation,[status(thm)],[f1044]) ).
fof(f1044_sk,plain,
! [Na] :
( ( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),Na))
| Na != zero_zero_nat )
& ( hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),Na))
| Na = zero_zero_nat ) ),
inference(skolemisation,[status(esa)],[f1044_nnf]) ).
cnf(c1606,plain,
( ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,zero_zero_nat),X0))
| X0 != zero_zero_nat ),
inference(cnf_transformation,[status(esa)],[f1044_sk]) ).
fof(f1045,axiom,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_939_not__less0) ).
fof(f1045_nnf,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(nnf_transformation,[status(thm)],[f1045]) ).
fof(f1045_sk,plain,
! [N] : ~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,N),zero_zero_nat)),
inference(skolemisation,[status(esa)],[f1045_nnf]) ).
cnf(c1607,plain,
~ hBOOL(hAPP_nat_bool(hAPP_n1699378549t_bool(ord_less_nat,X0),zero_zero_nat)),
inference(cnf_transformation,[status(esa)],[f1045_sk]) ).
fof(f1046,axiom,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_940_Suc__neq__Zero) ).
fof(f1046_nnf,plain,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f1046]) ).
fof(f1046_sk,plain,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f1046_nnf]) ).
cnf(c1608,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f1046_sk]) ).
fof(f1047,axiom,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_941_Zero__neq__Suc) ).
fof(f1047_nnf,plain,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
inference(nnf_transformation,[status(thm)],[f1047]) ).
fof(f1047_sk,plain,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
inference(skolemisation,[status(esa)],[f1047_nnf]) ).
cnf(c1609,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f1047_sk]) ).
fof(f1048,axiom,
! [Nat_2] : hAPP_nat_nat(suc,Nat_2) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_942_nat_Osimps_I3_J) ).
fof(f1048_nnf,plain,
! [Nat_2] : hAPP_nat_nat(suc,Nat_2) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f1048]) ).
fof(f1048_sk,plain,
! [Nat_2] : hAPP_nat_nat(suc,Nat_2) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f1048_nnf]) ).
cnf(c1610,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f1048_sk]) ).
fof(f1049,axiom,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_943_Suc__not__Zero) ).
fof(f1049_nnf,plain,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
inference(nnf_transformation,[status(thm)],[f1049]) ).
fof(f1049_sk,plain,
! [M_1] : hAPP_nat_nat(suc,M_1) != zero_zero_nat,
inference(skolemisation,[status(esa)],[f1049_nnf]) ).
cnf(c1611,plain,
hAPP_nat_nat(suc,X0) != zero_zero_nat,
inference(cnf_transformation,[status(esa)],[f1049_sk]) ).
fof(f1050,axiom,
! [Nat_1] : zero_zero_nat != hAPP_nat_nat(suc,Nat_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_944_nat_Osimps_I2_J) ).
fof(f1050_nnf,plain,
! [Nat_1] : zero_zero_nat != hAPP_nat_nat(suc,Nat_1),
inference(nnf_transformation,[status(thm)],[f1050]) ).
fof(f1050_sk,plain,
! [Nat_1] : zero_zero_nat != hAPP_nat_nat(suc,Nat_1),
inference(skolemisation,[status(esa)],[f1050_nnf]) ).
cnf(c1612,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f1050_sk]) ).
fof(f1051,axiom,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_945_Zero__not__Suc) ).
fof(f1051_nnf,plain,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
inference(nnf_transformation,[status(thm)],[f1051]) ).
fof(f1051_sk,plain,
! [M_1] : zero_zero_nat != hAPP_nat_nat(suc,M_1),
inference(skolemisation,[status(esa)],[f1051_nnf]) ).
cnf(c1613,plain,
zero_zero_nat != hAPP_nat_nat(suc,X0),
inference(cnf_transformation,[status(esa)],[f1051_sk]) ).
fof(f1070,axiom,
! [I_2,M_3] :
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,zero_zero_nat),M_3))
=> hAPP_f22106695ol_nat(finite_card_nat,collect_nat(cOMBS_nat_bool_bool(cOMBB_1015721476ol_nat(fconj,hAPP_f800510211t_bool(cOMBC_226598744l_bool(member_nat),M_3)),hAPP_n1699378549t_bool(cOMBC_nat_nat_bool(ord_less_nat),hAPP_nat_nat(suc,I_2))))) != zero_zero_nat ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_964_card__less) ).
fof(f1070_nnf,plain,
! [I_2,M_3] :
( hAPP_f22106695ol_nat(finite_card_nat,collect_nat(cOMBS_nat_bool_bool(cOMBB_1015721476ol_nat(fconj,hAPP_f800510211t_bool(cOMBC_226598744l_bool(member_nat),M_3)),hAPP_n1699378549t_bool(cOMBC_nat_nat_bool(ord_less_nat),hAPP_nat_nat(suc,I_2))))) != zero_zero_nat
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,zero_zero_nat),M_3)) ),
inference(nnf_transformation,[status(thm)],[f1070]) ).
fof(f1070_sk,plain,
! [M_3,I_2] :
( hAPP_f22106695ol_nat(finite_card_nat,collect_nat(cOMBS_nat_bool_bool(cOMBB_1015721476ol_nat(fconj,hAPP_f800510211t_bool(cOMBC_226598744l_bool(member_nat),M_3)),hAPP_n1699378549t_bool(cOMBC_nat_nat_bool(ord_less_nat),hAPP_nat_nat(suc,I_2))))) != zero_zero_nat
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,zero_zero_nat),M_3)) ),
inference(skolemisation,[status(esa)],[f1070_nnf]) ).
cnf(c1661,plain,
( hAPP_f22106695ol_nat(finite_card_nat,collect_nat(cOMBS_nat_bool_bool(cOMBB_1015721476ol_nat(fconj,hAPP_f800510211t_bool(cOMBC_226598744l_bool(member_nat),X1)),hAPP_n1699378549t_bool(cOMBC_nat_nat_bool(ord_less_nat),hAPP_nat_nat(suc,X0))))) != zero_zero_nat
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,zero_zero_nat),X1)) ),
inference(cnf_transformation,[status(esa)],[f1070_sk]) ).
fof(f1138,axiom,
! [Z] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),Z)),Z) != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1032_odd__nonzero) ).
fof(f1138_nnf,plain,
! [Z] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),Z)),Z) != zero_zero_int,
inference(nnf_transformation,[status(thm)],[f1138]) ).
fof(f1138_sk,plain,
! [Z] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),Z)),Z) != zero_zero_int,
inference(skolemisation,[status(esa)],[f1138_nnf]) ).
cnf(c1770,plain,
hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),X0)),X0) != zero_zero_int,
inference(cnf_transformation,[status(esa)],[f1138_sk]) ).
fof(f1156,axiom,
! [Z_2,W_1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1))
<=> ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1050_zless__le) ).
fof(f1156_nnf,plain,
! [Z_2,W_1] :
( ( Z_2 = W_1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) )
& ( ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) ) ),
inference(nnf_transformation,[status(thm)],[f1156]) ).
fof(f1156_sk,plain,
! [Z_2,W_1] :
( ( Z_2 = W_1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) )
& ( ( Z_2 != W_1
& hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,Z_2),W_1)) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,Z_2),W_1)) ) ),
inference(skolemisation,[status(esa)],[f1156_nnf]) ).
cnf(c1793,plain,
( X0 != X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f1156_sk]) ).
fof(f1178,axiom,
zero_zero_int != one_one_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1072_int__0__neq__1) ).
fof(f1178_nnf,plain,
zero_zero_int != one_one_int,
inference(nnf_transformation,[status(thm)],[f1178]) ).
fof(f1178_sk,plain,
zero_zero_int != one_one_int,
inference(skolemisation,[status(esa)],[f1178_nnf]) ).
cnf(c1830,plain,
zero_zero_int != one_one_int,
inference(cnf_transformation,[status(esa)],[f1178_sk]) ).
fof(f1203,axiom,
! [K_1] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,K_1)),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1097_int__less__0__conv) ).
fof(f1203_nnf,plain,
! [K_1] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,K_1)),zero_zero_int)),
inference(nnf_transformation,[status(thm)],[f1203]) ).
fof(f1203_sk,plain,
! [K_1] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,K_1)),zero_zero_int)),
inference(skolemisation,[status(esa)],[f1203_nnf]) ).
cnf(c1954,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
inference(cnf_transformation,[status(esa)],[f1203_sk]) ).
fof(f1253,axiom,
! [X_1] :
( ~ hBOOL(hAPP_int_bool(nat_neg,X_1))
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1147_not__neg__eq__ge__0) ).
fof(f1253_nnf,plain,
! [X_1] :
( ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X_1))
| ~ hBOOL(hAPP_int_bool(nat_neg,X_1)) )
& ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X_1))
| hBOOL(hAPP_int_bool(nat_neg,X_1)) ) ),
inference(nnf_transformation,[status(thm)],[f1253]) ).
fof(f1253_sk,plain,
! [X_1] :
( ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X_1))
| ~ hBOOL(hAPP_int_bool(nat_neg,X_1)) )
& ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X_1))
| hBOOL(hAPP_int_bool(nat_neg,X_1)) ) ),
inference(skolemisation,[status(esa)],[f1253_nnf]) ).
cnf(c2034,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),X0))
| ~ hBOOL(hAPP_int_bool(nat_neg,X0)) ),
inference(cnf_transformation,[status(esa)],[f1253_sk]) ).
fof(f1254,axiom,
~ hBOOL(hAPP_int_bool(nat_neg,one_one_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1148_not__neg__1) ).
fof(f1254_nnf,plain,
~ hBOOL(hAPP_int_bool(nat_neg,one_one_int)),
inference(nnf_transformation,[status(thm)],[f1254]) ).
fof(f1254_sk,plain,
~ hBOOL(hAPP_int_bool(nat_neg,one_one_int)),
inference(skolemisation,[status(esa)],[f1254_nnf]) ).
cnf(c2035,plain,
~ hBOOL(hAPP_int_bool(nat_neg,one_one_int)),
inference(cnf_transformation,[status(esa)],[f1254_sk]) ).
fof(f1255,axiom,
~ hBOOL(hAPP_int_bool(nat_neg,zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1149_not__neg__0) ).
fof(f1255_nnf,plain,
~ hBOOL(hAPP_int_bool(nat_neg,zero_zero_int)),
inference(nnf_transformation,[status(thm)],[f1255]) ).
fof(f1255_sk,plain,
~ hBOOL(hAPP_int_bool(nat_neg,zero_zero_int)),
inference(skolemisation,[status(esa)],[f1255_nnf]) ).
cnf(c2036,plain,
~ hBOOL(hAPP_int_bool(nat_neg,zero_zero_int)),
inference(cnf_transformation,[status(esa)],[f1255_sk]) ).
fof(f1257,axiom,
! [N] : ~ hBOOL(hAPP_int_bool(nat_neg,hAPP_nat_int(semiri1621563631at_int,N))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1151_not__neg__int) ).
fof(f1257_nnf,plain,
! [N] : ~ hBOOL(hAPP_int_bool(nat_neg,hAPP_nat_int(semiri1621563631at_int,N))),
inference(nnf_transformation,[status(thm)],[f1257]) ).
fof(f1257_sk,plain,
! [N] : ~ hBOOL(hAPP_int_bool(nat_neg,hAPP_nat_int(semiri1621563631at_int,N))),
inference(skolemisation,[status(esa)],[f1257_nnf]) ).
cnf(c2038,plain,
~ hBOOL(hAPP_int_bool(nat_neg,hAPP_nat_int(semiri1621563631at_int,X0))),
inference(cnf_transformation,[status(esa)],[f1257_sk]) ).
fof(f1274,axiom,
~ hBOOL(hAPP_int_bool(nat_neg,number_number_of_int(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1168_not__neg__number__of__Pls) ).
fof(f1274_nnf,plain,
~ hBOOL(hAPP_int_bool(nat_neg,number_number_of_int(pls))),
inference(nnf_transformation,[status(thm)],[f1274]) ).
fof(f1274_sk,plain,
~ hBOOL(hAPP_int_bool(nat_neg,number_number_of_int(pls))),
inference(skolemisation,[status(esa)],[f1274_nnf]) ).
cnf(c2089,plain,
~ hBOOL(hAPP_int_bool(nat_neg,number_number_of_int(pls))),
inference(cnf_transformation,[status(esa)],[f1274_sk]) ).
fof(f1288,axiom,
! [K_1] : bit1(K_1) != pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1182_rel__simps_I46_J) ).
fof(f1288_nnf,plain,
! [K_1] : bit1(K_1) != pls,
inference(nnf_transformation,[status(thm)],[f1288]) ).
fof(f1288_sk,plain,
! [K_1] : bit1(K_1) != pls,
inference(skolemisation,[status(esa)],[f1288_nnf]) ).
cnf(c2104,plain,
bit1(X0) != pls,
inference(cnf_transformation,[status(esa)],[f1288_sk]) ).
fof(f1289,axiom,
! [L_1] : pls != bit1(L_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1183_rel__simps_I39_J) ).
fof(f1289_nnf,plain,
! [L_1] : pls != bit1(L_1),
inference(nnf_transformation,[status(thm)],[f1289]) ).
fof(f1289_sk,plain,
! [L_1] : pls != bit1(L_1),
inference(skolemisation,[status(esa)],[f1289_nnf]) ).
cnf(c2105,plain,
pls != bit1(X0),
inference(cnf_transformation,[status(esa)],[f1289_sk]) ).
fof(f1299,axiom,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1193_rel__simps_I2_J) ).
fof(f1299_nnf,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(nnf_transformation,[status(thm)],[f1299]) ).
fof(f1299_sk,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(skolemisation,[status(esa)],[f1299_nnf]) ).
cnf(c2118,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(cnf_transformation,[status(esa)],[f1299_sk]) ).
fof(f1305,axiom,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fNot_1_1_U) ).
fof(f1305_nnf,plain,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
inference(nnf_transformation,[status(thm)],[f1305]) ).
fof(f1305_sk,plain,
! [P] :
( ~ hBOOL(P)
| ~ hBOOL(hAPP_bool_bool(fNot,P)) ),
inference(skolemisation,[status(esa)],[f1305_nnf]) ).
cnf(c2129,plain,
( ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(fNot,X0)) ),
inference(cnf_transformation,[status(esa)],[f1305_sk]) ).
fof(f1313,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1313_nnf,plain,
~ hBOOL(fFalse),
inference(nnf_transformation,[status(thm)],[f1313]) ).
fof(f1313_sk,plain,
~ hBOOL(fFalse),
inference(skolemisation,[status(esa)],[f1313_nnf]) ).
cnf(c2137,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(esa)],[f1313_sk]) ).
fof(f1413,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(f1413_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)],[f1413]) ).
fof(f1413_sk,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
inference(skolemisation,[status(esa)],[f1413_nnf]) ).
cnf(c2237,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),g)),
inference(cnf_transformation,[status(esa)],[f1413_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c247,c248,c320,c321,c861,c862,c863,c864,c875,c876,c877,c878,c879,c881,c883,c892,c893,c894,c895,c896,c898,c900,c906,c908,c910,c913,c917,c919,c922,c925,c1046,c1047,c1048,c1049,c1050,c1051,c1253,c1255,c1257,c1259,c1264,c1265,c1266,c1267,c1273,c1276,c1279,c1282,c1486,c1488,c1489,c1491,c1492,c1493,c1503,c1518,c1519,c1531,c1585,c1603,c1604,c1606,c1607,c1608,c1609,c1610,c1611,c1612,c1613,c1661,c1770,c1793,c1830,c1954,c2034,c2035,c2036,c2038,c2089,c2104,c2105,c2118,c2129,c2137,c2237,c2238]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2011]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW473+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 22:33:47 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 182.78/24.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 182.78/24.57 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------