%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW273+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 01:29:59 PM UTC 2026
% Result : Theorem 151.52s 29.42s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 85
% Syntax : Number of formulae : 495 ( 269 unt; 32 def)
% Number of atoms : 896 ( 516 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 654 ( 253 ~; 339 |; 11 &)
% ( 17 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 9 prp; 0-3 aty)
% Number of functors : 52 ( 52 usr; 35 con; 0-3 aty)
% Number of variables : 539 ( 0 sgn 537 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
v_k____ != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_k) ).
fof(f4,axiom,
v_pa____ != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pne) ).
fof(f7,axiom,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_kpn) ).
fof(f8,axiom,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),v_r____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_r) ).
fof(f10,axiom,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_s) ).
fof(f11,axiom,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_pa____) = v_na____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_dpn) ).
fof(f14,axiom,
v_s____ != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_sne) ).
fof(f15,axiom,
c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____)),v_pa____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ap_I1_J) ).
fof(f23,axiom,
! [X0] :
( class_Rings_Ocomm__semiring__1(X0)
=> c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_one__poly__def) ).
fof(f25,axiom,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_s____) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ds0) ).
fof(f57,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Polynomial_Odegree(X2,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,X1,c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_degree__linear__power) ).
fof(f58,axiom,
! [X0,X1,X2,X3,X4] :
( class_Groups_Ozero(X4)
=> ( c_Polynomial_OpCons(X4,X3,X2) = c_Polynomial_OpCons(X4,X1,X0)
<=> ( X3 = X1
& X2 = X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pCons__eq__iff) ).
fof(f73,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__0(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X1)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mult__poly__0__left) ).
fof(f83,axiom,
! [X0] :
( class_Groups_Ozero(X0)
=> c_Polynomial_OpCons(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pCons__0__0) ).
fof(f84,axiom,
~ c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Nat_OSuc(c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_pa____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ap_I2_J) ).
fof(f85,axiom,
~ ! [X0] : v_s____ != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096_B_Bthesis_O_A_I_B_Bk_O_As_A_061_A_091_058k_058_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) ).
fof(f86,axiom,
? [X0] : v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096EX_Ak_O_As_A_061_A_091_058k_058_093_096) ).
fof(f94,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(hAPP(c_Power_Opower__class_Opower(X1),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J) ).
fof(f148,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__mult) ).
fof(f149,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__power) ).
fof(f154,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(f155,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(f157,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
fof(f158,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0)),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J) ).
fof(f187,axiom,
! [X0,X1,X2] :
( class_Groups_Ozero(X2)
=> ( ( X1 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
=> c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,X1)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
& ( X1 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
=> c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,X1)) = c_Nat_OSuc(c_Polynomial_Odegree(X2,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_degree__pCons__eq__if) ).
fof(f192,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
fof(f200,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Oone__class_Oone(X1)),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J) ).
fof(f201,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Oone__class_Oone(X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J) ).
fof(f218,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X2),X0)),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J) ).
fof(f231,axiom,
! [X0] : c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,X0) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__self__eq__0) ).
fof(f264,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Odivision__ring(X3)
=> ( X2 != c_Groups_Ozero__class_Ozero(X3)
=> ( c_Rings_Oinverse__class_Odivide(X3,X1,X2) = X0
<=> X1 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_nonzero__divide__eq__eq) ).
fof(f489,axiom,
! [X0,X1,X2] :
( class_Groups_Oab__group__add(X2)
=> ( X1 = X0
<=> c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_eq__iff__diff__eq__0) ).
fof(f683,axiom,
! [X0,X1] :
( class_Groups_Ozero(X1)
=> c_Polynomial_Omonom(X1,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Polynomial_OpCons(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_monom__0) ).
fof(f696,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__0(X2)
=> ( c_Polynomial_Osynthetic__div(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> c_Polynomial_Odegree(X2,X1) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_synthetic__div__eq__0__iff) ).
fof(f716,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__ring__1(X2)
=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),c_Polynomial_Osynthetic__div(X2,X0,X1)),c_Polynomial_OpCons(X2,hAPP(c_Polynomial_Opoly(X2,X0),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)))) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_synthetic__div__correct_H) ).
fof(f733,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J) ).
fof(f766,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f797,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__diff__cancel) ).
fof(f798,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(f860,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__pCons) ).
fof(f879,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Nat_Oadd__0__right) ).
fof(f931,axiom,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Suc__eq__plus1__left) ).
fof(f965,axiom,
! [X0,X1,X2] :
( class_Rings_Oidom(X2)
=> ( X1 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
=> ( X0 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
=> c_Polynomial_Odegree(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X2,X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_degree__mult__eq) ).
fof(f1123,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(f1124,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(f1126,axiom,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Odivision__ring) ).
fof(f1128,axiom,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Oab__group__add) ).
fof(f1131,axiom,
class_Rings_Ocomm__ring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__ring__1) ).
fof(f1134,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(f1144,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ozero) ).
fof(f1146,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oidom) ).
fof(f1177,axiom,
! [X0] :
( class_Rings_Ocomm__semiring__1(X0)
=> class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Polynomial__Opoly__Rings_Ocomm__semiring__1) ).
fof(f1208,conjecture,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_qa____),v_na____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_k____),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_r____),v_na____))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1209,negated_conjecture,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_qa____),v_na____) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_k____),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_r____),v_na____))),
inference(negated_conjecture,[status(cth)],[f1208]) ).
fof(f1212,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_qa____),v_na____) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_k____),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_r____),v_na____))),
inference(flattening,[],[f1209]) ).
fof(f1269,plain,
! [X0] :
( c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f1308,plain,
! [X0,X1,X2] :
( c_Polynomial_Odegree(X2,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,X1,c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),X0)) = X0
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f57]) ).
fof(f1309,plain,
! [X0,X1,X2,X3,X4] :
( ( c_Polynomial_OpCons(X4,X3,X2) = c_Polynomial_OpCons(X4,X1,X0)
<=> ( X3 = X1
& X2 = X0 ) )
| ~ class_Groups_Ozero(X4) ),
inference(ennf_transformation,[],[f58]) ).
fof(f1326,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X1)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f1341,plain,
! [X0] :
( c_Polynomial_OpCons(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Groups_Ozero(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f1342,plain,
? [X0] : v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(ennf_transformation,[],[f85]) ).
fof(f1350,plain,
! [X0,X1] :
( hAPP(hAPP(c_Power_Opower__class_Opower(X1),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f1379,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),hAPP(c_Polynomial_Opoly(X3,X1),X0))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f148]) ).
fof(f1380,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),X1)
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f149]) ).
fof(f1388,plain,
! [X0,X1,X2] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X0),X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f154]) ).
fof(f1389,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0))
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f155]) ).
fof(f1391,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0))
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f157]) ).
fof(f1392,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0)),X1)
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f158]) ).
fof(f1415,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,X1)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X1 )
& ( c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,X1)) = c_Nat_OSuc(c_Polynomial_Odegree(X2,X1))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X1 ) )
| ~ class_Groups_Ozero(X2) ),
inference(ennf_transformation,[],[f187]) ).
fof(f1420,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f192]) ).
fof(f1430,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Oone__class_Oone(X1)),X0) = X0
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f200]) ).
fof(f1431,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Oone__class_Oone(X1)) = X0
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f201]) ).
fof(f1455,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X2),X0)),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X1),X0))
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f218]) ).
fof(f1517,plain,
! [X0,X1,X2,X3] :
( ( c_Rings_Oinverse__class_Odivide(X3,X1,X2) = X0
<=> X1 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2) )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(ennf_transformation,[],[f264]) ).
fof(f1518,plain,
! [X0,X1,X2,X3] :
( ( c_Rings_Oinverse__class_Odivide(X3,X1,X2) = X0
<=> X1 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2) )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(flattening,[],[f1517]) ).
fof(f1776,plain,
! [X0,X1,X2] :
( ( X1 = X0
<=> c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2) )
| ~ class_Groups_Oab__group__add(X2) ),
inference(ennf_transformation,[],[f489]) ).
fof(f2005,plain,
! [X0,X1] :
( c_Polynomial_Omonom(X1,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Polynomial_OpCons(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)))
| ~ class_Groups_Ozero(X1) ),
inference(ennf_transformation,[],[f683]) ).
fof(f2022,plain,
! [X0,X1,X2] :
( ( c_Polynomial_Osynthetic__div(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> c_Polynomial_Odegree(X2,X1) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
| ~ class_Rings_Ocomm__semiring__0(X2) ),
inference(ennf_transformation,[],[f696]) ).
fof(f2047,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),c_Polynomial_Osynthetic__div(X2,X0,X1)),c_Polynomial_OpCons(X2,hAPP(c_Polynomial_Opoly(X2,X0),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)))) = X0
| ~ class_Rings_Ocomm__ring__1(X2) ),
inference(ennf_transformation,[],[f716]) ).
fof(f2069,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f733]) ).
fof(f2107,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f766]) ).
fof(f2147,plain,
! [X0,X1,X2] :
( c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f797]) ).
fof(f2148,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f798]) ).
fof(f2237,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0)))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f860]) ).
fof(f2300,plain,
! [X0,X1,X2] :
( c_Polynomial_Odegree(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X2,X0))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X1
| ~ class_Rings_Oidom(X2) ),
inference(ennf_transformation,[],[f965]) ).
fof(f2301,plain,
! [X0,X1,X2] :
( c_Polynomial_Odegree(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X2,X0))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X1
| ~ class_Rings_Oidom(X2) ),
inference(flattening,[],[f2300]) ).
fof(f2371,plain,
! [X0] :
( class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(ennf_transformation,[],[f1177]) ).
fof(f2408,plain,
! [X0,X1,X2,X3,X4] :
( ( ( c_Polynomial_OpCons(X4,X3,X2) = c_Polynomial_OpCons(X4,X1,X0)
| X1 != X3
| X0 != X2 )
& ( ( X3 = X1
& X2 = X0 )
| c_Polynomial_OpCons(X4,X3,X2) != c_Polynomial_OpCons(X4,X1,X0) ) )
| ~ class_Groups_Ozero(X4) ),
inference(nnf_transformation,[],[f1309]) ).
fof(f2409,plain,
! [X0,X1,X2,X3,X4] :
( ( ( c_Polynomial_OpCons(X4,X3,X2) = c_Polynomial_OpCons(X4,X1,X0)
| X1 != X3
| X0 != X2 )
& ( ( X3 = X1
& X2 = X0 )
| c_Polynomial_OpCons(X4,X3,X2) != c_Polynomial_OpCons(X4,X1,X0) ) )
| ~ class_Groups_Ozero(X4) ),
inference(flattening,[],[f2408]) ).
fof(f2419,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f1342]) ).
fof(f2420,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f86]) ).
fof(f2471,plain,
! [X0,X1,X2,X3] :
( ( ( c_Rings_Oinverse__class_Odivide(X3,X1,X2) = X0
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2) != X1 )
& ( X1 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2)
| c_Rings_Oinverse__class_Odivide(X3,X1,X2) != X0 ) )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(nnf_transformation,[],[f1518]) ).
fof(f2557,plain,
! [X0,X1,X2] :
( ( ( X1 = X0
| c_Groups_Ozero__class_Ozero(X2) != c_Groups_Ominus__class_Ominus(X2,X1,X0) )
& ( c_Groups_Ominus__class_Ominus(X2,X1,X0) = c_Groups_Ozero__class_Ozero(X2)
| X0 != X1 ) )
| ~ class_Groups_Oab__group__add(X2) ),
inference(nnf_transformation,[],[f1776]) ).
fof(f2630,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_Osynthetic__div(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Polynomial_Odegree(X2,X1) )
& ( c_Polynomial_Odegree(X2,X1) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_Osynthetic__div(X2,X1,X0) ) )
| ~ class_Rings_Ocomm__semiring__0(X2) ),
inference(nnf_transformation,[],[f2022]) ).
fof(f2738,plain,
v_k____ != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f3]) ).
fof(f2739,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_pa____,
inference(cnf_transformation,[],[f4]) ).
fof(f2742,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cnf_transformation,[],[f7]) ).
fof(f2743,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),v_r____),
inference(cnf_transformation,[],[f8]) ).
fof(f2745,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),
inference(cnf_transformation,[],[f10]) ).
fof(f2746,plain,
v_na____ = c_Polynomial_Odegree(tc_Complex_Ocomplex,v_pa____),
inference(cnf_transformation,[],[f11]) ).
fof(f2749,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_s____,
inference(cnf_transformation,[],[f14]) ).
fof(f2750,plain,
c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____)),v_pa____),
inference(cnf_transformation,[],[f15]) ).
fof(f2758,plain,
! [X0] :
( ~ class_Rings_Ocomm__semiring__1(X0)
| c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) ),
inference(cnf_transformation,[],[f1269]) ).
fof(f2760,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,v_s____),
inference(cnf_transformation,[],[f25]) ).
fof(f2788,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Polynomial_Odegree(X2,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,X1,c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),X0)) = X0 ),
inference(cnf_transformation,[],[f1308]) ).
fof(f2789,plain,
! [X2,X3,X0,X1,X4] :
( c_Polynomial_OpCons(X4,X3,X2) != c_Polynomial_OpCons(X4,X1,X0)
| X0 = X2
| ~ class_Groups_Ozero(X4) ),
inference(cnf_transformation,[],[f2409]) ).
fof(f2808,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X1)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X1)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) ),
inference(cnf_transformation,[],[f1326]) ).
fof(f2832,plain,
! [X0] :
( ~ class_Groups_Ozero(X0)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = c_Polynomial_OpCons(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) ),
inference(cnf_transformation,[],[f1341]) ).
fof(f2833,plain,
~ c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Nat_OSuc(c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_pa____),
inference(cnf_transformation,[],[f84]) ).
fof(f2834,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cnf_transformation,[],[f2419]) ).
fof(f2835,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cnf_transformation,[],[f2420]) ).
fof(f2845,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| hAPP(hAPP(c_Power_Opower__class_Opower(X1),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(X1) ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2920,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
inference(cnf_transformation,[],[f1379]) ).
fof(f2921,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(c_Polynomial_Opoly(X3,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(X3)),X2),X1)),X0) = hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(c_Polynomial_Opoly(X3,X2),X0)),X1) ),
inference(cnf_transformation,[],[f1380]) ).
fof(f2926,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X0),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) ),
inference(cnf_transformation,[],[f1388]) ).
fof(f2927,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0)) ),
inference(cnf_transformation,[],[f1389]) ).
fof(f2929,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) ),
inference(cnf_transformation,[],[f1391]) ).
fof(f2930,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X0)),X1) ),
inference(cnf_transformation,[],[f1392]) ).
fof(f2966,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,X1))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X1
| ~ class_Groups_Ozero(X2) ),
inference(cnf_transformation,[],[f1415]) ).
fof(f2973,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Ozero__class_Ozero(X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) ),
inference(cnf_transformation,[],[f1420]) ).
fof(f2985,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Oone__class_Oone(X1)),X0) = X0 ),
inference(cnf_transformation,[],[f1430]) ).
fof(f2986,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Oone__class_Oone(X1)) = X0 ),
inference(cnf_transformation,[],[f1431]) ).
fof(f3005,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(hAPP(c_Power_Opower__class_Opower(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X2),X0)),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X1),X0)) ),
inference(cnf_transformation,[],[f1455]) ).
fof(f3021,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,X0),
inference(cnf_transformation,[],[f231]) ).
fof(f3074,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),X2) = X1
| c_Rings_Oinverse__class_Odivide(X3,X1,X2) != X0
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(cnf_transformation,[],[f2471]) ).
fof(f3374,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(X2) = c_Groups_Ominus__class_Ominus(X2,X1,X0)
| X0 != X1
| ~ class_Groups_Oab__group__add(X2) ),
inference(cnf_transformation,[],[f2557]) ).
fof(f3638,plain,
! [X0,X1] :
( ~ class_Groups_Ozero(X1)
| c_Polynomial_OpCons(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_Polynomial_Omonom(X1,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
inference(cnf_transformation,[],[f2005]) ).
fof(f3657,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Polynomial_Odegree(X2,X1)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = c_Polynomial_Osynthetic__div(X2,X1,X0)
| ~ class_Rings_Ocomm__semiring__0(X2) ),
inference(cnf_transformation,[],[f2630]) ).
fof(f3683,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__ring__1(X2)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),c_Polynomial_OpCons(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Polynomial_OpCons(X2,c_Groups_Oone__class_Oone(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))))),c_Polynomial_Osynthetic__div(X2,X0,X1)),c_Polynomial_OpCons(X2,hAPP(c_Polynomial_Opoly(X2,X0),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)))) = X0 ),
inference(cnf_transformation,[],[f2047]) ).
fof(f3706,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X0) = X0 ),
inference(cnf_transformation,[],[f2069]) ).
fof(f3749,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
inference(cnf_transformation,[],[f2107]) ).
fof(f3789,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Ominus__class_Ominus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f2147]) ).
fof(f3790,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f2148]) ).
fof(f3870,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(c_Polynomial_Opoly(X3,c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0))) ),
inference(cnf_transformation,[],[f2237]) ).
fof(f3901,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = X0,
inference(cnf_transformation,[],[f879]) ).
fof(f3972,plain,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
inference(cnf_transformation,[],[f931]) ).
fof(f4028,plain,
! [X2,X0,X1] :
( ~ class_Rings_Oidom(X2)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = X1
| c_Polynomial_Odegree(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X2)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(X2,X1),c_Polynomial_Odegree(X2,X0)) ),
inference(cnf_transformation,[],[f2301]) ).
fof(f4205,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1123]) ).
fof(f4206,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1124]) ).
fof(f4208,plain,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1126]) ).
fof(f4210,plain,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1128]) ).
fof(f4213,plain,
class_Rings_Ocomm__ring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1131]) ).
fof(f4216,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1134]) ).
fof(f4226,plain,
class_Groups_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1144]) ).
fof(f4228,plain,
class_Rings_Oidom(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1146]) ).
fof(f4259,plain,
! [X0] :
( class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[],[f2371]) ).
fof(f4290,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_qa____),v_na____) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_pa____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_k____),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))))),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_r____),v_na____))),
inference(cnf_transformation,[],[f1212]) ).
fof(f4291,plain,
~ c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_pa____),
inference(definition_unfolding,[],[f2833,f3972]) ).
fof(f4485,plain,
! [X2,X0] :
( ~ class_Groups_Ozero(X2)
| c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(X2,c_Polynomial_OpCons(X2,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)))) ),
inference(equality_resolution,[],[f2966]) ).
fof(f4499,plain,
! [X2,X3,X1] :
( ~ class_Rings_Odivision__ring(X3)
| c_Groups_Ozero__class_Ozero(X3) = X2
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),c_Rings_Oinverse__class_Odivide(X3,X1,X2)),X2) = X1 ),
inference(equality_resolution,[],[f3074]) ).
fof(f4559,plain,
! [X2,X1] :
( ~ class_Groups_Oab__group__add(X2)
| c_Groups_Ozero__class_Ozero(X2) = c_Groups_Ominus__class_Ominus(X2,X1,X1) ),
inference(equality_resolution,[],[f3374]) ).
fof(f4683,definition,
sF23 = tc_Polynomial_Opoly(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f4684,plain,
tc_Polynomial_Opoly(tc_Complex_Ocomplex) = sF23,
inference(reorient_equations,[],[f4683]) ).
fof(f4685,definition,
sF24 = c_Power_Opower__class_Opower(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f4686,plain,
c_Power_Opower__class_Opower(sF23) = sF24,
inference(reorient_equations,[],[f4685]) ).
fof(f4687,definition,
sF25 = hAPP(sF24,v_qa____),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f4688,plain,
hAPP(sF24,v_qa____) = sF25,
inference(reorient_equations,[],[f4687]) ).
fof(f4689,definition,
sF26 = hAPP(sF25,v_na____),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f4690,plain,
hAPP(sF25,v_na____) = sF26,
inference(reorient_equations,[],[f4689]) ).
fof(f4691,definition,
sF27 = c_Groups_Otimes__class_Otimes(sF23),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f4692,plain,
c_Groups_Otimes__class_Otimes(sF23) = sF27,
inference(reorient_equations,[],[f4691]) ).
fof(f4693,definition,
sF28 = hAPP(sF27,v_pa____),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f4694,plain,
hAPP(sF27,v_pa____) = sF28,
inference(reorient_equations,[],[f4693]) ).
fof(f4695,definition,
sF29 = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f4696,plain,
c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = sF29,
inference(reorient_equations,[],[f4695]) ).
fof(f4697,definition,
sF30 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sF29,v_k____),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f4698,plain,
c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sF29,v_k____) = sF30,
inference(reorient_equations,[],[f4697]) ).
fof(f4699,definition,
sF31 = c_Groups_Ozero__class_Ozero(sF23),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f4700,plain,
c_Groups_Ozero__class_Ozero(sF23) = sF31,
inference(reorient_equations,[],[f4699]) ).
fof(f4701,definition,
sF32 = c_Polynomial_OpCons(tc_Complex_Ocomplex,sF30,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f4702,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF30,sF31) = sF32,
inference(reorient_equations,[],[f4701]) ).
fof(f4703,definition,
sF33 = hAPP(sF27,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f4704,plain,
hAPP(sF27,sF32) = sF33,
inference(reorient_equations,[],[f4703]) ).
fof(f4705,definition,
sF34 = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f4706,plain,
c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____) = sF34,
inference(reorient_equations,[],[f4705]) ).
fof(f4707,definition,
sF35 = c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f4708,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31) = sF35,
inference(reorient_equations,[],[f4707]) ).
fof(f4709,definition,
sF36 = c_Polynomial_OpCons(tc_Complex_Ocomplex,sF34,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f4710,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF34,sF35) = sF36,
inference(reorient_equations,[],[f4709]) ).
fof(f4711,definition,
sF37 = hAPP(sF24,sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f4712,plain,
hAPP(sF24,sF36) = sF37,
inference(reorient_equations,[],[f4711]) ).
fof(f4713,definition,
sF38 = c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f4714,plain,
c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____) = sF38,
inference(reorient_equations,[],[f4713]) ).
fof(f4715,definition,
sF39 = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f4716,plain,
c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_na____,sF38) = sF39,
inference(reorient_equations,[],[f4715]) ).
fof(f4717,definition,
sF40 = hAPP(sF37,sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
fof(f4718,plain,
hAPP(sF37,sF39) = sF40,
inference(reorient_equations,[],[f4717]) ).
fof(f4719,definition,
sF41 = hAPP(sF33,sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f4720,plain,
hAPP(sF33,sF40) = sF41,
inference(reorient_equations,[],[f4719]) ).
fof(f4721,definition,
sF42 = hAPP(sF27,sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
fof(f4722,plain,
hAPP(sF27,sF41) = sF42,
inference(reorient_equations,[],[f4721]) ).
fof(f4723,definition,
sF43 = hAPP(sF24,v_r____),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
fof(f4724,plain,
hAPP(sF24,v_r____) = sF43,
inference(reorient_equations,[],[f4723]) ).
fof(f4725,definition,
sF44 = hAPP(sF43,v_na____),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
fof(f4726,plain,
hAPP(sF43,v_na____) = sF44,
inference(reorient_equations,[],[f4725]) ).
fof(f4727,definition,
sF45 = hAPP(sF42,sF44),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f4728,plain,
hAPP(sF42,sF44) = sF45,
inference(reorient_equations,[],[f4727]) ).
fof(f4729,definition,
sF46 = hAPP(sF28,sF45),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f4730,plain,
hAPP(sF28,sF45) = sF46,
inference(reorient_equations,[],[f4729]) ).
fof(f4731,plain,
sF26 != sF46,
inference(definition_folding,[],[f4290,f4730,f4728,f4726,f4724,f4686,f4684,f4722,f4720,f4718,f4716,f4714,f4712,f4710,f4708,f4700,f4684,f4696,f4706,f4686,f4684,f4704,f4702,f4700,f4684,f4698,f4696,f4692,f4684,f4692,f4684,f4694,f4692,f4684,f4690,f4688,f4686,f4684]) ).
fof(f4809,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,c_Groups_Ozero__class_Ozero(sF23)),
inference(superposition,[],[f2742,f4684]) ).
fof(f4810,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,sF31),
inference(forward_demodulation,[],[f4809,f4700]) ).
fof(f4811,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,c_Groups_Ozero__class_Ozero(sF23)),
inference(superposition,[],[f2834,f4684]) ).
fof(f4812,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,sF31),
inference(forward_demodulation,[],[f4811,f4700]) ).
fof(f4813,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(sF23)),
inference(superposition,[],[f2835,f4684]) ).
fof(f4814,plain,
v_s____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,sF31),
inference(forward_demodulation,[],[f4813,f4700]) ).
fof(f4817,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)))),v_r____),
inference(superposition,[],[f2743,f4684]) ).
fof(f4818,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31))),v_r____),
inference(forward_demodulation,[],[f4817,f4700]) ).
fof(f4821,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31))),v_r____),
inference(forward_demodulation,[],[f4818,f4696]) ).
fof(f4824,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),sF35)),v_r____),
inference(forward_demodulation,[],[f4821,f4708]) ).
fof(f4827,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF34,sF35)),v_r____),
inference(forward_demodulation,[],[f4824,f4706]) ).
fof(f4830,plain,
v_qa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),sF36),v_r____),
inference(forward_demodulation,[],[f4827,f4710]) ).
fof(f4833,plain,
v_qa____ = hAPP(hAPP(sF27,sF36),v_r____),
inference(forward_demodulation,[],[f4830,f4692]) ).
fof(f4876,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),X1)) = X1,
inference(resolution,[],[f4205,f2788]) ).
fof(f4877,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(resolution,[],[f4205,f2973]) ).
fof(f4878,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)))),X1)) = X1,
inference(forward_demodulation,[],[f4876,f4684]) ).
fof(f4879,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31))),X1)) = X1,
inference(forward_demodulation,[],[f4878,f4700]) ).
fof(f4880,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31))),X1)) = X1,
inference(forward_demodulation,[],[f4879,f4696]) ).
fof(f4881,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF35)),X1)) = X1,
inference(forward_demodulation,[],[f4880,f4708]) ).
fof(f4882,plain,
! [X0,X1] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF24,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF35)),X1)) = X1,
inference(forward_demodulation,[],[f4881,f4686]) ).
fof(f4883,plain,
! [X0] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF24,sF36),X0)) = X0,
inference(superposition,[],[f4882,f4710]) ).
fof(f4884,plain,
! [X0] : c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(sF37,X0)) = X0,
inference(forward_demodulation,[],[f4883,f4712]) ).
fof(f4907,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),X0),
inference(resolution,[],[f2926,f4205]) ).
fof(f4911,plain,
c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),sF38),v_pa____),
inference(superposition,[],[f2750,f4714]) ).
fof(f4912,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)))),sF38),v_pa____),
inference(forward_demodulation,[],[f4911,f4684]) ).
fof(f4916,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31))),sF38),v_pa____),
inference(forward_demodulation,[],[f4912,f4700]) ).
fof(f4920,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31))),sF38),v_pa____),
inference(forward_demodulation,[],[f4916,f4696]) ).
fof(f4924,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),sF35)),sF38),v_pa____),
inference(forward_demodulation,[],[f4920,f4708]) ).
fof(f4928,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF34,sF35)),sF38),v_pa____),
inference(forward_demodulation,[],[f4924,f4706]) ).
fof(f4932,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),sF36),sF38),v_pa____),
inference(forward_demodulation,[],[f4928,f4710]) ).
fof(f4936,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(hAPP(sF24,sF36),sF38),v_pa____),
inference(forward_demodulation,[],[f4932,f4686]) ).
fof(f4940,plain,
c_Rings_Odvd__class_Odvd(sF23,hAPP(sF37,sF38),v_pa____),
inference(forward_demodulation,[],[f4936,f4712]) ).
fof(f4947,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),sF38)),v_s____),
inference(superposition,[],[f2745,f4714]) ).
fof(f4948,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)))),sF38)),v_s____),
inference(forward_demodulation,[],[f4947,f4684]) ).
fof(f4952,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31))),sF38)),v_s____),
inference(forward_demodulation,[],[f4948,f4700]) ).
fof(f4956,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31))),sF38)),v_s____),
inference(forward_demodulation,[],[f4952,f4696]) ).
fof(f4960,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),sF35)),sF38)),v_s____),
inference(forward_demodulation,[],[f4956,f4708]) ).
fof(f4964,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF34,sF35)),sF38)),v_s____),
inference(forward_demodulation,[],[f4960,f4706]) ).
fof(f4968,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),sF36),sF38)),v_s____),
inference(forward_demodulation,[],[f4964,f4710]) ).
fof(f4972,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(sF24,sF36),sF38)),v_s____),
inference(forward_demodulation,[],[f4968,f4686]) ).
fof(f4976,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(sF37,sF38)),v_s____),
inference(forward_demodulation,[],[f4972,f4712]) ).
fof(f4980,plain,
v_pa____ = hAPP(hAPP(sF27,hAPP(sF37,sF38)),v_s____),
inference(forward_demodulation,[],[f4976,f4692]) ).
fof(f4984,plain,
v_pa____ != c_Groups_Ozero__class_Ozero(sF23),
inference(superposition,[],[f2739,f4684]) ).
fof(f4985,plain,
v_pa____ != sF31,
inference(forward_demodulation,[],[f4984,f4700]) ).
fof(f4986,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),X0) = X0,
inference(resolution,[],[f2985,f4205]) ).
fof(f4987,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF29),X0) = X0,
inference(forward_demodulation,[],[f4986,f4696]) ).
fof(f4996,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X2),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2))),
inference(resolution,[],[f3870,f4206]) ).
fof(f5065,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0),
inference(resolution,[],[f3749,f4205]) ).
fof(f5070,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(resolution,[],[f2758,f4205]) ).
fof(f5071,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)) = c_Groups_Oone__class_Oone(sF23),
inference(forward_demodulation,[],[f5070,f4684]) ).
fof(f5072,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31) = c_Groups_Oone__class_Oone(sF23),
inference(forward_demodulation,[],[f5071,f4700]) ).
fof(f5073,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31) = c_Groups_Oone__class_Oone(sF23),
inference(forward_demodulation,[],[f5072,f4696]) ).
fof(f5074,plain,
sF35 = c_Groups_Oone__class_Oone(sF23),
inference(forward_demodulation,[],[f5073,f4708]) ).
fof(f5075,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),X2)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X1)),X2),
inference(resolution,[],[f2929,f4205]) ).
fof(f5099,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0),
inference(resolution,[],[f2808,f4206]) ).
fof(f5100,plain,
! [X0] : c_Groups_Ozero__class_Ozero(sF23) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Groups_Ozero__class_Ozero(sF23)),X0),
inference(forward_demodulation,[],[f5099,f4684]) ).
fof(f5101,plain,
! [X0] : sF31 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),sF31),X0),
inference(forward_demodulation,[],[f5100,f4700]) ).
fof(f5102,plain,
! [X0] : sF31 = hAPP(hAPP(sF27,sF31),X0),
inference(forward_demodulation,[],[f5101,f4692]) ).
fof(f5104,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) ),
inference(resolution,[],[f4028,f4228]) ).
fof(f5105,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(sF23) = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) ),
inference(forward_demodulation,[],[f5104,f4684]) ).
fof(f5106,plain,
! [X0,X1] :
( sF31 = X0
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) ),
inference(forward_demodulation,[],[f5105,f4700]) ).
fof(f5107,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(sF23) = X1
| sF31 = X0
| c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) ),
inference(forward_demodulation,[],[f5106,f4684]) ).
fof(f5108,plain,
! [X0,X1] :
( sF31 = X1
| sF31 = X0
| c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) ),
inference(forward_demodulation,[],[f5107,f4700]) ).
fof(f5109,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X1),X0))
| sF31 = X1
| sF31 = X0 ),
inference(forward_demodulation,[],[f5108,f4684]) ).
fof(f5110,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X1),c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X1),X0))
| sF31 = X1
| sF31 = X0 ),
inference(forward_demodulation,[],[f5109,f4692]) ).
fof(f5120,plain,
! [X0] :
( c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),v_s____)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Polynomial_Odegree(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| sF31 = X0
| v_s____ = sF31 ),
inference(superposition,[],[f5110,f2760]) ).
fof(f5139,plain,
! [X0] :
( c_Polynomial_Odegree(tc_Complex_Ocomplex,X0) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),v_s____))
| sF31 = X0
| v_s____ = sF31 ),
inference(forward_demodulation,[],[f5120,f3901]) ).
fof(f5152,definition,
( spl47_9
<=> v_s____ = sF31 ),
introduced(definition,[new_symbols(definition,[spl47_9])],[avatar_definition]) ).
fof(f5154,plain,
( v_s____ = sF31
| ~ spl47_9 ),
inference(avatar_component_clause,[],[f5152]) ).
fof(f5156,definition,
( spl47_10
<=> ! [X0] :
( c_Polynomial_Odegree(tc_Complex_Ocomplex,X0) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),v_s____))
| sF31 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl47_10])],[avatar_definition]) ).
fof(f5157,plain,
( ! [X0] :
( c_Polynomial_Odegree(tc_Complex_Ocomplex,X0) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),v_s____))
| sF31 = X0 )
| ~ spl47_10 ),
inference(avatar_component_clause,[],[f5156]) ).
fof(f5158,plain,
( spl47_9
| spl47_10 ),
inference(avatar_split_clause,[],[f5139,f5156,f5152]) ).
fof(f5375,definition,
( spl47_31
<=> sF31 = sF32 ),
introduced(definition,[new_symbols(definition,[spl47_31])],[avatar_definition]) ).
fof(f5376,plain,
( sF31 != sF32
| spl47_31 ),
inference(avatar_component_clause,[],[f5375]) ).
fof(f5377,plain,
( sF31 = sF32
| ~ spl47_31 ),
inference(avatar_component_clause,[],[f5375]) ).
fof(f5406,plain,
! [X0] : c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolution,[],[f2845,f4205]) ).
fof(f5407,plain,
! [X0] : sF29 = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f5406,f4696]) ).
fof(f5414,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X2)),X1),
inference(resolution,[],[f2930,f4205]) ).
fof(f5415,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X2),X1)),
inference(forward_demodulation,[],[f5414,f5075]) ).
fof(f5416,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),X2)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X2),X1)),
inference(forward_demodulation,[],[f5415,f5075]) ).
fof(f5640,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0),
inference(resolution,[],[f4559,f4210]) ).
fof(f5675,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(sF33,v_s____))
| sF31 = sF32
| ~ spl47_10 ),
inference(superposition,[],[f5157,f4704]) ).
fof(f5677,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_pa____) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(sF37,sF38))
| sF31 = hAPP(sF37,sF38)
| ~ spl47_10 ),
inference(superposition,[],[f5157,f4980]) ).
fof(f5684,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_pa____) = sF38
| sF31 = hAPP(sF37,sF38)
| ~ spl47_10 ),
inference(forward_demodulation,[],[f5677,f4884]) ).
fof(f5690,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32) = c_Polynomial_Odegree(tc_Complex_Ocomplex,hAPP(sF33,v_s____))
| ~ spl47_10
| spl47_31 ),
inference(forward_subsumption_resolution,[],[f5675,f5376]) ).
fof(f5692,plain,
( v_na____ = sF38
| sF31 = hAPP(sF37,sF38)
| ~ spl47_10 ),
inference(forward_demodulation,[],[f5684,f2746]) ).
fof(f5696,definition,
( spl47_41
<=> sF31 = hAPP(sF37,sF38) ),
introduced(definition,[new_symbols(definition,[spl47_41])],[avatar_definition]) ).
fof(f5697,plain,
( sF31 != hAPP(sF37,sF38)
| spl47_41 ),
inference(avatar_component_clause,[],[f5696]) ).
fof(f5698,plain,
( sF31 = hAPP(sF37,sF38)
| ~ spl47_41 ),
inference(avatar_component_clause,[],[f5696]) ).
fof(f5704,plain,
( v_pa____ = hAPP(hAPP(sF27,sF31),v_s____)
| ~ spl47_41 ),
inference(superposition,[],[f4980,f5698]) ).
fof(f5710,plain,
( v_pa____ = sF31
| ~ spl47_41 ),
inference(forward_demodulation,[],[f5704,f5102]) ).
fof(f5714,plain,
( $false
| ~ spl47_41 ),
inference(forward_subsumption_resolution,[],[f5710,f4985]) ).
fof(f5715,plain,
~ spl47_41,
inference(avatar_contradiction_clause,[],[f5714]) ).
fof(f5743,plain,
( class_Rings_Ocomm__semiring__1(sF23)
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f4259,f4684]) ).
fof(f5744,plain,
class_Rings_Ocomm__semiring__1(sF23),
inference(forward_subsumption_resolution,[],[f5743,f4205]) ).
fof(f5748,plain,
! [X0] : c_Groups_Oone__class_Oone(sF23) = hAPP(hAPP(c_Power_Opower__class_Opower(sF23),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolution,[],[f5744,f2845]) ).
fof(f5749,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X1),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X1),
inference(resolution,[],[f5744,f2926]) ).
fof(f5750,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X1),X2)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X2)),
inference(resolution,[],[f5744,f2927]) ).
fof(f5751,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X1),X2)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X1)),X2),
inference(resolution,[],[f5744,f2929]) ).
fof(f5754,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Groups_Oone__class_Oone(sF23)),X0) = X0,
inference(resolution,[],[f5744,f2985]) ).
fof(f5755,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),c_Groups_Oone__class_Oone(sF23)) = X0,
inference(resolution,[],[f5744,f2986]) ).
fof(f5756,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Power_Opower__class_Opower(sF23),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),X0),X2)),hAPP(hAPP(c_Power_Opower__class_Opower(sF23),X1),X2)),
inference(resolution,[],[f5744,f3005]) ).
fof(f5758,plain,
! [X2,X0,X1] : hAPP(hAPP(sF24,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),hAPP(hAPP(sF24,X0),X2)),hAPP(hAPP(sF24,X1),X2)),
inference(forward_demodulation,[],[f5756,f4686]) ).
fof(f5759,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),sF35) = X0,
inference(forward_demodulation,[],[f5755,f5074]) ).
fof(f5760,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),sF35),X0) = X0,
inference(forward_demodulation,[],[f5754,f5074]) ).
fof(f5763,plain,
! [X2,X0,X1] : hAPP(hAPP(sF27,hAPP(hAPP(sF27,X0),X1)),X2) = hAPP(hAPP(sF27,X0),hAPP(hAPP(sF27,X1),X2)),
inference(forward_demodulation,[],[f5751,f4692]) ).
fof(f5764,plain,
! [X2,X0,X1] : hAPP(hAPP(sF27,X0),hAPP(hAPP(sF27,X1),X2)) = hAPP(hAPP(sF27,X1),hAPP(hAPP(sF27,X0),X2)),
inference(forward_demodulation,[],[f5750,f4692]) ).
fof(f5765,plain,
! [X0,X1] : hAPP(hAPP(sF27,X1),X0) = hAPP(hAPP(sF27,X0),X1),
inference(forward_demodulation,[],[f5749,f4692]) ).
fof(f5769,plain,
! [X2,X0,X1] : hAPP(hAPP(sF24,hAPP(hAPP(sF27,X0),X1)),X2) = hAPP(hAPP(sF27,hAPP(hAPP(sF24,X0),X2)),hAPP(hAPP(sF24,X1),X2)),
inference(forward_demodulation,[],[f5758,f4692]) ).
fof(f5770,plain,
! [X0] : hAPP(hAPP(sF27,X0),sF35) = X0,
inference(forward_demodulation,[],[f5759,f4692]) ).
fof(f5771,plain,
! [X0] : hAPP(hAPP(sF27,sF35),X0) = X0,
inference(forward_demodulation,[],[f5760,f4692]) ).
fof(f5783,plain,
! [X0] : hAPP(hAPP(sF27,X0),v_pa____) = hAPP(sF28,X0),
inference(superposition,[],[f5765,f4694]) ).
fof(f5784,plain,
! [X0] : hAPP(sF33,X0) = hAPP(hAPP(sF27,X0),sF32),
inference(superposition,[],[f5765,f4704]) ).
fof(f5785,plain,
! [X0] : hAPP(hAPP(sF27,X0),sF41) = hAPP(sF42,X0),
inference(superposition,[],[f5765,f4722]) ).
fof(f5888,plain,
! [X0,X1] : hAPP(hAPP(sF27,X0),hAPP(sF33,X1)) = hAPP(sF33,hAPP(hAPP(sF27,X0),X1)),
inference(superposition,[],[f5764,f4704]) ).
fof(f5892,plain,
! [X2,X0,X1] : hAPP(hAPP(sF27,X1),hAPP(hAPP(sF27,X2),X0)) = hAPP(hAPP(sF27,X2),hAPP(hAPP(sF27,X0),X1)),
inference(superposition,[],[f5764,f5765]) ).
fof(f5968,plain,
! [X0,X1] : hAPP(sF33,hAPP(hAPP(sF27,X0),X1)) = hAPP(hAPP(sF27,hAPP(sF33,X0)),X1),
inference(superposition,[],[f5763,f4704]) ).
fof(f6059,plain,
! [X0] : hAPP(sF28,hAPP(sF33,X0)) = hAPP(sF33,hAPP(sF28,X0)),
inference(superposition,[],[f5888,f4694]) ).
fof(f6061,plain,
! [X0] : hAPP(hAPP(sF27,X0),sF41) = hAPP(sF33,hAPP(hAPP(sF27,X0),sF40)),
inference(superposition,[],[f5888,f4720]) ).
fof(f6086,plain,
! [X0] : hAPP(sF42,X0) = hAPP(sF33,hAPP(hAPP(sF27,X0),sF40)),
inference(forward_demodulation,[],[f6061,f5785]) ).
fof(f6262,plain,
! [X0] : c_Groups_Oone__class_Oone(sF23) = hAPP(hAPP(sF24,X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f5748,f4686]) ).
fof(f6267,plain,
! [X0] : sF35 = hAPP(hAPP(sF24,X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f6262,f5074]) ).
fof(f6277,plain,
( v_na____ = sF38
| ~ spl47_10
| spl47_41 ),
inference(forward_subsumption_resolution,[],[f5692,f5697]) ).
fof(f6363,plain,
( sF26 = hAPP(sF25,sF38)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4690,f6277]) ).
fof(f6364,plain,
( sF39 = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,sF38,sF38)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4716,f6277]) ).
fof(f6365,plain,
( sF44 = hAPP(sF43,sF38)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4726,f6277]) ).
fof(f6372,plain,
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = sF39
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f6364,f3021]) ).
fof(f6384,plain,
( ! [X0] : sF29 = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),sF39)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f5407,f6372]) ).
fof(f7176,plain,
! [X0,X1] : hAPP(hAPP(sF24,hAPP(hAPP(sF27,v_r____),X0)),X1) = hAPP(hAPP(sF27,hAPP(sF43,X1)),hAPP(hAPP(sF24,X0),X1)),
inference(superposition,[],[f5769,f4724]) ).
fof(f7459,plain,
sF35 = hAPP(sF37,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(superposition,[],[f6267,f4712]) ).
fof(f7460,plain,
( ! [X0] : sF35 = hAPP(hAPP(sF24,X0),sF39)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f6267,f6372]) ).
fof(f7467,plain,
( sF35 = hAPP(sF37,sF39)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f7459,f6372]) ).
fof(f7472,plain,
( sF35 = sF40
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f7467,f4718]) ).
fof(f7473,plain,
( ! [X0] : hAPP(sF42,X0) = hAPP(sF33,hAPP(hAPP(sF27,X0),sF35))
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f6086,f7472]) ).
fof(f7479,plain,
( ! [X0] : hAPP(sF33,X0) = hAPP(sF42,X0)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f7473,f5770]) ).
fof(f7592,plain,
( sF45 = hAPP(sF33,sF44)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4728,f7479]) ).
fof(f7790,plain,
! [X0] : hAPP(hAPP(sF27,X0),v_pa____) = hAPP(hAPP(sF27,v_s____),hAPP(hAPP(sF27,X0),hAPP(sF37,sF38))),
inference(superposition,[],[f5892,f4980]) ).
fof(f7791,plain,
! [X0] : hAPP(hAPP(sF27,X0),v_qa____) = hAPP(hAPP(sF27,v_r____),hAPP(hAPP(sF27,X0),sF36)),
inference(superposition,[],[f5892,f4833]) ).
fof(f7893,plain,
! [X0] : hAPP(sF28,X0) = hAPP(hAPP(sF27,v_s____),hAPP(hAPP(sF27,X0),hAPP(sF37,sF38))),
inference(forward_demodulation,[],[f7790,f5783]) ).
fof(f8695,plain,
hAPP(hAPP(sF27,v_r____),sF36) = hAPP(hAPP(sF27,sF35),v_qa____),
inference(superposition,[],[f7791,f5771]) ).
fof(f8736,plain,
v_qa____ = hAPP(hAPP(sF27,v_r____),sF36),
inference(forward_demodulation,[],[f8695,f5771]) ).
fof(f8958,plain,
! [X0] : hAPP(hAPP(sF24,hAPP(hAPP(sF27,v_r____),sF36)),X0) = hAPP(hAPP(sF27,hAPP(sF43,X0)),hAPP(sF37,X0)),
inference(superposition,[],[f7176,f4712]) ).
fof(f8979,plain,
! [X0] : hAPP(hAPP(sF24,v_qa____),X0) = hAPP(hAPP(sF27,hAPP(sF43,X0)),hAPP(sF37,X0)),
inference(forward_demodulation,[],[f8958,f8736]) ).
fof(f8986,plain,
! [X0] : hAPP(sF25,X0) = hAPP(hAPP(sF27,hAPP(sF43,X0)),hAPP(sF37,X0)),
inference(forward_demodulation,[],[f8979,f4688]) ).
fof(f8995,plain,
hAPP(sF28,hAPP(sF43,sF38)) = hAPP(hAPP(sF27,v_s____),hAPP(sF25,sF38)),
inference(superposition,[],[f7893,f8986]) ).
fof(f9012,plain,
( hAPP(sF28,hAPP(sF43,sF38)) = hAPP(hAPP(sF27,v_s____),sF26)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f8995,f6363]) ).
fof(f9019,plain,
( hAPP(sF28,sF44) = hAPP(hAPP(sF27,v_s____),sF26)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f9012,f6365]) ).
fof(f12443,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X0)),X0) = X1
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(resolution,[],[f4499,f4208]) ).
fof(f12447,plain,
( sF29 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),v_k____)
| v_k____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f12443,f4698]) ).
fof(f12472,plain,
sF29 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),v_k____),
inference(forward_subsumption_resolution,[],[f12447,f2738]) ).
fof(f14327,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF29),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),v_k____),X0)),
inference(superposition,[],[f5075,f12472]) ).
fof(f14328,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),v_k____),X0)) = X0,
inference(forward_demodulation,[],[f14327,f4987]) ).
fof(f14338,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),v_k____)) = X0,
inference(superposition,[],[f5416,f14328]) ).
fof(f14349,plain,
! [X0] :
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),X0)
| v_k____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f14338,f12443]) ).
fof(f14359,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),X0),
inference(forward_subsumption_resolution,[],[f14349,f2738]) ).
fof(f14374,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF30),
inference(superposition,[],[f4907,f14359]) ).
fof(f14381,plain,
sF29 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,v_k____,v_k____),
inference(superposition,[],[f12472,f14359]) ).
fof(f14436,definition,
( spl47_61
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF30 ),
introduced(definition,[new_symbols(definition,[spl47_61])],[avatar_definition]) ).
fof(f14437,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF30
| spl47_61 ),
inference(avatar_component_clause,[],[f14436]) ).
fof(f14438,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF30
| ~ spl47_61 ),
inference(avatar_component_clause,[],[f14436]) ).
fof(f14448,plain,
( ! [X0] : sF30 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF30)
| ~ spl47_61 ),
inference(superposition,[],[f4877,f14438]) ).
fof(f14452,plain,
( ! [X0] : sF30 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____)
| ~ spl47_61 ),
inference(forward_demodulation,[],[f14448,f14374]) ).
fof(f14459,plain,
( ! [X0] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),v_k____) = X0
| v_k____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
| ~ spl47_61 ),
inference(superposition,[],[f12443,f14452]) ).
fof(f14464,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF30),v_k____) = X0
| ~ spl47_61 ),
inference(forward_subsumption_resolution,[],[f14459,f2738]) ).
fof(f14468,plain,
( ! [X0] : sF29 = X0
| ~ spl47_61 ),
inference(forward_demodulation,[],[f14464,f12472]) ).
fof(f14629,plain,
( ~ c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex),sF29,v_pa____)
| ~ spl47_61 ),
inference(superposition,[],[f4291,f14468]) ).
fof(f14883,plain,
( c_Rings_Odvd__class_Odvd(sF23,sF29,v_pa____)
| ~ spl47_61 ),
inference(superposition,[],[f4940,f14468]) ).
fof(f16129,plain,
( ~ c_Rings_Odvd__class_Odvd(sF23,sF29,v_pa____)
| ~ spl47_61 ),
inference(forward_demodulation,[],[f14629,f4684]) ).
fof(f16242,plain,
( $false
| ~ spl47_61 ),
inference(forward_subsumption_resolution,[],[f16129,f14883]) ).
fof(f16243,plain,
~ spl47_61,
inference(avatar_contradiction_clause,[],[f16242]) ).
fof(f16987,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0) = X0,
inference(resolution,[],[f3706,f4205]) ).
fof(f16989,plain,
! [X0] : c_Groups_Oplus__class_Oplus(sF23,c_Groups_Ozero__class_Ozero(sF23),X0) = X0,
inference(resolution,[],[f3706,f5744]) ).
fof(f16990,plain,
! [X0] : c_Groups_Oplus__class_Oplus(sF23,sF31,X0) = X0,
inference(forward_demodulation,[],[f16989,f4700]) ).
fof(f17002,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X1)),X0),
inference(superposition,[],[f4996,f16987]) ).
fof(f17005,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X0,
inference(superposition,[],[f5065,f16987]) ).
fof(f17320,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1),X1) = X0,
inference(resolution,[],[f3790,f4216]) ).
fof(f17329,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)) = X0,
inference(superposition,[],[f5065,f17320]) ).
fof(f17619,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X1)),X2) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),X1),
inference(resolution,[],[f2921,f4205]) ).
fof(f17623,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),X1) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Power_Opower__class_Opower(sF23),X0),X1)),X2),
inference(forward_demodulation,[],[f17619,f4684]) ).
fof(f17624,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),X1) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF24,X0),X1)),X2),
inference(forward_demodulation,[],[f17623,f4686]) ).
fof(f17633,plain,
( ! [X0,X1] : sF29 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF24,X0),sF39)),X1)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f6384,f17624]) ).
fof(f17636,plain,
( ! [X1] : sF29 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF35),X1)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f17633,f7460]) ).
fof(f17780,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(resolution,[],[f2832,f4226]) ).
fof(f17781,plain,
c_Groups_Ozero__class_Ozero(sF23) = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)),
inference(forward_demodulation,[],[f17780,f4684]) ).
fof(f17782,plain,
sF31 = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF31),
inference(forward_demodulation,[],[f17781,f4700]) ).
fof(f18282,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1),X1) = X0,
inference(resolution,[],[f3789,f4216]) ).
fof(f18285,plain,
! [X2,X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X2),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2))) = X0,
inference(superposition,[],[f18282,f4996]) ).
fof(f18287,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)) = X1,
inference(superposition,[],[f18282,f17329]) ).
fof(f18308,plain,
! [X2,X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X1)),X2)) = X0,
inference(forward_demodulation,[],[f18285,f17002]) ).
fof(f18504,plain,
! [X0] : v_k____ = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF31)),X0)),
inference(superposition,[],[f18308,f4810]) ).
fof(f18505,plain,
! [X0] : sK6 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF31)),X0)),
inference(superposition,[],[f18308,f4812]) ).
fof(f18506,plain,
! [X0] : sK7 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF31)),X0)),
inference(superposition,[],[f18308,f4814]) ).
fof(f18507,plain,
! [X0] : sF29 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF35),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF31)),X0)),
inference(superposition,[],[f18308,f4708]) ).
fof(f18523,plain,
! [X0] : sF29 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF35),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)),
inference(forward_demodulation,[],[f18507,f17782]) ).
fof(f18524,plain,
! [X0] : sK7 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)),
inference(forward_demodulation,[],[f18506,f17782]) ).
fof(f18525,plain,
! [X0] : sK6 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)),
inference(forward_demodulation,[],[f18505,f17782]) ).
fof(f18526,plain,
! [X0] : v_k____ = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)),
inference(forward_demodulation,[],[f18504,f17782]) ).
fof(f18533,plain,
( ! [X0] : sF29 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,sF29,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0))
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f18523,f17636]) ).
fof(f18534,plain,
sK6 = sK7,
inference(forward_demodulation,[],[f18525,f18524]) ).
fof(f18535,plain,
v_k____ = sK7,
inference(forward_demodulation,[],[f18526,f18524]) ).
fof(f18539,plain,
v_k____ = sK6,
inference(forward_demodulation,[],[f18535,f18534]) ).
fof(f18552,plain,
sF29 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sK6,sK6),
inference(superposition,[],[f14381,f18539]) ).
fof(f18578,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,sF29,sF29)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f18287,f18533]) ).
fof(f18585,plain,
( ! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f18578,f5640]) ).
fof(f18588,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF31)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4996,f18585]) ).
fof(f18591,plain,
( ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF31)),X1)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f18588,f4877]) ).
fof(f18592,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF31)),X1) = X0
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f18591,f17005]) ).
fof(f18595,plain,
( ! [X0] : sK6 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f18592,f4812]) ).
fof(f18598,plain,
( ! [X0] : sF30 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32),X0)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f18592,f4702]) ).
fof(f21041,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),
inference(resolution,[],[f2920,f4206]) ).
fof(f21045,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),X0),X1)),X2),
inference(forward_demodulation,[],[f21041,f4684]) ).
fof(f21046,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),X1)),X2),
inference(forward_demodulation,[],[f21045,f4692]) ).
fof(f21058,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),sF32)),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)),sF30)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f21046,f18598]) ).
fof(f21094,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),sF32)),X1) = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1),v_k____)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f21058,f14374]) ).
fof(f21107,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF27,X0),sF32)),X1) = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1),sK6)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f21094,f18539]) ).
fof(f21117,plain,
( ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1),sK6) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF33,X0)),X1)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f21107,f5784]) ).
fof(f23481,plain,
( ! [X0] : sF30 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF31),X0)
| ~ spl47_10
| ~ spl47_31
| spl47_41 ),
inference(superposition,[],[f18598,f5377]) ).
fof(f23485,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF30
| ~ spl47_10
| ~ spl47_31
| spl47_41 ),
inference(forward_demodulation,[],[f23481,f18585]) ).
fof(f23488,plain,
( $false
| ~ spl47_10
| ~ spl47_31
| spl47_41
| spl47_61 ),
inference(forward_subsumption_resolution,[],[f23485,f14437]) ).
fof(f23489,plain,
( ~ spl47_10
| ~ spl47_31
| spl47_41
| spl47_61 ),
inference(avatar_contradiction_clause,[],[f23488]) ).
fof(f28934,plain,
! [X0,X1] :
( sF31 != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)
| sF31 = X1
| ~ class_Groups_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f2789,f17782]) ).
fof(f28949,plain,
! [X0,X1] :
( sF31 != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)
| sF31 = X1 ),
inference(forward_subsumption_resolution,[],[f28934,f4226]) ).
fof(f58527,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) = X1,
inference(resolution,[],[f3683,f4213]) ).
fof(f58528,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF23)))),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),c_Groups_Ozero__class_Ozero(sF23))) = X1,
inference(forward_demodulation,[],[f58527,f4684]) ).
fof(f58529,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF31))),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),sF31)) = X1,
inference(forward_demodulation,[],[f58528,f4700]) ).
fof(f58530,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,sF29,sF31))),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),sF31)) = X1,
inference(forward_demodulation,[],[f58529,f4696]) ).
fof(f58531,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF23),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),sF31)) = X1,
inference(forward_demodulation,[],[f58530,f4708]) ).
fof(f58532,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X0),sF31)) = X1,
inference(forward_demodulation,[],[f58531,f4692]) ).
fof(f58542,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1),sF35)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1),sF31)) = X0,
inference(superposition,[],[f58532,f5765]) ).
fof(f69843,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0)
| ~ class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) )
| ~ spl47_10
| spl47_31 ),
inference(superposition,[],[f3657,f5690]) ).
fof(f69903,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0) )
| ~ spl47_10
| spl47_31 ),
inference(forward_subsumption_resolution,[],[f69843,f4206]) ).
fof(f69948,plain,
( ! [X0] :
( sF39 != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0) )
| ~ spl47_10
| spl47_31
| spl47_41 ),
inference(forward_demodulation,[],[f69903,f6372]) ).
fof(f69993,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(sF23) = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0)
| sF39 != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32) )
| ~ spl47_10
| spl47_31
| spl47_41 ),
inference(forward_demodulation,[],[f69948,f4684]) ).
fof(f70037,plain,
( ! [X0] :
( sF31 = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0)
| sF39 != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32) )
| ~ spl47_10
| spl47_31
| spl47_41 ),
inference(forward_demodulation,[],[f69993,f4700]) ).
fof(f70099,definition,
( spl47_411
<=> sF39 = c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32) ),
introduced(definition,[new_symbols(definition,[spl47_411])],[avatar_definition]) ).
fof(f70101,plain,
( sF39 != c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32)
| spl47_411 ),
inference(avatar_component_clause,[],[f70099]) ).
fof(f70103,definition,
( spl47_412
<=> ! [X0] : sF31 = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0) ),
introduced(definition,[new_symbols(definition,[spl47_412])],[avatar_definition]) ).
fof(f70104,plain,
( ! [X0] : sF31 = c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,hAPP(sF33,v_s____),X0)
| ~ spl47_412 ),
inference(avatar_component_clause,[],[f70103]) ).
fof(f70105,plain,
( ~ spl47_411
| spl47_412
| ~ spl47_10
| spl47_31
| spl47_41 ),
inference(avatar_split_clause,[],[f70037,f5696,f5375,f5156,f70103,f70099]) ).
fof(f74706,plain,
( v_s____ != sF31
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = sF31 ),
inference(superposition,[],[f28949,f2742]) ).
fof(f85222,definition,
( spl47_556
<=> sF35 = hAPP(sF33,v_s____) ),
introduced(definition,[new_symbols(definition,[spl47_556])],[avatar_definition]) ).
fof(f85223,plain,
( sF35 = hAPP(sF33,v_s____)
| ~ spl47_556 ),
inference(avatar_component_clause,[],[f85222]) ).
fof(f85224,plain,
( sF35 != hAPP(sF33,v_s____)
| spl47_556 ),
inference(avatar_component_clause,[],[f85222]) ).
fof(f111899,plain,
( ! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sK6,sK6) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF33,v_s____)),X0)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f21117,f18595]) ).
fof(f112060,plain,
( ! [X0] : sF29 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF33,v_s____)),X0)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f111899,f18552]) ).
fof(f246995,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = sF31
| ~ spl47_9 ),
inference(forward_subsumption_resolution,[],[f74706,f5154]) ).
fof(f247136,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_s____
| ~ spl47_9 ),
inference(forward_demodulation,[],[f246995,f5154]) ).
fof(f247206,plain,
( $false
| ~ spl47_9 ),
inference(forward_subsumption_resolution,[],[f247136,f2749]) ).
fof(f247207,plain,
~ spl47_9,
inference(avatar_contradiction_clause,[],[f247206]) ).
fof(f350823,plain,
! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolution,[],[f3638,f4226]) ).
fof(f350824,plain,
( ! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,sF39)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f350823,f6372]) ).
fof(f350825,plain,
( ! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(sF23)) = c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,sF39)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f350824,f4684]) ).
fof(f350826,plain,
( ! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF31) = c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,sF39)
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f350825,f4700]) ).
fof(f350991,plain,
( sF35 = c_Polynomial_Omonom(tc_Complex_Ocomplex,sF29,sF39)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4708,f350826]) ).
fof(f350992,plain,
( sF32 = c_Polynomial_Omonom(tc_Complex_Ocomplex,sF30,sF39)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f4702,f350826]) ).
fof(f379593,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
inference(resolution,[],[f4485,f4226]) ).
fof(f379594,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(sF23))),
inference(forward_demodulation,[],[f379593,f4684]) ).
fof(f379595,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF31)),
inference(forward_demodulation,[],[f379594,f4700]) ).
fof(f379596,plain,
( ! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,sF39))
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f379595,f350826]) ).
fof(f379597,plain,
( ! [X0] : sF39 = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,sF39))
| ~ spl47_10
| spl47_41 ),
inference(forward_demodulation,[],[f379596,f6372]) ).
fof(f379602,plain,
( sF39 = c_Polynomial_Odegree(tc_Complex_Ocomplex,sF32)
| ~ spl47_10
| spl47_41 ),
inference(superposition,[],[f379597,f350992]) ).
fof(f379701,plain,
( $false
| ~ spl47_10
| spl47_41
| spl47_411 ),
inference(forward_subsumption_resolution,[],[f379602,f70101]) ).
fof(f379702,plain,
( ~ spl47_10
| spl47_41
| spl47_411 ),
inference(avatar_contradiction_clause,[],[f379701]) ).
fof(f394540,plain,
( ! [X0] : hAPP(sF33,v_s____) = c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,sF31),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),c_Polynomial_OpCons(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF33,v_s____)),X0),sF31))
| ~ spl47_412 ),
inference(superposition,[],[f58542,f70104]) ).
fof(f394559,plain,
( ! [X0] : hAPP(sF33,v_s____) = c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,sF31),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),c_Polynomial_Omonom(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF33,v_s____)),X0),sF39))
| ~ spl47_10
| spl47_41
| ~ spl47_412 ),
inference(forward_demodulation,[],[f394540,f350826]) ).
fof(f394569,plain,
( ! [X0] : hAPP(sF33,v_s____) = c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,sF31),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),c_Polynomial_Omonom(tc_Complex_Ocomplex,sF29,sF39))
| ~ spl47_10
| spl47_41
| ~ spl47_412 ),
inference(forward_demodulation,[],[f394559,f112060]) ).
fof(f394579,plain,
( ! [X0] : hAPP(sF33,v_s____) = c_Groups_Oplus__class_Oplus(sF23,hAPP(hAPP(sF27,sF31),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),sF35)),sF35)
| ~ spl47_10
| spl47_41
| ~ spl47_412 ),
inference(forward_demodulation,[],[f394569,f350991]) ).
fof(f394588,plain,
( hAPP(sF33,v_s____) = c_Groups_Oplus__class_Oplus(sF23,sF31,sF35)
| ~ spl47_10
| spl47_41
| ~ spl47_412 ),
inference(forward_demodulation,[],[f394579,f5102]) ).
fof(f394598,plain,
( sF35 = hAPP(sF33,v_s____)
| ~ spl47_10
| spl47_41
| ~ spl47_412 ),
inference(forward_demodulation,[],[f394588,f16990]) ).
fof(f394608,plain,
( $false
| ~ spl47_10
| spl47_41
| ~ spl47_412
| spl47_556 ),
inference(forward_subsumption_resolution,[],[f394598,f85224]) ).
fof(f394609,plain,
( ~ spl47_10
| spl47_41
| ~ spl47_412
| spl47_556 ),
inference(avatar_contradiction_clause,[],[f394608]) ).
fof(f394616,plain,
( ! [X0] : hAPP(hAPP(sF27,sF35),X0) = hAPP(sF33,hAPP(hAPP(sF27,v_s____),X0))
| ~ spl47_556 ),
inference(superposition,[],[f5968,f85223]) ).
fof(f394635,plain,
( ! [X0] : hAPP(sF33,hAPP(hAPP(sF27,v_s____),X0)) = X0
| ~ spl47_556 ),
inference(forward_demodulation,[],[f394616,f5771]) ).
fof(f399640,plain,
( sF26 = hAPP(sF33,hAPP(sF28,sF44))
| ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(superposition,[],[f394635,f9019]) ).
fof(f399689,plain,
( sF26 = hAPP(sF28,hAPP(sF33,sF44))
| ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(forward_demodulation,[],[f399640,f6059]) ).
fof(f399726,plain,
( sF26 = hAPP(sF28,sF45)
| ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(forward_demodulation,[],[f399689,f7592]) ).
fof(f399743,plain,
( sF26 = sF46
| ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(forward_demodulation,[],[f399726,f4730]) ).
fof(f399757,plain,
( $false
| ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(forward_subsumption_resolution,[],[f399743,f4731]) ).
fof(f399758,plain,
( ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(avatar_contradiction_clause,[],[f399757]) ).
cnf(s7,plain,
( spl47_9
| spl47_10 ),
inference(sat_conversion,[],[f5158]) ).
cnf(s44,plain,
~ spl47_41,
inference(sat_conversion,[],[f5715]) ).
cnf(s139,plain,
~ spl47_61,
inference(sat_conversion,[],[f16243]) ).
cnf(s177,plain,
( ~ spl47_10
| ~ spl47_31
| spl47_41
| spl47_61 ),
inference(sat_conversion,[],[f23489]) ).
cnf(s528,plain,
( ~ spl47_10
| spl47_31
| spl47_41
| ~ spl47_411
| spl47_412 ),
inference(sat_conversion,[],[f70105]) ).
cnf(s4558,plain,
~ spl47_9,
inference(sat_conversion,[],[f247207]) ).
cnf(s6881,plain,
( ~ spl47_10
| spl47_41
| spl47_411 ),
inference(sat_conversion,[],[f379702]) ).
cnf(s7621,plain,
( ~ spl47_10
| spl47_41
| ~ spl47_412
| spl47_556 ),
inference(sat_conversion,[],[f394609]) ).
cnf(s7800,plain,
( ~ spl47_10
| spl47_41
| ~ spl47_556 ),
inference(sat_conversion,[],[f399758]) ).
cnf(s8002,plain,
spl47_10,
inference(rat,[],[s7,s4558]) ).
cnf(s8003,plain,
~ spl47_556,
inference(rat,[],[s7800,s44,s8002]) ).
cnf(s8004,plain,
~ spl47_412,
inference(rat,[],[s7621,s8003,s44,s8002]) ).
cnf(s8007,plain,
spl47_411,
inference(rat,[],[s6881,s44,s8002]) ).
cnf(s8072,plain,
spl47_31,
inference(rat,[],[s528,s8004,s8007,s44,s8002]) ).
cnf(s8075,plain,
$false,
inference(rat,[],[s177,s139,s44,s8072,s8002]) ).
fof(f399762,plain,
$false,
inference(avatar_sat_refutation,[],[s8075]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW273+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 13:27:21 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 12.63/2.50 % (1176377)Detected formulas, will run a generic FOF schedule.
% 12.63/2.50 % (1176491)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1218056420:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.63/2.50 % (1176488)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=762425621:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.63/2.50 % (1176489)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3682746013:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.63/2.50 % (1176486)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=3316879785:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.63/2.50 % (1176487)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3700915901:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.63/2.50 % (1176491)Instruction limit reached!
% 12.63/2.50 % (1176491)------------------------------
% 12.63/2.50 % (1176491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.50 % (1176491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.50 % (1176491)CaDiCaL version: 2.1.3
% 12.63/2.50 % (1176491)Termination reason: Instruction limit
% 12.63/2.50 % (1176491)Termination phase: Saturation
% 12.63/2.50 % (1176491)Time elapsed: 0.044 s
% 12.63/2.50 % (1176491)Peak memory usage: 91 MB
% 12.63/2.50 % (1176491)Instructions burned: 141 (million)
% 12.63/2.50 % (1176489)Refutation not found, incomplete strategy
% 12.63/2.50 % (1176489)------------------------------
% 12.63/2.50 % (1176489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.50 % (1176489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.50 % (1176489)CaDiCaL version: 2.1.3
% 12.63/2.50 % (1176489)Termination reason: Refutation not found, incomplete strategy
% 12.63/2.50 % (1176489)Time elapsed: 0.015 s
% 12.63/2.50 % (1176489)Peak memory usage: 90 MB
% 12.63/2.50 % (1176489)Instructions burned: 25 (million)
% 12.63/2.50 % (1176490)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=327738074:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.63/2.50 % (1176492)dis-21_1_sil=8000:lcm=predicate:random_seed=306226781:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.63/2.50 % (1176492)Instruction limit reached!
% 12.63/2.50 % (1176492)------------------------------
% 12.63/2.50 % (1176492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.50 % (1176492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.50 % (1176492)CaDiCaL version: 2.1.3
% 12.63/2.50 % (1176492)Termination reason: Instruction limit
% 12.63/2.50 % (1176492)Termination phase: Saturation
% 12.63/2.50 % (1176492)Time elapsed: 0.070 s
% 12.63/2.50 % (1176492)Peak memory usage: 91 MB
% 12.63/2.50 % (1176492)Instructions burned: 129 (million)
% 12.63/2.50 % (1176490)Instruction limit reached!
% 12.63/2.50 % (1176490)------------------------------
% 12.63/2.50 % (1176490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.50 % (1176490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.50 % (1176490)CaDiCaL version: 2.1.3
% 12.63/2.50 % (1176490)Termination reason: Instruction limit
% 12.63/2.50 % (1176490)Termination phase: Saturation
% 12.63/2.50 % (1176490)Time elapsed: 0.073 s
% 12.63/2.50 % (1176490)Peak memory usage: 90 MB
% 12.63/2.50 % (1176490)Instructions burned: 119 (million)
% 12.63/2.50 % (1176498)lrs+10_1_sil=8000:sp=occurrence:random_seed=3607819902:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.63/2.50 % (1176498)Instruction limit reached!
% 12.63/2.50 % (1176498)------------------------------
% 12.63/2.50 % (1176498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.63/2.50 % (1176498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.50 % (1176498)CaDiCaL version: 2.1.3
% 12.63/2.50 % (1176498)Termination reason: Instruction limit
% 12.63/2.50 % (1176498)Termination phase: Saturation
% 12.63/2.50 % (1176498)Time elapsed: 0.098 s
% 12.63/2.50 % (1176498)Peak memory usage: 92 MB
% 12.63/2.50 % (1176498)Instructions burned: 286 (million)
% 18.53/3.38 % (1176501)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2011867969:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.53/3.38 % (1176502)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3498685932:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.53/3.38 % (1176489)------------------------------
% 18.53/3.38 % (1176489)------------------------------
% 18.53/3.38 % (1176504)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1037510687:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 18.53/3.38 % (1176501)Instruction limit reached!
% 18.53/3.38 % (1176501)------------------------------
% 18.53/3.38 % (1176501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.38 % (1176501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.38 % (1176501)CaDiCaL version: 2.1.3
% 18.53/3.38 % (1176501)Termination reason: Instruction limit
% 18.53/3.38 % (1176501)Termination phase: Saturation
% 18.53/3.38 % (1176501)Time elapsed: 0.091 s
% 18.53/3.38 % (1176501)Peak memory usage: 91 MB
% 18.53/3.38 % (1176501)Instructions burned: 159 (million)
% 18.53/3.38 % (1176504)Instruction limit reached!
% 18.53/3.38 % (1176504)------------------------------
% 18.53/3.38 % (1176504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.38 % (1176504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.38 % (1176504)CaDiCaL version: 2.1.3
% 18.53/3.38 % (1176504)Termination reason: Instruction limit
% 18.53/3.38 % (1176504)Termination phase: Saturation
% 18.53/3.38 % (1176504)Time elapsed: 0.071 s
% 18.53/3.38 % (1176504)Peak memory usage: 94 MB
% 18.53/3.38 % (1176504)Instructions burned: 253 (million)
% 18.53/3.38 % (1176507)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=703693836:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.53/3.38 % (1176502)Instruction limit reached!
% 18.53/3.38 % (1176502)------------------------------
% 18.53/3.38 % (1176502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.38 % (1176502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.38 % (1176502)CaDiCaL version: 2.1.3
% 18.53/3.38 % (1176502)Termination reason: Instruction limit
% 18.53/3.38 % (1176502)Termination phase: Saturation
% 18.53/3.38 % (1176502)Time elapsed: 0.201 s
% 18.53/3.38 % (1176502)Peak memory usage: 93 MB
% 18.53/3.38 % (1176502)Instructions burned: 325 (million)
% 18.53/3.38 % (1176510)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3422745390:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.53/3.38 % (1176509)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3753060388:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 18.53/3.38 % (1176510)Instruction limit reached!
% 18.53/3.38 % (1176510)------------------------------
% 18.53/3.38 % (1176510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.38 % (1176510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.38 % (1176510)CaDiCaL version: 2.1.3
% 18.53/3.38 % (1176510)Termination reason: Instruction limit
% 18.53/3.38 % (1176510)Termination phase: Saturation
% 18.53/3.38 % (1176510)Time elapsed: 0.032 s
% 18.53/3.38 % (1176510)Peak memory usage: 90 MB
% 18.53/3.38 % (1176510)Instructions burned: 117 (million)
% 18.53/3.38 % (1176512)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2341392742:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 18.53/3.38 % (1176507)Instruction limit reached!
% 18.53/3.38 % (1176507)------------------------------
% 18.53/3.38 % (1176507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.38 % (1176507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.38 % (1176507)CaDiCaL version: 2.1.3
% 18.53/3.38 % (1176507)Termination reason: Instruction limit
% 18.53/3.38 % (1176507)Termination phase: Saturation
% 18.53/3.38 % (1176507)Time elapsed: 0.166 s
% 18.53/3.38 % (1176507)Peak memory usage: 91 MB
% 18.53/3.38 % (1176507)Instructions burned: 294 (million)
% 18.53/3.38 % (1176515)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=28145016:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 18.53/3.38 % (1176512)Refutation not found, incomplete strategy
% 18.53/3.38 % (1176512)------------------------------
% 18.53/3.38 % (1176512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176512)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176512)Termination reason: Refutation not found, incomplete strategy
% 27.18/4.55 % (1176512)Time elapsed: 0.057 s
% 27.18/4.55 % (1176512)Peak memory usage: 90 MB
% 27.18/4.55 % (1176512)Instructions burned: 112 (million)
% 27.18/4.55 % (1176515)Instruction limit reached!
% 27.18/4.55 % (1176515)------------------------------
% 27.18/4.55 % (1176515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176515)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176515)Termination reason: Instruction limit
% 27.18/4.55 % (1176515)Termination phase: Saturation
% 27.18/4.55 % (1176515)Time elapsed: 0.031 s
% 27.18/4.55 % (1176515)Peak memory usage: 90 MB
% 27.18/4.55 % (1176515)Instructions burned: 114 (million)
% 27.18/4.55 % (1176517)lrs+10_1_sil=8000:sp=occurrence:random_seed=567836375:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 27.18/4.55 % (1176519)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=381104466:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 27.18/4.55 % (1176519)Instruction limit reached!
% 27.18/4.55 % (1176519)------------------------------
% 27.18/4.55 % (1176519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176519)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176519)Termination reason: Instruction limit
% 27.18/4.55 % (1176519)Termination phase: Saturation
% 27.18/4.55 % (1176519)Time elapsed: 0.122 s
% 27.18/4.55 % (1176519)Peak memory usage: 93 MB
% 27.18/4.55 % (1176519)Instructions burned: 437 (million)
% 27.18/4.55 % (1176512)------------------------------
% 27.18/4.55 % (1176512)------------------------------
% 27.18/4.55 % (1176522)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2942304080:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 27.18/4.55 % (1176523)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2018402015:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 27.18/4.55 % (1176523)Instruction limit reached!
% 27.18/4.55 % (1176523)------------------------------
% 27.18/4.55 % (1176523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176523)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176523)Termination reason: Instruction limit
% 27.18/4.55 % (1176523)Termination phase: Saturation
% 27.18/4.55 % (1176523)Time elapsed: 0.073 s
% 27.18/4.55 % (1176523)Peak memory usage: 92 MB
% 27.18/4.55 % (1176523)Instructions burned: 134 (million)
% 27.18/4.55 % (1176526)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3281671723:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 27.18/4.55 % (1176517)Instruction limit reached!
% 27.18/4.55 % (1176517)------------------------------
% 27.18/4.55 % (1176517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176517)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176517)Termination reason: Instruction limit
% 27.18/4.55 % (1176517)Termination phase: Saturation
% 27.18/4.55 % (1176517)Time elapsed: 0.574 s
% 27.18/4.55 % (1176517)Peak memory usage: 98 MB
% 27.18/4.55 % (1176517)Instructions burned: 907 (million)
% 27.18/4.55 % (1176528)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3473827712:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 27.18/4.55 % (1176526)Instruction limit reached!
% 27.18/4.55 % (1176526)------------------------------
% 27.18/4.55 % (1176526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.18/4.55 % (1176526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.18/4.55 % (1176526)CaDiCaL version: 2.1.3
% 27.18/4.55 % (1176526)Termination reason: Instruction limit
% 27.18/4.55 % (1176526)Termination phase: Saturation
% 27.18/4.55 % (1176526)Time elapsed: 0.312 s
% 27.18/4.55 % (1176526)Peak memory usage: 98 MB
% 27.18/4.55 % (1176526)Instructions burned: 592 (million)
% 27.18/4.55 % (1176530)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=652840582:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 63.16/9.66 % (1176530)Instruction limit reached!
% 63.16/9.66 % (1176530)------------------------------
% 63.16/9.66 % (1176530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/9.66 % (1176530)CaDiCaL version: 2.1.3
% 63.16/9.66 % (1176530)Termination reason: Instruction limit
% 63.16/9.66 % (1176530)Termination phase: Saturation
% 63.16/9.66 % (1176530)Time elapsed: 0.062 s
% 63.16/9.66 % (1176530)Peak memory usage: 90 MB
% 63.16/9.66 % (1176530)Instructions burned: 125 (million)
% 63.16/9.66 % (1176532)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3939692867:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 63.16/9.66 % (1176532)Instruction limit reached!
% 63.16/9.66 % (1176532)------------------------------
% 63.16/9.66 % (1176532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/9.66 % (1176532)CaDiCaL version: 2.1.3
% 63.16/9.66 % (1176532)Termination reason: Instruction limit
% 63.16/9.66 % (1176532)Termination phase: Saturation
% 63.16/9.66 % (1176532)Time elapsed: 0.064 s
% 63.16/9.66 % (1176532)Peak memory usage: 90 MB
% 63.16/9.66 % (1176532)Instructions burned: 134 (million)
% 63.16/9.66 % (1176509)Instruction limit reached!
% 63.16/9.66 % (1176509)------------------------------
% 63.16/9.66 % (1176509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/9.66 % (1176509)CaDiCaL version: 2.1.3
% 63.16/9.66 % (1176509)Termination reason: Instruction limit
% 63.16/9.66 % (1176509)Termination phase: Saturation
% 63.16/9.66 % (1176509)Time elapsed: 1.458 s
% 63.16/9.66 % (1176509)Peak memory usage: 146 MB
% 63.16/9.66 % (1176509)Instructions burned: 2351 (million)
% 63.16/9.66 % (1176534)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2706172892:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 63.16/9.66 % (1176534)Refutation not found, incomplete strategy
% 63.16/9.66 % (1176534)------------------------------
% 63.16/9.66 % (1176534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/9.66 % (1176534)CaDiCaL version: 2.1.3
% 63.16/9.66 % (1176534)Termination reason: Refutation not found, incomplete strategy
% 63.16/9.66 % (1176534)Time elapsed: 0.009 s
% 63.16/9.66 % (1176534)Peak memory usage: 89 MB
% 63.16/9.66 % (1176534)Instructions burned: 14 (million)
% 63.16/9.66 % (1176535)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3520186251:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 63.16/9.66 % (1176534)------------------------------
% 63.16/9.66 % (1176534)------------------------------
% 63.16/9.66 % (1176535)Instruction limit reached!
% 63.16/9.66 % (1176535)------------------------------
% 63.16/9.66 % (1176535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/9.66 % (1176535)CaDiCaL version: 2.1.3
% 63.16/9.66 % (1176535)Termination reason: Instruction limit
% 63.16/9.66 % (1176535)Termination phase: Saturation
% 63.16/9.66 % (1176535)Time elapsed: 0.260 s
% 63.16/9.66 % (1176535)Peak memory usage: 92 MB
% 63.16/9.66 % (1176535)Instructions burned: 432 (million)
% 63.16/9.66 % (1176538)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3895385321:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 63.16/9.66 % (1176539)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2592299018:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 63.16/9.66 % (1176539)Instruction limit reached!
% 63.16/9.66 % (1176539)------------------------------
% 63.16/9.66 % (1176539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/9.66 % (1176539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176539)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176539)Termination reason: Instruction limit
% 93.12/13.85 % (1176539)Termination phase: Saturation
% 93.12/13.85 % (1176539)Time elapsed: 0.080 s
% 93.12/13.85 % (1176539)Peak memory usage: 92 MB
% 93.12/13.85 % (1176539)Instructions burned: 150 (million)
% 93.12/13.85 % (1176522)Instruction limit reached!
% 93.12/13.85 % (1176522)------------------------------
% 93.12/13.85 % (1176522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.12/13.85 % (1176522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176522)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176522)Termination reason: Instruction limit
% 93.12/13.85 % (1176522)Termination phase: Saturation
% 93.12/13.85 % (1176522)Time elapsed: 1.636 s
% 93.12/13.85 % (1176522)Peak memory usage: 160 MB
% 93.12/13.85 % (1176522)Instructions burned: 5204 (million)
% 93.12/13.85 % (1176542)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1663883423:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 93.12/13.85 % (1176543)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=234519691:i=667:av=off:fsr=off_2972 on theBenchmark for (2972ds/667Mi)
% 93.12/13.85 % (1176543)Refutation not found, incomplete strategy
% 93.12/13.85 % (1176543)------------------------------
% 93.12/13.85 % (1176543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.12/13.85 % (1176543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176543)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176543)Termination reason: Refutation not found, incomplete strategy
% 93.12/13.85 % (1176543)Time elapsed: 0.033 s
% 93.12/13.85 % (1176543)Peak memory usage: 91 MB
% 93.12/13.85 % (1176543)Instructions burned: 124 (million)
% 93.12/13.85 % (1176543)------------------------------
% 93.12/13.85 % (1176543)------------------------------
% 93.12/13.85 % (1176546)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2482379072:s2a=on:i=185:s2at=1.8:fdi=4_2969 on theBenchmark for (2969ds/185Mi)
% 93.12/13.85 % (1176546)Instruction limit reached!
% 93.12/13.85 % (1176546)------------------------------
% 93.12/13.85 % (1176546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.12/13.85 % (1176546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176546)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176546)Termination reason: Instruction limit
% 93.12/13.85 % (1176546)Termination phase: Saturation
% 93.12/13.85 % (1176546)Time elapsed: 0.053 s
% 93.12/13.85 % (1176546)Peak memory usage: 92 MB
% 93.12/13.85 % (1176546)Instructions burned: 186 (million)
% 93.12/13.85 % (1176548)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=131266159:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi)
% 93.12/13.85 % (1176548)Instruction limit reached!
% 93.12/13.85 % (1176548)------------------------------
% 93.12/13.85 % (1176548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.12/13.85 % (1176548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176548)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176548)Termination reason: Instruction limit
% 93.12/13.85 % (1176548)Termination phase: Saturation
% 93.12/13.85 % (1176548)Time elapsed: 0.065 s
% 93.12/13.85 % (1176548)Peak memory usage: 92 MB
% 93.12/13.85 % (1176548)Instructions burned: 195 (million)
% 93.12/13.85 % (1176550)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1713020396:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2966 on theBenchmark for (2966ds/4850Mi)
% 93.12/13.85 % (1176550)Refutation not found, incomplete strategy
% 93.12/13.85 % (1176550)------------------------------
% 93.12/13.85 % (1176550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.12/13.85 % (1176550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.12/13.85 % (1176550)CaDiCaL version: 2.1.3
% 93.12/13.85 % (1176550)Termination reason: Refutation not found, incomplete strategy
% 93.12/13.85 % (1176550)Time elapsed: 0.047 s
% 93.12/13.85 % (1176550)Peak memory usage: 90 MB
% 93.12/13.85 % (1176550)Instructions burned: 92 (million)
% 93.12/13.85 % (1176550)------------------------------
% 93.12/13.85 % (1176550)------------------------------
% 93.12/13.85 % (1176552)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3093982015:i=12111:sd=1:ss=included_2962 on theBenchmark for (2962ds/12111Mi)
% 121.62/17.89 % (1176538)Instruction limit reached!
% 121.62/17.89 % (1176538)------------------------------
% 121.62/17.89 % (1176538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176538)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176538)Termination reason: Instruction limit
% 121.62/17.89 % (1176538)Termination phase: Saturation
% 121.62/17.89 % (1176538)Time elapsed: 3.827 s
% 121.62/17.89 % (1176538)Peak memory usage: 181 MB
% 121.62/17.89 % (1176538)Instructions burned: 6060 (million)
% 121.62/17.89 % (1176554)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4151401032:i=319:kws=precedence:fsr=off_2935 on theBenchmark for (2935ds/319Mi)
% 121.62/17.89 % (1176554)Instruction limit reached!
% 121.62/17.89 % (1176554)------------------------------
% 121.62/17.89 % (1176554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176554)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176554)Termination reason: Instruction limit
% 121.62/17.89 % (1176554)Termination phase: Saturation
% 121.62/17.89 % (1176554)Time elapsed: 0.183 s
% 121.62/17.89 % (1176554)Peak memory usage: 94 MB
% 121.62/17.89 % (1176554)Instructions burned: 319 (million)
% 121.62/17.89 % (1176556)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2919058348:i=2064:ep=RST_2932 on theBenchmark for (2932ds/2064Mi)
% 121.62/17.89 % (1176552)Instruction limit reached!
% 121.62/17.89 % (1176552)------------------------------
% 121.62/17.89 % (1176552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176552)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176552)Termination reason: Instruction limit
% 121.62/17.89 % (1176552)Termination phase: Saturation
% 121.62/17.89 % (1176552)Time elapsed: 3.884 s
% 121.62/17.89 % (1176552)Peak memory usage: 208 MB
% 121.62/17.89 % (1176552)Instructions burned: 12111 (million)
% 121.62/17.89 % (1176558)dis-1011_128_sil=32000:random_seed=1435599360:i=3706:ep=RST:av=off_2922 on theBenchmark for (2922ds/3706Mi)
% 121.62/17.89 % (1176556)Instruction limit reached!
% 121.62/17.89 % (1176556)------------------------------
% 121.62/17.89 % (1176556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176556)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176556)Termination reason: Instruction limit
% 121.62/17.89 % (1176556)Termination phase: Saturation
% 121.62/17.89 % (1176556)Time elapsed: 1.161 s
% 121.62/17.89 % (1176556)Peak memory usage: 105 MB
% 121.62/17.89 % (1176556)Instructions burned: 2065 (million)
% 121.62/17.89 % (1176560)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=611039570:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2919 on theBenchmark for (2919ds/757Mi)
% 121.62/17.89 % (1176560)Instruction limit reached!
% 121.62/17.89 % (1176560)------------------------------
% 121.62/17.89 % (1176560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176560)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176560)Termination reason: Instruction limit
% 121.62/17.89 % (1176560)Termination phase: Saturation
% 121.62/17.89 % (1176560)Time elapsed: 0.451 s
% 121.62/17.89 % (1176560)Peak memory usage: 98 MB
% 121.62/17.89 % (1176560)Instructions burned: 757 (million)
% 121.62/17.89 % (1176562)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1517849339:i=13913:ss=axioms:sgt=8_2913 on theBenchmark for (2913ds/13913Mi)
% 121.62/17.89 % (1176558)Instruction limit reached!
% 121.62/17.89 % (1176558)------------------------------
% 121.62/17.89 % (1176558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.62/17.89 % (1176558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.62/17.89 % (1176558)CaDiCaL version: 2.1.3
% 121.62/17.89 % (1176558)Termination reason: Instruction limit
% 121.62/17.89 % (1176558)Termination phase: Saturation
% 121.62/17.89 % (1176558)Time elapsed: 1.039 s
% 121.62/17.89 % (1176558)Peak memory usage: 125 MB
% 121.62/17.89 % (1176558)Instructions burned: 3707 (million)
% 121.62/17.89 % (1176564)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=400697939:i=9925:aac=none_2910 on theBenchmark for (2910ds/9925Mi)
% 134.70/19.85 % (1176528)Instruction limit reached!
% 134.70/19.85 % (1176528)------------------------------
% 134.70/19.85 % (1176528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176528)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176528)Termination reason: Instruction limit
% 134.70/19.85 % (1176528)Termination phase: Saturation
% 134.70/19.85 % (1176528)Time elapsed: 8.085 s
% 134.70/19.85 % (1176528)Peak memory usage: 230 MB
% 134.70/19.85 % (1176528)Instructions burned: 13193 (million)
% 134.70/19.85 % (1176566)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2468863370:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/2479Mi)
% 134.70/19.85 % (1176566)Refutation not found, incomplete strategy
% 134.70/19.85 % (1176566)------------------------------
% 134.70/19.85 % (1176566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176566)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176566)Termination reason: Refutation not found, incomplete strategy
% 134.70/19.85 % (1176566)Time elapsed: 0.157 s
% 134.70/19.85 % (1176566)Peak memory usage: 91 MB
% 134.70/19.85 % (1176566)Instructions burned: 301 (million)
% 134.70/19.85 % (1176566)------------------------------
% 134.70/19.85 % (1176566)------------------------------
% 134.70/19.85 % (1176568)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3101902403:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2897 on theBenchmark for (2897ds/440Mi)
% 134.70/19.85 % (1176568)Instruction limit reached!
% 134.70/19.85 % (1176568)------------------------------
% 134.70/19.85 % (1176568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176568)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176568)Termination reason: Instruction limit
% 134.70/19.85 % (1176568)Termination phase: Saturation
% 134.70/19.85 % (1176568)Time elapsed: 0.238 s
% 134.70/19.85 % (1176568)Peak memory usage: 94 MB
% 134.70/19.85 % (1176568)Instructions burned: 441 (million)
% 134.70/19.85 % (1176570)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2706968425:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2894 on theBenchmark for (2894ds/11145Mi)
% 134.70/19.85 % (1176542)Instruction limit reached!
% 134.70/19.85 % (1176542)------------------------------
% 134.70/19.85 % (1176542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176542)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176542)Termination reason: Instruction limit
% 134.70/19.85 % (1176542)Termination phase: Saturation
% 134.70/19.85 % (1176542)Time elapsed: 8.502 s
% 134.70/19.85 % (1176542)Peak memory usage: 205 MB
% 134.70/19.85 % (1176542)Instructions burned: 14157 (million)
% 134.70/19.85 % (1176572)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4028909428:cts=off:i=3034:av=off:er=known:fsd=on_2886 on theBenchmark for (2886ds/3034Mi)
% 134.70/19.85 % (1176562)Instruction limit reached!
% 134.70/19.85 % (1176562)------------------------------
% 134.70/19.85 % (1176562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176562)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176562)Termination reason: Instruction limit
% 134.70/19.85 % (1176562)Termination phase: Saturation
% 134.70/19.85 % (1176562)Time elapsed: 4.206 s
% 134.70/19.85 % (1176562)Peak memory usage: 198 MB
% 134.70/19.85 % (1176562)Instructions burned: 13913 (million)
% 134.70/19.85 % (1176574)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2382975167:st=2:s2a=on:i=524:s2at=2:ss=axioms_2869 on theBenchmark for (2869ds/524Mi)
% 134.70/19.85 % (1176572)Instruction limit reached!
% 134.70/19.85 % (1176572)------------------------------
% 134.70/19.85 % (1176572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.70/19.85 % (1176572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.70/19.85 % (1176572)CaDiCaL version: 2.1.3
% 134.70/19.85 % (1176572)Termination reason: Instruction limit
% 156.37/22.84 % (1176572)Termination phase: Saturation
% 156.37/22.84 % (1176572)Time elapsed: 1.702 s
% 156.37/22.84 % (1176572)Peak memory usage: 145 MB
% 156.37/22.84 % (1176572)Instructions burned: 3034 (million)
% 156.37/22.84 % (1176574)Instruction limit reached!
% 156.37/22.84 % (1176574)------------------------------
% 156.37/22.84 % (1176574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176574)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176574)Termination reason: Instruction limit
% 156.37/22.84 % (1176574)Termination phase: Saturation
% 156.37/22.84 % (1176574)Time elapsed: 0.144 s
% 156.37/22.84 % (1176574)Peak memory usage: 97 MB
% 156.37/22.84 % (1176574)Instructions burned: 529 (million)
% 156.37/22.84 % (1176576)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3911820583:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2868 on theBenchmark for (2868ds/1016Mi)
% 156.37/22.84 % (1176577)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3456000322:i=14123:bd=preordered:ins=4_2867 on theBenchmark for (2867ds/14123Mi)
% 156.37/22.84 % (1176576)Instruction limit reached!
% 156.37/22.84 % (1176576)------------------------------
% 156.37/22.84 % (1176576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176576)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176576)Termination reason: Instruction limit
% 156.37/22.84 % (1176576)Termination phase: Saturation
% 156.37/22.84 % (1176576)Time elapsed: 0.509 s
% 156.37/22.84 % (1176576)Peak memory usage: 100 MB
% 156.37/22.84 % (1176576)Instructions burned: 1017 (million)
% 156.37/22.84 % (1176564)Instruction limit reached!
% 156.37/22.84 % (1176564)------------------------------
% 156.37/22.84 % (1176564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176564)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176564)Termination reason: Instruction limit
% 156.37/22.84 % (1176564)Termination phase: Saturation
% 156.37/22.84 % (1176564)Time elapsed: 4.851 s
% 156.37/22.84 % (1176564)Peak memory usage: 166 MB
% 156.37/22.84 % (1176564)Instructions burned: 9926 (million)
% 156.37/22.84 % (1176582)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=879934710:i=5781:kws=precedence:bd=all:rawr=on_2861 on theBenchmark for (2861ds/5781Mi)
% 156.37/22.84 % (1176583)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2197305230:i=2448:gtgl=5:bd=preordered:gtg=all_2861 on theBenchmark for (2861ds/2448Mi)
% 156.37/22.84 % (1176583)Instruction limit reached!
% 156.37/22.84 % (1176583)------------------------------
% 156.37/22.84 % (1176583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176583)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176583)Termination reason: Instruction limit
% 156.37/22.84 % (1176583)Termination phase: Saturation
% 156.37/22.84 % (1176583)Time elapsed: 1.392 s
% 156.37/22.84 % (1176583)Peak memory usage: 148 MB
% 156.37/22.84 % (1176583)Instructions burned: 2449 (million)
% 156.37/22.84 % (1176646)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3452131907:i=3223:kws=precedence:fgj=on:av=off_2846 on theBenchmark for (2846ds/3223Mi)
% 156.37/22.84 % (1176570)Instruction limit reached!
% 156.37/22.84 % (1176570)------------------------------
% 156.37/22.84 % (1176570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176570)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176570)Termination reason: Instruction limit
% 156.37/22.84 % (1176570)Termination phase: Saturation
% 156.37/22.84 % (1176570)Time elapsed: 6.437 s
% 156.37/22.84 % (1176570)Peak memory usage: 214 MB
% 156.37/22.84 % (1176570)Instructions burned: 11146 (million)
% 156.37/22.84 % (1176582)Instruction limit reached!
% 156.37/22.84 % (1176582)------------------------------
% 156.37/22.84 % (1176582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.37/22.84 % (1176582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.37/22.84 % (1176582)CaDiCaL version: 2.1.3
% 156.37/22.84 % (1176582)Termination reason: Instruction limit
% 151.52/29.42 % (1176582)Termination phase: Saturation
% 151.52/29.42 % (1176582)Time elapsed: 3.260 s
% 151.52/29.42 % (1176582)Peak memory usage: 126 MB
% 151.52/29.42 % (1176582)Instructions burned: 5782 (million)
% 151.52/29.42 % (1176649)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1227561961:st=5.6:i=2033:sd=3:ss=axioms_2828 on theBenchmark for (2828ds/2033Mi)
% 151.52/29.42 % (1176650)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3676173320:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2827 on theBenchmark for (2827ds/2055Mi)
% 151.52/29.42 % (1176646)Instruction limit reached!
% 151.52/29.42 % (1176646)------------------------------
% 151.52/29.42 % (1176646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176646)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176646)Termination reason: Instruction limit
% 151.52/29.42 % (1176646)Termination phase: Saturation
% 151.52/29.42 % (1176646)Time elapsed: 2.038 s
% 151.52/29.42 % (1176646)Peak memory usage: 152 MB
% 151.52/29.42 % (1176646)Instructions burned: 3223 (million)
% 151.52/29.42 % (1176577)Instruction limit reached!
% 151.52/29.42 % (1176577)------------------------------
% 151.52/29.42 % (1176577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176577)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176577)Termination reason: Instruction limit
% 151.52/29.42 % (1176577)Termination phase: Saturation
% 151.52/29.42 % (1176577)Time elapsed: 4.272 s
% 151.52/29.42 % (1176577)Peak memory usage: 189 MB
% 151.52/29.42 % (1176577)Instructions burned: 14123 (million)
% 151.52/29.42 % (1176654)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1044008051:i=4835:sd=13:ss=axioms:sgt=23_2823 on theBenchmark for (2823ds/4835Mi)
% 151.52/29.42 % (1176653)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1891096034:i=21611:sd=3:ss=axioms_2824 on theBenchmark for (2824ds/21611Mi)
% 151.52/29.42 % (1176649)Instruction limit reached!
% 151.52/29.42 % (1176649)------------------------------
% 151.52/29.42 % (1176649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176649)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176649)Termination reason: Instruction limit
% 151.52/29.42 % (1176649)Termination phase: Saturation
% 151.52/29.42 % (1176649)Time elapsed: 1.274 s
% 151.52/29.42 % (1176649)Peak memory usage: 139 MB
% 151.52/29.42 % (1176649)Instructions burned: 2034 (million)
% 151.52/29.42 % (1176650)Instruction limit reached!
% 151.52/29.42 % (1176650)------------------------------
% 151.52/29.42 % (1176650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176650)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176650)Termination reason: Instruction limit
% 151.52/29.42 % (1176650)Termination phase: Saturation
% 151.52/29.42 % (1176650)Time elapsed: 1.228 s
% 151.52/29.42 % (1176650)Peak memory usage: 138 MB
% 151.52/29.42 % (1176650)Instructions burned: 2055 (million)
% 151.52/29.42 % (1176657)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=772524879:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2814 on theBenchmark for (2814ds/797Mi)
% 151.52/29.42 % (1176658)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1469381912:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2814 on theBenchmark for (2814ds/2326Mi)
% 151.52/29.42 % (1176654)Instruction limit reached!
% 151.52/29.42 % (1176654)------------------------------
% 151.52/29.42 % (1176654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176654)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176654)Termination reason: Instruction limit
% 151.52/29.42 % (1176654)Termination phase: Saturation
% 151.52/29.42 % (1176654)Time elapsed: 1.392 s
% 151.52/29.42 % (1176654)Peak memory usage: 115 MB
% 151.52/29.42 % (1176654)Instructions burned: 4836 (million)
% 151.52/29.42 % (1176657)Instruction limit reached!
% 151.52/29.42 % (1176657)------------------------------
% 151.52/29.42 % (1176657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176657)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176657)Termination reason: Instruction limit
% 151.52/29.42 % (1176657)Termination phase: Saturation
% 151.52/29.42 % (1176657)Time elapsed: 0.466 s
% 151.52/29.42 % (1176657)Peak memory usage: 95 MB
% 151.52/29.42 % (1176657)Instructions burned: 798 (million)
% 151.52/29.42 % (1176661)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3404835353:i=6038:nm=6_2809 on theBenchmark for (2809ds/6038Mi)
% 151.52/29.42 % (1176663)lrs+10_1_sil=32000:sp=occurrence:random_seed=1976293816:st=2:i=33334:sd=3:ss=included:sgt=32_2808 on theBenchmark for (2808ds/33334Mi)
% 151.52/29.42 % (1176658)Instruction limit reached!
% 151.52/29.42 % (1176658)------------------------------
% 151.52/29.42 % (1176658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176658)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176658)Termination reason: Instruction limit
% 151.52/29.42 % (1176658)Termination phase: Saturation
% 151.52/29.42 % (1176658)Time elapsed: 1.395 s
% 151.52/29.42 % (1176658)Peak memory usage: 99 MB
% 151.52/29.42 % (1176658)Instructions burned: 2327 (million)
% 151.52/29.42 % (1176665)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2283170114:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2798 on theBenchmark for (2798ds/1008Mi)
% 151.52/29.42 % (1176661)Instruction limit reached!
% 151.52/29.42 % (1176661)------------------------------
% 151.52/29.42 % (1176661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176661)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176661)Termination reason: Instruction limit
% 151.52/29.42 % (1176661)Termination phase: Saturation
% 151.52/29.42 % (1176661)Time elapsed: 1.523 s
% 151.52/29.42 % (1176661)Peak memory usage: 155 MB
% 151.52/29.42 % (1176661)Instructions burned: 6041 (million)
% 151.52/29.42 % (1176665)Instruction limit reached!
% 151.52/29.42 % (1176665)------------------------------
% 151.52/29.42 % (1176665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176665)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176665)Termination reason: Instruction limit
% 151.52/29.42 % (1176665)Termination phase: Saturation
% 151.52/29.42 % (1176665)Time elapsed: 0.521 s
% 151.52/29.42 % (1176665)Peak memory usage: 97 MB
% 151.52/29.42 % (1176665)Instructions burned: 1010 (million)
% 151.52/29.42 % (1176667)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=860666774:i=8327:s2at=5:bd=preordered_2792 on theBenchmark for (2792ds/8327Mi)
% 151.52/29.42 % (1176668)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3930633463:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2792 on theBenchmark for (2792ds/1083Mi)
% 151.52/29.42 % (1176668)Instruction limit reached!
% 151.52/29.42 % (1176668)------------------------------
% 151.52/29.42 % (1176668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176668)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176668)Termination reason: Instruction limit
% 151.52/29.42 % (1176668)Termination phase: Saturation
% 151.52/29.42 % (1176668)Time elapsed: 0.479 s
% 151.52/29.42 % (1176668)Peak memory usage: 98 MB
% 151.52/29.42 % (1176668)Instructions burned: 1084 (million)
% 151.52/29.42 % (1176671)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=242663061:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2785 on theBenchmark for (2785ds/1084Mi)
% 151.52/29.42 % (1176671)Instruction limit reached!
% 151.52/29.42 % (1176671)------------------------------
% 151.52/29.42 % (1176671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176671)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176671)Termination reason: Instruction limit
% 151.52/29.42 % (1176671)Termination phase: Saturation
% 151.52/29.42 % (1176671)Time elapsed: 0.634 s
% 151.52/29.42 % (1176671)Peak memory usage: 98 MB
% 151.52/29.42 % (1176671)Instructions burned: 1085 (million)
% 151.52/29.42 % (1176673)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2888312210:i=6995:s2at=5:gtg=all_2778 on theBenchmark for (2778ds/6995Mi)
% 151.52/29.42 % (1176667)Instruction limit reached!
% 151.52/29.42 % (1176667)------------------------------
% 151.52/29.42 % (1176667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176667)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176667)Termination reason: Instruction limit
% 151.52/29.42 % (1176667)Termination phase: Saturation
% 151.52/29.42 % (1176667)Time elapsed: 2.893 s
% 151.52/29.42 % (1176667)Peak memory usage: 187 MB
% 151.52/29.42 % (1176667)Instructions burned: 8329 (million)
% 151.52/29.42 % (1176675)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2192570938:st=2:i=6225:sd=15:ss=axioms_2762 on theBenchmark for (2762ds/6225Mi)
% 151.52/29.42 % (1176675)Instruction limit reached!
% 151.52/29.42 % (1176675)------------------------------
% 151.52/29.42 % (1176675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176675)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176675)Termination reason: Instruction limit
% 151.52/29.42 % (1176675)Termination phase: Saturation
% 151.52/29.42 % (1176675)Time elapsed: 1.520 s
% 151.52/29.42 % (1176675)Peak memory usage: 137 MB
% 151.52/29.42 % (1176675)Instructions burned: 6229 (million)
% 151.52/29.42 % (1176677)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1530491676:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2746 on theBenchmark for (2746ds/3372Mi)
% 151.52/29.42 % (1176673)Instruction limit reached!
% 151.52/29.42 % (1176673)------------------------------
% 151.52/29.42 % (1176673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176673)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176673)Termination reason: Instruction limit
% 151.52/29.42 % (1176673)Termination phase: Saturation
% 151.52/29.42 % (1176673)Time elapsed: 4.158 s
% 151.52/29.42 % (1176673)Peak memory usage: 185 MB
% 151.52/29.42 % (1176673)Instructions burned: 6995 (million)
% 151.52/29.42 % (1176677)Instruction limit reached!
% 151.52/29.42 % (1176677)------------------------------
% 151.52/29.42 % (1176677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.52/29.42 % (1176677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.52/29.42 % (1176677)CaDiCaL version: 2.1.3
% 151.52/29.42 % (1176677)Termination reason: Instruction limit
% 151.52/29.42 % (1176677)Termination phase: Saturation
% 151.52/29.42 % (1176677)Time elapsed: 1.088 s
% 151.52/29.42 % (1176677)Peak memory usage: 149 MB
% 151.52/29.42 % (1176677)Instructions burned: 3374 (million)
% 151.52/29.42 % (1176679)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1414945827:st=2.3:i=26457:sd=10:ss=included:sgt=8_2735 on theBenchmark for (2735ds/26457Mi)
% 151.52/29.42 % (1176680)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=3487126967:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2734 on theBenchmark for (2734ds/13494Mi)
% 151.52/29.42 % (1176486)First to succeed.
% 151.52/29.42 % (1176680)Also succeeded, but the first one will report.
% 151.52/29.42 % (1176486)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1176377"
% 151.52/29.42 % (1176683)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=3968157102:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2714 on theBenchmark for (2714ds/2503Mi)
% 151.52/29.42 % (1176486)Refutation found. Thanks to Tanya!
% 151.52/29.42 % SZS status Theorem for theBenchmark
% 151.52/29.42 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/29.61 % (1176486)------------------------------
% 0.21/29.61 % (1176486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/29.61 % (1176486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/29.61 % (1176486)CaDiCaL version: 2.1.3
% 0.21/29.61 % (1176486)Termination reason: Refutation
% 0.21/29.61 % (1176486)Time elapsed: 28.192 s
% 0.21/29.61 % (1176486)Peak memory usage: 517 MB
% 0.21/29.61 % (1176486)Instructions burned: 47065 (million)
% 0.21/29.61 % (1176486)------------------------------
% 0.21/29.61 % (1176486)------------------------------
% 0.21/29.61 % (1176377)Success in time 28.746 s
% 0.21/29.61 % Vampire exiting
%------------------------------------------------------------------------------