%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWW473+3 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 01:28:37 EDT 2022
% Result : Theorem 92.46s 92.67s
% Output : Refutation 92.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 50
% Syntax : Number of clauses : 127 ( 60 unt; 30 nHn; 127 RR)
% Number of literals : 210 ( 0 equ; 73 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 66 ( 66 usr; 31 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
is_bool(bot_bot_bool),
file('SWW473+3.p',unknown),
[] ).
cnf(6,axiom,
is_bool(fFalse),
file('SWW473+3.p',unknown),
[] ).
cnf(9,axiom,
is_fun_pname_bool(u__dfg),
file('SWW473+3.p',unknown),
[] ).
cnf(10,axiom,
is_pname(pn),
file('SWW473+3.p',unknown),
[] ).
cnf(42,axiom,
equal(zero_zero_nat,bot_bot_nat),
file('SWW473+3.p',unknown),
[] ).
cnf(43,axiom,
equal(zero_zero_int,pls),
file('SWW473+3.p',unknown),
[] ).
cnf(44,axiom,
~ hBOOL(fFalse),
file('SWW473+3.p',unknown),
[] ).
cnf(66,axiom,
is_bool(hAPP_int_bool(u,v)),
file('SWW473+3.p',unknown),
[] ).
cnf(71,axiom,
is_bool(hAPP_nat_bool(u,v)),
file('SWW473+3.p',unknown),
[] ).
cnf(85,axiom,
equal(collect_int(u),u),
file('SWW473+3.p',unknown),
[] ).
cnf(86,axiom,
equal(collect_nat(u),u),
file('SWW473+3.p',unknown),
[] ).
cnf(97,axiom,
equal(number_number_of_int(u),u),
file('SWW473+3.p',unknown),
[] ).
cnf(134,axiom,
equal(collect_nat(cOMBK_bool_nat(fFalse)),bot_bot_fun_nat_bool),
file('SWW473+3.p',unknown),
[] ).
cnf(219,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,u),u)),
file('SWW473+3.p',unknown),
[] ).
cnf(224,axiom,
( hBOOL(u)
| hBOOL(hAPP_bool_bool(fNot,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(229,axiom,
equal(hAPP_nat_int(cOMBK_int_nat(u),v),u),
file('SWW473+3.p',unknown),
[] ).
cnf(234,axiom,
hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u__dfg)),
file('SWW473+3.p',unknown),
[] ).
cnf(248,axiom,
( ~ is_fun_pname_bool(u)
| is_fun_a_bool(image_pname_a(v,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(259,axiom,
( ~ is_a(u)
| is_fun949378684l_bool(hAPP_a85458249l_bool(v,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(260,axiom,
( ~ is_pname(u)
| is_a(hAPP_pname_a(v,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(311,axiom,
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_nat_bool(bot_bot_fun_nat_bool,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(312,axiom,
( ~ hBOOL(hAPP_int_bool(bot_bot_fun_int_bool,u))
| hBOOL(bot_bot_bool) ),
file('SWW473+3.p',unknown),
[] ).
cnf(346,axiom,
~ hBOOL(hAPP_int_bool(nat_neg,hAPP_nat_int(semiri1621563631at_int,u))),
file('SWW473+3.p',unknown),
[] ).
cnf(358,axiom,
~ equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v),bot_bot_fun_nat_bool),
file('SWW473+3.p',unknown),
[] ).
cnf(372,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),skf410(v,u))),
file('SWW473+3.p',unknown),
[] ).
cnf(384,axiom,
( ~ hBOOL(u)
| ~ hBOOL(hAPP_bool_bool(fNot,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(388,axiom,
hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u__dfg))),
file('SWW473+3.p',unknown),
[] ).
cnf(408,axiom,
( hBOOL(hAPP_int_bool(u,skf310(u)))
| equal(collect_int(u),bot_bot_fun_int_bool) ),
file('SWW473+3.p',unknown),
[] ).
cnf(409,axiom,
( hBOOL(hAPP_nat_bool(u,skf311(u)))
| equal(collect_nat(u),bot_bot_fun_nat_bool) ),
file('SWW473+3.p',unknown),
[] ).
cnf(449,axiom,
( ~ is_bool(u)
| equal(u,fFalse)
| equal(u,fTrue) ),
file('SWW473+3.p',unknown),
[] ).
cnf(453,axiom,
( ~ is_bool(u)
| equal(hAPP_nat_bool(cOMBK_bool_nat(u),v),u) ),
file('SWW473+3.p',unknown),
[] ).
cnf(457,axiom,
( ~ is_fun_a_bool(u)
| ~ is_fun949378684l_bool(v)
| is_bool(hAPP_fun_a_bool_bool(v,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(483,axiom,
( ~ equal(collect_nat(u),bot_bot_fun_nat_bool)
| ~ hBOOL(hAPP_nat_bool(u,v)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(489,axiom,
hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,u),v)),u)),
file('SWW473+3.p',unknown),
[] ).
cnf(506,axiom,
equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),bot_bot_fun_nat_bool),collect_nat(hAPP_n1699378549t_bool(fequal_nat,u))),
file('SWW473+3.p',unknown),
[] ).
cnf(518,axiom,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),u))
| skP4(v,w,u) ),
file('SWW473+3.p',unknown),
[] ).
cnf(523,axiom,
( ~ hBOOL(hAPP_int_bool(nat_neg,number_number_of_int(u)))
| equal(number_number_of_nat(u),zero_zero_nat) ),
file('SWW473+3.p',unknown),
[] ).
cnf(622,axiom,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),zero_zero_int))
| hBOOL(hAPP_int_bool(nat_neg,u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(630,axiom,
equal(hAPP_int_bool(u,hAPP_nat_int(v,w)),hAPP_nat_bool(cOMBB_int_bool_nat(u,v),w)),
file('SWW473+3.p',unknown),
[] ).
cnf(632,axiom,
equal(hAPP_bool_bool(u,hAPP_nat_bool(v,w)),hAPP_nat_bool(cOMBB_bool_bool_nat(u,v),w)),
file('SWW473+3.p',unknown),
[] ).
cnf(820,axiom,
( hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,u),v))
| hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,skf296(v,u)),u)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(858,axiom,
~ 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__dfg))),
file('SWW473+3.p',unknown),
[] ).
cnf(1086,axiom,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,u),v))
| ~ hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,v),u))
| equal(v,u) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1091,axiom,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,u),v))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(w,u)),image_pname_a(w,v))) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1179,axiom,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),v))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(minus_minus_int,u),v)),zero_zero_int)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1192,axiom,
( ~ hBOOL(u)
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),v))
| ~ skP4(u,w,v)
| hBOOL(w) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1341,axiom,
equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),bot_bot_fun_nat_bool))),hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)),
file('SWW473+3.p',unknown),
[] ).
cnf(1527,axiom,
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)),hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),bot_bot_fun_nat_bool)),v) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1590,axiom,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),w)),v),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,w),v)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(1738,axiom,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,u),v))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,w),v))
| hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,hAPP_f2050579477a_bool(hAPP_a1206381875a_bool(insert_a,u),w)),v)) ),
file('SWW473+3.p',unknown),
[] ).
cnf(2141,plain,
equal(cOMBK_bool_nat(fFalse),bot_bot_fun_nat_bool),
inference(rew,[status(thm),theory(equality)],[86,134]),
[iquote('0:Rew:86.0,134.0')] ).
cnf(2190,plain,
( hBOOL(hAPP_nat_bool(u,skf311(u)))
| equal(u,bot_bot_fun_nat_bool) ),
inference(rew,[status(thm),theory(equality)],[86,409]),
[iquote('0:Rew:86.0,409.1')] ).
cnf(2191,plain,
( hBOOL(hAPP_int_bool(u,skf310(u)))
| equal(u,bot_bot_fun_int_bool) ),
inference(rew,[status(thm),theory(equality)],[85,408]),
[iquote('0:Rew:85.0,408.1')] ).
cnf(2195,plain,
( ~ hBOOL(hAPP_int_bool(nat_neg,u))
| equal(number_number_of_nat(u),bot_bot_nat) ),
inference(rew,[status(thm),theory(equality)],[42,523,97]),
[iquote('0:Rew:42.0,523.1,97.0,523.0')] ).
cnf(2198,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),u))
| skP4(v,w,u) ),
inference(rew,[status(thm),theory(equality)],[43,518]),
[iquote('0:Rew:43.0,518.0')] ).
cnf(2203,plain,
equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),bot_bot_fun_nat_bool),hAPP_n1699378549t_bool(fequal_nat,u)),
inference(rew,[status(thm),theory(equality)],[86,506]),
[iquote('0:Rew:86.0,506.0')] ).
cnf(2207,plain,
( ~ hBOOL(hAPP_nat_bool(u,v))
| ~ equal(u,bot_bot_fun_nat_bool) ),
inference(rew,[status(thm),theory(equality)],[86,483]),
[iquote('0:Rew:86.0,483.0')] ).
cnf(2213,plain,
~ hBOOL(hAPP_nat_bool(cOMBB_int_bool_nat(nat_neg,semiri1621563631at_int),u)),
inference(rew,[status(thm),theory(equality)],[630,346]),
[iquote('0:Rew:630.0,346.0')] ).
cnf(2217,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),pls))
| hBOOL(hAPP_int_bool(nat_neg,u)) ),
inference(rew,[status(thm),theory(equality)],[43,622]),
[iquote('0:Rew:43.0,622.0')] ).
cnf(2349,plain,
( ~ hBOOL(u)
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),v))
| ~ skP4(u,w,v)
| hBOOL(w) ),
inference(rew,[status(thm),theory(equality)],[43,1192]),
[iquote('0:Rew:43.0,1192.1')] ).
cnf(2359,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),v))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(minus_minus_int,u),v)),pls)) ),
inference(rew,[status(thm),theory(equality)],[43,1179]),
[iquote('0:Rew:43.0,1179.1')] ).
cnf(2422,plain,
equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_n1699378549t_bool(fequal_nat,u))),hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)),
inference(rew,[status(thm),theory(equality)],[2203,1341]),
[iquote('0:Rew:2203.0,1341.0')] ).
cnf(2464,plain,
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)),hAPP_n1699378549t_bool(fequal_nat,u)),v) ),
inference(rew,[status(thm),theory(equality)],[2203,1527]),
[iquote('0:Rew:2203.0,1527.1')] ).
cnf(2671,plain,
( ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u__dfg)))
| ~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u__dfg))) ),
inference(res,[status(thm),theory(equality)],[1738,858]),
[iquote('0:Res:1738.2,858.0')] ).
cnf(2702,plain,
~ hBOOL(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u__dfg))),
inference(mrr,[status(thm)],[2671,388]),
[iquote('0:MRR:2671.0,388.0')] ).
cnf(2799,plain,
equal(cOMBB_int_bool_nat(nat_neg,semiri1621563631at_int),bot_bot_fun_nat_bool),
inference(res,[status(thm),theory(equality)],[2190,2213]),
[iquote('0:Res:2190.0,2213.0')] ).
cnf(2801,plain,
~ hBOOL(hAPP_nat_bool(bot_bot_fun_nat_bool,u)),
inference(rew,[status(thm),theory(equality)],[2799,2213]),
[iquote('0:Rew:2799.0,2213.0')] ).
cnf(2802,plain,
~ hBOOL(bot_bot_bool),
inference(mrr,[status(thm)],[311,2801]),
[iquote('0:MRR:311.1,2801.0')] ).
cnf(2804,plain,
~ hBOOL(hAPP_int_bool(bot_bot_fun_int_bool,u)),
inference(mrr,[status(thm)],[312,2802]),
[iquote('0:MRR:312.1,2802.0')] ).
cnf(2887,plain,
( equal(bot_bot_fun_int_bool,nat_neg)
| equal(number_number_of_nat(skf310(nat_neg)),bot_bot_nat) ),
inference(res,[status(thm),theory(equality)],[2191,2195]),
[iquote('0:Res:2191.0,2195.0')] ).
cnf(2891,plain,
equal(bot_bot_fun_int_bool,nat_neg),
inference(spt,[spt(split,[position(s1)])],[2887]),
[iquote('1:Spt:2887.0')] ).
cnf(2905,plain,
~ hBOOL(hAPP_int_bool(nat_neg,u)),
inference(rew,[status(thm),theory(equality)],[2891,2804]),
[iquote('1:Rew:2891.0,2804.0')] ).
cnf(2946,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),pls)),
inference(mrr,[status(thm)],[2217,2905]),
[iquote('1:MRR:2217.1,2905.0')] ).
cnf(2980,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,u),v)),
inference(mrr,[status(thm)],[2359,2946]),
[iquote('1:MRR:2359.1,2946.0')] ).
cnf(2981,plain,
$false,
inference(unc,[status(thm)],[2980,372]),
[iquote('1:UnC:2980.0,372.0')] ).
cnf(2984,plain,
~ equal(bot_bot_fun_int_bool,nat_neg),
inference(spt,[spt(split,[position(sa)])],[2981,2891]),
[iquote('1:Spt:2981.0,2887.0,2891.0')] ).
cnf(2985,plain,
equal(number_number_of_nat(skf310(nat_neg)),bot_bot_nat),
inference(spt,[spt(split,[position(s2)])],[2887]),
[iquote('1:Spt:2981.0,2887.1')] ).
cnf(3057,plain,
( equal(hAPP_int_bool(u,v),fFalse)
| equal(hAPP_int_bool(u,v),fTrue) ),
inference(ems,[status(thm)],[449,66]),
[iquote('0:EmS:449.0,66.0')] ).
cnf(3068,plain,
( equal(fFalse,bot_bot_bool)
| equal(fTrue,bot_bot_bool) ),
inference(ems,[status(thm)],[449,3]),
[iquote('0:EmS:449.0,3.0')] ).
cnf(3071,plain,
equal(fFalse,bot_bot_bool),
inference(spt,[spt(split,[position(s2s1)])],[3068]),
[iquote('2:Spt:3068.0')] ).
cnf(3074,plain,
equal(cOMBK_bool_nat(bot_bot_bool),bot_bot_fun_nat_bool),
inference(rew,[status(thm),theory(equality)],[3071,2141]),
[iquote('2:Rew:3071.0,2141.0')] ).
cnf(3183,plain,
( ~ is_bool(u)
| hBOOL(u)
| equal(cOMBK_bool_nat(u),bot_bot_fun_nat_bool) ),
inference(spr,[status(thm),theory(equality)],[453,2190]),
[iquote('0:SpR:453.1,2190.0')] ).
cnf(3186,plain,
( ~ is_bool(bot_bot_bool)
| equal(hAPP_nat_bool(bot_bot_fun_nat_bool,u),bot_bot_bool) ),
inference(spr,[status(thm),theory(equality)],[3074,453]),
[iquote('2:SpR:3074.0,453.1')] ).
cnf(3188,plain,
equal(hAPP_nat_bool(bot_bot_fun_nat_bool,u),bot_bot_bool),
inference(ssi,[status(thm)],[3186,3]),
[iquote('2:SSi:3186.0,3.0')] ).
cnf(3197,plain,
( ~ is_bool(u)
| ~ is_bool(u)
| hBOOL(u)
| equal(hAPP_nat_bool(bot_bot_fun_nat_bool,v),u) ),
inference(spr,[status(thm),theory(equality)],[3183,453]),
[iquote('0:SpR:3183.2,453.1')] ).
cnf(3199,plain,
( ~ is_bool(u)
| hBOOL(u)
| equal(hAPP_nat_bool(bot_bot_fun_nat_bool,v),u) ),
inference(obv,[status(thm),theory(equality)],[3197]),
[iquote('0:Obv:3197.0')] ).
cnf(3200,plain,
( ~ is_bool(u)
| hBOOL(u)
| equal(bot_bot_bool,u) ),
inference(rew,[status(thm),theory(equality)],[3188,3199]),
[iquote('2:Rew:3188.0,3199.2')] ).
cnf(3234,plain,
( ~ is_bool(hAPP_nat_bool(u,v))
| ~ equal(u,bot_bot_fun_nat_bool)
| equal(hAPP_nat_bool(u,v),bot_bot_bool) ),
inference(res,[status(thm),theory(equality)],[3200,2207]),
[iquote('2:Res:3200.1,2207.0')] ).
cnf(3261,plain,
( ~ equal(u,bot_bot_fun_nat_bool)
| equal(hAPP_nat_bool(u,v),bot_bot_bool) ),
inference(ssi,[status(thm)],[3234,71]),
[iquote('2:SSi:3234.0,71.0')] ).
cnf(6157,plain,
( ~ is_bool(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u__dfg)))
| equal(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u__dfg)),bot_bot_bool) ),
inference(res,[status(thm),theory(equality)],[3200,2702]),
[iquote('2:Res:3200.1,2702.0')] ).
cnf(6158,plain,
equal(hAPP_fun_a_bool_bool(hAPP_a85458249l_bool(member_a,hAPP_pname_a(mgt_call,pn)),image_pname_a(mgt_call,u__dfg)),bot_bot_bool),
inference(ssi,[status(thm)],[6157,457,259,260,10,248,9]),
[iquote('2:SSi:6157.0,457.0,259.1,260.0,10.1,248.1,9.2')] ).
cnf(10299,plain,
equal(hAPP_nat_bool(cOMBB_int_bool_nat(u,cOMBK_int_nat(v)),w),hAPP_int_bool(u,v)),
inference(spr,[status(thm),theory(equality)],[229,630]),
[iquote('0:SpR:229.0,630.0')] ).
cnf(10379,plain,
( hBOOL(hAPP_nat_bool(u,v))
| hBOOL(hAPP_nat_bool(cOMBB_bool_bool_nat(fNot,u),v)) ),
inference(spr,[status(thm),theory(equality)],[632,224]),
[iquote('0:SpR:632.0,224.1')] ).
cnf(10408,plain,
equal(hAPP_nat_bool(cOMBB_bool_bool_nat(u,bot_bot_fun_nat_bool),v),hAPP_bool_bool(u,bot_bot_bool)),
inference(spr,[status(thm),theory(equality)],[3188,632]),
[iquote('2:SpR:3188.0,632.0')] ).
cnf(10423,plain,
( hBOOL(hAPP_bool_bool(u,bot_bot_bool))
| equal(cOMBB_bool_bool_nat(u,bot_bot_fun_nat_bool),bot_bot_fun_nat_bool) ),
inference(spr,[status(thm),theory(equality)],[10408,2190]),
[iquote('2:SpR:10408.0,2190.0')] ).
cnf(10479,plain,
( ~ hBOOL(bot_bot_bool)
| equal(cOMBB_bool_bool_nat(fNot,bot_bot_fun_nat_bool),bot_bot_fun_nat_bool) ),
inference(res,[status(thm),theory(equality)],[10423,384]),
[iquote('2:Res:10423.0,384.1')] ).
cnf(37496,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,u),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,u),v)))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,u),v),u) ),
inference(res,[status(thm),theory(equality)],[489,1086]),
[iquote('0:Res:489.0,1086.0')] ).
cnf(39009,plain,
( ~ hBOOL(u)
| ~ skP4(u,v,pls)
| hBOOL(v) ),
inference(res,[status(thm),theory(equality)],[219,2349]),
[iquote('0:Res:219.0,2349.1')] ).
cnf(39571,plain,
( ~ equal(cOMBB_bool_bool_nat(fNot,u),bot_bot_fun_nat_bool)
| hBOOL(hAPP_nat_bool(u,v))
| hBOOL(bot_bot_bool) ),
inference(spr,[status(thm),theory(equality)],[3261,10379]),
[iquote('2:SpR:3261.1,10379.1')] ).
cnf(39575,plain,
( ~ equal(cOMBB_bool_bool_nat(fNot,u),bot_bot_fun_nat_bool)
| hBOOL(hAPP_nat_bool(u,v)) ),
inference(mrr,[status(thm)],[39571,2802]),
[iquote('2:MRR:39571.2,2802.0')] ).
cnf(39700,plain,
( ~ equal(cOMBB_bool_bool_nat(fNot,bot_bot_fun_nat_bool),bot_bot_fun_nat_bool)
| hBOOL(bot_bot_bool) ),
inference(spr,[status(thm),theory(equality)],[3188,39575]),
[iquote('2:SpR:3188.0,39575.1')] ).
cnf(39723,plain,
~ equal(cOMBB_bool_bool_nat(fNot,bot_bot_fun_nat_bool),bot_bot_fun_nat_bool),
inference(mrr,[status(thm)],[39700,2802]),
[iquote('2:MRR:39700.1,2802.0')] ).
cnf(39724,plain,
~ hBOOL(bot_bot_bool),
inference(mrr,[status(thm)],[10479,39723]),
[iquote('2:MRR:10479.1,39723.0')] ).
cnf(45523,plain,
( hBOOL(hAPP_int_bool(u,v))
| equal(cOMBB_int_bool_nat(u,cOMBK_int_nat(v)),bot_bot_fun_nat_bool) ),
inference(spr,[status(thm),theory(equality)],[10299,2190]),
[iquote('0:SpR:10299.0,2190.0')] ).
cnf(45554,plain,
( hBOOL(hAPP_int_bool(u,v))
| equal(hAPP_nat_bool(bot_bot_fun_nat_bool,w),hAPP_int_bool(u,v)) ),
inference(spr,[status(thm),theory(equality)],[45523,10299]),
[iquote('0:SpR:45523.1,10299.0')] ).
cnf(45711,plain,
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_n1699378549t_bool(fequal_nat,u))))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)),hAPP_n1699378549t_bool(fequal_nat,u)),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_n1699378549t_bool(fequal_nat,u))) ),
inference(spr,[status(thm),theory(equality)],[2422,2464]),
[iquote('0:SpR:2422.0,2464.1')] ).
cnf(50975,plain,
( ~ hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u__dfg))
| hBOOL(bot_bot_bool) ),
inference(spr,[status(thm),theory(equality)],[6158,1091]),
[iquote('2:SpR:6158.0,1091.1')] ).
cnf(50986,plain,
$false,
inference(mrr,[status(thm)],[50975,234,39724]),
[iquote('2:MRR:50975.0,50975.1,234.0,39724.0')] ).
cnf(50988,plain,
~ equal(fFalse,bot_bot_bool),
inference(spt,[spt(split,[position(s2sa)])],[50986,3071]),
[iquote('2:Spt:50986.0,3068.0,3071.0')] ).
cnf(50989,plain,
equal(fTrue,bot_bot_bool),
inference(spt,[spt(split,[position(s2s2)])],[3068]),
[iquote('2:Spt:50986.0,3068.1')] ).
cnf(51089,plain,
( equal(hAPP_int_bool(u,v),fFalse)
| equal(hAPP_int_bool(u,v),bot_bot_bool) ),
inference(rew,[status(thm),theory(equality)],[50989,3057]),
[iquote('2:Rew:50989.0,3057.1')] ).
cnf(51547,plain,
( ~ is_bool(fFalse)
| equal(hAPP_nat_bool(bot_bot_fun_nat_bool,u),fFalse) ),
inference(spr,[status(thm),theory(equality)],[2141,453]),
[iquote('0:SpR:2141.0,453.1')] ).
cnf(51551,plain,
equal(hAPP_nat_bool(bot_bot_fun_nat_bool,u),fFalse),
inference(ssi,[status(thm)],[51547,6]),
[iquote('0:SSi:51547.0,6.0')] ).
cnf(51554,plain,
( hBOOL(hAPP_int_bool(u,v))
| equal(hAPP_int_bool(u,v),fFalse) ),
inference(rew,[status(thm),theory(equality)],[51551,45554]),
[iquote('0:Rew:51551.0,45554.1')] ).
cnf(51557,plain,
( hBOOL(bot_bot_bool)
| equal(hAPP_int_bool(u,v),fFalse) ),
inference(rew,[status(thm),theory(equality)],[51089,51554]),
[iquote('2:Rew:51089.1,51554.0')] ).
cnf(51558,plain,
equal(hAPP_int_bool(u,v),fFalse),
inference(mrr,[status(thm)],[51557,2802]),
[iquote('2:MRR:51557.0,2802.0')] ).
cnf(51608,plain,
( hBOOL(fFalse)
| skP4(u,v,w) ),
inference(rew,[status(thm),theory(equality)],[51558,2198]),
[iquote('2:Rew:51558.0,2198.0')] ).
cnf(52882,plain,
skP4(u,v,w),
inference(mrr,[status(thm)],[51608,44]),
[iquote('2:MRR:51608.0,44.0')] ).
cnf(52883,plain,
( ~ hBOOL(u)
| hBOOL(v) ),
inference(mrr,[status(thm)],[39009,52882]),
[iquote('2:MRR:39009.1,52882.0')] ).
cnf(52958,plain,
hBOOL(hAPP_f54304608l_bool(hAPP_f103356543l_bool(ord_le1568362934t_bool,u),v)),
inference(mrr,[status(thm)],[820,52883]),
[iquote('2:MRR:820.1,52883.0')] ).
cnf(53943,plain,
equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,u),v),u),
inference(mrr,[status(thm)],[37496,52958]),
[iquote('2:MRR:37496.0,52958.0')] ).
cnf(54546,plain,
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_n1699378549t_bool(fequal_nat,u))))
| equal(hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,v),hAPP_n1699378549t_bool(fequal_nat,u)),hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v)) ),
inference(rew,[status(thm),theory(equality)],[53943,45711]),
[iquote('2:Rew:53943.0,45711.1')] ).
cnf(54552,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),w),hAPP_f800510211t_bool(hAPP_f1730770594t_bool(minus_2067140911t_bool,w),v)) ),
inference(rew,[status(thm),theory(equality)],[53943,1590]),
[iquote('2:Rew:53943.0,1590.1')] ).
cnf(57911,plain,
( ~ hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),w),w) ),
inference(rew,[status(thm),theory(equality)],[53943,54552]),
[iquote('2:Rew:53943.0,54552.1')] ).
cnf(58218,plain,
( hBOOL(hAPP_f54304608l_bool(hAPP_n215258509l_bool(member_nat,u),v))
| equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v),v) ),
inference(rew,[status(thm),theory(equality)],[53943,54546]),
[iquote('2:Rew:53943.0,54546.1,53943.0,54546.0')] ).
cnf(58219,plain,
equal(hAPP_f800510211t_bool(hAPP_n1512601776t_bool(insert_nat,u),v),v),
inference(mrr,[status(thm)],[58218,57911]),
[iquote('2:MRR:58218.0,57911.0')] ).
cnf(58220,plain,
$false,
inference(unc,[status(thm)],[58219,358]),
[iquote('2:UnC:58219.0,358.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SWW473+3 : TPTP v8.1.0. Released v5.3.0.
% 0.08/0.15 % Command : run_spass %d %s
% 0.16/0.37 % Computer : n021.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 600
% 0.16/0.37 % DateTime : Sat Jun 4 11:35:33 EDT 2022
% 0.16/0.37 % CPUTime :
% 92.46/92.67
% 92.46/92.67 SPASS V 3.9
% 92.46/92.67 SPASS beiseite: Proof found.
% 92.46/92.67 % SZS status Theorem
% 92.46/92.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 92.46/92.67 SPASS derived 43749 clauses, backtracked 2365 clauses, performed 4 splits and kept 17775 clauses.
% 92.46/92.67 SPASS allocated 142281 KBytes.
% 92.46/92.67 SPASS spent 0:1:32.23 on the problem.
% 92.46/92.67 0:00:00.07 for the input.
% 92.46/92.67 0:00:03.39 for the FLOTTER CNF translation.
% 92.46/92.67 0:00:02.32 for inferences.
% 92.46/92.67 0:00:03.46 for the backtracking.
% 92.46/92.67 0:1:20.69 for the reduction.
% 92.46/92.67
% 92.46/92.67
% 92.46/92.67 Here is a proof with depth 5, length 127 :
% 92.46/92.67 % SZS output start Refutation
% See solution above
% 92.46/92.67 Formulae used in the proof : gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool gsy_c_fFalse gsy_v_U gsy_v_pn fact_930_bot__nat__def fact_1180_Pls__def help_fFalse_1_1_U gsy_c_hAPP_000tc__Int__Oint_000tc__HOL__Obool gsy_c_hAPP_000tc__Nat__Onat_000tc__HOL__Obool fact_380_Collect__def fact_381_Collect__def fact_1071_number__of__is__id fact_539_empty__def fact_1044_zle__refl help_fNot_2_1_U help_COMBK_1_1_COMBK_000tc__Int__Oint_000tc__Nat__Onat_U conj_4 gsy_c_Set_Oimage_000tc__Com__Opname_000t__a gsy_c_hAPP_000t__a_000tc__fun_Itc__fun_It__a_Mtc__HOL__Obool_J_Mtc__HOL__Obool_J gsy_c_hAPP_000tc__Com__Opname_000t__a fact_541_bot__fun__def fact_542_bot__fun__def fact_1151_not__neg__int fact_607_empty__not__insert fact_1081_int__gr__induct fact_1056_zless__add1__eq help_fNot_1_1_U conj_1 fact_521_empty__Collect__eq fact_522_empty__Collect__eq help_If_3_1_If_000tc__Nat__Onat_T help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Nat__Onat_U gsy_c_hAPP_000tc__fun_It__a_Mtc__HOL__Obool_J_000tc__HOL__Obool fact_587_Diff__subset fact_641_singleton__conv2 fact_1089_conj__le__cong fact_1153_neg__imp__number__of__eq__0 fact_1146_neg__def help_COMBB_1_1_COMBB_000tc__Int__Oint_000tc__HOL__Obool_000tc__Nat__Onat_U help_COMBB_1_1_COMBB_000tc__HOL__Obool_000tc__HOL__Obool_000tc__Nat__Onat_U fact_478_subsetI conj_6 fact_405_set__eq__subset fact_436_rev__image__eqI fact_1037_less__bin__lemma fact_553_insert__Diff__single fact_550_Diff__insert__absorb fact_578_insert__Diff__if fact_453_insert__subset
% 94.33/94.58
%------------------------------------------------------------------------------