%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG389-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 09:19:55 AM UTC 2026
% Result : Unsatisfiable 7.87s 2.91s
% Output : Refutation 16.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 53
% Syntax : Number of formulae : 280 ( 71 unt; 25 def)
% Number of atoms : 805 ( 312 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 964 ( 439 ~; 512 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 14 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 16 con; 0-4 aty)
% Number of variables : 280 ( 0 sgn 280 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f602,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X0),X3) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),hAPP(c_Polynomial_Opoly(X2,X0),X3))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__smult_0) ).
fof(f603,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(X0)),X1),X2),X0),X3) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),hAPP(c_Polynomial_Opoly(X1,X0),X3)),hAPP(c_Polynomial_Opoly(X2,X0),X3))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__mult_0) ).
fof(f604,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oidom(t_a)
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1) = c_HOL_Ozero__class_Ozero(t_a)
| X1 = c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pCons_Ohyps_3) ).
fof(f605,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oidom(t_a)
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1)
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(reorient_equations,[],[f604]) ).
fof(f786,axiom,
! [X2,X0,X1] :
( c_Polynomial_Omonom(X1,c_Suc(X2),X0) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_Polynomial_Omonom(X1,X2,X0),X0)
| ~ class_HOL_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_monom__Suc_0) ).
fof(f794,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(X1,X2,X0),X0),X3) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),hAPP(hAPP(c_Power_Opower__class_Opower(X0),X3),X2))
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__monom_0) ).
fof(f799,axiom,
! [X0,X1] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_Omonom(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) = c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_monom__0_0) ).
fof(f800,plain,
! [X0,X1] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_Polynomial_Omonom(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) ),
inference(reorient_equations,[],[f799]) ).
fof(f807,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(t_a)
| v_sko__local__XpCons__Xhyps__2(v_cs____) != c_HOL_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = c_HOL_Ozero__class_Ozero(t_a)
| X0 = c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pCons_Ohyps_0) ).
fof(f808,plain,
! [X0] :
( ~ class_Ring__and__Field_Oidom(t_a)
| c_HOL_Ozero__class_Ozero(t_a) != v_sko__local__XpCons__Xhyps__2(v_cs____)
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(reorient_equations,[],[f807]) ).
fof(f823,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(t_a)
| c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),v_sko__local__XpCons__Xhyps__3(v_cs____)),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____))) = c_Suc(c_Polynomial_Odegree(v_cs____,t_a))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = c_HOL_Ozero__class_Ozero(t_a)
| X0 = c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pCons_Ohyps_2) ).
fof(f824,plain,
! [X0] :
( ~ class_Ring__and__Field_Oidom(t_a)
| c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),v_sko__local__XpCons__Xhyps__3(v_cs____)),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____))) = c_Suc(c_Polynomial_Odegree(v_cs____,t_a))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(reorient_equations,[],[f823]) ).
fof(f836,axiom,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(X0)),X1) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__Suc_0) ).
fof(f840,axiom,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__add__commute_0) ).
fof(f842,axiom,
! [X2,X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),X1)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__commute_0) ).
fof(f863,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),c_HOL_Ozero__class_Ozero(X0)) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I10_J_0) ).
fof(f864,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),c_HOL_Ozero__class_Ozero(X0))
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(reorient_equations,[],[f863]) ).
fof(f894,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X0),X3) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X3),hAPP(c_Polynomial_Opoly(X2,X0),X3)))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__pCons_0) ).
fof(f904,axiom,
! [X0] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pCons__0__0_0) ).
fof(f905,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0)
| ~ class_HOL_Ozero(X0) ),
inference(reorient_equations,[],[f904]) ).
fof(f915,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X1) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__root_1) ).
fof(f916,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X1)
| ~ class_Ring__and__Field_Oidom(X0) ),
inference(reorient_equations,[],[f915]) ).
fof(f988,axiom,
! [X2,X0,X1] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_Odegree(c_Polynomial_OpCons(X1,X2,X0),X0) = c_Suc(c_Polynomial_Odegree(X2,X0))
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_degree__pCons__eq_0) ).
fof(f989,plain,
! [X2,X0,X1] :
( c_Polynomial_Odegree(c_Polynomial_OpCons(X1,X2,X0),X0) = c_Suc(c_Polynomial_Odegree(X2,X0))
| ~ class_HOL_Ozero(X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = X2 ),
inference(reorient_equations,[],[f988]) ).
fof(f1003,axiom,
! [X2,X0,X1] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X2),X1)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I7_J_0) ).
fof(f1041,axiom,
! [X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Ozero__class_Ozero(X0)),X1) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I5_J_0) ).
fof(f1042,axiom,
( ~ class_Ring__and__Field_Oidom(t_a)
| v_c____ = c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f1043,plain,
( ~ class_Ring__and__Field_Oidom(t_a)
| c_HOL_Ozero__class_Ozero(t_a) = v_c____ ),
inference(reorient_equations,[],[f1042]) ).
fof(f1044,axiom,
( ~ class_Ring__and__Field_Oidom(t_a)
| hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),hAPP(v_sko__CHAINED__1(v_c____),v_cs____)) != c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f1045,plain,
( ~ class_Ring__and__Field_Oidom(t_a)
| c_HOL_Ozero__class_Ozero(t_a) != hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),hAPP(v_sko__CHAINED__1(v_c____),v_cs____)) ),
inference(reorient_equations,[],[f1044]) ).
fof(f1046,axiom,
( ~ class_Ring__and__Field_Oidom(t_a)
| hAPP(v_sko__CHAINED__1(v_c____),v_cs____) != c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f1047,plain,
( ~ class_Ring__and__Field_Oidom(t_a)
| c_HOL_Ozero__class_Ozero(t_a) != hAPP(v_sko__CHAINED__1(v_c____),v_cs____) ),
inference(reorient_equations,[],[f1046]) ).
fof(f1056,negated_conjecture,
class_Ring__and__Field_Oidom(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f1057,negated_conjecture,
! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),v_x(X0,X1,X2)) != hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),X2),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != c_Suc(c_Polynomial_Odegree(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a))
| c_Polynomial_OpCons(v_c____,v_cs____,t_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| X1 = c_HOL_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1058,plain,
! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),v_x(X0,X1,X2)) != hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),X2),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != c_Suc(c_Polynomial_Odegree(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a))
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Polynomial_OpCons(v_c____,v_cs____,t_a)
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(reorient_equations,[],[f1057]) ).
fof(f1068,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(X0)
| class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oidom_Ring__and__Field_Ocomm__semiring__1) ).
fof(f1069,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(X0)
| class_Ring__and__Field_Ocomm__semiring__0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oidom_Ring__and__Field_Ocomm__semiring__0) ).
fof(f1074,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(X0)
| class_OrderedGroup_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oidom_OrderedGroup_Ocomm__monoid__add) ).
fof(f1084,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oidom(X0)
| class_HOL_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oidom_HOL_Ozero) ).
fof(f1215,axiom,
! [X0] :
( class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Oidom(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Polynomial__Opoly__Ring__and__Field_Oidom) ).
fof(f1227,definition,
sF0 = c_Polynomial_OpCons(v_c____,v_cs____,t_a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1228,plain,
c_Polynomial_OpCons(v_c____,v_cs____,t_a) = sF0,
inference(reorient_equations,[],[f1227]) ).
fof(f1229,definition,
sF1 = c_Polynomial_Opoly(sF0,t_a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1230,plain,
c_Polynomial_Opoly(sF0,t_a) = sF1,
inference(reorient_equations,[],[f1229]) ).
fof(f1231,definition,
sF2 = c_HOL_Otimes__class_Otimes(t_a),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1232,plain,
c_HOL_Otimes__class_Otimes(t_a) = sF2,
inference(reorient_equations,[],[f1231]) ).
fof(f1233,definition,
sF3 = c_Power_Opower__class_Opower(t_a),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1234,plain,
c_Power_Opower__class_Opower(t_a) = sF3,
inference(reorient_equations,[],[f1233]) ).
fof(f1235,definition,
sF4 = c_HOL_Oplus__class_Oplus(tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1236,plain,
c_HOL_Oplus__class_Oplus(tc_nat) = sF4,
inference(reorient_equations,[],[f1235]) ).
fof(f1237,definition,
sF5 = tc_Polynomial_Opoly(t_a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1238,plain,
tc_Polynomial_Opoly(t_a) = sF5,
inference(reorient_equations,[],[f1237]) ).
fof(f1239,definition,
sF6 = c_fequal(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1240,plain,
c_fequal(sF5) = sF6,
inference(reorient_equations,[],[f1239]) ).
fof(f1241,definition,
sF7 = c_HOL_Ozero__class_Ozero(sF5),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1242,plain,
c_HOL_Ozero__class_Ozero(sF5) = sF7,
inference(reorient_equations,[],[f1241]) ).
fof(f1243,definition,
sF8 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1244,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF8,
inference(reorient_equations,[],[f1243]) ).
fof(f1245,definition,
sF9 = c_Polynomial_Odegree(sF0,t_a),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1246,plain,
c_Polynomial_Odegree(sF0,t_a) = sF9,
inference(reorient_equations,[],[f1245]) ).
fof(f1247,definition,
sF10 = c_Suc(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1248,plain,
c_Suc(sF9) = sF10,
inference(reorient_equations,[],[f1247]) ).
fof(f1249,definition,
sF11 = c_HOL_Ozero__class_Ozero(t_a),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1250,plain,
c_HOL_Ozero__class_Ozero(t_a) = sF11,
inference(reorient_equations,[],[f1249]) ).
fof(f1251,plain,
! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(hAPP(sF2,hAPP(hAPP(sF3,v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10
| sF0 = sF7
| sF11 = X1 ),
inference(definition_folding,[],[f1058,f1250,f1228,f1242,f1238,f1248,f1246,f1228,f1244,f1242,f1238,f1240,f1238,f1236,f1234,f1232,f1230,f1228]) ).
fof(f1256,definition,
( spl12_1
<=> sF0 = sF7 ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f1257,plain,
( sF0 = sF7
| ~ spl12_1 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1258,plain,
( sF0 != sF7
| spl12_1 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1264,definition,
( spl12_3
<=> ! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(hAPP(sF2,hAPP(hAPP(sF3,v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| sF11 = X1
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10 ) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f1265,plain,
( ! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(hAPP(sF2,hAPP(hAPP(sF3,v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| sF11 = X1
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10 )
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1266,plain,
( spl12_1
| spl12_3 ),
inference(avatar_split_clause,[],[f1251,f1264,f1256]) ).
fof(f1271,plain,
c_HOL_Ozero__class_Ozero(t_a) != hAPP(v_sko__CHAINED__1(v_c____),v_cs____),
inference(forward_subsumption_resolution,[],[f1047,f1056]) ).
fof(f1272,plain,
c_HOL_Ozero__class_Ozero(t_a) != hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),hAPP(v_sko__CHAINED__1(v_c____),v_cs____)),
inference(forward_subsumption_resolution,[],[f1045,f1056]) ).
fof(f1273,plain,
c_HOL_Ozero__class_Ozero(t_a) = v_c____,
inference(forward_subsumption_resolution,[],[f1043,f1056]) ).
fof(f1278,plain,
! [X0] :
( c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),v_sko__local__XpCons__Xhyps__3(v_cs____)),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____))) = c_Suc(c_Polynomial_Odegree(v_cs____,t_a))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_subsumption_resolution,[],[f824,f1056]) ).
fof(f1285,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(t_a) != v_sko__local__XpCons__Xhyps__2(v_cs____)
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_subsumption_resolution,[],[f808,f1056]) ).
fof(f1293,definition,
( spl12_5
<=> class_HOL_Ozero(t_a) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f1294,plain,
( class_HOL_Ozero(t_a)
| ~ spl12_5 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1295,plain,
( ~ class_HOL_Ozero(t_a)
| spl12_5 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1298,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1)
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(forward_subsumption_resolution,[],[f605,f1056]) ).
fof(f1323,plain,
! [X0,X1] : hAPP(hAPP(sF4,c_Suc(X0)),X1) = c_Suc(hAPP(hAPP(sF4,X0),X1)),
inference(backward_demodulation,[],[f836,f1236]) ).
fof(f1325,plain,
! [X0,X1] : hAPP(hAPP(sF4,X1),X0) = hAPP(hAPP(sF4,X0),X1),
inference(backward_demodulation,[],[f840,f1236]) ).
fof(f1362,plain,
! [X0,X1] :
( c_Polynomial_OpCons(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_Polynomial_Omonom(X1,sF8,X0)
| ~ class_HOL_Ozero(X0) ),
inference(backward_demodulation,[],[f800,f1244]) ).
fof(f1374,plain,
hAPP(v_sko__CHAINED__1(v_c____),v_cs____) != sF11,
inference(forward_demodulation,[],[f1271,f1250]) ).
fof(f1375,plain,
c_HOL_Ozero__class_Ozero(t_a) != hAPP(c_Polynomial_Opoly(sF0,t_a),hAPP(v_sko__CHAINED__1(v_c____),v_cs____)),
inference(forward_demodulation,[],[f1272,f1228]) ).
fof(f1376,plain,
v_c____ = sF11,
inference(backward_demodulation,[],[f1250,f1273]) ).
fof(f1380,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(tc_Polynomial_Opoly(t_a)),v_sko__local__XpCons__Xhyps__3(v_cs____)),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1278,f1244]) ).
fof(f1387,plain,
! [X0] :
( v_sko__local__XpCons__Xhyps__2(v_cs____) != v_c____
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1285,f1273]) ).
fof(f1391,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1)
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(forward_demodulation,[],[f1298,f1234]) ).
fof(f1406,plain,
c_HOL_Ozero__class_Ozero(t_a) != hAPP(sF1,hAPP(v_sko__CHAINED__1(v_c____),v_cs____)),
inference(forward_demodulation,[],[f1375,f1230]) ).
fof(f1407,plain,
v_c____ != hAPP(v_sko__CHAINED__1(v_c____),v_cs____),
inference(backward_demodulation,[],[f1374,f1376]) ).
fof(f1411,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(sF5),v_sko__local__XpCons__Xhyps__3(v_cs____)),c_HOL_Ozero__class_Ozero(sF5)),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1380,f1238]) ).
fof(f1416,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____
| v_sko__local__XpCons__Xhyps__2(v_cs____) != v_c____
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1387,f1273]) ).
fof(f1420,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(sF2,hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1)
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(forward_demodulation,[],[f1391,f1232]) ).
fof(f1431,plain,
v_c____ != hAPP(sF1,hAPP(v_sko__CHAINED__1(v_c____),v_cs____)),
inference(forward_demodulation,[],[f1406,f1273]) ).
fof(f1434,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(c_fequal(sF5),v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1411,f1242]) ).
fof(f1439,plain,
! [X0] :
( v_c____ = X0
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____
| v_sko__local__XpCons__Xhyps__2(v_cs____) != v_c____ ),
inference(forward_demodulation,[],[f1416,f1273]) ).
fof(f1443,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1) = v_c____
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(sF2,hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| c_HOL_Ozero__class_Ozero(t_a) = X1 ),
inference(forward_demodulation,[],[f1420,f1273]) ).
fof(f1452,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1434,f1240]) ).
fof(f1461,definition,
( spl12_9
<=> ! [X0] :
( v_c____ = X0
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____ ) ),
introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition]) ).
fof(f1462,plain,
( ! [X0] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____
| v_c____ = X0 )
| ~ spl12_9 ),
inference(avatar_component_clause,[],[f1461]) ).
fof(f1465,definition,
( spl12_10
<=> v_sko__local__XpCons__Xhyps__2(v_cs____) = v_c____ ),
introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition]) ).
fof(f1467,plain,
( v_sko__local__XpCons__Xhyps__2(v_cs____) != v_c____
| spl12_10 ),
inference(avatar_component_clause,[],[f1465]) ).
fof(f1468,plain,
( ~ spl12_10
| spl12_9 ),
inference(avatar_split_clause,[],[f1439,f1461,f1465]) ).
fof(f1471,plain,
! [X0,X1] :
( v_c____ = X1
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X1) = v_c____
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(sF2,hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0)) ),
inference(forward_demodulation,[],[f1443,f1273]) ).
fof(f1483,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),v_sko__local__XpCons__Xhyps__1(v_cs____)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1452,f1236]) ).
fof(f1492,definition,
( spl12_14
<=> ! [X0] : hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(sF2,hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0)) ),
introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition]) ).
fof(f1493,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(hAPP(sF2,hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____))),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0))
| ~ spl12_14 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1494,plain,
( spl12_14
| spl12_9 ),
inference(avatar_split_clause,[],[f1471,f1461,f1492]) ).
fof(f1497,plain,
! [X0] :
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1483,f1325]) ).
fof(f1502,definition,
( spl12_15
<=> v_cs____ = sF7 ),
introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition]) ).
fof(f1503,plain,
( v_cs____ = sF7
| ~ spl12_15 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1507,plain,
! [X0] :
( v_cs____ = c_HOL_Ozero__class_Ozero(sF5)
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1497,f1238]) ).
fof(f1512,plain,
! [X0] :
( v_cs____ = sF7
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0)
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1507,f1242]) ).
fof(f1515,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____
| v_cs____ = sF7
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| c_HOL_Ozero__class_Ozero(t_a) = X0 ),
inference(forward_demodulation,[],[f1512,f1273]) ).
fof(f1518,plain,
! [X0] :
( v_c____ = X0
| hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = v_c____
| v_cs____ = sF7
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat))) ),
inference(forward_demodulation,[],[f1515,f1273]) ).
fof(f1526,definition,
( spl12_17
<=> c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat))) ),
introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition]) ).
fof(f1528,plain,
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| ~ spl12_17 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1529,plain,
( spl12_17
| spl12_15
| spl12_9 ),
inference(avatar_split_clause,[],[f1518,f1461,f1502,f1526]) ).
fof(f1535,plain,
( ! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(hAPP(sF2,hAPP(hAPP(sF3,v_x(X0,X1,X2)),X0)),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)))
| v_c____ = X1
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10 )
| ~ spl12_3 ),
inference(forward_demodulation,[],[f1265,f1376]) ).
fof(f1536,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(sF5),t_a),X0)
| ~ class_Ring__and__Field_Oidom(t_a) ),
inference(superposition,[],[f916,f1238]) ).
fof(f1537,plain,
! [X0] : c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(sF5),t_a),X0),
inference(forward_subsumption_resolution,[],[f1536,f1056]) ).
fof(f1538,plain,
! [X0] : c_HOL_Ozero__class_Ozero(t_a) = hAPP(c_Polynomial_Opoly(sF7,t_a),X0),
inference(forward_demodulation,[],[f1537,f1242]) ).
fof(f1539,plain,
! [X0] : v_c____ = hAPP(c_Polynomial_Opoly(sF7,t_a),X0),
inference(forward_demodulation,[],[f1538,f1273]) ).
fof(f1540,plain,
( class_Ring__and__Field_Oidom(sF5)
| ~ class_Ring__and__Field_Oidom(t_a) ),
inference(superposition,[],[f1215,f1238]) ).
fof(f1541,plain,
class_Ring__and__Field_Oidom(sF5),
inference(forward_subsumption_resolution,[],[f1540,f1056]) ).
fof(f1542,plain,
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Polynomial_Odegree(sF0,t_a)
| ~ class_HOL_Ozero(t_a)
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(superposition,[],[f989,f1228]) ).
fof(f1573,plain,
( c_HOL_Ozero__class_Ozero(sF5) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(t_a),c_HOL_Ozero__class_Ozero(sF5),t_a)
| ~ class_HOL_Ozero(t_a) ),
inference(superposition,[],[f905,f1238]) ).
fof(f1587,plain,
class_HOL_Ozero(t_a),
inference(resolution,[],[f1084,f1056]) ).
fof(f1588,plain,
( $false
| spl12_5 ),
inference(forward_subsumption_resolution,[],[f1587,f1295]) ).
fof(f1589,plain,
spl12_5,
inference(avatar_contradiction_clause,[],[f1588]) ).
fof(f1591,plain,
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = c_Polynomial_Odegree(sF0,t_a)
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ spl12_5 ),
inference(forward_subsumption_resolution,[],[f1542,f1294]) ).
fof(f1592,plain,
( c_HOL_Ozero__class_Ozero(sF5) = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(t_a),c_HOL_Ozero__class_Ozero(sF5),t_a)
| ~ spl12_5 ),
inference(forward_subsumption_resolution,[],[f1573,f1294]) ).
fof(f1595,plain,
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = sF9
| v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1591,f1246]) ).
fof(f1596,plain,
( sF7 = c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(t_a),sF7,t_a)
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1592,f1242]) ).
fof(f1599,plain,
( v_cs____ = c_HOL_Ozero__class_Ozero(sF5)
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = sF9
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1595,f1238]) ).
fof(f1600,plain,
( sF7 = c_Polynomial_OpCons(v_c____,sF7,t_a)
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1596,f1273]) ).
fof(f1603,plain,
( v_cs____ = sF7
| c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = sF9
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1599,f1242]) ).
fof(f1605,definition,
( spl12_23
<=> c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = sF9 ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
fof(f1607,plain,
( c_Suc(c_Polynomial_Odegree(v_cs____,t_a)) = sF9
| ~ spl12_23 ),
inference(avatar_component_clause,[],[f1605]) ).
fof(f1608,plain,
( spl12_23
| spl12_15
| ~ spl12_5 ),
inference(avatar_split_clause,[],[f1603,f1293,f1502,f1605]) ).
fof(f1610,plain,
( v_cs____ != sF0
| spl12_1
| ~ spl12_15 ),
inference(backward_demodulation,[],[f1258,f1503]) ).
fof(f1615,plain,
( v_cs____ = c_Polynomial_OpCons(v_c____,v_cs____,t_a)
| ~ spl12_5
| ~ spl12_15 ),
inference(backward_demodulation,[],[f1600,f1503]) ).
fof(f1617,plain,
( v_cs____ = sF0
| ~ spl12_5
| ~ spl12_15 ),
inference(backward_demodulation,[],[f1228,f1615]) ).
fof(f1618,plain,
( $false
| spl12_1
| ~ spl12_5
| ~ spl12_15 ),
inference(forward_subsumption_resolution,[],[f1617,f1610]) ).
fof(f1619,plain,
( spl12_1
| ~ spl12_5
| ~ spl12_15 ),
inference(avatar_contradiction_clause,[],[f1618]) ).
fof(f1639,definition,
( spl12_26
<=> class_OrderedGroup_Ocomm__monoid__add(t_a) ),
introduced(definition,[new_symbols(definition,[spl12_26])],[avatar_definition]) ).
fof(f1640,plain,
( class_OrderedGroup_Ocomm__monoid__add(t_a)
| ~ spl12_26 ),
inference(avatar_component_clause,[],[f1639]) ).
fof(f1641,plain,
( ~ class_OrderedGroup_Ocomm__monoid__add(t_a)
| spl12_26 ),
inference(avatar_component_clause,[],[f1639]) ).
fof(f1643,definition,
( spl12_27
<=> ! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),v_c____),X0) = X0 ),
introduced(definition,[new_symbols(definition,[spl12_27])],[avatar_definition]) ).
fof(f1644,plain,
( ! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),v_c____),X0) = X0
| ~ spl12_27 ),
inference(avatar_component_clause,[],[f1643]) ).
fof(f1653,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),v_c____),X0) = X0
| ~ class_Ring__and__Field_Ocomm__semiring__1(t_a) ),
inference(superposition,[],[f1041,f1273]) ).
fof(f1656,definition,
( spl12_28
<=> class_Ring__and__Field_Ocomm__semiring__1(sF5) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
fof(f1657,plain,
( class_Ring__and__Field_Ocomm__semiring__1(sF5)
| ~ spl12_28 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1658,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(sF5)
| spl12_28 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1661,definition,
( spl12_29
<=> class_Ring__and__Field_Ocomm__semiring__1(t_a) ),
introduced(definition,[new_symbols(definition,[spl12_29])],[avatar_definition]) ).
fof(f1662,plain,
( class_Ring__and__Field_Ocomm__semiring__1(t_a)
| ~ spl12_29 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1663,plain,
( ~ class_Ring__and__Field_Ocomm__semiring__1(t_a)
| spl12_29 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1664,plain,
( ~ spl12_29
| spl12_27 ),
inference(avatar_split_clause,[],[f1653,f1643,f1661]) ).
fof(f1700,plain,
class_OrderedGroup_Ocomm__monoid__add(t_a),
inference(resolution,[],[f1074,f1056]) ).
fof(f1704,plain,
( $false
| spl12_26 ),
inference(forward_subsumption_resolution,[],[f1700,f1641]) ).
fof(f1705,plain,
spl12_26,
inference(avatar_contradiction_clause,[],[f1704]) ).
fof(f1709,plain,
! [X0] :
( v_c____ = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),v_c____)
| ~ class_Ring__and__Field_Ocomm__semiring__1(t_a) ),
inference(superposition,[],[f864,f1273]) ).
fof(f1713,plain,
class_Ring__and__Field_Ocomm__semiring__0(t_a),
inference(resolution,[],[f1069,f1056]) ).
fof(f1745,plain,
class_Ring__and__Field_Ocomm__semiring__1(t_a),
inference(resolution,[],[f1068,f1056]) ).
fof(f1746,plain,
class_Ring__and__Field_Ocomm__semiring__1(sF5),
inference(resolution,[],[f1068,f1541]) ).
fof(f1747,plain,
( $false
| spl12_28 ),
inference(forward_subsumption_resolution,[],[f1746,f1658]) ).
fof(f1748,plain,
spl12_28,
inference(avatar_contradiction_clause,[],[f1747]) ).
fof(f1749,plain,
( $false
| spl12_29 ),
inference(forward_subsumption_resolution,[],[f1745,f1663]) ).
fof(f1750,plain,
spl12_29,
inference(avatar_contradiction_clause,[],[f1749]) ).
fof(f1751,plain,
( ! [X0] : v_c____ = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),v_c____)
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f1709,f1662]) ).
fof(f1754,plain,
( ! [X0] : v_c____ = hAPP(hAPP(sF2,X0),v_c____)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f1751,f1232]) ).
fof(f2317,plain,
( ! [X0] : v_c____ = hAPP(c_Polynomial_Opoly(sF0,t_a),X0)
| ~ spl12_1 ),
inference(backward_demodulation,[],[f1539,f1257]) ).
fof(f2351,plain,
( ! [X0] : v_c____ = hAPP(sF1,X0)
| ~ spl12_1 ),
inference(forward_demodulation,[],[f2317,f1230]) ).
fof(f2357,plain,
( v_c____ != v_c____
| ~ spl12_1 ),
inference(backward_demodulation,[],[f1431,f2351]) ).
fof(f2365,plain,
( $false
| ~ spl12_1 ),
inference(trivial_inequality_removal,[],[f2357]) ).
fof(f2366,plain,
~ spl12_1,
inference(avatar_contradiction_clause,[],[f2365]) ).
fof(f2979,plain,
( ! [X0] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),v_c____) = X0
| ~ class_OrderedGroup_Ocomm__monoid__add(t_a) )
| ~ spl12_27 ),
inference(superposition,[],[f1644,f842]) ).
fof(f2991,plain,
( ! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),v_c____) = X0
| ~ spl12_26
| ~ spl12_27 ),
inference(forward_subsumption_resolution,[],[f2979,f1640]) ).
fof(f3171,plain,
! [X0,X1] :
( c_Polynomial_Omonom(X0,c_Suc(X1),t_a) = c_Polynomial_OpCons(v_c____,c_Polynomial_Omonom(X0,X1,t_a),t_a)
| ~ class_HOL_Ozero(t_a) ),
inference(superposition,[],[f786,f1273]) ).
fof(f3187,plain,
( ! [X0,X1] : c_Polynomial_Omonom(X0,c_Suc(X1),t_a) = c_Polynomial_OpCons(v_c____,c_Polynomial_Omonom(X0,X1,t_a),t_a)
| ~ spl12_5 ),
inference(forward_subsumption_resolution,[],[f3171,f1294]) ).
fof(f3441,plain,
! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(sF2,X2),hAPP(c_Polynomial_Opoly(X1,t_a),X2)))
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) ),
inference(superposition,[],[f894,f1232]) ).
fof(f3445,plain,
( ! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),v_c____))
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a)
| v_c____ = X1 )
| ~ spl12_9 ),
inference(superposition,[],[f894,f1462]) ).
fof(f3446,plain,
! [X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),v_c____)) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,sF7,t_a),t_a),X1)
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) ),
inference(superposition,[],[f894,f1539]) ).
fof(f3462,plain,
( ! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,X0,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),hAPP(c_Polynomial_Opoly(X0,t_a),X1))
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) )
| ~ spl12_27 ),
inference(superposition,[],[f1644,f894]) ).
fof(f3475,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,X0,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),hAPP(c_Polynomial_Opoly(X0,t_a),X1))
| ~ spl12_27 ),
inference(forward_subsumption_resolution,[],[f3462,f1713]) ).
fof(f3481,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),v_c____)) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,sF7,t_a),t_a),X1),
inference(forward_subsumption_resolution,[],[f3446,f1713]) ).
fof(f3482,plain,
( ! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X1),v_c____))
| v_c____ = X1 )
| ~ spl12_9 ),
inference(forward_subsumption_resolution,[],[f3445,f1713]) ).
fof(f3485,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(sF2,X2),hAPP(c_Polynomial_Opoly(X1,t_a),X2))),
inference(forward_subsumption_resolution,[],[f3441,f1713]) ).
fof(f3487,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,X0,t_a),t_a),X1) = hAPP(hAPP(sF2,X1),hAPP(c_Polynomial_Opoly(X0,t_a),X1))
| ~ spl12_27 ),
inference(forward_demodulation,[],[f3475,f1232]) ).
fof(f3490,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,sF7,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(sF2,X1),v_c____)),
inference(forward_demodulation,[],[f3481,f1232]) ).
fof(f3491,plain,
( ! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(sF2,X1),v_c____))
| v_c____ = X1 )
| ~ spl12_9 ),
inference(forward_demodulation,[],[f3482,f1232]) ).
fof(f3493,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,X1,t_a),t_a),X2))
| ~ spl12_27 ),
inference(backward_demodulation,[],[f3485,f3487]) ).
fof(f3494,plain,
( ! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),v_c____) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,sF7,t_a),t_a),X1)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3490,f1754]) ).
fof(f3495,plain,
( ! [X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),v_c____) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,t_a),t_a),X1)
| v_c____ = X1 )
| ~ spl12_9
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3491,f1754]) ).
fof(f3496,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,sF7,t_a),t_a),X1) = X0
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3494,f2991]) ).
fof(f3497,plain,
( ! [X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,t_a),t_a),X1) = X0
| v_c____ = X1 )
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3495,f2991]) ).
fof(f3500,plain,
( ! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(X0,sF7,t_a),t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X2),X0))
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) )
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f894,f3496]) ).
fof(f3507,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(X0,sF7,t_a),t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X2),X0))
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f3500,f1713]) ).
fof(f3512,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(X0,sF7,t_a),t_a),t_a),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(sF2,X2),X0))
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3507,f1232]) ).
fof(f3516,plain,
( ! [X0] :
( v_c____ = hAPP(c_Polynomial_Opoly(sF0,t_a),X0)
| v_c____ = X0 )
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f3497,f1228]) ).
fof(f3527,plain,
( ! [X0] :
( v_c____ = hAPP(sF1,X0)
| v_c____ = X0 )
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f3516,f1230]) ).
fof(f3535,plain,
( v_c____ != v_c____
| v_c____ = hAPP(v_sko__CHAINED__1(v_c____),v_cs____)
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f1431,f3527]) ).
fof(f3540,plain,
( v_c____ = hAPP(v_sko__CHAINED__1(v_c____),v_cs____)
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(trivial_inequality_removal,[],[f3535]) ).
fof(f3545,plain,
( $false
| ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f3540,f1407]) ).
fof(f3546,plain,
( ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(avatar_contradiction_clause,[],[f3545]) ).
fof(f3548,plain,
( sF9 = c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| ~ spl12_17
| ~ spl12_23 ),
inference(forward_demodulation,[],[f1528,f1607]) ).
fof(f4024,plain,
! [X0] :
( c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(sF5),t_a) = c_Polynomial_Omonom(X0,sF8,t_a)
| ~ class_HOL_Ozero(t_a) ),
inference(superposition,[],[f1362,f1238]) ).
fof(f4043,plain,
( ! [X0] : c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(sF5),t_a) = c_Polynomial_Omonom(X0,sF8,t_a)
| ~ spl12_5 ),
inference(forward_subsumption_resolution,[],[f4024,f1294]) ).
fof(f4045,plain,
( ! [X0] : c_Polynomial_OpCons(X0,sF7,t_a) = c_Polynomial_Omonom(X0,sF8,t_a)
| ~ spl12_5 ),
inference(forward_demodulation,[],[f4043,f1242]) ).
fof(f4054,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(X0,sF8,t_a),t_a),X1) = X0
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(backward_demodulation,[],[f3496,f4045]) ).
fof(f4056,plain,
( ! [X2,X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(sF2,X2),X0)) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(X0,sF8,t_a),t_a),t_a),X2)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(backward_demodulation,[],[f3512,f4045]) ).
fof(f4945,plain,
( ! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),c_Polynomial_Omonom(X0,sF8,t_a)),X1),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2))
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) )
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f603,f4054]) ).
fof(f4954,plain,
( ! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),X1),c_Polynomial_Omonom(X0,sF8,t_a)),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(c_Polynomial_Opoly(X1,t_a),X2)),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) )
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f603,f4054]) ).
fof(f4972,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),X1),c_Polynomial_Omonom(X0,sF8,t_a)),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),hAPP(c_Polynomial_Opoly(X1,t_a),X2)),X0)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f4954,f1713]) ).
fof(f4980,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),c_Polynomial_Omonom(X0,sF8,t_a)),X1),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2))
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f4945,f1713]) ).
fof(f4988,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),X1),c_Polynomial_Omonom(X0,sF8,t_a)),t_a),X2) = hAPP(hAPP(sF2,hAPP(c_Polynomial_Opoly(X1,t_a),X2)),X0)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f4972,f1232]) ).
fof(f4994,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Polynomial_Opoly(t_a)),c_Polynomial_Omonom(X0,sF8,t_a)),X1),t_a),X2) = hAPP(hAPP(sF2,X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2))
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f4980,f1232]) ).
fof(f5001,plain,
( ! [X2,X0,X1] : hAPP(hAPP(sF2,hAPP(c_Polynomial_Opoly(X1,t_a),X2)),X0) = hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(sF5),X1),c_Polynomial_Omonom(X0,sF8,t_a)),t_a),X2)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f4988,f1238]) ).
fof(f5007,plain,
( ! [X2,X0,X1] : hAPP(hAPP(sF2,X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2)) = hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(sF5),c_Polynomial_Omonom(X0,sF8,t_a)),X1),t_a),X2)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f4994,f1238]) ).
fof(f6226,plain,
( ! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(sF5),X0),c_Polynomial_Omonom(X1,sF8,t_a)),t_a),X2) = hAPP(hAPP(sF2,X1),hAPP(c_Polynomial_Opoly(X0,t_a),X2))
| ~ class_Ring__and__Field_Ocomm__semiring__1(sF5) )
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f5007,f1003]) ).
fof(f6266,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(sF5),X0),c_Polynomial_Omonom(X1,sF8,t_a)),t_a),X2) = hAPP(hAPP(sF2,X1),hAPP(c_Polynomial_Opoly(X0,t_a),X2))
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f6226,f1657]) ).
fof(f6319,plain,
( ! [X2,X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X2),hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,X0,t_a),t_a),X1)) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X2,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(X0,t_a),X1),sF8,t_a),t_a),t_a),X1)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f4056,f3487]) ).
fof(f6322,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X2,X0,t_a),t_a),X1) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X2,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(X0,t_a),X1),sF8,t_a),t_a),t_a),X1)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(forward_demodulation,[],[f6319,f3493]) ).
fof(f7664,plain,
! [X2,X0,X1] :
( hAPP(hAPP(sF2,X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2)) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,t_a),t_a),X2)
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) ),
inference(superposition,[],[f602,f1232]) ).
fof(f7772,plain,
! [X2,X0,X1] : hAPP(hAPP(sF2,X0),hAPP(c_Polynomial_Opoly(X1,t_a),X2)) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,t_a),t_a),X2),
inference(forward_subsumption_resolution,[],[f7664,f1713]) ).
fof(f7806,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(hAPP(hAPP(c_HOL_Otimes__class_Otimes(sF5),X0),c_Polynomial_Omonom(X1,sF8,t_a)),t_a),X2) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X0,t_a),t_a),X2)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(backward_demodulation,[],[f6266,f7772]) ).
fof(f7817,plain,
( ! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(hAPP(hAPP(sF3,v_x(X0,X1,X2)),X0),c_Polynomial_OpCons(X1,X2,t_a),t_a),t_a),v_x(X0,X1,X2))
| v_c____ = X1
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10 )
| ~ spl12_3 ),
inference(backward_demodulation,[],[f1535,f7772]) ).
fof(f7820,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(hAPP(hAPP(sF3,X0),v_sko__local__XpCons__Xhyps__1(v_cs____)),c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_14 ),
inference(backward_demodulation,[],[f1493,f7772]) ).
fof(f7841,plain,
( ! [X2,X0,X1] : hAPP(hAPP(sF2,hAPP(c_Polynomial_Opoly(X1,t_a),X2)),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,t_a),t_a),X2)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(backward_demodulation,[],[f5001,f7806]) ).
fof(f8023,plain,
( ! [X2,X3,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X3,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(X1,t_a),X2),sF8,t_a),t_a),t_a),X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X3),hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,t_a),t_a),X2))
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(superposition,[],[f4056,f7772]) ).
fof(f8029,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X2,X0,t_a),t_a),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X2),hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X0,t_a),t_a),X1))
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(backward_demodulation,[],[f6322,f8023]) ).
fof(f16685,plain,
! [X2,X0,X1] :
( hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(X0,X1,t_a),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(hAPP(sF3,X2),X1))
| ~ class_Ring__and__Field_Ocomm__semiring__1(t_a) ),
inference(superposition,[],[f794,f1234]) ).
fof(f16786,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(X0,X1,t_a),t_a),X2) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(hAPP(sF3,X2),X1))
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f16685,f1662]) ).
fof(f16792,plain,
( ! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(X0,X1,t_a),t_a),X2) = hAPP(hAPP(sF2,X0),hAPP(hAPP(sF3,X2),X1))
| ~ spl12_29 ),
inference(forward_demodulation,[],[f16786,f1232]) ).
fof(f16833,plain,
( ! [X2,X3,X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(X0,t_a),X1),X2,t_a),t_a),X3) = hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(hAPP(hAPP(sF3,X3),X2),X0,t_a),t_a),X1)
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(superposition,[],[f7841,f16792]) ).
fof(f16834,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(backward_demodulation,[],[f7820,f16833]) ).
fof(f16847,plain,
( ! [X2,X0,X1] :
( hAPP(sF1,v_x(X0,X1,X2)) != hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,t_a),t_a),v_x(X0,X1,X2)),X0,t_a),t_a),v_x(X0,X1,X2))
| v_c____ = X1
| c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,X2),sF7),sF8,c_Suc(c_Polynomial_Odegree(X2,t_a)),tc_nat)),X0)) != sF10 )
| ~ spl12_3
| ~ spl12_5
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(backward_demodulation,[],[f7817,f16833]) ).
fof(f17137,plain,
( ! [X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0))) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(t_a) )
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(superposition,[],[f894,f16834]) ).
fof(f17145,plain,
( ! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(c_HOL_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0))) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f17137,f1713]) ).
fof(f17158,plain,
( ! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(sF2,X0),hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0))) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f17145,f1232]) ).
fof(f17166,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(v_cs____,t_a),X0),sF8,t_a),t_a),t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f17158,f4056]) ).
fof(f17172,plain,
( ! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(c_Polynomial_Opoly(c_Polynomial_Osmult(X0,v_cs____,t_a),t_a),X0)) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f17166,f8023]) ).
fof(f17176,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_cs____,t_a),t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),v_sko__local__XpCons__Xhyps__1(v_cs____),t_a),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f17172,f8029]) ).
fof(f29825,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_c____,v_cs____,t_a),t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____)),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(superposition,[],[f17176,f3187]) ).
fof(f29867,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(sF0,t_a),X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____)),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f29825,f1228]) ).
fof(f29879,plain,
( ! [X0] : hAPP(sF1,X0) = hAPP(c_Polynomial_Opoly(c_Polynomial_Omonom(hAPP(c_Polynomial_Opoly(c_Polynomial_OpCons(v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____),t_a),t_a),X0),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____)),t_a),t_a),X0)
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f29867,f1230]) ).
fof(f29919,plain,
( hAPP(sF1,v_x(c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____)),v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____))) != hAPP(sF1,v_x(c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____)),v_sko__local__XpCons__Xhyps__2(v_cs____),v_sko__local__XpCons__Xhyps__3(v_cs____)))
| v_sko__local__XpCons__Xhyps__2(v_cs____) = v_c____
| sF10 != c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____))))
| ~ spl12_3
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(superposition,[],[f16847,f29879]) ).
fof(f29924,plain,
( v_sko__local__XpCons__Xhyps__2(v_cs____) = v_c____
| sF10 != c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____))))
| ~ spl12_3
| ~ spl12_5
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(trivial_inequality_removal,[],[f29919]) ).
fof(f29925,plain,
( sF10 != c_Suc(hAPP(hAPP(sF4,c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)),c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____))))
| ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f29924,f1467]) ).
fof(f29939,plain,
( sF10 != c_Suc(hAPP(hAPP(sF4,c_Suc(v_sko__local__XpCons__Xhyps__1(v_cs____))),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat)))
| ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f29925,f1325]) ).
fof(f29948,plain,
( sF10 != c_Suc(c_Suc(hAPP(hAPP(sF4,v_sko__local__XpCons__Xhyps__1(v_cs____)),c_HOL_OIf(hAPP(hAPP(sF6,v_sko__local__XpCons__Xhyps__3(v_cs____)),sF7),sF8,c_Suc(c_Polynomial_Odegree(v_sko__local__XpCons__Xhyps__3(v_cs____),t_a)),tc_nat))))
| ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f29939,f1323]) ).
fof(f29954,plain,
( c_Suc(sF9) != sF10
| ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_17
| ~ spl12_23
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_demodulation,[],[f29948,f3548]) ).
fof(f29959,plain,
( $false
| ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_17
| ~ spl12_23
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(forward_subsumption_resolution,[],[f29954,f1248]) ).
fof(f29960,plain,
( ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_17
| ~ spl12_23
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(avatar_contradiction_clause,[],[f29959]) ).
cnf(s2,plain,
( spl12_1
| spl12_3 ),
inference(sat_conversion,[],[f1266]) ).
cnf(s6,plain,
( spl12_9
| ~ spl12_10 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s10,plain,
( spl12_9
| spl12_14 ),
inference(sat_conversion,[],[f1494]) ).
cnf(s15,plain,
( spl12_9
| spl12_15
| spl12_17 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s19,plain,
spl12_5,
inference(sat_conversion,[],[f1589]) ).
cnf(s20,plain,
( ~ spl12_5
| spl12_15
| spl12_23 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s21,plain,
( spl12_1
| ~ spl12_5
| ~ spl12_15 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s25,plain,
( spl12_27
| ~ spl12_29 ),
inference(sat_conversion,[],[f1664]) ).
cnf(s28,plain,
spl12_26,
inference(sat_conversion,[],[f1705]) ).
cnf(s30,plain,
spl12_28,
inference(sat_conversion,[],[f1748]) ).
cnf(s31,plain,
spl12_29,
inference(sat_conversion,[],[f1750]) ).
cnf(s41,plain,
~ spl12_1,
inference(sat_conversion,[],[f2366]) ).
cnf(s57,plain,
( ~ spl12_9
| ~ spl12_26
| ~ spl12_27
| ~ spl12_29 ),
inference(sat_conversion,[],[f3546]) ).
cnf(s371,plain,
( ~ spl12_3
| ~ spl12_5
| spl12_10
| ~ spl12_14
| ~ spl12_17
| ~ spl12_23
| ~ spl12_26
| ~ spl12_27
| ~ spl12_28
| ~ spl12_29 ),
inference(sat_conversion,[],[f29960]) ).
cnf(s464,plain,
spl12_27,
inference(rat,[],[s25,s31]) ).
cnf(s472,plain,
~ spl12_9,
inference(rat,[],[s57,s31,s28,s464]) ).
cnf(s475,plain,
( ~ spl12_5
| ~ spl12_15 ),
inference(rat,[],[s21,s41]) ).
cnf(s487,plain,
~ spl12_15,
inference(rat,[],[s475,s19]) ).
cnf(s491,plain,
spl12_23,
inference(rat,[],[s20,s19,s487]) ).
cnf(s498,plain,
spl12_17,
inference(rat,[],[s15,s487,s472]) ).
cnf(s500,plain,
spl12_14,
inference(rat,[],[s10,s472]) ).
cnf(s507,plain,
~ spl12_10,
inference(rat,[],[s6,s472]) ).
cnf(s508,plain,
~ spl12_3,
inference(rat,[],[s371,s31,s30,s464,s28,s491,s498,s500,s19,s507]) ).
cnf(s511,plain,
$false,
inference(rat,[],[s2,s508,s41]) ).
fof(f29962,plain,
$false,
inference(avatar_sat_refutation,[],[s511]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG389-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.16 % Computer : n014.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Mon Sep 28 20:14:45 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 Running first-order theorem proving
% 0.10/0.19 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.67/2.34 % (2127854)Input is clausal, will run a generic CNF schedule.
% 11.67/2.34 % (2127861)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=251308803:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.67/2.34 % (2127865)dis-21_1_sil=8000:lcm=predicate:random_seed=1102836070:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.67/2.34 % (2127862)lrs+10_1_sil=8000:sp=occurrence:random_seed=3729381784:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.67/2.34 % (2127863)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1388755243:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.67/2.34 % (2127860)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3264530656:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.67/2.34 % (2127859)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=991620018:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.67/2.35 % (2127864)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3441897833:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.67/2.35 % (2127865)Instruction limit reached!
% 11.67/2.35 % (2127865)------------------------------
% 11.67/2.35 % (2127865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.67/2.35 % (2127865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.67/2.35 % (2127865)CaDiCaL version: 2.1.3
% 11.67/2.35 % (2127865)Termination reason: Instruction limit
% 11.67/2.35 % (2127865)Termination phase: Saturation
% 11.67/2.35 % (2127865)Time elapsed: 0.066 s
% 11.67/2.35 % (2127865)Peak memory usage: 89 MB
% 11.67/2.35 % (2127865)Instructions burned: 117 (million)
% 11.67/2.35 % (2127862)Instruction limit reached!
% 11.67/2.35 % (2127862)------------------------------
% 11.67/2.35 % (2127862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.67/2.35 % (2127862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.67/2.35 % (2127862)CaDiCaL version: 2.1.3
% 11.67/2.35 % (2127862)Termination reason: Instruction limit
% 11.67/2.35 % (2127862)Termination phase: Saturation
% 11.67/2.35 % (2127862)Time elapsed: 0.068 s
% 11.67/2.35 % (2127862)Peak memory usage: 89 MB
% 11.67/2.35 % (2127862)Instructions burned: 108 (million)
% 11.67/2.35 % (2127863)Instruction limit reached!
% 11.67/2.35 % (2127863)------------------------------
% 11.67/2.35 % (2127863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.67/2.35 % (2127863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.67/2.35 % (2127863)CaDiCaL version: 2.1.3
% 11.67/2.35 % (2127863)Termination reason: Instruction limit
% 11.67/2.35 % (2127863)Termination phase: Saturation
% 11.67/2.35 % (2127863)Time elapsed: 0.073 s
% 11.67/2.35 % (2127863)Peak memory usage: 89 MB
% 11.67/2.35 % (2127863)Instructions burned: 114 (million)
% 11.67/2.35 % (2127864)Instruction limit reached!
% 11.67/2.35 % (2127864)------------------------------
% 11.67/2.35 % (2127864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.67/2.35 % (2127864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.67/2.35 % (2127864)CaDiCaL version: 2.1.3
% 11.67/2.35 % (2127864)Termination reason: Instruction limit
% 11.67/2.35 % (2127864)Termination phase: Saturation
% 11.67/2.35 % (2127864)Time elapsed: 0.113 s
% 11.67/2.35 % (2127864)Peak memory usage: 90 MB
% 11.67/2.35 % (2127864)Instructions burned: 180 (million)
% 11.67/2.35 % (2127875)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3804306970:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.67/2.35 % (2127873)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2082335499:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.67/2.35 % (2127874)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2005058770:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.67/2.35 % (2127873)Refutation not found, incomplete strategy
% 11.67/2.35 % (2127873)------------------------------
% 11.67/2.35 % (2127873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127873)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127873)Termination reason: Refutation not found, incomplete strategy
% 7.87/2.91 % (2127873)Time elapsed: 0.013 s
% 7.87/2.91 % (2127873)Peak memory usage: 89 MB
% 7.87/2.91 % (2127873)Instructions burned: 18 (million)
% 7.87/2.91 % (2127876)lrs+10_64_to=lpo:sil=8000:random_seed=506063762:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 7.87/2.91 % (2127874)Instruction limit reached!
% 7.87/2.91 % (2127874)------------------------------
% 7.87/2.91 % (2127874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127874)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127874)Termination reason: Instruction limit
% 7.87/2.91 % (2127874)Termination phase: Saturation
% 7.87/2.91 % (2127874)Time elapsed: 0.108 s
% 7.87/2.91 % (2127874)Peak memory usage: 90 MB
% 7.87/2.91 % (2127874)Instructions burned: 190 (million)
% 7.87/2.91 % (2127875)Instruction limit reached!
% 7.87/2.91 % (2127875)------------------------------
% 7.87/2.91 % (2127875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127875)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127875)Termination reason: Instruction limit
% 7.87/2.91 % (2127875)Termination phase: Saturation
% 7.87/2.91 % (2127875)Time elapsed: 0.116 s
% 7.87/2.91 % (2127875)Peak memory usage: 90 MB
% 7.87/2.91 % (2127875)Instructions burned: 221 (million)
% 7.87/2.91 % (2127876)Instruction limit reached!
% 7.87/2.91 % (2127876)------------------------------
% 7.87/2.91 % (2127876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127876)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127876)Termination reason: Instruction limit
% 7.87/2.91 % (2127876)Termination phase: Saturation
% 7.87/2.91 % (2127876)Time elapsed: 0.080 s
% 7.87/2.91 % (2127876)Peak memory usage: 90 MB
% 7.87/2.91 % (2127876)Instructions burned: 127 (million)
% 7.87/2.91 % (2127873)------------------------------
% 7.87/2.91 % (2127873)------------------------------
% 7.87/2.91 % (2127881)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1709110620:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 7.87/2.91 % (2127882)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1470326601:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 7.87/2.91 % (2127883)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=647752382:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 7.87/2.91 % (2127882)Instruction limit reached!
% 7.87/2.91 % (2127882)------------------------------
% 7.87/2.91 % (2127882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127882)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127882)Termination reason: Instruction limit
% 7.87/2.91 % (2127882)Termination phase: Saturation
% 7.87/2.91 % (2127882)Time elapsed: 0.098 s
% 7.87/2.91 % (2127882)Peak memory usage: 91 MB
% 7.87/2.91 % (2127882)Instructions burned: 158 (million)
% 7.87/2.91 % (2127881)Instruction limit reached!
% 7.87/2.91 % (2127881)------------------------------
% 7.87/2.91 % (2127881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127881)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127881)Termination reason: Instruction limit
% 7.87/2.91 % (2127881)Termination phase: Saturation
% 7.87/2.91 % (2127881)Time elapsed: 0.125 s
% 7.87/2.91 % (2127881)Peak memory usage: 91 MB
% 7.87/2.91 % (2127881)Instructions burned: 195 (million)
% 7.87/2.91 % (2127885)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4259854639:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 7.87/2.91 % (2127885)Instruction limit reached!
% 7.87/2.91 % (2127885)------------------------------
% 7.87/2.91 % (2127885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127885)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127885)Termination reason: Instruction limit
% 7.87/2.91 % (2127885)Termination phase: Saturation
% 7.87/2.91 % (2127885)Time elapsed: 0.058 s
% 7.87/2.91 % (2127885)Peak memory usage: 89 MB
% 7.87/2.91 % (2127885)Instructions burned: 107 (million)
% 7.87/2.91 % (2127888)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=859642601:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 7.87/2.91 % (2127889)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3783870804:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 7.87/2.91 % (2127888)Instruction limit reached!
% 7.87/2.91 % (2127888)------------------------------
% 7.87/2.91 % (2127888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127888)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127888)Termination reason: Instruction limit
% 7.87/2.91 % (2127888)Termination phase: Saturation
% 7.87/2.91 % (2127888)Time elapsed: 0.067 s
% 7.87/2.91 % (2127888)Peak memory usage: 90 MB
% 7.87/2.91 % (2127888)Instructions burned: 108 (million)
% 7.87/2.91 % (2127891)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1937405862:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 7.87/2.91 % (2127889)Instruction limit reached!
% 7.87/2.91 % (2127889)------------------------------
% 7.87/2.91 % (2127889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127889)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127889)Termination reason: Instruction limit
% 7.87/2.91 % (2127889)Termination phase: Saturation
% 7.87/2.91 % (2127889)Time elapsed: 0.135 s
% 7.87/2.91 % (2127889)Peak memory usage: 90 MB
% 7.87/2.91 % (2127889)Instructions burned: 243 (million)
% 7.87/2.91 % (2127894)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3450586201:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 7.87/2.91 % (2127896)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1356725928:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 7.87/2.91 % (2127894)Instruction limit reached!
% 7.87/2.91 % (2127894)------------------------------
% 7.87/2.91 % (2127894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127894)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127894)Termination reason: Instruction limit
% 7.87/2.91 % (2127894)Termination phase: Saturation
% 7.87/2.91 % (2127894)Time elapsed: 0.087 s
% 7.87/2.91 % (2127894)Peak memory usage: 89 MB
% 7.87/2.91 % (2127894)Instructions burned: 135 (million)
% 7.87/2.91 % (2127899)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1142505282:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 7.87/2.91 % (2127899)Instruction limit reached!
% 7.87/2.91 % (2127899)------------------------------
% 7.87/2.91 % (2127899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127899)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127899)Termination reason: Instruction limit
% 7.87/2.91 % (2127899)Termination phase: Saturation
% 7.87/2.91 % (2127899)Time elapsed: 0.117 s
% 7.87/2.91 % (2127899)Peak memory usage: 92 MB
% 7.87/2.91 % (2127899)Instructions burned: 192 (million)
% 7.87/2.91 % (2127896)Instruction limit reached!
% 7.87/2.91 % (2127896)------------------------------
% 7.87/2.91 % (2127896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127896)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127896)Termination reason: Instruction limit
% 7.87/2.91 % (2127896)Termination phase: Saturation
% 7.87/2.91 % (2127896)Time elapsed: 0.293 s
% 7.87/2.91 % (2127896)Peak memory usage: 96 MB
% 7.87/2.91 % (2127896)Instructions burned: 500 (million)
% 7.87/2.91 % (2127901)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=671138785:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 7.87/2.91 % (2127902)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2882403188:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 7.87/2.91 % (2127902)Instruction limit reached!
% 7.87/2.91 % (2127902)------------------------------
% 7.87/2.91 % (2127902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127902)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127902)Termination reason: Instruction limit
% 7.87/2.91 % (2127902)Termination phase: Saturation
% 7.87/2.91 % (2127902)Time elapsed: 0.104 s
% 7.87/2.91 % (2127902)Peak memory usage: 90 MB
% 7.87/2.91 % (2127902)Instructions burned: 156 (million)
% 7.87/2.91 % (2127901)Instruction limit reached!
% 7.87/2.91 % (2127901)------------------------------
% 7.87/2.91 % (2127901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/2.91 % (2127901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/2.91 % (2127901)CaDiCaL version: 2.1.3
% 7.87/2.91 % (2127901)Termination reason: Instruction limit
% 7.87/2.91 % (2127901)Termination phase: Saturation
% 7.87/2.91 % (2127901)Time elapsed: 0.152 s
% 7.87/2.91 % (2127901)Peak memory usage: 92 MB
% 7.87/2.91 % (2127901)Instructions burned: 266 (million)
% 7.87/2.91 % (2127905)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3469509065:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 7.87/2.91 % (2127906)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3134527883:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 7.87/2.91 % (2127861)First to succeed.
% 7.87/2.91 % (2127861)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2127854"
% 7.87/2.91 % (2127861)Refutation found. Thanks to Tanya!
% 7.87/2.91 % SZS status Unsatisfiable for theBenchmark
% 7.87/2.91 % SZS output start Proof for theBenchmark
% See solution above
% 16.36/3.10 % (2127861)------------------------------
% 16.36/3.10 % (2127861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.36/3.10 % (2127861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.36/3.10 % (2127861)CaDiCaL version: 2.1.3
% 16.36/3.10 % (2127861)Termination reason: Refutation
% 16.36/3.10 % (2127861)Time elapsed: 1.925 s
% 16.36/3.10 % (2127861)Peak memory usage: 168 MB
% 16.36/3.10 % (2127861)Instructions burned: 5571 (million)
% 16.36/3.10 % (2127861)------------------------------
% 16.36/3.10 % (2127861)------------------------------
% 16.36/3.10 % (2127854)Success in time 2.273 s
% 16.36/3.10 % Vampire exiting
%------------------------------------------------------------------------------