%------------------------------------------------------------------------------
% File : SPASS+T---2.2.22
% Problem : ITP012_2 : TPTP v8.1.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : spasst-tptp-script %s %d
% Computer : n032.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 : Sun Jul 17 00:39:49 EDT 2022
% Result : Theorem 12.80s 7.20s
% Output : Refutation 12.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 40
% Syntax : Number of clauses : 157 ( 44 unt; 36 nHn; 145 RR)
% Number of literals : 394 ( 0 equ; 206 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 14 con; 0-3 aty)
% Number of variables : 127 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(20,axiom,
p(c_2Ebool_2ET),
file('ITP012_2.p',unknown),
[] ).
cnf(21,axiom,
tp__o(fo__c_2Ebool_2EF),
file('ITP012_2.p',unknown),
[] ).
cnf(23,axiom,
del(ty_2Einteger_2Eint),
file('ITP012_2.p',unknown),
[] ).
cnf(24,axiom,
tp__o(fo__c_2Ebool_2ET),
file('ITP012_2.p',unknown),
[] ).
cnf(29,axiom,
tp__ty_2Einteger_2Eint(skc8),
file('ITP012_2.p',unknown),
[] ).
cnf(30,axiom,
tp__ty_2Einteger_2Eint(skc7),
file('ITP012_2.p',unknown),
[] ).
cnf(31,axiom,
tp__ty_2Einteger_2Eint(skc6),
file('ITP012_2.p',unknown),
[] ).
cnf(32,axiom,
~ p(c_2Ebool_2EF),
file('ITP012_2.p',unknown),
[] ).
cnf(33,axiom,
mem(c_2Ebool_2EF,bool),
file('ITP012_2.p',unknown),
[] ).
cnf(34,axiom,
mem(c_2Ebool_2ET,bool),
file('ITP012_2.p',unknown),
[] ).
cnf(37,axiom,
equal(inj__o(fo__c_2Ebool_2EF),c_2Ebool_2EF),
file('ITP012_2.p',unknown),
[] ).
cnf(38,axiom,
equal(inj__o(fo__c_2Ebool_2ET),c_2Ebool_2ET),
file('ITP012_2.p',unknown),
[] ).
cnf(44,axiom,
( ~ tp__o(U)
| tp__o(fo__c_2Ebool_2E_7E(U)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(45,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(U)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(59,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| mem(inj__ty_2Einteger_2Eint(U),ty_2Einteger_2Eint) ),
file('ITP012_2.p',unknown),
[] ).
cnf(60,axiom,
( ~ tp__o(U)
| mem(inj__o(U),bool) ),
file('ITP012_2.p',unknown),
[] ).
cnf(66,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(U)),U) ),
file('ITP012_2.p',unknown),
[] ).
cnf(67,axiom,
( ~ tp__o(U)
| equal(surj__o(inj__o(U)),U) ),
file('ITP012_2.p',unknown),
[] ).
cnf(68,axiom,
p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(skc7))),
file('ITP012_2.p',unknown),
[] ).
cnf(78,axiom,
( mem(skf15(U,V,W),U)
| skP1(X,Y,U) ),
file('ITP012_2.p',unknown),
[] ).
cnf(79,axiom,
( ~ mem(U,bool)
| p(U)
| p(ap(c_2Ebool_2E_7E,U)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(83,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| tp__o(fo__c_2Einteger_2Eint__divides(U,V)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(84,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(U,V)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(85,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,V)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(96,axiom,
( ~ tp__o(U)
| equal(ap(c_2Ebool_2E_7E,inj__o(U)),inj__o(fo__c_2Ebool_2E_7E(U))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(97,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(U))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(111,axiom,
( ~ p(U)
| ~ p(ap(c_2Ebool_2E_7E,U))
| ~ mem(U,bool) ),
file('ITP012_2.p',unknown),
[] ).
cnf(114,axiom,
( ~ mem(U,V)
| ~ skP1(W,X,V)
| p(ap(W,U)) ),
file('ITP012_2.p',unknown),
[] ).
cnf(118,axiom,
( ~ del(U)
| ~ mem(V,U)
| equal(ap(k(U,W),V),W) ),
file('ITP012_2.p',unknown),
[] ).
cnf(120,axiom,
( ~ mem(U,bool)
| ~ mem(V,bool)
| p(U)
| p(V)
| equal(U,V) ),
file('ITP012_2.p',unknown),
[] ).
cnf(135,axiom,
( ~ p(U)
| ~ p(V)
| ~ mem(U,bool)
| ~ mem(V,bool)
| equal(U,V) ),
file('ITP012_2.p',unknown),
[] ).
cnf(144,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| equal(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(V)),inj__o(fo__c_2Einteger_2Eint__divides(U,V))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(145,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| equal(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(V)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(U,V))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(146,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| equal(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(V)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,V))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(154,axiom,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(skc6)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(skc7)))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(165,axiom,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(skc6)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(skc7)))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(170,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| equal(surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(U)))),surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V)),inj__ty_2Einteger_2Eint(U)))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(173,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(V)),inj__ty_2Einteger_2Eint(U)))
| ~ tp__ty_2Einteger_2Eint(V)
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(V)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(U)))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(187,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(V))))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),inj__ty_2Einteger_2Eint(V)))
| ~ tp__ty_2Einteger_2Eint(W)
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),inj__ty_2Einteger_2Eint(U))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(188,axiom,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),inj__ty_2Einteger_2Eint(U)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),inj__ty_2Einteger_2Eint(V)))
| ~ tp__ty_2Einteger_2Eint(W)
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(W)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(V)))) ),
file('ITP012_2.p',unknown),
[] ).
cnf(190,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| equal(surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(V)))),surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,V)))) ),
inference(rew,[status(thm),theory(equality)],[97,170,146]),
[iquote('0:Rew:97.1,170.2,146.2,170.2')] ).
cnf(193,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(U,V)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(V)))) ),
inference(rew,[status(thm),theory(equality)],[97,173,144]),
[iquote('0:Rew:97.1,173.3,144.2,173.1')] ).
cnf(196,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ tp__ty_2Einteger_2Eint(W)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(U,V)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(W,V))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(U,W))) ),
inference(rew,[status(thm),theory(equality)],[144,187,145]),
[iquote('0:Rew:144.2,187.5,144.2,187.3,145.2,187.2')] ).
cnf(197,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ tp__ty_2Einteger_2Eint(W)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(U,V)))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(U,W)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(W,V)))) ),
inference(rew,[status(thm),theory(equality)],[145,188,144]),
[iquote('0:Rew:145.2,188.5,144.2,188.3,144.2,188.2')] ).
cnf(209,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| tp__o(fo__c_2Einteger_2Eint__divides(U,skc6)) ),
inference(res,[status(thm),theory(equality)],[31,83]),
[iquote('0:Res:31.0,83.0')] ).
cnf(223,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,U))) ),
inference(res,[status(thm),theory(equality)],[31,145]),
[iquote('0:Res:31.0,145.1')] ).
cnf(226,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,U)) ),
inference(res,[status(thm),theory(equality)],[31,84]),
[iquote('0:Res:31.0,84.1')] ).
cnf(233,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(U,skc7)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7)))) ),
inference(res,[status(thm),theory(equality)],[30,193]),
[iquote('0:Res:30.0,193.0')] ).
cnf(236,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7)))),surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,skc7)))) ),
inference(res,[status(thm),theory(equality)],[30,190]),
[iquote('0:Res:30.0,190.0')] ).
cnf(239,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(U)),inj__ty_2Einteger_2Eint(skc7)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,skc7))) ),
inference(res,[status(thm),theory(equality)],[30,146]),
[iquote('0:Res:30.0,146.0')] ).
cnf(243,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(U,skc7)) ),
inference(res,[status(thm),theory(equality)],[30,85]),
[iquote('0:Res:30.0,85.0')] ).
cnf(245,plain,
mem(inj__ty_2Einteger_2Eint(skc7),ty_2Einteger_2Eint),
inference(res,[status(thm),theory(equality)],[30,59]),
[iquote('0:Res:30.0,59.0')] ).
cnf(246,plain,
tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7)),
inference(res,[status(thm),theory(equality)],[30,45]),
[iquote('0:Res:30.0,45.0')] ).
cnf(286,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(U)),inj__o(fo__c_2Einteger_2Eint__divides(skc8,U))) ),
inference(res,[status(thm),theory(equality)],[29,144]),
[iquote('0:Res:29.0,144.1')] ).
cnf(289,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| tp__o(fo__c_2Einteger_2Eint__divides(skc8,U)) ),
inference(res,[status(thm),theory(equality)],[29,83]),
[iquote('0:Res:29.0,83.1')] ).
cnf(292,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,U)))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,V)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(V,U)))) ),
inference(res,[status(thm),theory(equality)],[29,197]),
[iquote('0:Res:29.0,197.4')] ).
cnf(293,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| ~ tp__ty_2Einteger_2Eint(V)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,U)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(V,U))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,V))) ),
inference(res,[status(thm),theory(equality)],[29,196]),
[iquote('0:Res:29.0,196.4')] ).
cnf(337,plain,
equal(surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7)))),surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))),
inference(res,[status(thm),theory(equality)],[31,236]),
[iquote('0:Res:31.0,236.0')] ).
cnf(354,plain,
equal(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(skc6)),inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))),
inference(res,[status(thm),theory(equality)],[31,286]),
[iquote('0:Res:31.0,286.0')] ).
cnf(361,plain,
equal(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(skc7)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7))),
inference(res,[status(thm),theory(equality)],[31,239]),
[iquote('0:Res:31.0,239.0')] ).
cnf(372,plain,
tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)),
inference(res,[status(thm),theory(equality)],[31,289]),
[iquote('0:Res:31.0,289.0')] ).
cnf(379,plain,
tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)),
inference(res,[status(thm),theory(equality)],[31,243]),
[iquote('0:Res:31.0,243.0')] ).
cnf(406,plain,
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(skc7)))) ),
inference(rew,[status(thm),theory(equality)],[354,165]),
[iquote('0:Rew:354.0,165.0')] ).
cnf(407,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(skc6)),inj__ty_2Einteger_2Eint(skc7)))) ),
inference(rew,[status(thm),theory(equality)],[354,154]),
[iquote('0:Rew:354.0,154.0')] ).
cnf(408,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(rew,[status(thm),theory(equality)],[361,407]),
[iquote('0:Rew:361.0,407.1')] ).
cnf(409,plain,
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(rew,[status(thm),theory(equality)],[361,406]),
[iquote('0:Rew:361.0,406.1')] ).
cnf(434,plain,
( ~ tp__o(fo__c_2Ebool_2ET)
| equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET) ),
inference(spr,[status(thm),theory(equality)],[38,67]),
[iquote('0:SpR:38.0,67.1')] ).
cnf(435,plain,
( ~ tp__o(fo__c_2Ebool_2EF)
| equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF) ),
inference(spr,[status(thm),theory(equality)],[37,67]),
[iquote('0:SpR:37.0,67.1')] ).
cnf(436,plain,
equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET),
inference(mrr,[status(thm)],[434,24]),
[iquote('0:MRR:434.0,24.0')] ).
cnf(437,plain,
equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF),
inference(mrr,[status(thm)],[435,21]),
[iquote('0:MRR:435.0,21.0')] ).
cnf(462,plain,
( ~ tp__o(U)
| ~ mem(inj__o(U),bool)
| p(inj__o(U))
| p(inj__o(fo__c_2Ebool_2E_7E(U))) ),
inference(spr,[status(thm),theory(equality)],[96,79]),
[iquote('0:SpR:96.1,79.2')] ).
cnf(469,plain,
( ~ tp__o(U)
| p(inj__o(U))
| p(inj__o(fo__c_2Ebool_2E_7E(U))) ),
inference(mrr,[status(thm)],[462,60]),
[iquote('0:MRR:462.1,60.1')] ).
cnf(491,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| ~ p(inj__o(fo__c_2Ebool_2E_7E(U)))
| ~ mem(inj__o(U),bool) ),
inference(spl,[status(thm),theory(equality)],[96,111]),
[iquote('0:SpL:96.1,111.1')] ).
cnf(496,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| ~ p(inj__o(fo__c_2Ebool_2E_7E(U))) ),
inference(mrr,[status(thm)],[491,60]),
[iquote('0:MRR:491.3,60.1')] ).
cnf(556,plain,
( ~ mem(U,V)
| mem(skf15(V,W,X),V)
| p(ap(Y,U)) ),
inference(res,[status(thm),theory(equality)],[78,114]),
[iquote('0:Res:78.1,114.1')] ).
cnf(578,plain,
( mem(skf15(bool,U,V),bool)
| p(ap(W,c_2Ebool_2ET)) ),
inference(res,[status(thm),theory(equality)],[34,556]),
[iquote('0:Res:34.0,556.0')] ).
cnf(583,plain,
( mem(skf15(ty_2Einteger_2Eint,U,V),ty_2Einteger_2Eint)
| p(ap(W,inj__ty_2Einteger_2Eint(skc7))) ),
inference(res,[status(thm),theory(equality)],[245,556]),
[iquote('0:Res:245.0,556.0')] ).
cnf(658,plain,
( ~ mem(U,bool)
| p(c_2Ebool_2EF)
| p(U)
| equal(c_2Ebool_2EF,U) ),
inference(res,[status(thm),theory(equality)],[33,120]),
[iquote('0:Res:33.0,120.0')] ).
cnf(662,plain,
( ~ mem(U,bool)
| p(U)
| equal(c_2Ebool_2EF,U) ),
inference(mrr,[status(thm)],[658,32]),
[iquote('0:MRR:658.1,32.0')] ).
cnf(673,plain,
( ~ tp__o(U)
| p(inj__o(U))
| equal(inj__o(U),c_2Ebool_2EF) ),
inference(res,[status(thm),theory(equality)],[60,662]),
[iquote('0:Res:60.1,662.0')] ).
cnf(679,plain,
p(ap(U,c_2Ebool_2ET)),
inference(spt,[spt(split,[position(s1)])],[578]),
[iquote('1:Spt:578.1')] ).
cnf(683,plain,
( ~ p(c_2Ebool_2ET)
| ~ mem(c_2Ebool_2ET,bool) ),
inference(res,[status(thm),theory(equality)],[679,111]),
[iquote('1:Res:679.0,111.1')] ).
cnf(685,plain,
$false,
inference(mrr,[status(thm)],[683,20,34]),
[iquote('1:MRR:683.0,683.1,20.0,34.0')] ).
cnf(686,plain,
mem(skf15(bool,U,V),bool),
inference(spt,[spt(split,[position(s2)])],[578]),
[iquote('1:Spt:685.0,578.0')] ).
cnf(691,plain,
p(ap(U,inj__ty_2Einteger_2Eint(skc7))),
inference(spt,[spt(split,[position(s2s1)])],[583]),
[iquote('2:Spt:583.1')] ).
cnf(711,plain,
( ~ del(U)
| ~ mem(inj__ty_2Einteger_2Eint(skc7),U)
| p(V) ),
inference(spr,[status(thm),theory(equality)],[118,691]),
[iquote('2:SpR:118.2,691.0')] ).
cnf(769,plain,
( ~ tp__o(fo__c_2Ebool_2E_7E(U))
| ~ tp__o(U)
| ~ p(inj__o(U))
| equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF) ),
inference(res,[status(thm),theory(equality)],[673,496]),
[iquote('0:Res:673.1,496.2')] ).
cnf(772,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF) ),
inference(mrr,[status(thm)],[769,44]),
[iquote('0:MRR:769.0,44.1')] ).
cnf(807,plain,
( ~ tp__ty_2Einteger_2Eint(skc7)
| ~ del(ty_2Einteger_2Eint)
| p(U) ),
inference(res,[status(thm),theory(equality)],[59,711]),
[iquote('2:Res:59.1,711.1')] ).
cnf(818,plain,
p(U),
inference(mrr,[status(thm)],[807,30,23]),
[iquote('2:MRR:807.0,807.1,30.0,23.0')] ).
cnf(819,plain,
$false,
inference(unc,[status(thm)],[818,32]),
[iquote('2:UnC:818.0,32.0')] ).
cnf(823,plain,
mem(skf15(ty_2Einteger_2Eint,U,V),ty_2Einteger_2Eint),
inference(spt,[spt(split,[position(s2s2)])],[583]),
[iquote('2:Spt:819.0,583.0')] ).
cnf(827,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| ~ tp__o(fo__c_2Ebool_2E_7E(U))
| equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2E_7E(U)) ),
inference(spr,[status(thm),theory(equality)],[772,67]),
[iquote('0:SpR:772.2,67.1')] ).
cnf(835,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| ~ tp__o(fo__c_2Ebool_2E_7E(U))
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) ),
inference(rew,[status(thm),theory(equality)],[437,827]),
[iquote('0:Rew:437.0,827.3')] ).
cnf(836,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) ),
inference(mrr,[status(thm)],[835,44]),
[iquote('0:MRR:835.2,44.1')] ).
cnf(848,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) ),
inference(res,[status(thm),theory(equality)],[673,836]),
[iquote('0:Res:673.1,836.1')] ).
cnf(851,plain,
( ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) ),
inference(obv,[status(thm),theory(equality)],[848]),
[iquote('0:Obv:848.0')] ).
cnf(860,plain,
p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))),
inference(spt,[spt(split,[position(s2s2s1)])],[408]),
[iquote('3:Spt:408.0')] ).
cnf(863,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))),
inference(mrr,[status(thm)],[409,860]),
[iquote('3:MRR:409.0,860.0')] ).
cnf(872,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)
| equal(surj__o(c_2Ebool_2EF),U) ),
inference(spr,[status(thm),theory(equality)],[851,67]),
[iquote('0:SpR:851.1,67.1')] ).
cnf(881,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)
| equal(surj__o(c_2Ebool_2EF),U) ),
inference(obv,[status(thm),theory(equality)],[872]),
[iquote('0:Obv:872.0')] ).
cnf(882,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)
| equal(fo__c_2Ebool_2EF,U) ),
inference(rew,[status(thm),theory(equality)],[437,881]),
[iquote('0:Rew:437.0,881.2')] ).
cnf(892,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| p(inj__o(U))
| p(inj__o(fo__c_2Ebool_2EF)) ),
inference(spr,[status(thm),theory(equality)],[882,469]),
[iquote('0:SpR:882.1,469.2')] ).
cnf(901,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| p(inj__o(U))
| p(inj__o(fo__c_2Ebool_2EF)) ),
inference(obv,[status(thm),theory(equality)],[892]),
[iquote('0:Obv:892.0')] ).
cnf(902,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| p(inj__o(U))
| p(c_2Ebool_2EF) ),
inference(rew,[status(thm),theory(equality)],[37,901]),
[iquote('0:Rew:37.0,901.3')] ).
cnf(903,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| p(inj__o(U)) ),
inference(mrr,[status(thm)],[902,32]),
[iquote('0:MRR:902.3,32.0')] ).
cnf(1036,plain,
( ~ p(c_2Ebool_2ET)
| ~ p(U)
| ~ mem(U,bool)
| equal(c_2Ebool_2ET,U) ),
inference(res,[status(thm),theory(equality)],[34,135]),
[iquote('0:Res:34.0,135.2')] ).
cnf(1042,plain,
( ~ p(U)
| ~ mem(U,bool)
| equal(c_2Ebool_2ET,U) ),
inference(mrr,[status(thm)],[1036,20]),
[iquote('0:MRR:1036.0,20.0')] ).
cnf(1052,plain,
( ~ tp__o(U)
| ~ p(inj__o(U))
| equal(inj__o(U),c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[60,1042]),
[iquote('0:Res:60.1,1042.1')] ).
cnf(1067,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| equal(inj__o(U),c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[903,1052]),
[iquote('0:Res:903.2,1052.1')] ).
cnf(1068,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(inj__o(U),c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[673,1052]),
[iquote('0:Res:673.1,1052.1')] ).
cnf(1071,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))
| equal(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)),c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[860,1052]),
[iquote('3:Res:860.0,1052.1')] ).
cnf(1072,plain,
equal(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)),c_2Ebool_2ET),
inference(mrr,[status(thm)],[1071,372]),
[iquote('3:MRR:1071.0,372.0')] ).
cnf(1075,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| equal(inj__o(U),c_2Ebool_2ET) ),
inference(obv,[status(thm),theory(equality)],[1067]),
[iquote('0:Obv:1067.0')] ).
cnf(1077,plain,
( ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(inj__o(U),c_2Ebool_2ET) ),
inference(obv,[status(thm),theory(equality)],[1068]),
[iquote('0:Obv:1068.0')] ).
cnf(1087,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),surj__o(c_2Ebool_2ET)) ),
inference(spr,[status(thm),theory(equality)],[1072,67]),
[iquote('3:SpR:1072.0,67.1')] ).
cnf(1090,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),fo__c_2Ebool_2ET) ),
inference(rew,[status(thm),theory(equality)],[436,1087]),
[iquote('3:Rew:436.0,1087.1')] ).
cnf(1091,plain,
equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),fo__c_2Ebool_2ET),
inference(mrr,[status(thm)],[1090,372]),
[iquote('3:MRR:1090.0,372.0')] ).
cnf(1162,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| equal(surj__o(c_2Ebool_2ET),U) ),
inference(spr,[status(thm),theory(equality)],[1075,67]),
[iquote('0:SpR:1075.2,67.1')] ).
cnf(1170,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| equal(surj__o(c_2Ebool_2ET),U) ),
inference(obv,[status(thm),theory(equality)],[1162]),
[iquote('0:Obv:1162.0')] ).
cnf(1171,plain,
( ~ tp__o(U)
| equal(fo__c_2Ebool_2EF,U)
| equal(fo__c_2Ebool_2ET,U) ),
inference(rew,[status(thm),theory(equality)],[436,1170]),
[iquote('0:Rew:436.0,1170.2')] ).
cnf(1183,plain,
( ~ tp__ty_2Einteger_2Eint(U)
| equal(fo__c_2Einteger_2Eint__divides(U,skc6),fo__c_2Ebool_2EF)
| equal(fo__c_2Einteger_2Eint__divides(U,skc6),fo__c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[209,1171]),
[iquote('0:Res:209.1,1171.0')] ).
cnf(1354,plain,
( ~ tp__ty_2Einteger_2Eint(skc8)
| ~ tp__ty_2Einteger_2Eint(skc7)
| p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc7))) ),
inference(spr,[status(thm),theory(equality)],[144,68]),
[iquote('0:SpR:144.2,68.0')] ).
cnf(1360,plain,
p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc7))),
inference(mrr,[status(thm)],[1354,29,30]),
[iquote('0:MRR:1354.0,1354.1,29.0,30.0')] ).
cnf(1684,plain,
( ~ tp__o(U)
| ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(surj__o(c_2Ebool_2ET),U) ),
inference(spr,[status(thm),theory(equality)],[1077,67]),
[iquote('0:SpR:1077.2,67.1')] ).
cnf(1711,plain,
( ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(surj__o(c_2Ebool_2ET),U) ),
inference(obv,[status(thm),theory(equality)],[1684]),
[iquote('0:Obv:1684.0')] ).
cnf(1712,plain,
( ~ tp__o(U)
| equal(inj__o(U),c_2Ebool_2EF)
| equal(fo__c_2Ebool_2ET,U) ),
inference(rew,[status(thm),theory(equality)],[436,1711]),
[iquote('0:Rew:436.0,1711.2')] ).
cnf(1763,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc7))
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc7),fo__c_2Ebool_2ET)
| p(c_2Ebool_2EF) ),
inference(spr,[status(thm),theory(equality)],[1712,1360]),
[iquote('0:SpR:1712.1,1360.0')] ).
cnf(1776,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,skc7))
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc7),fo__c_2Ebool_2ET) ),
inference(mrr,[status(thm)],[1763,32]),
[iquote('0:MRR:1763.2,32.0')] ).
cnf(1804,plain,
( ~ tp__ty_2Einteger_2Eint(skc7)
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc7),fo__c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[289,1776]),
[iquote('0:Res:289.1,1776.0')] ).
cnf(1807,plain,
equal(fo__c_2Einteger_2Eint__divides(skc8,skc7),fo__c_2Ebool_2ET),
inference(mrr,[status(thm)],[1804,30]),
[iquote('0:MRR:1804.0,30.0')] ).
cnf(10131,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| equal(surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)))),surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(spr,[status(thm),theory(equality)],[223,337]),
[iquote('0:SpR:223.1,337.0')] ).
cnf(10132,plain,
equal(surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)))),surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))),
inference(mrr,[status(thm)],[10131,246]),
[iquote('0:MRR:10131.0,246.0')] ).
cnf(10137,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)))
| equal(surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7))),fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7))) ),
inference(spr,[status(thm),theory(equality)],[10132,66]),
[iquote('0:SpR:10132.0,66.1')] ).
cnf(13161,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)))
| ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7))
| equal(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Einteger_2Eint__sub(skc6,skc7)) ),
inference(spr,[status(thm),theory(equality)],[10137,66]),
[iquote('0:SpR:10137.1,66.1')] ).
cnf(13163,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)))
| equal(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Einteger_2Eint__sub(skc6,skc7)) ),
inference(mrr,[status(thm)],[13161,379]),
[iquote('0:MRR:13161.1,379.0')] ).
cnf(13167,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| equal(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Einteger_2Eint__sub(skc6,skc7)) ),
inference(res,[status(thm),theory(equality)],[226,13163]),
[iquote('0:Res:226.1,13163.0')] ).
cnf(13169,plain,
equal(fo__c_2Einteger_2Eint__add(skc6,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Einteger_2Eint__sub(skc6,skc7)),
inference(mrr,[status(thm)],[13167,246]),
[iquote('0:MRR:13167.0,246.0')] ).
cnf(15863,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc8)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc7)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)))) ),
inference(spr,[status(thm),theory(equality)],[286,233]),
[iquote('0:SpR:286.1,233.2')] ).
cnf(15879,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc8)
| ~ p(c_2Ebool_2ET)
| p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)))) ),
inference(rew,[status(thm),theory(equality)],[38,15863,1807]),
[iquote('0:Rew:38.0,15863.2,1807.0,15863.2')] ).
cnf(15880,plain,
p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)))),
inference(mrr,[status(thm)],[15879,246,29,20]),
[iquote('0:MRR:15879.0,15879.1,15879.2,246.0,29.0,20.0')] ).
cnf(15895,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)))
| equal(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Ebool_2ET)
| p(c_2Ebool_2EF) ),
inference(spr,[status(thm),theory(equality)],[1712,15880]),
[iquote('0:SpR:1712.1,15880.0')] ).
cnf(15901,plain,
( ~ tp__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)))
| equal(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Ebool_2ET) ),
inference(mrr,[status(thm)],[15895,32]),
[iquote('0:MRR:15895.2,32.0')] ).
cnf(15915,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| equal(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Ebool_2ET) ),
inference(res,[status(thm),theory(equality)],[289,15901]),
[iquote('0:Res:289.1,15901.0')] ).
cnf(15917,plain,
equal(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7)),fo__c_2Ebool_2ET),
inference(mrr,[status(thm)],[15915,246]),
[iquote('0:MRR:15915.0,246.0')] ).
cnf(23895,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc6)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7))))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(spr,[status(thm),theory(equality)],[13169,292]),
[iquote('0:SpR:13169.0,292.4')] ).
cnf(23907,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc6)
| ~ p(c_2Ebool_2ET)
| ~ p(c_2Ebool_2ET)
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(rew,[status(thm),theory(equality)],[38,23895,1091,15917]),
[iquote('3:Rew:38.0,23895.3,1091.0,23895.3,38.0,23895.2,15917.0,23895.2')] ).
cnf(23908,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc6)
| ~ p(c_2Ebool_2ET)
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))) ),
inference(obv,[status(thm),theory(equality)],[23907]),
[iquote('3:Obv:23907.2')] ).
cnf(23909,plain,
$false,
inference(mrr,[status(thm)],[23908,246,31,20,863]),
[iquote('3:MRR:23908.0,23908.1,23908.2,23908.3,246.0,31.0,20.0,863.0')] ).
cnf(23915,plain,
~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))),
inference(spt,[spt(split,[position(s2s2sa)])],[23909,860]),
[iquote('3:Spt:23909.0,408.0,860.0')] ).
cnf(23916,plain,
p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7)))),
inference(spt,[spt(split,[position(s2s2s2)])],[408]),
[iquote('3:Spt:23909.0,408.1')] ).
cnf(26338,plain,
( ~ tp__ty_2Einteger_2Eint(skc8)
| ~ p(inj__o(fo__c_2Ebool_2ET))
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),fo__c_2Ebool_2EF) ),
inference(spl,[status(thm),theory(equality)],[1183,23915]),
[iquote('3:SpL:1183.2,23915.0')] ).
cnf(26340,plain,
( ~ tp__ty_2Einteger_2Eint(skc8)
| ~ p(c_2Ebool_2ET)
| equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),fo__c_2Ebool_2EF) ),
inference(rew,[status(thm),theory(equality)],[38,26338]),
[iquote('3:Rew:38.0,26338.1')] ).
cnf(26341,plain,
equal(fo__c_2Einteger_2Eint__divides(skc8,skc6),fo__c_2Ebool_2EF),
inference(mrr,[status(thm)],[26340,29,20]),
[iquote('3:MRR:26340.0,26340.1,29.0,20.0')] ).
cnf(42986,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc6)
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,fo__c_2Einteger_2Eint__neg(skc7))))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(skc8,skc6))) ),
inference(spl,[status(thm),theory(equality)],[13169,293]),
[iquote('0:SpL:13169.0,293.3')] ).
cnf(42996,plain,
( ~ tp__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(skc7))
| ~ tp__ty_2Einteger_2Eint(skc6)
| ~ p(c_2Ebool_2ET)
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(skc8)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(skc6,skc7))))
| p(c_2Ebool_2EF) ),
inference(rew,[status(thm),theory(equality)],[37,42986,26341,38,15917]),
[iquote('3:Rew:37.0,42986.4,26341.0,42986.4,38.0,42986.2,15917.0,42986.2')] ).
cnf(42997,plain,
$false,
inference(mrr,[status(thm)],[42996,246,31,20,23916,32]),
[iquote('3:MRR:42996.0,42996.1,42996.2,42996.3,42996.4,246.0,31.0,20.0,23916.0,32.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : ITP012_2 : TPTP v8.1.0. Bugfixed v7.5.0.
% 0.10/0.10 % Command : spasst-tptp-script %s %d
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 600
% 0.10/0.29 % DateTime : Fri Jun 3 12:40:46 EDT 2022
% 0.10/0.29 % CPUTime :
% 0.14/0.39 % Using EUF theory
% 12.80/7.20
% 12.80/7.20
% 12.80/7.20 % SZS status Theorem for /tmp/SPASST_9944_n032.cluster.edu
% 12.80/7.20
% 12.80/7.20 SPASS V 2.2.22 in combination with yices.
% 12.80/7.20 SPASS beiseite: Proof found by SPASS.
% 12.80/7.20 Problem: /tmp/SPASST_9944_n032.cluster.edu
% 12.80/7.20 SPASS derived 25255 clauses, backtracked 4176 clauses and kept 8490 clauses.
% 12.80/7.20 SPASS backtracked 16 times (0 times due to theory inconsistency).
% 12.80/7.20 SPASS allocated 37556 KBytes.
% 12.80/7.20 SPASS spent 0:00:06.05 on the problem.
% 12.80/7.20 0:00:00.00 for the input.
% 12.80/7.20 0:00:00.03 for the FLOTTER CNF translation.
% 12.80/7.20 0:00:00.18 for inferences.
% 12.80/7.20 0:00:00.20 for the backtracking.
% 12.80/7.20 0:00:04.84 for the reduction.
% 12.80/7.20 0:00:00.25 for interacting with the SMT procedure.
% 12.80/7.20
% 12.80/7.20
% 12.80/7.20 % SZS output start CNFRefutation for /tmp/SPASST_9944_n032.cluster.edu
% See solution above
% 12.80/7.20
% 12.80/7.20 Formulae used in the proof : fof_ax_true_p fof_stp_fo_c_2Ebool_2EF fof_tp_ty_2Einteger_2Eint fof_stp_fo_c_2Ebool_2ET fof_conj_thm_2Einteger_2EINT__DIVIDES__RSUB fof_ax_false_p fof_mem_c_2Ebool_2EF fof_mem_c_2Ebool_2ET fof_stp_eq_fo_c_2Ebool_2EF fof_stp_eq_fo_c_2Ebool_2ET fof_stp_fo_c_2Ebool_2E_7E fof_stp_fo_c_2Einteger_2Eint__neg fof_stp_inj_mem_ty_2Einteger_2Eint fof_stp_inj_mem_o fof_stp_inj_surj_ty_2Einteger_2Eint fof_stp_inj_surj_o fof_conj_thm_2Ebool_2EFORALL__AND__THM fof_ax_neg_p fof_stp_fo_c_2Einteger_2Eint__divides fof_stp_fo_c_2Einteger_2Eint__add fof_stp_fo_c_2Einteger_2Eint__sub fof_stp_eq_fo_c_2Ebool_2E_7E fof_stp_eq_fo_c_2Einteger_2Eint__neg fof_kbeta fof_boolext fof_stp_eq_fo_c_2Einteger_2Eint__divides fof_stp_eq_fo_c_2Einteger_2Eint__add fof_stp_eq_fo_c_2Einteger_2Eint__sub fof_ax_thm_2Einteger_2Eint__sub fof_conj_thm_2Einteger_2EINT__DIVIDES__NEG fof_conj_thm_2Einteger_2EINT__DIVIDES__RADD
% 19.42/10.58
% 19.42/10.58 SPASS+T ended
%------------------------------------------------------------------------------