%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW285+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 : ContradictoryAxioms 12.02s 2.29s
% Output : Refutation 13.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 135 ( 62 unt; 2 def)
% Number of atoms : 232 ( 142 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 170 ( 73 ~; 67 |; 8 &)
% ( 4 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-3 aty)
% Number of variables : 228 ( 0 sgn 226 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ! [X2] : hAPP(X1,X2) = hAPP(X0,X2)
=> X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ext) ).
fof(f2,axiom,
v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_pe) ).
fof(f11,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__0(X1)
=> hAPP(c_Polynomial_Opoly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_poly__0) ).
fof(f47,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/sandbox2/benchmark/theBenchmark.p',fact_poly__pCons) ).
fof(f53,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/sandbox2/benchmark/theBenchmark.p',fact_poly__power) ).
fof(f57,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/sandbox2/benchmark/theBenchmark.p',fact_poly__mult) ).
fof(f68,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Omonom(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_poly__monom) ).
fof(f83,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/sandbox2/benchmark/theBenchmark.p',fact_pCons__eq__0__iff) ).
fof(f90,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/sandbox2/benchmark/theBenchmark.p',fact_monom__0) ).
fof(f94,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/sandbox2/benchmark/theBenchmark.p',fact_poly__smult) ).
fof(f95,axiom,
~ ! [X0] : 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),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096_B_Bthesis_O_A_I_B_Br_O_Aq_A_094_Adegree_Ap_A_061_Ap_A_K_Ar_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) ).
fof(f113,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/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(f132,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/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J) ).
fof(f186,axiom,
! [X0,X1] :
( class_RealVector_Oreal__normed__algebra(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/sandbox2/benchmark/theBenchmark.p',fact_mult__right_Ozero) ).
fof(f230,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(c_Polynomial_Opoly(X1,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Oone__class_Oone(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_poly__1) ).
fof(f237,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/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J) ).
fof(f238,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/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J) ).
fof(f290,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/sandbox2/benchmark/theBenchmark.p',fact_degree__pCons__eq__if) ).
fof(f1088,axiom,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra) ).
fof(f1101,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(f1102,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(f1120,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ozero) ).
fof(f1177,axiom,
! [X0,X1] :
( X1 != X0
| hBOOL(c_fequal(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fequal__2) ).
fof(f1178,axiom,
~ hBOOL(c_fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fFalse__1) ).
fof(f1223,plain,
! [X0,X1] :
( X1 = X0
| ? [X2] : hAPP(X1,X2) != hAPP(X0,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f1233,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f1275,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,[],[f47]) ).
fof(f1282,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,[],[f53]) ).
fof(f1286,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,[],[f57]) ).
fof(f1298,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Omonom(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X0),X1))
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f68]) ).
fof(f1315,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,[],[f83]) ).
fof(f1327,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,[],[f90]) ).
fof(f1331,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,[],[f94]) ).
fof(f1332,plain,
? [X0] : 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),X0),
inference(ennf_transformation,[],[f95]) ).
fof(f1356,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,[],[f113]) ).
fof(f1378,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,[],[f132]) ).
fof(f1423,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_RealVector_Oreal__normed__algebra(X1) ),
inference(ennf_transformation,[],[f186]) ).
fof(f1475,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(X1,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Oone__class_Oone(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f230]) ).
fof(f1480,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,[],[f237]) ).
fof(f1481,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,[],[f238]) ).
fof(f1513,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,[],[f290]) ).
fof(f2350,plain,
! [X0,X1] :
( X1 = X0
| hAPP(X1,sK4(X0,X1)) != hAPP(X0,sK4(X0,X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f1223]) ).
fof(f2378,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,[],[f1315]) ).
fof(f2379,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,[],[f2378]) ).
fof(f2381,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),sK8),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X0,sK8)],[f1332]) ).
fof(f2642,plain,
! [X0,X1] :
( hAPP(X1,sK4(X0,X1)) != hAPP(X0,sK4(X0,X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f2350]) ).
fof(f2643,plain,
v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[],[f2]) ).
fof(f2657,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X1)
| c_Groups_Ozero__class_Ozero(X1) = hAPP(c_Polynomial_Opoly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))),X0) ),
inference(cnf_transformation,[],[f1233]) ).
fof(f2714,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,[],[f1275]) ).
fof(f2720,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,[],[f1282]) ).
fof(f2724,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,[],[f1286]) ).
fof(f2736,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| hAPP(c_Polynomial_Opoly(X3,c_Polynomial_Omonom(X3,X2,X1)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X2),hAPP(hAPP(c_Power_Opower__class_Opower(X3),X0),X1)) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f2753,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,[],[f2379]) ).
fof(f2762,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,[],[f1327]) ).
fof(f2766,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,[],[f1331]) ).
fof(f2767,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),sK8),
inference(cnf_transformation,[],[f2381]) ).
fof(f2796,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,[],[f1356]) ).
fof(f2818,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,[],[f1378]) ).
fof(f2889,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__algebra(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,[],[f1423]) ).
fof(f2958,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| hAPP(c_Polynomial_Opoly(X1,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X1))),X0) = c_Groups_Oone__class_Oone(X1) ),
inference(cnf_transformation,[],[f1475]) ).
fof(f2966,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,[],[f1480]) ).
fof(f2967,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,[],[f1481]) ).
fof(f3042,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,[],[f1513]) ).
fof(f4068,plain,
class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1088]) ).
fof(f4081,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1101]) ).
fof(f4082,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1102]) ).
fof(f4100,plain,
class_Groups_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1120]) ).
fof(f4157,plain,
! [X0,X1] :
( X0 != X1
| hBOOL(c_fequal(X1,X0)) ),
inference(cnf_transformation,[],[f1177]) ).
fof(f4158,plain,
~ hBOOL(c_fFalse),
inference(cnf_transformation,[],[f1178]) ).
fof(f4304,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,[],[f2753]) ).
fof(f4305,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,[],[f4304]) ).
fof(f4378,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,[],[f3042]) ).
fof(f4512,plain,
! [X1] : hBOOL(c_fequal(X1,X1)),
inference(equality_resolution,[],[f4157]) ).
fof(f4604,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,[],[f2796,f4081]) ).
fof(f4616,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,[],[f2714,f4082]) ).
fof(f4621,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),
inference(resolution,[],[f2958,f4081]) ).
fof(f4645,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = X0,
inference(resolution,[],[f2966,f4081]) ).
fof(f4646,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,[],[f2766,f4082]) ).
fof(f4647,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1),
inference(superposition,[],[f4646,f4621]) ).
fof(f4655,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),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),X0),
inference(superposition,[],[f4604,f4646]) ).
fof(f4659,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1) = X0,
inference(forward_demodulation,[],[f4647,f4645]) ).
fof(f4688,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,[],[f4378,f4100]) ).
fof(f4689,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_p)),
inference(forward_demodulation,[],[f4688,f2643]) ).
fof(f4690,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),X0) = X0,
inference(resolution,[],[f2967,f4081]) ).
fof(f4707,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,[],[f2889,f4068]) ).
fof(f4722,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0),
inference(resolution,[],[f2657,f4082]) ).
fof(f4724,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f4722,f2643]) ).
fof(f4726,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_p)),X1),
inference(superposition,[],[f4646,f4724]) ).
fof(f4727,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_p)),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))),
inference(superposition,[],[f4616,f4724]) ).
fof(f4730,plain,
! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(X0,sK4(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p)))
| c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p) = X0 ),
inference(superposition,[],[f2642,f4724]) ).
fof(f4732,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_p)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(forward_demodulation,[],[f4727,f4707]) ).
fof(f4733,plain,
! [X0,X1] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_p)),X1),
inference(forward_demodulation,[],[f4726,f4707]) ).
fof(f4764,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
inference(superposition,[],[f4730,f4621]) ).
fof(f4783,definition,
( spl29_11
<=> c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f4785,plain,
( c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f4783]) ).
fof(f4787,definition,
( spl29_12
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f4789,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)
| spl29_12 ),
inference(avatar_component_clause,[],[f4787]) ).
fof(f4790,plain,
( spl29_11
| ~ spl29_12 ),
inference(avatar_split_clause,[],[f4764,f4787,f4783]) ).
fof(f5083,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,[],[f2724,f4082]) ).
fof(f5085,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(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2),X1)),X2),
inference(forward_demodulation,[],[f5083,f4646]) ).
fof(f5089,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),X0)),X1) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)),X1),
inference(superposition,[],[f5085,f4724]) ).
fof(f5168,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X0,
inference(resolution,[],[f2818,f4081]) ).
fof(f5217,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X2),X1)),
inference(resolution,[],[f2736,f4081]) ).
fof(f5222,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),X0)),X1) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X1),X0),
inference(superposition,[],[f4690,f5217]) ).
fof(f5251,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,[],[f2720,f4081]) ).
fof(f5253,plain,
! [X0] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK8)),X0),
inference(superposition,[],[f5251,f2767]) ).
fof(f5276,plain,
! [X0] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),sK8)),X0),
inference(forward_demodulation,[],[f5253,f5089]) ).
fof(f5332,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,[],[f4305,f4100]) ).
fof(f5334,plain,
v_p = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p),
inference(forward_demodulation,[],[f5332,f2643]) ).
fof(f5336,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p),
inference(superposition,[],[f4689,f5334]) ).
fof(f5747,plain,
! [X0,X1] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)),X1),
inference(superposition,[],[f4707,f4655]) ).
fof(f8109,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,[],[f2762,f4100]) ).
fof(f8111,plain,
! [X0] : c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_p) = c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f8109,f2643]) ).
fof(f8117,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),v_p)),X0) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(superposition,[],[f5222,f8111]) ).
fof(f8119,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),X0),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f8117,f4732]) ).
fof(f8123,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(forward_demodulation,[],[f8119,f5168]) ).
fof(f8233,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X1)),X0)
| ~ spl29_11 ),
inference(superposition,[],[f4655,f4785]) ).
fof(f8256,plain,
( ! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_p)),X1)
| ~ spl29_11 ),
inference(forward_demodulation,[],[f8233,f4655]) ).
fof(f8272,plain,
( ! [X0,X1] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1)
| ~ spl29_11 ),
inference(forward_demodulation,[],[f8256,f4733]) ).
fof(f8287,plain,
( ! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| ~ spl29_11 ),
inference(forward_demodulation,[],[f8272,f4659]) ).
fof(f8300,plain,
( ! [X0,X1] : X0 = X1
| ~ spl29_11 ),
inference(superposition,[],[f8287,f8287]) ).
fof(f9272,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)),
inference(forward_demodulation,[],[f5276,f5747]) ).
fof(f9274,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(forward_demodulation,[],[f9272,f5336]) ).
fof(f9276,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f9274,f8123]) ).
fof(f9277,plain,
( $false
| spl29_12 ),
inference(forward_subsumption_resolution,[],[f9276,f4789]) ).
fof(f9278,plain,
spl29_12,
inference(avatar_contradiction_clause,[],[f9277]) ).
fof(f10082,plain,
( ! [X0] : hBOOL(X0)
| ~ spl29_11 ),
inference(superposition,[],[f4512,f8300]) ).
fof(f11111,plain,
( ! [X0] : ~ hBOOL(X0)
| ~ spl29_11 ),
inference(superposition,[],[f4158,f8300]) ).
fof(f11170,plain,
( $false
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f10082,f11111]) ).
fof(f11171,plain,
~ spl29_11,
inference(avatar_contradiction_clause,[],[f11170]) ).
cnf(s8,plain,
( spl29_11
| ~ spl29_12 ),
inference(sat_conversion,[],[f4790]) ).
cnf(s33,plain,
spl29_12,
inference(sat_conversion,[],[f9278]) ).
cnf(s57,plain,
~ spl29_11,
inference(sat_conversion,[],[f11171]) ).
cnf(s69,plain,
$false,
inference(rat,[],[s8,s33,s57]) ).
fof(f11185,plain,
$false,
inference(avatar_sat_refutation,[],[s69]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW285+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n002.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 13:32:52 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.08/1.75 % (351205)Detected formulas, will run a generic FOF schedule.
% 8.08/1.75 % (351216)dis-21_1_sil=8000:lcm=predicate:random_seed=2960708618: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)
% 8.08/1.75 % (351216)Instruction limit reached!
% 8.08/1.75 % (351216)------------------------------
% 8.08/1.75 % (351216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.08/1.75 % (351216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.75 % (351216)CaDiCaL version: 2.1.3
% 8.08/1.75 % (351216)Termination reason: Instruction limit
% 8.08/1.75 % (351216)Termination phase: Saturation
% 8.08/1.75 % (351216)Time elapsed: 0.037 s
% 8.08/1.75 % (351216)Peak memory usage: 91 MB
% 8.08/1.75 % (351216)Instructions burned: 132 (million)
% 8.08/1.75 % (351215)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3422427206:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.08/1.75 % (351214)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2957857382:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.08/1.76 % (351213)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1566526004:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.08/1.76 % (351210)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=3000896192:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.08/1.76 % (351211)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=2106066475:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.08/1.76 % (351212)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=1717663034:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.08/1.76 % (351214)Refutation not found, incomplete strategy
% 8.08/1.76 % (351214)------------------------------
% 8.08/1.76 % (351214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.08/1.76 % (351213)Refutation not found, incomplete strategy
% 8.08/1.76 % (351213)------------------------------
% 8.08/1.76 % (351213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.08/1.76 % (351213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.76 % (351214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.76 % (351214)CaDiCaL version: 2.1.3
% 8.08/1.76 % (351213)CaDiCaL version: 2.1.3
% 8.08/1.76 % (351214)Termination reason: Refutation not found, incomplete strategy
% 8.08/1.76 % (351214)Time elapsed: 0.004 s
% 8.08/1.76 % (351214)Peak memory usage: 87 MB
% 8.08/1.76 % (351213)Termination reason: Refutation not found, incomplete strategy
% 8.08/1.76 % (351213)Time elapsed: 0.004 s
% 8.08/1.76 % (351213)Peak memory usage: 87 MB
% 8.08/1.76 % (351214)Instructions burned: 4 (million)
% 8.08/1.76 % (351213)Instructions burned: 4 (million)
% 8.08/1.76 % (351215)Instruction limit reached!
% 8.08/1.76 % (351215)------------------------------
% 8.08/1.76 % (351215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.08/1.76 % (351215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.76 % (351215)CaDiCaL version: 2.1.3
% 8.08/1.76 % (351215)Termination reason: Instruction limit
% 8.08/1.76 % (351215)Termination phase: Saturation
% 8.08/1.76 % (351215)Time elapsed: 0.080 s
% 8.08/1.76 % (351215)Peak memory usage: 91 MB
% 8.08/1.76 % (351215)Instructions burned: 139 (million)
% 8.08/1.76 % (351224)lrs+10_1_sil=8000:sp=occurrence:random_seed=1545937207:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.08/1.76 % (351224)Refutation not found, incomplete strategy
% 8.08/1.76 % (351224)------------------------------
% 8.08/1.76 % (351224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.08/1.76 % (351224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.08/1.76 % (351224)CaDiCaL version: 2.1.3
% 8.08/1.76 % (351224)Termination reason: Refutation not found, incomplete strategy
% 8.08/1.76 % (351224)Time elapsed: 0.002 s
% 8.08/1.76 % (351224)Peak memory usage: 88 MB
% 8.08/1.76 % (351224)Instructions burned: 4 (million)
% 8.08/1.76 % (351225)lrs+10_1_sil=32000:urr=on:br=off:random_seed=931766017:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.72/1.95 % (351225)Refutation not found, incomplete strategy
% 8.72/1.95 % (351225)------------------------------
% 8.72/1.95 % (351225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351225)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351225)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351225)Time elapsed: 0.009 s
% 8.72/1.95 % (351225)Peak memory usage: 88 MB
% 8.72/1.95 % (351225)Instructions burned: 17 (million)
% 8.72/1.95 % (351224)------------------------------
% 8.72/1.95 % (351224)------------------------------
% 8.72/1.95 % (351213)------------------------------
% 8.72/1.95 % (351213)------------------------------
% 8.72/1.95 % (351214)------------------------------
% 8.72/1.95 % (351214)------------------------------
% 8.72/1.95 % (351228)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3794296912:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 8.72/1.95 % (351228)Refutation not found, incomplete strategy
% 8.72/1.95 % (351228)------------------------------
% 8.72/1.95 % (351228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351228)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351228)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351228)Time elapsed: 0.002 s
% 8.72/1.95 % (351228)Peak memory usage: 87 MB
% 8.72/1.95 % (351228)Instructions burned: 4 (million)
% 8.72/1.95 % (351230)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2520503073:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.72/1.95 % (351229)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=3897611553:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.72/1.95 % (351230)Refutation not found, incomplete strategy
% 8.72/1.95 % (351230)------------------------------
% 8.72/1.95 % (351230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351230)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351230)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351230)Time elapsed: 0.005 s
% 8.72/1.95 % (351230)Peak memory usage: 87 MB
% 8.72/1.95 % (351230)Instructions burned: 6 (million)
% 8.72/1.95 % (351225)------------------------------
% 8.72/1.95 % (351225)------------------------------
% 8.72/1.95 % (351228)------------------------------
% 8.72/1.95 % (351228)------------------------------
% 8.72/1.95 % (351229)Instruction limit reached!
% 8.72/1.95 % (351229)------------------------------
% 8.72/1.95 % (351229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351229)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351229)Termination reason: Instruction limit
% 8.72/1.95 % (351229)Termination phase: Saturation
% 8.72/1.95 % (351229)Time elapsed: 0.144 s
% 8.72/1.95 % (351229)Peak memory usage: 92 MB
% 8.72/1.95 % (351229)Instructions burned: 248 (million)
% 8.72/1.95 % (351234)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=124138266:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.72/1.95 % (351235)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=308755528:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.72/1.95 % (351236)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=622540885:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 8.72/1.95 % (351230)------------------------------
% 8.72/1.95 % (351230)------------------------------
% 8.72/1.95 % (351236)Refutation not found, incomplete strategy
% 8.72/1.95 % (351236)------------------------------
% 8.72/1.95 % (351236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351236)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351236)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351236)Time elapsed: 0.029 s
% 8.72/1.95 % (351236)Peak memory usage: 90 MB
% 8.72/1.95 % (351236)Instructions burned: 109 (million)
% 8.72/1.95 % (351235)Instruction limit reached!
% 8.72/1.95 % (351235)------------------------------
% 8.72/1.95 % (351235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351235)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351235)Termination reason: Instruction limit
% 8.72/1.95 % (351235)Termination phase: Saturation
% 8.72/1.95 % (351235)Time elapsed: 0.063 s
% 8.72/1.95 % (351235)Peak memory usage: 90 MB
% 8.72/1.95 % (351235)Instructions burned: 114 (million)
% 8.72/1.95 % (351212)Refutation not found, incomplete strategy
% 8.72/1.95 % (351212)------------------------------
% 8.72/1.95 % (351212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351212)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351212)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351212)Time elapsed: 0.763 s
% 8.72/1.95 % (351212)Peak memory usage: 146 MB
% 8.72/1.95 % (351212)Instructions burned: 1141 (million)
% 8.72/1.95 % (351240)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=348521628:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.72/1.95 % (351236)------------------------------
% 8.72/1.95 % (351236)------------------------------
% 8.72/1.95 % (351241)lrs+10_1_sil=8000:sp=occurrence:random_seed=3819510364:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 8.72/1.95 % (351241)Refutation not found, incomplete strategy
% 8.72/1.95 % (351241)------------------------------
% 8.72/1.95 % (351241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351241)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351241)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351241)Time elapsed: 0.005 s
% 8.72/1.95 % (351241)Peak memory usage: 87 MB
% 8.72/1.95 % (351241)Instructions burned: 5 (million)
% 8.72/1.95 % (351240)Instruction limit reached!
% 8.72/1.95 % (351240)------------------------------
% 8.72/1.95 % (351240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351240)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351240)Termination reason: Instruction limit
% 8.72/1.95 % (351240)Termination phase: Saturation
% 8.72/1.95 % (351240)Time elapsed: 0.062 s
% 8.72/1.95 % (351240)Peak memory usage: 90 MB
% 8.72/1.95 % (351240)Instructions burned: 115 (million)
% 8.72/1.95 % (351243)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3640179316:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.72/1.95 % (351243)Refutation not found, incomplete strategy
% 8.72/1.95 % (351243)------------------------------
% 8.72/1.95 % (351243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/1.95 % (351243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/1.95 % (351243)CaDiCaL version: 2.1.3
% 8.72/1.95 % (351243)Termination reason: Refutation not found, incomplete strategy
% 8.72/1.95 % (351243)Time elapsed: 0.034 s
% 8.72/1.95 % (351243)Peak memory usage: 91 MB
% 8.72/1.95 % (351243)Instructions burned: 117 (million)
% 8.72/1.95 % (351245)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2593325118:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.72/1.95 % (351212)------------------------------
% 8.72/1.95 % (351212)------------------------------
% 8.72/1.95 % (351241)------------------------------
% 8.72/1.95 % (351241)------------------------------
% 8.72/1.95 % (351243)------------------------------
% 8.72/1.95 % (351243)------------------------------
% 8.72/1.95 % (351248)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3524856136:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 8.72/1.95 % (351250)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2874500383:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 8.72/1.95 % (351249)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1310723691:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 8.72/1.95 % (351249)Refutation not found, incomplete strategy
% 8.72/1.95 % (351249)------------------------------
% 8.72/1.95 % (351249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351249)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351249)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.29 % (351249)Time elapsed: 0.005 s
% 12.02/2.29 % (351249)Peak memory usage: 87 MB
% 12.02/2.29 % (351249)Instructions burned: 6 (million)
% 12.02/2.29 % (351248)Instruction limit reached!
% 12.02/2.29 % (351248)------------------------------
% 12.02/2.29 % (351248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351248)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351248)Termination reason: Instruction limit
% 12.02/2.29 % (351248)Termination phase: Saturation
% 12.02/2.29 % (351248)Time elapsed: 0.079 s
% 12.02/2.29 % (351248)Peak memory usage: 91 MB
% 12.02/2.29 % (351248)Instructions burned: 135 (million)
% 12.02/2.29 % (351254)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=94766576:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi)
% 12.02/2.29 % (351254)Refutation not found, incomplete strategy
% 12.02/2.29 % (351254)------------------------------
% 12.02/2.29 % (351254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351254)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351254)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.29 % (351254)Time elapsed: 0.011 s
% 12.02/2.29 % (351254)Peak memory usage: 88 MB
% 12.02/2.29 % (351254)Instructions burned: 21 (million)
% 12.02/2.29 [W928 13:32:54.650897258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650920077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650941994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650948261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650961740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650967157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650980697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.650986237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.651007630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.651017496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.651039550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.651045576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655841677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655879584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655917824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655930371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655957284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655969017 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.655995131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.656016911 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.656043438 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.656055151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.656084241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 [W928 13:32:54.656094771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 12.02/2.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.02/2.29 % (351249)------------------------------
% 12.02/2.29 % (351249)------------------------------
% 12.02/2.29 % (351210)First to succeed.
% 12.02/2.29 % (351210)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-351205"
% 12.02/2.29 % (351250)Refutation not found, incomplete strategy
% 12.02/2.29 % (351250)------------------------------
% 12.02/2.29 % (351250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351250)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351250)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.29 % (351250)Time elapsed: 0.311 s
% 12.02/2.29 % (351250)Peak memory usage: 127 MB
% 12.02/2.29 % (351250)Instructions burned: 838 (million)
% 12.02/2.29 % (351245)Refutation not found, incomplete strategy
% 12.02/2.29 % (351245)------------------------------
% 12.02/2.29 % (351245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351245)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351245)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.29 % (351245)Time elapsed: 0.569 s
% 12.02/2.29 % (351245)Peak memory usage: 126 MB
% 12.02/2.29 % (351245)Instructions burned: 838 (million)
% 12.02/2.29 % (351256)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3320286418:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 12.02/2.29 % (351254)------------------------------
% 12.02/2.29 % (351254)------------------------------
% 12.02/2.29 % (351250)------------------------------
% 12.02/2.29 % (351250)------------------------------
% 12.02/2.29 % (351256)Instruction limit reached!
% 12.02/2.29 % (351256)------------------------------
% 12.02/2.29 % (351256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.29 % (351256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.29 % (351256)CaDiCaL version: 2.1.3
% 12.02/2.29 % (351256)Termination reason: Instruction limit
% 12.02/2.29 % (351256)Termination phase: Saturation
% 12.02/2.29 % (351256)Time elapsed: 0.066 s
% 12.02/2.29 % (351256)Peak memory usage: 91 MB
% 12.02/2.29 % (351256)Instructions burned: 134 (million)
% 12.02/2.29 % (351210)Refutation found. Thanks to Tanya!
% 12.02/2.29 % SZS status ContradictoryAxioms for theBenchmark
% 12.02/2.29 % SZS output start Proof for theBenchmark
% See solution above
% 13.53/2.48 % (351210)------------------------------
% 13.53/2.48 % (351210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.53/2.48 % (351210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.53/2.48 % (351210)CaDiCaL version: 2.1.3
% 13.53/2.48 % (351210)Termination reason: Refutation
% 13.53/2.48 % (351210)Time elapsed: 1.459 s
% 13.53/2.48 % (351210)Peak memory usage: 147 MB
% 13.53/2.48 % (351210)Instructions burned: 2290 (million)
% 13.53/2.48 % (351210)------------------------------
% 13.53/2.48 % (351210)------------------------------
% 13.53/2.48 % (351205)Success in time 1.89 s
% 13.53/2.48 % Vampire exiting
%------------------------------------------------------------------------------