%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP012_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 : Tue Sep 29 11:34:57 AM UTC 2026
% Result : Theorem 0.16s 0.53s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 11
% Syntax : Number of formulae : 81 ( 24 unt; 0 typ; 2 def)
% Number of atoms : 476 ( 17 equ)
% Maximal formula atoms : 4 ( 5 avg)
% Number of connectives : 141 ( 55 ~; 72 |; 2 &)
% ( 8 <=>; 3 =>; 0 <=; 1 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of FOOLs : 309 ( 309 fml; 0 var)
% Number of types : 5 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 7 prp; 0-3 aty)
% Number of functors : 34 ( 34 usr; 8 con; 0-3 aty)
% Number of variables : 99 ( 0 sgn 96 !; 3 ?; 99 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__o: $tType ).
tff(type_def_7,type,
tp__ty_2Einteger_2Eint: $tType ).
tff(func_def_0,type,
bool: del ).
tff(func_def_1,type,
ind: del ).
tff(func_def_2,type,
arr: ( del * del ) > del ).
tff(func_def_4,type,
k: ( del * $i ) > $i ).
tff(func_def_5,type,
i: del > $i ).
tff(func_def_6,type,
inj__o: tp__o > $i ).
tff(func_def_7,type,
surj__o: $i > tp__o ).
tff(func_def_9,type,
fo__c_2Ebool_2ET: tp__o ).
tff(func_def_10,type,
c_2Ebool_2E_3F: del > $i ).
tff(func_def_11,type,
ty_2Einteger_2Eint: del ).
tff(func_def_12,type,
inj__ty_2Einteger_2Eint: tp__ty_2Einteger_2Eint > $i ).
tff(func_def_13,type,
surj__ty_2Einteger_2Eint: $i > tp__ty_2Einteger_2Eint ).
tff(func_def_15,type,
fo__c_2Einteger_2Eint__sub: ( tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint ) > tp__ty_2Einteger_2Eint ).
tff(func_def_17,type,
fo__c_2Einteger_2Eint__add: ( tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint ) > tp__ty_2Einteger_2Eint ).
tff(func_def_19,type,
fo__c_2Einteger_2Eint__neg: tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint ).
tff(func_def_21,type,
fo__c_2Einteger_2Eint__divides: ( tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint ) > tp__o ).
tff(func_def_23,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_25,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_27,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_29,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_31,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_32,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_33,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_34,type,
sK0: ( del * $i * $i ) > $i ).
tff(func_def_35,type,
sK1: ( del * $i ) > $i ).
tff(func_def_36,type,
sK2: ( del * $i ) > $i ).
tff(func_def_37,type,
sK3: ( del * $i ) > $i ).
tff(func_def_38,type,
sK4: ( del * $i ) > $i ).
tff(func_def_39,type,
sK5: ( del * $i * $i ) > $i ).
tff(func_def_40,type,
sK6: ( del * $i ) > $i ).
tff(func_def_41,type,
sK7: ( del * $i ) > $i ).
tff(func_def_42,type,
sK15: tp__ty_2Einteger_2Eint ).
tff(func_def_43,type,
sK16: tp__ty_2Einteger_2Eint ).
tff(func_def_44,type,
sK17: tp__ty_2Einteger_2Eint ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
tff(pred_def_3,type,
sP8: ( tp__o * tp__o ) > $o ).
tff(pred_def_4,type,
sP9: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_5,type,
sP10: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_6,type,
sP11: ( tp__o * tp__o ) > $o ).
tff(pred_def_7,type,
sP12: ( tp__o * tp__o ) > $o ).
tff(pred_def_8,type,
sP13: ( tp__o * tp__o ) > $o ).
tff(pred_def_9,type,
sP14: ( tp__o * tp__o ) > $o ).
tff(f14,axiom,
! [X0: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_inj_surj_ty_2Einteger_2Eint) ).
tff(f18,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(X0,X1)) = ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__sub) ).
tff(f20,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X0,X1)) = ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__add) ).
tff(f22,axiom,
! [X0: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(X0)) = ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__neg) ).
tff(f24,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)) = ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stp_eq_fo_c_2Einteger_2Eint__divides) ).
tff(f56,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Einteger_2Eint__sub) ).
tff(f57,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint,X2: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
=> ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1))))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__RADD) ).
tff(f58,axiom,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1))))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) )
& ( p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X0))),inj__ty_2Einteger_2Eint(X1)))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__NEG) ).
tff(f69,conjecture,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint,X2: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
=> ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1))))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__DIVIDES__RSUB) ).
tff(f70,negated_conjecture,
~ ! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint,X2: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
=> ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1))))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2))) ) ),
inference(negated_conjecture,[status(cth)],[f69]) ).
tff(f97,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint,X2: tp__ty_2Einteger_2Eint] :
( ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1))))
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2))) )
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) ),
inference(ennf_transformation,[],[f57]) ).
tff(f107,plain,
? [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint,X2: tp__ty_2Einteger_2Eint] :
( ( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1))))
<~> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2))) )
& p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) ),
inference(ennf_transformation,[],[f70]) ).
tff(f125,plain,
! [X0: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(X0)) = X0 ),
inference(cnf_transformation,[],[f14]) ).
tff(f129,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(X0,X1)) = ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
inference(cnf_transformation,[],[f18]) ).
tff(f131,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X0,X1)) = ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
inference(cnf_transformation,[],[f20]) ).
tff(f133,plain,
! [X0: tp__ty_2Einteger_2Eint] : ( inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(X0)) = ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X0)) ),
inference(cnf_transformation,[],[f22]) ).
tff(f135,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)) = ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)) ),
inference(cnf_transformation,[],[f24]) ).
tff(f181,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1)))) ),
inference(cnf_transformation,[],[f56]) ).
tff(f182,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(cnf_transformation,[],[f97]) ).
tff(f183,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(cnf_transformation,[],[f97]) ).
tff(f184,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1)))) ),
inference(cnf_transformation,[],[f58]) ).
tff(f251,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16)))) ),
inference(cnf_transformation,[],[f107]) ).
tff(f252,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16)))) ),
inference(cnf_transformation,[],[f107]) ).
tff(f253,plain,
p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK16))),
inference(cnf_transformation,[],[f107]) ).
tff(f316,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(consistent_polarity_flipping,[],[f183]) ).
tff(f317,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(consistent_polarity_flipping,[],[f182]) ).
tff(f321,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1)))) ),
inference(consistent_polarity_flipping,[],[f184]) ).
tff(f385,plain,
~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK16))),
inference(consistent_polarity_flipping,[],[f253]) ).
tff(f386,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16)))) ),
inference(consistent_polarity_flipping,[],[f252]) ).
tff(f387,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16)))) ),
inference(consistent_polarity_flipping,[],[f251]) ).
tff(f390,definition,
( spl18_1
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl18_1])],[avatar_definition]) ).
tff(f391,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16))))
| ~ spl18_1 ),
inference(avatar_component_clause,[],[f390]) ).
tff(f392,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(sK17)),inj__ty_2Einteger_2Eint(sK16))))
| spl18_1 ),
inference(avatar_component_clause,[],[f390]) ).
tff(f394,definition,
( spl18_2
<=> p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17))) ),
introduced(definition,[new_symbols(definition,[spl18_2])],[avatar_definition]) ).
tff(f395,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| ~ spl18_2 ),
inference(avatar_component_clause,[],[f394]) ).
tff(f396,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(sK17)))
| spl18_2 ),
inference(avatar_component_clause,[],[f394]) ).
tff(f397,plain,
( ~ spl18_1
| ~ spl18_2 ),
inference(avatar_split_clause,[],[f387,f394,f390]) ).
tff(f398,plain,
( spl18_1
| spl18_2 ),
inference(avatar_split_clause,[],[f386,f394,f390]) ).
tff(f562,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(sK17,sK16))))
| spl18_1 ),
inference(superposition,[],[f392,f129]) ).
tff(f563,plain,
~ p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK16))),
inference(superposition,[],[f385,f135]) ).
tff(f564,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK17)))
| ~ spl18_2 ),
inference(superposition,[],[f395,f135]) ).
tff(f565,plain,
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__sub(sK17,sK16))))
| spl18_1 ),
inference(superposition,[],[f562,f135]) ).
tff(f905,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X1)))) ),
inference(forward_demodulation,[],[f321,f135]) ).
tff(f906,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(X1))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f905,f133]) ).
tff(f907,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X0,fo__c_2Einteger_2Eint__neg(X1))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f906,f135]) ).
tff(f922,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(X1)))) ),
inference(forward_demodulation,[],[f181,f133]) ).
tff(f923,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) = surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X0,fo__c_2Einteger_2Eint__neg(X1)))) ),
inference(forward_demodulation,[],[f922,f131]) ).
tff(f924,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1))) = fo__c_2Einteger_2Eint__add(X0,fo__c_2Einteger_2Eint__neg(X1)) ),
inference(forward_demodulation,[],[f923,f125]) ).
tff(f925,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( fo__c_2Einteger_2Eint__add(X0,fo__c_2Einteger_2Eint__neg(X1)) = surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(X0,X1))) ),
inference(forward_demodulation,[],[f924,f129]) ).
tff(f926,plain,
! [X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] : ( fo__c_2Einteger_2Eint__sub(X0,X1) = fo__c_2Einteger_2Eint__add(X0,fo__c_2Einteger_2Eint__neg(X1)) ),
inference(forward_demodulation,[],[f925,f125]) ).
tff(f1251,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(forward_demodulation,[],[f316,f135]) ).
tff(f1252,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(forward_demodulation,[],[f1251,f135]) ).
tff(f1253,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X2,X1))))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f1252,f131]) ).
tff(f1254,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X0,fo__c_2Einteger_2Eint__add(X2,X1))))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f1253,f135]) ).
tff(f1263,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X2,fo__c_2Einteger_2Eint__sub(X0,X1))))
| ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X2,X0)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X2,fo__c_2Einteger_2Eint__neg(X1)))) ),
inference(superposition,[],[f1254,f926]) ).
tff(f1265,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)))
| p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X2)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(forward_demodulation,[],[f317,f135]) ).
tff(f1266,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)))
| ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X2)),inj__ty_2Einteger_2Eint(X1)))) ),
inference(forward_demodulation,[],[f1265,f135]) ).
tff(f1267,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X2,X1))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f1266,f131]) ).
tff(f1268,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X0,fo__c_2Einteger_2Eint__add(X2,X1))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X2)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X0,X1))) ),
inference(forward_demodulation,[],[f1267,f135]) ).
tff(f1271,plain,
! [X2: tp__ty_2Einteger_2Eint,X0: tp__ty_2Einteger_2Eint,X1: tp__ty_2Einteger_2Eint] :
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(X2,fo__c_2Einteger_2Eint__sub(X0,X1))))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X2,X0)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(X2,fo__c_2Einteger_2Eint__neg(X1)))) ),
inference(superposition,[],[f1268,f926]) ).
tff(f4055,plain,
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK17)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__neg(sK16))))
| spl18_1 ),
inference(resolution,[],[f1263,f565]) ).
tff(f4066,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__neg(sK16))))
| spl18_1
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f4055,f564]) ).
tff(f4067,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK16)))
| spl18_1
| ~ spl18_2 ),
inference(resolution,[],[f4066,f907]) ).
tff(f4077,plain,
( $false
| spl18_1
| ~ spl18_2 ),
inference(forward_subsumption_resolution,[],[f4067,f563]) ).
tff(f4078,plain,
( spl18_1
| ~ spl18_2 ),
inference(avatar_contradiction_clause,[],[f4077]) ).
tff(f4079,plain,
( p(ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(sK15)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(sK17,sK16))))
| ~ spl18_1 ),
inference(forward_demodulation,[],[f391,f129]) ).
tff(f4080,plain,
( ~ p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK17)))
| spl18_2 ),
inference(forward_demodulation,[],[f396,f135]) ).
tff(f4081,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__sub(sK17,sK16))))
| ~ spl18_1 ),
inference(forward_demodulation,[],[f4079,f135]) ).
tff(f4155,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK17)))
| p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__neg(sK16))))
| ~ spl18_1 ),
inference(resolution,[],[f1271,f4081]) ).
tff(f4168,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,fo__c_2Einteger_2Eint__neg(sK16))))
| ~ spl18_1
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f4155,f4080]) ).
tff(f4218,plain,
( p(inj__o(fo__c_2Einteger_2Eint__divides(sK15,sK16)))
| ~ spl18_1
| spl18_2 ),
inference(resolution,[],[f4168,f907]) ).
tff(f4229,plain,
( $false
| ~ spl18_1
| spl18_2 ),
inference(forward_subsumption_resolution,[],[f4218,f563]) ).
tff(f4230,plain,
( ~ spl18_1
| spl18_2 ),
inference(avatar_contradiction_clause,[],[f4229]) ).
cnf(s1,plain,
( ~ spl18_1
| ~ spl18_2 ),
inference(sat_conversion,[],[f397]) ).
cnf(s2,plain,
( spl18_1
| spl18_2 ),
inference(sat_conversion,[],[f398]) ).
cnf(s282,plain,
( spl18_1
| ~ spl18_2 ),
inference(sat_conversion,[],[f4078]) ).
cnf(s292,plain,
( ~ spl18_1
| spl18_2 ),
inference(sat_conversion,[],[f4230]) ).
cnf(s296,plain,
spl18_1,
inference(rat,[],[s2,s282]) ).
cnf(s297,plain,
spl18_2,
inference(rat,[],[s292,s296]) ).
cnf(s298,plain,
$false,
inference(rat,[],[s1,s297,s296]) ).
tff(f4231,plain,
$false,
inference(avatar_sat_refutation,[],[s298]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP012_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 12:00:56 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.53 % (2720499)Will run a generic schedule for satisfiability detection.
% 0.16/0.53 % (2720510)% WARNING: option uhcvi not known.
% 0.16/0.53 % (2720510)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4007930094:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.53 % (2720511)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2535461227:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.53 % (2720509)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3197091214_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.53 % (2720513)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=273602558:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.53 % (2720512)dis+10_1_sil=32000:sp=arity:random_seed=1593545137:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.53 % (2720514)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1336614559:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.53 % (2720515)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1182673100:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.53 % TRYING [1,1,1,1]
% 0.16/0.53 % TRYING [1,2,1,1]
% 0.16/0.53 % TRYING [1,3,1,1]
% 0.16/0.53 % TRYING [1,2,2,1]
% 0.16/0.53 % TRYING [2,2,2,1]
% 0.16/0.53 % TRYING [1,3,2,1]
% 0.16/0.53 % (2720510) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2720499-2720510"...
% 0.16/0.53 % (2720510)...printing done.
% 0.16/0.53 % (2720510)Refutation found. Thanks to Tanya!
% 0.16/0.53 % SZS status Theorem for theBenchmark
% 0.16/0.53 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/0.53 % (2720510)------------------------------
% 0.16/0.53 % (2720510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.53 % (2720510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.53 % (2720510)CaDiCaL version: 2.1.3
% 0.16/0.53 % (2720510)Termination reason: Refutation
% 0.16/0.53 % (2720510)Time elapsed: 0.065 s
% 0.16/0.53 % (2720510)Peak memory usage: 14 MB
% 0.16/0.53 % (2720510)Instructions burned: 199 (million)
% 0.16/0.53 % (2720499)Success in time 0.098 s
% 0.16/0.53 % Vampire exiting
%------------------------------------------------------------------------------