%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW286+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:01 PM UTC 2026
% Result : Theorem 18.95s 3.47s
% Output : Refutation 20.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 41
% Syntax : Number of formulae : 229 ( 151 unt; 12 def)
% Number of atoms : 352 ( 265 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 209 ( 86 ~; 84 |; 11 &)
% ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 18 con; 0-3 aty)
% Number of variables : 311 ( 309 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ! [X2] : hAPP(X1,X2) = hAPP(X0,X2)
=> X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ext) ).
fof(f3,axiom,
v_k____ != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_k_I2_J) ).
fof(f4,axiom,
v_p = 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_k_I1_J) ).
fof(f5,axiom,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_dp) ).
fof(f7,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(f9,axiom,
! [X0,X1,X2] :
( class_Groups_Ozero(X2)
=> ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pCons__eq__0__iff) ).
fof(f44,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(f51,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Odivision__ring(X3)
=> ( X2 != c_Groups_Ozero__class_Ozero(X3)
=> ( X1 = c_Rings_Oinverse__class_Odivide(X3,X0,X2)
<=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) = X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_nonzero__eq__divide__eq) ).
fof(f52,axiom,
~ ! [X0] :
( v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))
=> X0 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096_B_Bthesis_O_A_I_B_Bk_O_A_091_124_Ap_A_061_A_091_058k_058_093_059_Ak_A_126_061_A0_A_124_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) ).
fof(f53,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(f60,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(f63,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(f66,axiom,
! [X0,X1,X2] :
( ( class_Int_Oring__char__0(X2)
& class_Rings_Oidom(X2) )
=> ( c_Polynomial_Opoly(X2,X1) = c_Polynomial_Opoly(X2,X0)
<=> X1 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__eq__iff) ).
fof(f84,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(f88,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(f92,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(f253,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J) ).
fof(f355,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Opcompose(X3,X2,X1)),X0) = hAPP(c_Polynomial_Opoly(X3,X2),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__pcompose) ).
fof(f364,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),c_Polynomial_OpCons(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X1,X2),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mult__pCons__right) ).
fof(f450,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Osmult(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__smult) ).
fof(f477,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X0),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mult__pCons__left) ).
fof(f1095,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(f1096,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(f1098,axiom,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Odivision__ring) ).
fof(f1109,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Int_Oring__char__0) ).
fof(f1114,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ozero) ).
fof(f1116,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oidom) ).
fof(f1142,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(f1170,conjecture,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),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)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1171,negated_conjecture,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),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)))),
inference(negated_conjecture,[status(cth)],[f1170]) ).
fof(f1173,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),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)))),
inference(flattening,[],[f1171]) ).
fof(f1214,plain,
! [X0,X1] :
( X1 = X0
| ? [X2] : hAPP(X1,X2) != hAPP(X0,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f1216,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,[],[f7]) ).
fof(f1218,plain,
! [X0,X1,X2] :
( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) ) )
| ~ class_Groups_Ozero(X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f1261,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,[],[f44]) ).
fof(f1274,plain,
! [X0,X1,X2,X3] :
( ( X1 = c_Rings_Oinverse__class_Odivide(X3,X0,X2)
<=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) = X0 )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(ennf_transformation,[],[f51]) ).
fof(f1275,plain,
! [X0,X1,X2,X3] :
( ( X1 = c_Rings_Oinverse__class_Odivide(X3,X0,X2)
<=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) = X0 )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(flattening,[],[f1274]) ).
fof(f1276,plain,
? [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != X0
& v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
inference(ennf_transformation,[],[f52]) ).
fof(f1277,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,[],[f53]) ).
fof(f1283,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,[],[f60]) ).
fof(f1286,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,[],[f63]) ).
fof(f1289,plain,
! [X0,X1,X2] :
( ( c_Polynomial_Opoly(X2,X1) = c_Polynomial_Opoly(X2,X0)
<=> X1 = X0 )
| ~ class_Int_Oring__char__0(X2)
| ~ class_Rings_Oidom(X2) ),
inference(ennf_transformation,[],[f66]) ).
fof(f1290,plain,
! [X0,X1,X2] :
( ( c_Polynomial_Opoly(X2,X1) = c_Polynomial_Opoly(X2,X0)
<=> X1 = X0 )
| ~ class_Int_Oring__char__0(X2)
| ~ class_Rings_Oidom(X2) ),
inference(flattening,[],[f1289]) ).
fof(f1318,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,[],[f84]) ).
fof(f1321,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,[],[f88]) ).
fof(f1325,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,[],[f92]) ).
fof(f1499,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f253]) ).
fof(f1584,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Opcompose(X3,X2,X1)),X0) = hAPP(c_Polynomial_Opoly(X3,X2),hAPP(c_Polynomial_Opoly(X3,X1),X0))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f355]) ).
fof(f1594,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),c_Polynomial_OpCons(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X1,X2),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X0)))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f364]) ).
fof(f1648,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Osmult(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(c_Polynomial_Opoly(X3,X1),X0))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f450]) ).
fof(f1684,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X0),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X1),X0)))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f477]) ).
fof(f2283,plain,
! [X0] :
( class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(ennf_transformation,[],[f1142]) ).
fof(f2318,plain,
! [X0,X1] :
( X1 = X0
| hAPP(X1,sK5(X0,X1)) != hAPP(X0,sK5(X0,X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f1214]) ).
fof(f2319,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Groups_Ozero__class_Ozero(X2) != X1
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0 )
& ( ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_OpCons(X2,X1,X0) ) )
| ~ class_Groups_Ozero(X2) ),
inference(nnf_transformation,[],[f1218]) ).
fof(f2320,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Groups_Ozero__class_Ozero(X2) != X1
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0 )
& ( ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_OpCons(X2,X1,X0) ) )
| ~ class_Groups_Ozero(X2) ),
inference(flattening,[],[f2319]) ).
fof(f2334,plain,
! [X0,X1,X2,X3] :
( ( ( X1 = c_Rings_Oinverse__class_Odivide(X3,X0,X2)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) != X0 )
& ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) = X0
| c_Rings_Oinverse__class_Odivide(X3,X0,X2) != X1 ) )
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(nnf_transformation,[],[f1275]) ).
fof(f2335,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK6
& v_p = 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)],[f1276]) ).
fof(f2340,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_Opoly(X2,X1) = c_Polynomial_Opoly(X2,X0)
| X0 != X1 )
& ( X1 = X0
| c_Polynomial_Opoly(X2,X1) != c_Polynomial_Opoly(X2,X0) ) )
| ~ class_Int_Oring__char__0(X2)
| ~ class_Rings_Oidom(X2) ),
inference(nnf_transformation,[],[f1290]) ).
fof(f2612,plain,
! [X0,X1] :
( hAPP(X1,sK5(X0,X1)) != hAPP(X0,sK5(X0,X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f2318]) ).
fof(f2614,plain,
v_k____ != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f3]) ).
fof(f2615,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cnf_transformation,[],[f4]) ).
fof(f2616,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[],[f5]) ).
fof(f2618,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,[],[f1216]) ).
fof(f2622,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = c_Polynomial_OpCons(X2,X1,X0)
| c_Groups_Ozero__class_Ozero(X2) != X1
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0
| ~ class_Groups_Ozero(X2) ),
inference(cnf_transformation,[],[f2320]) ).
fof(f2676,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,[],[f1261]) ).
fof(f2685,plain,
! [X2,X3,X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X1),X2) = X0
| c_Rings_Oinverse__class_Odivide(X3,X0,X2) != X1
| c_Groups_Ozero__class_Ozero(X3) = X2
| ~ class_Rings_Odivision__ring(X3) ),
inference(cnf_transformation,[],[f2334]) ).
fof(f2687,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cnf_transformation,[],[f2335]) ).
fof(f2689,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oone__class_Oone(X1) = hAPP(hAPP(c_Power_Opower__class_Opower(X1),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
inference(cnf_transformation,[],[f1277]) ).
fof(f2701,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,[],[f1283]) ).
fof(f2704,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,[],[f1286]) ).
fof(f2707,plain,
! [X2,X0,X1] :
( c_Polynomial_Opoly(X2,X1) != c_Polynomial_Opoly(X2,X0)
| X0 = X1
| ~ class_Int_Oring__char__0(X2)
| ~ class_Rings_Oidom(X2) ),
inference(cnf_transformation,[],[f2340]) ).
fof(f2731,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,[],[f1318]) ).
fof(f2736,plain,
! [X2,X0,X1] :
( ~ 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) ),
inference(cnf_transformation,[],[f1321]) ).
fof(f2740,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,[],[f1325]) ).
fof(f2970,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
inference(cnf_transformation,[],[f1499]) ).
fof(f3121,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Opcompose(X3,X2,X1)),X0) = hAPP(c_Polynomial_Opoly(X3,X2),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
inference(cnf_transformation,[],[f1584]) ).
fof(f3132,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),c_Polynomial_OpCons(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X1,X2),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X2),X0))) ),
inference(cnf_transformation,[],[f1594]) ).
fof(f3227,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Osmult(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
inference(cnf_transformation,[],[f1648]) ).
fof(f3268,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X0),c_Polynomial_OpCons(X3,c_Groups_Ozero__class_Ozero(X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3)),X1),X0))) ),
inference(cnf_transformation,[],[f1684]) ).
fof(f4049,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1095]) ).
fof(f4050,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1096]) ).
fof(f4052,plain,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1098]) ).
fof(f4063,plain,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1109]) ).
fof(f4068,plain,
class_Groups_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1114]) ).
fof(f4070,plain,
class_Rings_Oidom(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1116]) ).
fof(f4096,plain,
! [X0] :
( class_Rings_Ocomm__semiring__1(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[],[f2283]) ).
fof(f4124,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),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)))),
inference(cnf_transformation,[],[f1173]) ).
fof(f4245,plain,
! [X2,X0] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = c_Polynomial_OpCons(X2,c_Groups_Ozero__class_Ozero(X2),X0)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0
| ~ class_Groups_Ozero(X2) ),
inference(equality_resolution,[],[f2622]) ).
fof(f4246,plain,
! [X2] :
( ~ class_Groups_Ozero(X2)
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) = c_Polynomial_OpCons(X2,c_Groups_Ozero__class_Ozero(X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))) ),
inference(equality_resolution,[],[f4245]) ).
fof(f4279,plain,
! [X2,X3,X0] :
( ~ 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,X0,X2)),X2) = X0 ),
inference(equality_resolution,[],[f2685]) ).
fof(f4488,definition,
sF28 = tc_Polynomial_Opoly(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f4489,plain,
tc_Polynomial_Opoly(tc_Complex_Ocomplex) = sF28,
inference(reorient_equations,[],[f4488]) ).
fof(f4490,definition,
sF29 = c_Power_Opower__class_Opower(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f4491,plain,
c_Power_Opower__class_Opower(sF28) = sF29,
inference(reorient_equations,[],[f4490]) ).
fof(f4492,definition,
sF30 = hAPP(sF29,v_q),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f4493,plain,
hAPP(sF29,v_q) = sF30,
inference(reorient_equations,[],[f4492]) ).
fof(f4494,definition,
sF31 = c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f4495,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = sF31,
inference(reorient_equations,[],[f4494]) ).
fof(f4496,definition,
sF32 = hAPP(sF30,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f4497,plain,
hAPP(sF30,sF31) = sF32,
inference(reorient_equations,[],[f4496]) ).
fof(f4498,definition,
sF33 = c_Groups_Otimes__class_Otimes(sF28),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f4499,plain,
c_Groups_Otimes__class_Otimes(sF28) = sF33,
inference(reorient_equations,[],[f4498]) ).
fof(f4500,definition,
sF34 = hAPP(sF33,v_p),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f4501,plain,
hAPP(sF33,v_p) = sF34,
inference(reorient_equations,[],[f4500]) ).
fof(f4502,definition,
sF35 = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f4503,plain,
c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = sF35,
inference(reorient_equations,[],[f4502]) ).
fof(f4504,definition,
sF36 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sF35,v_k____),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f4505,plain,
c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sF35,v_k____) = sF36,
inference(reorient_equations,[],[f4504]) ).
fof(f4506,definition,
sF37 = c_Groups_Ozero__class_Ozero(sF28),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f4507,plain,
c_Groups_Ozero__class_Ozero(sF28) = sF37,
inference(reorient_equations,[],[f4506]) ).
fof(f4508,definition,
sF38 = c_Polynomial_OpCons(tc_Complex_Ocomplex,sF36,sF37),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f4509,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF36,sF37) = sF38,
inference(reorient_equations,[],[f4508]) ).
fof(f4510,definition,
sF39 = hAPP(sF34,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f4511,plain,
hAPP(sF34,sF38) = sF39,
inference(reorient_equations,[],[f4510]) ).
fof(f4512,plain,
sF32 != sF39,
inference(definition_folding,[],[f4124,f4511,f4509,f4507,f4489,f4505,f4503,f4501,f4499,f4489,f4497,f4495,f4493,f4491,f4489]) ).
fof(f4592,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = sF31,
inference(forward_demodulation,[],[f4495,f2616]) ).
fof(f4618,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,c_Groups_Ozero__class_Ozero(sF28)),
inference(superposition,[],[f2687,f4489]) ).
fof(f4619,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK6,sF37),
inference(forward_demodulation,[],[f4618,f4507]) ).
fof(f4620,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,c_Groups_Ozero__class_Ozero(sF28)),
inference(superposition,[],[f2615,f4489]) ).
fof(f4621,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_k____,sF37),
inference(forward_demodulation,[],[f4620,f4507]) ).
fof(f4628,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,[],[f2736,f4049]) ).
fof(f4629,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X2),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),X2))),
inference(resolution,[],[f3268,f4050]) ).
fof(f4630,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X2),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X1),X2))),
inference(forward_demodulation,[],[f4629,f4489]) ).
fof(f4631,plain,
! [X2,X0,X1] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X2),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(sF33,X1),X2))),
inference(forward_demodulation,[],[f4630,f4499]) ).
fof(f4633,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_Osmult(tc_Complex_Ocomplex,X1,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X2))),
inference(resolution,[],[f3132,f4050]) ).
fof(f4634,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X1,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X0),X2))),
inference(forward_demodulation,[],[f4633,f4489]) ).
fof(f4635,plain,
! [X2,X0,X1] : hAPP(hAPP(sF33,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X1,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(hAPP(sF33,X0),X2))),
inference(forward_demodulation,[],[f4634,f4499]) ).
fof(f4636,plain,
! [X0,X1] : hAPP(sF34,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_p),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(sF34,X1))),
inference(superposition,[],[f4635,f4501]) ).
fof(f4638,plain,
! [X0,X1] : hAPP(hAPP(sF33,X0),c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X0)) = hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X0)),X0),
inference(superposition,[],[f4631,f4635]) ).
fof(f4643,plain,
hAPP(hAPP(sF33,sF37),v_p) = hAPP(hAPP(sF33,v_p),sF37),
inference(superposition,[],[f4638,f4621]) ).
fof(f4648,plain,
hAPP(hAPP(sF33,sF37),v_p) = hAPP(sF34,sF37),
inference(forward_demodulation,[],[f4643,f4501]) ).
fof(f4657,plain,
! [X0] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37)),v_p) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_p),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),hAPP(sF34,sF37))),
inference(superposition,[],[f4631,f4648]) ).
fof(f4658,plain,
! [X0] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37)),v_p) = hAPP(sF34,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37)),
inference(forward_demodulation,[],[f4657,f4636]) ).
fof(f4703,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),
inference(resolution,[],[f3227,f4050]) ).
fof(f4709,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),X0) = X0,
inference(resolution,[],[f2704,f4049]) ).
fof(f4710,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF35),X0) = X0,
inference(forward_demodulation,[],[f4709,f4503]) ).
fof(f4715,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF35) = X0,
inference(superposition,[],[f4628,f4710]) ).
fof(f4724,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,[],[f4279,f4052]) ).
fof(f4725,plain,
( sF35 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),v_k____)
| v_k____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f4724,f4505]) ).
fof(f4743,plain,
sF35 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),v_k____),
inference(forward_subsumption_resolution,[],[f4725,f2614]) ).
fof(f4986,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,[],[f2740,f4049]) ).
fof(f4994,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF35),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),v_k____),X0)),
inference(superposition,[],[f4986,f4743]) ).
fof(f5012,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),v_k____),X0)) = X0,
inference(forward_demodulation,[],[f4994,f4710]) ).
fof(f5025,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),v_k____)) = X0,
inference(superposition,[],[f5012,f4628]) ).
fof(f5036,plain,
! [X0] :
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),X0)
| v_k____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f5025,f4724]) ).
fof(f5040,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF36),X0),
inference(forward_subsumption_resolution,[],[f5036,f2614]) ).
fof(f5051,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF36),
inference(superposition,[],[f4628,f5040]) ).
fof(f5057,plain,
sF35 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,v_k____,v_k____),
inference(superposition,[],[f4743,f5040]) ).
fof(f5429,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,[],[f2618,f4049]) ).
fof(f5430,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF28)) = c_Groups_Oone__class_Oone(sF28),
inference(forward_demodulation,[],[f5429,f4489]) ).
fof(f5431,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),sF37) = c_Groups_Oone__class_Oone(sF28),
inference(forward_demodulation,[],[f5430,f4507]) ).
fof(f5432,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,sF35,sF37) = c_Groups_Oone__class_Oone(sF28),
inference(forward_demodulation,[],[f5431,f4503]) ).
fof(f5435,plain,
hAPP(hAPP(sF33,c_Groups_Oone__class_Oone(sF28)),v_p) = hAPP(sF34,c_Groups_Oone__class_Oone(sF28)),
inference(superposition,[],[f4658,f5432]) ).
fof(f5505,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,[],[f2676,f4050]) ).
fof(f5506,plain,
! [X0] : c_Groups_Ozero__class_Ozero(sF28) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),c_Groups_Ozero__class_Ozero(sF28)),X0),
inference(forward_demodulation,[],[f5505,f4489]) ).
fof(f5507,plain,
! [X0] : sF37 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),sF37),X0),
inference(forward_demodulation,[],[f5506,f4507]) ).
fof(f5508,plain,
! [X0] : sF37 = hAPP(hAPP(sF33,sF37),X0),
inference(forward_demodulation,[],[f5507,f4499]) ).
fof(f5511,plain,
! [X0,X1] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37)),X1) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF37)),
inference(superposition,[],[f4631,f5508]) ).
fof(f5543,plain,
( class_Rings_Ocomm__semiring__1(sF28)
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(superposition,[],[f4096,f4489]) ).
fof(f5544,plain,
class_Rings_Ocomm__semiring__1(sF28),
inference(forward_subsumption_resolution,[],[f5543,f4049]) ).
fof(f5548,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X0),c_Groups_Oone__class_Oone(sF28)) = X0,
inference(resolution,[],[f5544,f2701]) ).
fof(f5550,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X0),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(sF28),X1),X0),
inference(resolution,[],[f5544,f2736]) ).
fof(f5558,plain,
! [X0,X1] : hAPP(hAPP(sF33,X0),X1) = hAPP(hAPP(sF33,X1),X0),
inference(forward_demodulation,[],[f5550,f4499]) ).
fof(f5560,plain,
! [X0] : hAPP(hAPP(sF33,X0),c_Groups_Oone__class_Oone(sF28)) = X0,
inference(forward_demodulation,[],[f5548,f4499]) ).
fof(f5599,plain,
hAPP(sF34,c_Groups_Oone__class_Oone(sF28)) = hAPP(hAPP(sF33,v_p),c_Groups_Oone__class_Oone(sF28)),
inference(superposition,[],[f5435,f5558]) ).
fof(f5600,plain,
v_p = hAPP(sF34,c_Groups_Oone__class_Oone(sF28)),
inference(forward_demodulation,[],[f5599,f5560]) ).
fof(f5636,plain,
! [X0,X1] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X0)),c_Groups_Oone__class_Oone(sF28)) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X1,c_Groups_Oone__class_Oone(sF28)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)),
inference(superposition,[],[f4631,f5560]) ).
fof(f5639,plain,
! [X0,X1] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X0) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X1,c_Groups_Oone__class_Oone(sF28)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)),
inference(forward_demodulation,[],[f5636,f5560]) ).
fof(f6119,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,[],[f2731,f4049]) ).
fof(f6123,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(sF28),X0),X1)),X2),
inference(forward_demodulation,[],[f6119,f4489]) ).
fof(f6124,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(sF29,X0),X1)),X2),
inference(forward_demodulation,[],[f6123,f4491]) ).
fof(f6542,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,[],[f2689,f4049]) ).
fof(f6544,plain,
! [X0] : c_Groups_Oone__class_Oone(sF28) = hAPP(hAPP(c_Power_Opower__class_Opower(sF28),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolution,[],[f2689,f5544]) ).
fof(f6545,plain,
! [X0] : c_Groups_Oone__class_Oone(sF28) = hAPP(hAPP(c_Power_Opower__class_Opower(sF28),X0),sF31),
inference(forward_demodulation,[],[f6544,f4592]) ).
fof(f6547,plain,
! [X0] : c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),sF31),
inference(forward_demodulation,[],[f6542,f4592]) ).
fof(f6548,plain,
! [X0] : c_Groups_Oone__class_Oone(sF28) = hAPP(hAPP(sF29,X0),sF31),
inference(forward_demodulation,[],[f6545,f4491]) ).
fof(f6549,plain,
! [X0] : sF35 = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),sF31),
inference(forward_demodulation,[],[f6547,f4503]) ).
fof(f6555,plain,
! [X0,X1] : sF35 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(sF29,X0),sF31)),X1),
inference(superposition,[],[f6124,f6549]) ).
fof(f6556,plain,
! [X1] : sF35 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(sF28)),X1),
inference(forward_demodulation,[],[f6555,f6548]) ).
fof(f6581,plain,
hAPP(sF30,sF31) = c_Groups_Oone__class_Oone(sF28),
inference(superposition,[],[f6548,f4493]) ).
fof(f6604,plain,
sF32 = c_Groups_Oone__class_Oone(sF28),
inference(forward_demodulation,[],[f6581,f4497]) ).
fof(f6617,plain,
v_p = hAPP(sF34,sF32),
inference(superposition,[],[f5600,f6604]) ).
fof(f6620,plain,
! [X0] : sF35 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32),X0),
inference(superposition,[],[f6556,f6604]) ).
fof(f6631,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF35) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF32)),X1),
inference(superposition,[],[f4703,f6620]) ).
fof(f6634,plain,
! [X0] :
( sF35 != hAPP(X0,sK5(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32),X0))
| c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) = X0 ),
inference(superposition,[],[f2612,f6620]) ).
fof(f6638,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF32)),X1) = X0,
inference(forward_demodulation,[],[f6631,f4715]) ).
fof(f6840,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,[],[f4246,f4068]) ).
fof(f6841,plain,
c_Groups_Ozero__class_Ozero(sF28) = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(sF28)),
inference(forward_demodulation,[],[f6840,f4489]) ).
fof(f6842,plain,
sF37 = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sF37),
inference(forward_demodulation,[],[f6841,f4507]) ).
fof(f6843,plain,
! [X0,X1] : hAPP(hAPP(sF33,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37)),X1) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1),sF37),
inference(superposition,[],[f5511,f6842]) ).
fof(f6844,plain,
! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(sF28)),sF37),
inference(superposition,[],[f5639,f6842]) ).
fof(f6851,plain,
! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF32),sF37),
inference(forward_demodulation,[],[f6844,f6604]) ).
fof(f7030,plain,
! [X0] : hAPP(hAPP(sF33,v_p),X0) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,v_k____,X0),sF37),
inference(superposition,[],[f6843,f4621]) ).
fof(f7031,plain,
! [X0] : hAPP(hAPP(sF33,v_p),X0) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,sK6,X0),sF37),
inference(superposition,[],[f6843,f4619]) ).
fof(f7087,plain,
! [X0] : hAPP(sF34,X0) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,sK6,X0),sF37),
inference(forward_demodulation,[],[f7031,f4501]) ).
fof(f7088,plain,
! [X0] : hAPP(sF34,X0) = c_Groups_Oplus__class_Oplus(sF28,c_Polynomial_Osmult(tc_Complex_Ocomplex,v_k____,X0),sF37),
inference(forward_demodulation,[],[f7030,f4501]) ).
fof(f8640,plain,
! [X0] : c_Groups_Oplus__class_Oplus(sF28,X0,c_Groups_Ozero__class_Ozero(sF28)) = X0,
inference(resolution,[],[f2970,f5544]) ).
fof(f8641,plain,
! [X0] : c_Groups_Oplus__class_Oplus(sF28,X0,sF37) = X0,
inference(forward_demodulation,[],[f8640,f4507]) ).
fof(f8650,plain,
! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,sF37) = c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF32),
inference(superposition,[],[f6851,f8641]) ).
fof(f8651,plain,
! [X0] : hAPP(sF34,X0) = c_Polynomial_Osmult(tc_Complex_Ocomplex,v_k____,X0),
inference(superposition,[],[f7088,f8641]) ).
fof(f8652,plain,
! [X0] : hAPP(sF34,X0) = c_Polynomial_Osmult(tc_Complex_Ocomplex,sK6,X0),
inference(superposition,[],[f7087,f8641]) ).
fof(f8665,plain,
! [X0] : v_k____ = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF34,sF32)),X0),
inference(superposition,[],[f6638,f8651]) ).
fof(f8669,plain,
! [X0] : v_k____ = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0),
inference(forward_demodulation,[],[f8665,f6617]) ).
fof(f8718,plain,
! [X0] : sK6 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF34,sF32)),X0),
inference(superposition,[],[f6638,f8652]) ).
fof(f8722,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = sK6,
inference(forward_demodulation,[],[f8718,f6617]) ).
fof(f8733,plain,
v_k____ = sK6,
inference(forward_demodulation,[],[f8722,f8669]) ).
fof(f8755,plain,
sF35 = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sK6,sK6),
inference(superposition,[],[f5057,f8733]) ).
fof(f10838,plain,
sF38 = c_Polynomial_Osmult(tc_Complex_Ocomplex,sF36,sF32),
inference(superposition,[],[f4509,f8650]) ).
fof(f10860,plain,
! [X0] : sF36 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF38),X0),
inference(superposition,[],[f6638,f10838]) ).
fof(f10898,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF36) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF38)),X1),
inference(superposition,[],[f4703,f10860]) ).
fof(f10907,plain,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,v_k____) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF38)),X1),
inference(forward_demodulation,[],[f10898,f5051]) ).
fof(f10920,plain,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,sK6) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,sF38)),X1),
inference(forward_demodulation,[],[f10907,f8733]) ).
fof(f11708,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Opcompose(tc_Complex_Ocomplex,X0,X1)),X2),
inference(resolution,[],[f3121,f4050]) ).
fof(f11739,plain,
! [X0,X1] : sF35 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0)),X1),
inference(superposition,[],[f6620,f11708]) ).
fof(f11822,plain,
! [X0] :
( sF35 != sF35
| c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0)) ),
inference(superposition,[],[f6634,f11739]) ).
fof(f11823,plain,
! [X0] : c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0)),
inference(trivial_inequality_removal,[],[f11822]) ).
fof(f11848,plain,
! [X0,X1] :
( c_Polynomial_Opoly(tc_Complex_Ocomplex,X1) != c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32)
| c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0) = X1
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex)
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(superposition,[],[f2707,f11823]) ).
fof(f11849,plain,
! [X0,X1] :
( c_Polynomial_Opoly(tc_Complex_Ocomplex,X1) != c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32)
| c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0) = X1
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f11848,f4063]) ).
fof(f11858,plain,
! [X0,X1] :
( c_Polynomial_Opoly(tc_Complex_Ocomplex,X1) != c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32)
| c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f11849,f4070]) ).
fof(f11869,plain,
! [X0] : sF32 = c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0),
inference(equality_resolution,[],[f11858]) ).
fof(f20653,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sK6,sK6) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(sF34,sF38)),X0),
inference(superposition,[],[f10920,f8652]) ).
fof(f20694,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,sK6,sK6) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF39),X0),
inference(forward_demodulation,[],[f20653,f4511]) ).
fof(f20701,plain,
! [X0] : sF35 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sF39),X0),
inference(forward_demodulation,[],[f20694,f8755]) ).
fof(f20725,plain,
( sF35 != sF35
| c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) = c_Polynomial_Opoly(tc_Complex_Ocomplex,sF39) ),
inference(superposition,[],[f6634,f20701]) ).
fof(f20726,plain,
c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) = c_Polynomial_Opoly(tc_Complex_Ocomplex,sF39),
inference(trivial_inequality_removal,[],[f20725]) ).
fof(f20763,plain,
! [X0] :
( c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32) != c_Polynomial_Opoly(tc_Complex_Ocomplex,sF32)
| sF39 = c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0) ),
inference(superposition,[],[f11858,f20726]) ).
fof(f20766,plain,
! [X0] : sF39 = c_Polynomial_Opcompose(tc_Complex_Ocomplex,sF32,X0),
inference(trivial_inequality_removal,[],[f20763]) ).
fof(f20769,plain,
sF32 = sF39,
inference(forward_demodulation,[],[f20766,f11869]) ).
fof(f20782,plain,
$false,
inference(forward_subsumption_resolution,[],[f20769,f4512]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW286+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n026.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 13:33:12 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 13.08/2.67 % (3848853)Detected formulas, will run a generic FOF schedule.
% 13.08/2.67 % (3848917)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=1508223659:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.08/2.67 % (3848920)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=378313701:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.08/2.67 % (3848919)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3317188779:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.08/2.67 % (3848918)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2500213027:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.08/2.67 % (3848916)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=3544133528:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.08/2.67 % (3848915)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=647740927:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.08/2.67 % (3848918)Refutation not found, incomplete strategy
% 13.08/2.67 % (3848918)------------------------------
% 13.08/2.67 % (3848918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.08/2.67 % (3848918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.67 % (3848918)CaDiCaL version: 2.1.3
% 13.08/2.67 % (3848918)Termination reason: Refutation not found, incomplete strategy
% 13.08/2.67 % (3848918)Time elapsed: 0.009 s
% 13.08/2.67 % (3848918)Peak memory usage: 89 MB
% 13.08/2.67 % (3848918)Instructions burned: 11 (million)
% 13.08/2.67 % (3848921)dis-21_1_sil=8000:lcm=predicate:random_seed=2213942216: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)
% 13.08/2.67 % (3848919)Instruction limit reached!
% 13.08/2.67 % (3848919)------------------------------
% 13.08/2.67 % (3848919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.08/2.67 % (3848919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.67 % (3848919)CaDiCaL version: 2.1.3
% 13.08/2.67 % (3848919)Termination reason: Instruction limit
% 13.08/2.67 % (3848919)Termination phase: Saturation
% 13.08/2.67 % (3848919)Time elapsed: 0.072 s
% 13.08/2.67 % (3848919)Peak memory usage: 89 MB
% 13.08/2.67 % (3848919)Instructions burned: 119 (million)
% 13.08/2.67 % (3848920)Instruction limit reached!
% 13.08/2.67 % (3848920)------------------------------
% 13.08/2.67 % (3848920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.08/2.67 % (3848920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.67 % (3848920)CaDiCaL version: 2.1.3
% 13.08/2.67 % (3848920)Termination reason: Instruction limit
% 13.08/2.67 % (3848920)Termination phase: Saturation
% 13.08/2.67 % (3848920)Time elapsed: 0.079 s
% 13.08/2.67 % (3848920)Peak memory usage: 91 MB
% 13.08/2.67 % (3848920)Instructions burned: 140 (million)
% 13.08/2.67 % (3848921)Instruction limit reached!
% 13.08/2.67 % (3848921)------------------------------
% 13.08/2.67 % (3848921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.08/2.67 % (3848921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.08/2.67 % (3848921)CaDiCaL version: 2.1.3
% 13.08/2.67 % (3848921)Termination reason: Instruction limit
% 13.08/2.67 % (3848921)Termination phase: Saturation
% 13.08/2.67 % (3848921)Time elapsed: 0.068 s
% 13.08/2.67 % (3848921)Peak memory usage: 91 MB
% 13.08/2.67 % (3848921)Instructions burned: 130 (million)
% 13.08/2.67 % (3848929)lrs+10_1_sil=8000:sp=occurrence:random_seed=1226966808:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.08/2.67 % (3848930)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3927512012:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.08/2.67 % (3848931)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2762272905:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.08/2.67 % (3848918)------------------------------
% 13.08/2.67 % (3848918)------------------------------
% 13.08/2.67 % (3848930)Instruction limit reached!
% 13.08/2.67 % (3848930)------------------------------
% 13.08/2.67 % (3848930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848930)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848930)Termination reason: Instruction limit
% 18.95/3.47 % (3848930)Termination phase: Saturation
% 18.95/3.47 % (3848930)Time elapsed: 0.094 s
% 18.95/3.47 % (3848930)Peak memory usage: 91 MB
% 18.95/3.47 % (3848930)Instructions burned: 158 (million)
% 18.95/3.47 % (3848929)Instruction limit reached!
% 18.95/3.47 % (3848929)------------------------------
% 18.95/3.47 % (3848929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848929)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848929)Termination reason: Instruction limit
% 18.95/3.47 % (3848929)Termination phase: Saturation
% 18.95/3.47 % (3848929)Time elapsed: 0.189 s
% 18.95/3.47 % (3848929)Peak memory usage: 92 MB
% 18.95/3.47 % (3848929)Instructions burned: 286 (million)
% 18.95/3.47 % (3848935)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=1227332319:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 18.95/3.47 % (3848931)Instruction limit reached!
% 18.95/3.47 % (3848931)------------------------------
% 18.95/3.47 % (3848931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848931)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848931)Termination reason: Instruction limit
% 18.95/3.47 % (3848931)Termination phase: Saturation
% 18.95/3.47 % (3848931)Time elapsed: 0.187 s
% 18.95/3.47 % (3848931)Peak memory usage: 92 MB
% 18.95/3.47 % (3848931)Instructions burned: 326 (million)
% 18.95/3.47 % (3848936)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2985651957:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.95/3.47 % (3848938)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=842642304:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.95/3.47 % (3848935)Instruction limit reached!
% 18.95/3.47 % (3848935)------------------------------
% 18.95/3.47 % (3848935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848935)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848935)Termination reason: Instruction limit
% 18.95/3.47 % (3848935)Termination phase: Saturation
% 18.95/3.47 % (3848935)Time elapsed: 0.134 s
% 18.95/3.47 % (3848935)Peak memory usage: 92 MB
% 18.95/3.47 % (3848935)Instructions burned: 250 (million)
% 18.95/3.47 % (3848939)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=708603951:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 18.95/3.47 % (3848936)Instruction limit reached!
% 18.95/3.47 % (3848936)------------------------------
% 18.95/3.47 % (3848936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848936)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848936)Termination reason: Instruction limit
% 18.95/3.47 % (3848936)Termination phase: Saturation
% 18.95/3.47 % (3848936)Time elapsed: 0.161 s
% 18.95/3.47 % (3848936)Peak memory usage: 92 MB
% 18.95/3.47 % (3848936)Instructions burned: 294 (million)
% 18.95/3.47 % (3848939)Instruction limit reached!
% 18.95/3.47 % (3848939)------------------------------
% 18.95/3.47 % (3848939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848939)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848939)Termination reason: Instruction limit
% 18.95/3.47 % (3848939)Termination phase: Saturation
% 18.95/3.47 % (3848939)Time elapsed: 0.059 s
% 18.95/3.47 % (3848939)Peak memory usage: 90 MB
% 18.95/3.47 % (3848939)Instructions burned: 114 (million)
% 18.95/3.47 % (3848942)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=579412986:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 18.95/3.47 % (3848942)Refutation not found, incomplete strategy
% 18.95/3.47 % (3848942)------------------------------
% 18.95/3.47 % (3848942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848942)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848942)Termination reason: Refutation not found, incomplete strategy
% 18.95/3.47 % (3848942)Time elapsed: 0.058 s
% 18.95/3.47 % (3848942)Peak memory usage: 90 MB
% 18.95/3.47 % (3848942)Instructions burned: 118 (million)
% 18.95/3.47 % (3848944)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2129251923:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 18.95/3.47 % (3848945)lrs+10_1_sil=8000:sp=occurrence:random_seed=1130923070:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 18.95/3.47 % (3848944)Instruction limit reached!
% 18.95/3.47 % (3848944)------------------------------
% 18.95/3.47 % (3848944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848944)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848944)Termination reason: Instruction limit
% 18.95/3.47 % (3848944)Termination phase: Saturation
% 18.95/3.47 % (3848944)Time elapsed: 0.059 s
% 18.95/3.47 % (3848944)Peak memory usage: 89 MB
% 18.95/3.47 % (3848944)Instructions burned: 114 (million)
% 18.95/3.47 % (3848949)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=189396417:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 18.95/3.47 % (3848942)------------------------------
% 18.95/3.47 % (3848942)------------------------------
% 18.95/3.47 % (3848949)Refutation not found, incomplete strategy
% 18.95/3.47 % (3848949)------------------------------
% 18.95/3.47 % (3848949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848949)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848949)Termination reason: Refutation not found, incomplete strategy
% 18.95/3.47 % (3848949)Time elapsed: 0.063 s
% 18.95/3.47 % (3848949)Peak memory usage: 91 MB
% 18.95/3.47 % (3848949)Instructions burned: 119 (million)
% 18.95/3.47 % (3848951)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1945263535:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 18.95/3.47 % (3848949)------------------------------
% 18.95/3.47 % (3848949)------------------------------
% 18.95/3.47 % (3848945)Instruction limit reached!
% 18.95/3.47 % (3848945)------------------------------
% 18.95/3.47 % (3848945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848945)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848945)Termination reason: Instruction limit
% 18.95/3.47 % (3848945)Termination phase: Saturation
% 18.95/3.47 % (3848945)Time elapsed: 0.595 s
% 18.95/3.47 % (3848945)Peak memory usage: 99 MB
% 18.95/3.47 % (3848945)Instructions burned: 908 (million)
% 18.95/3.47 % (3848953)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3744376904:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 18.95/3.47 % (3848953)Instruction limit reached!
% 18.95/3.47 % (3848953)------------------------------
% 18.95/3.47 % (3848953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848953)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848953)Termination reason: Instruction limit
% 18.95/3.47 % (3848953)Termination phase: Saturation
% 18.95/3.47 % (3848953)Time elapsed: 0.075 s
% 18.95/3.47 % (3848953)Peak memory usage: 92 MB
% 18.95/3.47 % (3848953)Instructions burned: 135 (million)
% 18.95/3.47 % (3848954)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3211640452:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 18.95/3.47 % (3848956)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3616004378:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 18.95/3.47 % (3848954)Instruction limit reached!
% 18.95/3.47 % (3848954)------------------------------
% 18.95/3.47 % (3848954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848954)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848954)Termination reason: Instruction limit
% 18.95/3.47 % (3848954)Termination phase: Saturation
% 18.95/3.47 % (3848954)Time elapsed: 0.343 s
% 18.95/3.47 % (3848954)Peak memory usage: 99 MB
% 18.95/3.47 % (3848954)Instructions burned: 592 (million)
% 18.95/3.47 % (3848959)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=3574140692:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 18.95/3.47 % (3848938)Instruction limit reached!
% 18.95/3.47 % (3848938)------------------------------
% 18.95/3.47 % (3848938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848938)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848938)Termination reason: Instruction limit
% 18.95/3.47 % (3848938)Termination phase: Saturation
% 18.95/3.47 % (3848938)Time elapsed: 1.456 s
% 18.95/3.47 % (3848938)Peak memory usage: 146 MB
% 18.95/3.47 % (3848938)Instructions burned: 2351 (million)
% 18.95/3.47 % (3848959)Instruction limit reached!
% 18.95/3.47 % (3848959)------------------------------
% 18.95/3.47 % (3848959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848959)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848959)Termination reason: Instruction limit
% 18.95/3.47 % (3848959)Termination phase: Saturation
% 18.95/3.47 % (3848959)Time elapsed: 0.065 s
% 18.95/3.47 % (3848959)Peak memory usage: 90 MB
% 18.95/3.47 % (3848959)Instructions burned: 126 (million)
% 18.95/3.47 % (3848961)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1192742997:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 18.95/3.47 % (3848962)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1360222411:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 18.95/3.47 % (3848962)Refutation not found, incomplete strategy
% 18.95/3.47 % (3848962)------------------------------
% 18.95/3.47 % (3848962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848962)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848962)Termination reason: Refutation not found, incomplete strategy
% 18.95/3.47 % (3848962)Time elapsed: 0.006 s
% 18.95/3.47 % (3848962)Peak memory usage: 89 MB
% 18.95/3.47 % (3848962)Instructions burned: 7 (million)
% 18.95/3.47 % (3848961)Instruction limit reached!
% 18.95/3.47 % (3848961)------------------------------
% 18.95/3.47 % (3848961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848961)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848961)Termination reason: Instruction limit
% 18.95/3.47 % (3848961)Termination phase: Saturation
% 18.95/3.47 % (3848961)Time elapsed: 0.066 s
% 18.95/3.47 % (3848961)Peak memory usage: 90 MB
% 18.95/3.47 % (3848961)Instructions burned: 135 (million)
% 18.95/3.47 % (3848965)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1719746221:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 18.95/3.47 % (3848965)Refutation not found, incomplete strategy
% 18.95/3.47 % (3848965)------------------------------
% 18.95/3.47 % (3848965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.95/3.47 % (3848965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.95/3.47 % (3848965)CaDiCaL version: 2.1.3
% 18.95/3.47 % (3848965)Termination reason: Refutation not found, incomplete strategy
% 18.95/3.47 % (3848965)Time elapsed: 0.013 s
% 18.95/3.47 % (3848965)Peak memory usage: 89 MB
% 18.95/3.47 % (3848965)Instructions burned: 19 (million)
% 18.95/3.47 % (3848915)First to succeed.
% 18.95/3.47 % (3848915)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3848853"
% 18.95/3.47 % (3848962)------------------------------
% 18.95/3.47 % (3848962)------------------------------
% 18.95/3.47 % (3848967)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=3921649275:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 18.95/3.47 % (3848965)------------------------------
% 18.95/3.47 % (3848965)------------------------------
% 18.95/3.47 % (3848915)Refutation found. Thanks to Tanya!
% 18.95/3.47 % SZS status Theorem for theBenchmark
% 18.95/3.47 % SZS output start Proof for theBenchmark
% See solution above
% 20.11/3.66 % (3848915)------------------------------
% 20.11/3.66 % (3848915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.11/3.66 % (3848915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.11/3.66 % (3848915)CaDiCaL version: 2.1.3
% 20.11/3.66 % (3848915)Termination reason: Refutation
% 20.11/3.66 % (3848915)Time elapsed: 2.340 s
% 20.11/3.66 % (3848915)Peak memory usage: 157 MB
% 20.11/3.66 % (3848915)Instructions burned: 3709 (million)
% 20.11/3.66 % (3848915)------------------------------
% 20.11/3.66 % (3848915)------------------------------
% 20.11/3.66 % (3848853)Success in time 2.802 s
% 20.11/3.66 % Vampire exiting
%------------------------------------------------------------------------------