%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW268+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:29:59 PM UTC 2026
% Result : Theorem 27.67s 4.76s
% Output : Refutation 28.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 25
% Syntax : Number of formulae : 166 ( 79 unt; 6 def)
% Number of atoms : 283 ( 181 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 208 ( 91 ~; 87 |; 10 &)
% ( 5 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 4 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-3 aty)
% Number of variables : 234 ( 0 sgn 227 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096_B_By_O_Apoly_A_IpCons_Ac_Acs_J_A0_A_061_Apoly_A_IpCons_Ac_Acs_J_Ay_096) ).
fof(f4,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/sandbox/benchmark/theBenchmark.p',fact_poly__0) ).
fof(f12,axiom,
( ~ ? [X0] :
( X0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
& v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) )
=> ? [X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X1) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pCons_Ohyps) ).
fof(f166,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(f274,axiom,
! [X0,X1,X2] :
( class_Rings_Oring__no__zero__divisors(X2)
=> ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = c_Groups_Ozero__class_Ozero(X2)
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
| X0 = c_Groups_Ozero__class_Ozero(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mult__eq__0__iff) ).
fof(f366,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(f377,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
fof(f385,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f394,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,hAPP(c_Polynomial_Opoly(X3,X2),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__add) ).
fof(f408,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(f473,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> hAPP(c_Polynomial_Opoly(X3,c_Polynomial_OpCons(X3,X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__pCons) ).
fof(f494,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(f589,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Groups_Oplus__class_Oplus(X2,X1,X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__add__cancel) ).
fof(f991,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(f1117,axiom,
class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors) ).
fof(f1125,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(f1126,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(f1136,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(f1212,conjecture,
! [X0] :
( X0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1213,negated_conjecture,
~ ! [X0] :
( X0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(negated_conjecture,[status(cth)],[f1212]) ).
fof(f1245,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,[],[f4]) ).
fof(f1253,plain,
( ? [X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X1) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ? [X0] :
( X0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
& v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f1438,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,[],[f166]) ).
fof(f1556,plain,
! [X0,X1,X2] :
( ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = c_Groups_Ozero__class_Ozero(X2)
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
| X0 = c_Groups_Ozero__class_Ozero(X2) ) )
| ~ class_Rings_Oring__no__zero__divisors(X2) ),
inference(ennf_transformation,[],[f274]) ).
fof(f1709,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,[],[f366]) ).
fof(f1719,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f377]) ).
fof(f1728,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f385]) ).
fof(f1737,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X3,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,hAPP(c_Polynomial_Opoly(X3,X2),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f394]) ).
fof(f1754,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,[],[f408]) ).
fof(f1852,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,[],[f473]) ).
fof(f1876,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,[],[f494]) ).
fof(f1954,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Groups_Oplus__class_Oplus(X2,X1,X0)) = X0
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f589]) ).
fof(f2365,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f991]) ).
fof(f2439,plain,
? [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X0)
& X0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(ennf_transformation,[],[f1213]) ).
fof(f2452,plain,
( ? [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X0)
| ? [X1] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != X1
& v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ) ),
inference(rectify,[],[f1253]) ).
fof(f2453,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK6)
| ( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK7
& v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f2452]) ).
fof(f2565,plain,
! [X0,X1,X2] :
( ( ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = c_Groups_Ozero__class_Ozero(X2)
| ( c_Groups_Ozero__class_Ozero(X2) != X1
& c_Groups_Ozero__class_Ozero(X2) != X0 ) )
& ( X1 = c_Groups_Ozero__class_Ozero(X2)
| X0 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Ozero__class_Ozero(X2) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) ) )
| ~ class_Rings_Oring__no__zero__divisors(X2) ),
inference(nnf_transformation,[],[f1556]) ).
fof(f2566,plain,
! [X0,X1,X2] :
( ( ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) = c_Groups_Ozero__class_Ozero(X2)
| ( c_Groups_Ozero__class_Ozero(X2) != X1
& c_Groups_Ozero__class_Ozero(X2) != X0 ) )
& ( X1 = c_Groups_Ozero__class_Ozero(X2)
| X0 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Ozero__class_Ozero(X2) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0) ) )
| ~ class_Rings_Oring__no__zero__divisors(X2) ),
inference(flattening,[],[f2565]) ).
fof(f2770,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK27)
& c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK27 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X0,sK27)],[f2439]) ).
fof(f2773,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0),
inference(cnf_transformation,[],[f3]) ).
fof(f2774,plain,
! [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) ),
inference(cnf_transformation,[],[f1245]) ).
fof(f2786,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK6)
| v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
inference(cnf_transformation,[],[f2453]) ).
fof(f2787,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK6)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK7 ),
inference(cnf_transformation,[],[f2453]) ).
fof(f3001,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,[],[f1438]) ).
fof(f3167,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(X2) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0)
| c_Groups_Ozero__class_Ozero(X2) = X0
| c_Groups_Ozero__class_Ozero(X2) = X1
| ~ class_Rings_Oring__no__zero__divisors(X2) ),
inference(cnf_transformation,[],[f2566]) ).
fof(f3316,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,[],[f1709]) ).
fof(f3327,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Ozero__class_Ozero(X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),c_Groups_Ozero__class_Ozero(X1)) ),
inference(cnf_transformation,[],[f1719]) ).
fof(f3336,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
inference(cnf_transformation,[],[f1728]) ).
fof(f3345,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__0(X3)
| hAPP(c_Polynomial_Opoly(X3,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),X2,X1)),X0) = c_Groups_Oplus__class_Oplus(X3,hAPP(c_Polynomial_Opoly(X3,X2),X0),hAPP(c_Polynomial_Opoly(X3,X1),X0)) ),
inference(cnf_transformation,[],[f1737]) ).
fof(f3363,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,[],[f1754]) ).
fof(f3448,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,[],[f1852]) ).
fof(f3485,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,[],[f1876]) ).
fof(f3618,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X1),c_Groups_Oplus__class_Oplus(X2,X1,X0)) = X0 ),
inference(cnf_transformation,[],[f1954]) ).
fof(f4104,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f2365]) ).
fof(f4231,plain,
class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1117]) ).
fof(f4239,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1125]) ).
fof(f4240,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1126]) ).
fof(f4250,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[],[f1136]) ).
fof(f4326,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK27,
inference(cnf_transformation,[],[f2770]) ).
fof(f4327,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK27),
inference(cnf_transformation,[],[f2770]) ).
fof(f4691,definition,
sF28 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f4692,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF28,
inference(reorient_equations,[],[f4691]) ).
fof(f4693,definition,
sF29 = c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f4694,plain,
c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____) = sF29,
inference(reorient_equations,[],[f4693]) ).
fof(f4695,definition,
sF30 = hAPP(sF29,sK27),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f4696,plain,
hAPP(sF29,sK27) = sF30,
inference(reorient_equations,[],[f4695]) ).
fof(f4697,plain,
sF28 != sF30,
inference(definition_folding,[],[f4327,f4696,f4694,f4692]) ).
fof(f4698,plain,
sK27 != sF28,
inference(definition_folding,[],[f4326,f4692]) ).
fof(f4754,definition,
( spl31_1
<=> v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
introduced(definition,[new_symbols(definition,[spl31_1])],[avatar_definition]) ).
fof(f4756,plain,
( v_cs____ = c_Polynomial_OpCons(tc_Complex_Ocomplex,sK7,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))
| ~ spl31_1 ),
inference(avatar_component_clause,[],[f4754]) ).
fof(f4758,definition,
( spl31_2
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK6) ),
introduced(definition,[new_symbols(definition,[spl31_2])],[avatar_definition]) ).
fof(f4760,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),sK6)
| ~ spl31_2 ),
inference(avatar_component_clause,[],[f4758]) ).
fof(f4761,plain,
( spl31_1
| spl31_2 ),
inference(avatar_split_clause,[],[f2786,f4758,f4754]) ).
fof(f4763,definition,
( spl31_3
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = sK7 ),
introduced(definition,[new_symbols(definition,[spl31_3])],[avatar_definition]) ).
fof(f4765,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sK7
| spl31_3 ),
inference(avatar_component_clause,[],[f4763]) ).
fof(f4766,plain,
( ~ spl31_3
| spl31_2 ),
inference(avatar_split_clause,[],[f2787,f4758,f4763]) ).
fof(f4802,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(sF29,sK6)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f4760,f4694]) ).
fof(f4804,plain,
( sF28 = hAPP(sF29,sK6)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f4802,f4692]) ).
fof(f4805,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,[],[f4240,f3448]) ).
fof(f4806,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,[],[f4240,f3001]) ).
fof(f4808,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(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X2,X1)),X2)),
inference(forward_demodulation,[],[f4805,f4806]) ).
fof(f4809,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,v_cs____)),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(sF29,X1)),
inference(superposition,[],[f4806,f4694]) ).
fof(f4810,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,v_cs____)),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(sF29,X0))),
inference(superposition,[],[f4808,f4809]) ).
fof(f4822,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X0),
inference(resolution,[],[f3336,f4239]) ).
fof(f4826,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X0),X2) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X2,X1)),X0),
inference(superposition,[],[f4808,f4822]) ).
fof(f4846,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,[],[f3316,f4239]) ).
fof(f4916,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,[],[f2774,f4240]) ).
fof(f4917,plain,
! [X0] : sF28 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0),
inference(forward_demodulation,[],[f4916,f4692]) ).
fof(f4922,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF28),
inference(superposition,[],[f4806,f4917]) ).
fof(f4930,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sK6),sF28))
| ~ spl31_2 ),
inference(superposition,[],[f4810,f4804]) ).
fof(f4937,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF28),sK6))
| ~ spl31_2 ),
inference(forward_demodulation,[],[f4930,f4846]) ).
fof(f4938,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,[],[f3327,f4239]) ).
fof(f4939,plain,
! [X0] : sF28 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF28),
inference(forward_demodulation,[],[f4938,f4692]) ).
fof(f4943,plain,
! [X0] : sF28 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF28),X0),
inference(superposition,[],[f4846,f4939]) ).
fof(f4950,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sF28) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,sF28),
inference(superposition,[],[f4810,f4943]) ).
fof(f4953,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,X1)),X2) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),
inference(resolution,[],[f3345,f4240]) ).
fof(f4962,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1),sF28),
inference(superposition,[],[f4953,f4917]) ).
fof(f4977,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,sF28,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X1),
inference(forward_demodulation,[],[f4962,f4822]) ).
fof(f5005,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X0,
inference(resolution,[],[f3363,f4239]) ).
fof(f5006,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,sF28) = X0,
inference(forward_demodulation,[],[f5005,f4692]) ).
fof(f5011,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,sF28,X0) = X0,
inference(superposition,[],[f4822,f5006]) ).
fof(f5012,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X0) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,X1)),X0),
inference(superposition,[],[f4826,f5006]) ).
fof(f5018,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(sF29,X0)) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0),
inference(superposition,[],[f4810,f5011]) ).
fof(f5143,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,sF28)
| ~ spl31_2 ),
inference(superposition,[],[f4937,f4943]) ).
fof(f5160,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6) = X0
| ~ spl31_2 ),
inference(forward_demodulation,[],[f5143,f5006]) ).
fof(f5200,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____),X0)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)),
inference(superposition,[],[f4953,f2773]) ).
fof(f5209,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____),X0)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),sF28),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)),
inference(forward_demodulation,[],[f5200,f4692]) ).
fof(f5227,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____),X0)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,sF28),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)),
inference(forward_demodulation,[],[f5209,f4950]) ).
fof(f5242,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____),X0)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)),
inference(forward_demodulation,[],[f5227,f5006]) ).
fof(f5353,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,sF28,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0)) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)),
inference(superposition,[],[f4977,f5242]) ).
fof(f5369,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,sF28) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,sF28,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0)),
inference(forward_demodulation,[],[f5353,f4917]) ).
fof(f5372,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,sF28),
inference(forward_demodulation,[],[f5369,f5011]) ).
fof(f5374,plain,
! [X0] : v_c____ = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0),
inference(forward_demodulation,[],[f5372,f5006]) ).
fof(f5776,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sF28)),
inference(superposition,[],[f4808,f4922]) ).
fof(f5806,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,sF28),
inference(forward_demodulation,[],[f5776,f4939]) ).
fof(f5823,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),X0) = X1,
inference(forward_demodulation,[],[f5806,f5006]) ).
fof(f5872,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Oone__class_Oone(tc_Complex_Ocomplex)),X0) = X0,
inference(resolution,[],[f3485,f4239]) ).
fof(f7027,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,v_cs____)),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0)),
inference(superposition,[],[f4810,f5018]) ).
fof(f7150,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1),X1) = X0,
inference(resolution,[],[f4104,f4250]) ).
fof(f7151,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)) = X0,
inference(forward_demodulation,[],[f7150,f4822]) ).
fof(f7196,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,X1)) = X1,
inference(resolution,[],[f3618,f4250]) ).
fof(f7199,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X2,X1)),X2) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2)),
inference(superposition,[],[f7196,f4808]) ).
fof(f7200,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),X1)),
inference(superposition,[],[f7196,f7027]) ).
fof(f7202,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF28),sK6) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6))
| ~ spl31_2 ),
inference(superposition,[],[f7196,f4937]) ).
fof(f7203,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1),X0),
inference(superposition,[],[f7196,f7151]) ).
fof(f7215,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF28),sK6) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),sK6),X0)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7202,f7203]) ).
fof(f7217,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X1) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),X1),X0),
inference(forward_demodulation,[],[f7200,f7203]) ).
fof(f7218,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X2,X1)),X2) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2),X0),
inference(forward_demodulation,[],[f7199,f7203]) ).
fof(f7222,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),sF28),sK6) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7215,f5160]) ).
fof(f7223,plain,
! [X2,X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,X1)),X2) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),X2),X0),
inference(forward_demodulation,[],[f7218,f5012]) ).
fof(f7224,plain,
( ! [X0] : sF28 = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7222,f4943]) ).
fof(f7280,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_c____,v_c____),
inference(superposition,[],[f7223,f5374]) ).
fof(f7290,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0),v_c____) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(superposition,[],[f7223,f2773]) ).
fof(f7298,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),sF28) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),X0),v_c____),
inference(forward_demodulation,[],[f7290,f4692]) ).
fof(f7306,plain,
( ! [X0] : sF28 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0)
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7280,f7224]) ).
fof(f7307,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),sF28),
inference(forward_demodulation,[],[f7298,f7217]) ).
fof(f7311,plain,
! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,sF28,sF28),
inference(forward_demodulation,[],[f7307,f4950]) ).
fof(f7313,plain,
! [X0] : sF28 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0),
inference(forward_demodulation,[],[f7311,f5006]) ).
fof(f7317,plain,
( ! [X0] : sF28 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(sF29,X0))
| ~ spl31_2 ),
inference(superposition,[],[f5018,f7306]) ).
fof(f7393,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF28
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(sF29,X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| ~ class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex) )
| ~ spl31_2 ),
inference(superposition,[],[f3167,f7317]) ).
fof(f7394,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(sF29,X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| ~ class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex) )
| ~ spl31_2 ),
inference(forward_subsumption_resolution,[],[f7393,f4692]) ).
fof(f7397,plain,
( ! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(sF29,X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 )
| ~ spl31_2 ),
inference(forward_subsumption_resolution,[],[f7394,f4231]) ).
fof(f7398,plain,
( ! [X0] :
( sF28 = hAPP(sF29,X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 )
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7397,f4692]) ).
fof(f7399,plain,
( ! [X0] :
( sF28 = hAPP(sF29,X0)
| sF28 = X0 )
| ~ spl31_2 ),
inference(forward_demodulation,[],[f7398,f4692]) ).
fof(f7400,plain,
( sF28 = sF30
| sK27 = sF28
| ~ spl31_2 ),
inference(superposition,[],[f7399,f4696]) ).
fof(f7427,plain,
( sK27 = sF28
| ~ spl31_2 ),
inference(forward_subsumption_resolution,[],[f7400,f4697]) ).
fof(f7434,plain,
( $false
| ~ spl31_2 ),
inference(forward_subsumption_resolution,[],[f7427,f4698]) ).
fof(f7435,plain,
~ spl31_2,
inference(avatar_contradiction_clause,[],[f7434]) ).
fof(f7437,plain,
( sK7 != sF28
| spl31_3 ),
inference(forward_demodulation,[],[f4765,f4692]) ).
fof(f7444,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,sF28),
inference(superposition,[],[f7027,f7313]) ).
fof(f7474,plain,
! [X0,X1] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,v_cs____)),X1) = X0,
inference(forward_demodulation,[],[f7444,f5006]) ).
fof(f7514,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),X0) = sK7
| ~ spl31_1 ),
inference(superposition,[],[f5823,f4756]) ).
fof(f7527,plain,
( ! [X0] : sK7 = hAPP(sF29,X0)
| ~ spl31_1 ),
inference(forward_demodulation,[],[f7514,f4694]) ).
fof(f7540,plain,
( ! [X0] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,sF28,v_cs____)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sK7)
| ~ spl31_1 ),
inference(superposition,[],[f5018,f7527]) ).
fof(f7553,plain,
( ! [X0] : sF28 = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),sK7)
| ~ spl31_1 ),
inference(forward_demodulation,[],[f7540,f7474]) ).
fof(f7560,plain,
( sK7 = sF28
| ~ spl31_1 ),
inference(superposition,[],[f7553,f5872]) ).
fof(f7570,plain,
( $false
| ~ spl31_1
| spl31_3 ),
inference(forward_subsumption_resolution,[],[f7560,f7437]) ).
fof(f7571,plain,
( ~ spl31_1
| spl31_3 ),
inference(avatar_contradiction_clause,[],[f7570]) ).
cnf(s1,plain,
( spl31_1
| spl31_2 ),
inference(sat_conversion,[],[f4761]) ).
cnf(s2,plain,
( spl31_2
| ~ spl31_3 ),
inference(sat_conversion,[],[f4766]) ).
cnf(s19,plain,
~ spl31_2,
inference(sat_conversion,[],[f7435]) ).
cnf(s21,plain,
( ~ spl31_1
| spl31_3 ),
inference(sat_conversion,[],[f7571]) ).
cnf(s22,plain,
~ spl31_3,
inference(rat,[],[s2,s19]) ).
cnf(s23,plain,
~ spl31_1,
inference(rat,[],[s21,s22]) ).
cnf(s24,plain,
$false,
inference(rat,[],[s1,s19,s23]) ).
fof(f7575,plain,
$false,
inference(avatar_sat_refutation,[],[s24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW268+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.25 % Computer : n001.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Mon Sep 28 13:31:18 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.31 Running first-order theorem proving
% 0.23/0.31 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
% 27.07/4.66 % (352209)Detected formulas, will run a generic FOF schedule.
% 27.07/4.66 % (352221)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1348069006:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 27.07/4.66 % (352216)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=709573771:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 27.07/4.66 % (352221)Instruction limit reached!
% 27.07/4.66 % (352221)------------------------------
% 27.07/4.66 % (352221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.07/4.66 % (352221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.07/4.66 % (352221)CaDiCaL version: 2.1.3
% 27.07/4.66 % (352221)Termination reason: Instruction limit
% 27.07/4.66 % (352221)Termination phase: Saturation
% 27.07/4.66 % (352221)Time elapsed: 0.078 s
% 27.07/4.66 % (352221)Peak memory usage: 91 MB
% 27.07/4.66 % (352221)Instructions burned: 140 (million)
% 27.07/4.66 % (352219)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3241868464:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 27.07/4.66 % (352218)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=3862362487:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 27.07/4.66 % (352217)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=3212794894:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 27.07/4.66 % (352219)Refutation not found, incomplete strategy
% 27.07/4.66 % (352219)------------------------------
% 27.07/4.66 % (352219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.07/4.66 % (352219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.07/4.66 % (352219)CaDiCaL version: 2.1.3
% 27.07/4.66 % (352219)Termination reason: Refutation not found, incomplete strategy
% 27.07/4.66 % (352219)Time elapsed: 0.008 s
% 27.07/4.66 % (352219)Peak memory usage: 89 MB
% 27.07/4.66 % (352219)Instructions burned: 5 (million)
% 27.07/4.66 % (352222)dis-21_1_sil=8000:lcm=predicate:random_seed=4114831796: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)
% 27.07/4.66 % (352220)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1943393031:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 27.07/4.66 % (352220)Instruction limit reached!
% 27.07/4.66 % (352220)------------------------------
% 27.07/4.66 % (352220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.07/4.66 % (352220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.07/4.66 % (352220)CaDiCaL version: 2.1.3
% 27.07/4.66 % (352220)Termination reason: Instruction limit
% 27.07/4.66 % (352220)Termination phase: Saturation
% 27.07/4.66 % (352220)Time elapsed: 0.118 s
% 27.07/4.66 % (352220)Peak memory usage: 89 MB
% 27.07/4.66 % (352220)Instructions burned: 120 (million)
% 27.07/4.66 % (352222)Instruction limit reached!
% 27.07/4.66 % (352222)------------------------------
% 27.07/4.66 % (352222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.07/4.66 % (352222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.07/4.66 % (352222)CaDiCaL version: 2.1.3
% 27.07/4.66 % (352222)Termination reason: Instruction limit
% 27.07/4.66 % (352222)Termination phase: Saturation
% 27.07/4.66 % (352222)Time elapsed: 0.120 s
% 27.07/4.66 % (352222)Peak memory usage: 91 MB
% 27.07/4.66 % (352222)Instructions burned: 129 (million)
% 27.07/4.66 % (352225)lrs+10_1_sil=8000:sp=occurrence:random_seed=1593743987:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 27.07/4.66 % (352231)lrs+10_1_sil=32000:urr=on:br=off:random_seed=740828630:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 27.07/4.66 % (352219)------------------------------
% 27.07/4.66 % (352219)------------------------------
% 27.07/4.66 % (352232)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3497500036:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 27.07/4.66 % (352231)Instruction limit reached!
% 27.07/4.66 % (352231)------------------------------
% 27.07/4.66 % (352231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.07/4.66 % (352231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352231)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352231)Termination reason: Instruction limit
% 27.67/4.76 % (352231)Termination phase: Saturation
% 27.67/4.76 % (352231)Time elapsed: 0.147 s
% 27.67/4.76 % (352231)Peak memory usage: 92 MB
% 27.67/4.76 % (352231)Instructions burned: 157 (million)
% 27.67/4.76 % (352225)Instruction limit reached!
% 27.67/4.76 % (352225)------------------------------
% 27.67/4.76 % (352225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352225)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352225)Termination reason: Instruction limit
% 27.67/4.76 % (352225)Termination phase: Saturation
% 27.67/4.76 % (352225)Time elapsed: 0.306 s
% 27.67/4.76 % (352225)Peak memory usage: 92 MB
% 27.67/4.76 % (352225)Instructions burned: 286 (million)
% 27.67/4.76 % (352235)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=1687008434:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 27.67/4.76 % (352232)Instruction limit reached!
% 27.67/4.76 % (352232)------------------------------
% 27.67/4.76 % (352232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352232)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352232)Termination reason: Instruction limit
% 27.67/4.76 % (352232)Termination phase: Saturation
% 27.67/4.76 % (352232)Time elapsed: 0.301 s
% 27.67/4.76 % (352232)Peak memory usage: 93 MB
% 27.67/4.76 % (352232)Instructions burned: 325 (million)
% 27.67/4.76 % (352237)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1553890924:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 27.67/4.76 % (352237)Refutation not found, incomplete strategy
% 27.67/4.76 % (352237)------------------------------
% 27.67/4.76 % (352237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352237)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352237)Termination reason: Refutation not found, incomplete strategy
% 27.67/4.76 % (352237)Time elapsed: 0.051 s
% 27.67/4.76 % (352237)Peak memory usage: 91 MB
% 27.67/4.76 % (352237)Instructions burned: 78 (million)
% 27.67/4.76 % (352238)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1217659292:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 27.67/4.76 % (352235)Instruction limit reached!
% 27.67/4.76 % (352235)------------------------------
% 27.67/4.76 % (352235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352235)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352235)Termination reason: Instruction limit
% 27.67/4.76 % (352235)Termination phase: Saturation
% 27.67/4.76 % (352235)Time elapsed: 0.228 s
% 27.67/4.76 % (352235)Peak memory usage: 93 MB
% 27.67/4.76 % (352235)Instructions burned: 249 (million)
% 27.67/4.76 % (352240)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2172557768:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 27.67/4.76 % (352240)Instruction limit reached!
% 27.67/4.76 % (352240)------------------------------
% 27.67/4.76 % (352240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352240)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352240)Termination reason: Instruction limit
% 27.67/4.76 % (352240)Termination phase: Saturation
% 27.67/4.76 % (352240)Time elapsed: 0.100 s
% 27.67/4.76 % (352240)Peak memory usage: 90 MB
% 27.67/4.76 % (352240)Instructions burned: 113 (million)
% 27.67/4.76 % (352243)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1489612957:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 27.67/4.76 % (352237)------------------------------
% 27.67/4.76 % (352237)------------------------------
% 27.67/4.76 % (352243)Refutation not found, incomplete strategy
% 27.67/4.76 % (352243)------------------------------
% 27.67/4.76 % (352243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352243)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352243)Termination reason: Refutation not found, incomplete strategy
% 27.67/4.76 % (352243)Time elapsed: 0.100 s
% 27.67/4.76 % (352243)Peak memory usage: 90 MB
% 27.67/4.76 % (352243)Instructions burned: 114 (million)
% 27.67/4.76 % (352245)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2942400918:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 27.67/4.76 % (352245)Instruction limit reached!
% 27.67/4.76 % (352245)------------------------------
% 27.67/4.76 % (352245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352245)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352245)Termination reason: Instruction limit
% 27.67/4.76 % (352245)Termination phase: Saturation
% 27.67/4.76 % (352245)Time elapsed: 0.106 s
% 27.67/4.76 % (352245)Peak memory usage: 90 MB
% 27.67/4.76 % (352245)Instructions burned: 114 (million)
% 27.67/4.76 % (352247)lrs+10_1_sil=8000:sp=occurrence:random_seed=1756997706:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 27.67/4.76 % (352243)------------------------------
% 27.67/4.76 % (352243)------------------------------
% 27.67/4.76 % (352250)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2604777368:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 27.67/4.76 % (352251)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2280979679:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 27.67/4.76 % (352250)Instruction limit reached!
% 27.67/4.76 % (352250)------------------------------
% 27.67/4.76 % (352250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352250)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352250)Termination reason: Instruction limit
% 27.67/4.76 % (352250)Termination phase: Saturation
% 27.67/4.76 % (352250)Time elapsed: 0.402 s
% 27.67/4.76 % (352250)Peak memory usage: 96 MB
% 27.67/4.76 % (352250)Instructions burned: 437 (million)
% 27.67/4.76 % (352256)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=636057495:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 27.67/4.76 % (352247)Instruction limit reached!
% 27.67/4.76 % (352247)------------------------------
% 27.67/4.76 % (352247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352247)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352247)Termination reason: Instruction limit
% 27.67/4.76 % (352247)Termination phase: Saturation
% 27.67/4.76 % (352247)Time elapsed: 0.885 s
% 27.67/4.76 % (352247)Peak memory usage: 96 MB
% 27.67/4.76 % (352247)Instructions burned: 907 (million)
% 27.67/4.76 % (352256)Instruction limit reached!
% 27.67/4.76 % (352256)------------------------------
% 27.67/4.76 % (352256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352256)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352256)Termination reason: Instruction limit
% 27.67/4.76 % (352256)Termination phase: Saturation
% 27.67/4.76 % (352256)Time elapsed: 0.117 s
% 27.67/4.76 % (352256)Peak memory usage: 92 MB
% 27.67/4.76 % (352256)Instructions burned: 134 (million)
% 27.67/4.76 % (352258)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2353277041:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 27.67/4.76 % (352259)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2784703602:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 27.67/4.76 % (352238)First to succeed.
% 27.67/4.76 % (352238)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-352209"
% 27.67/4.76 % (352258)Instruction limit reached!
% 27.67/4.76 % (352258)------------------------------
% 27.67/4.76 % (352258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.67/4.76 % (352258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.67/4.76 % (352258)CaDiCaL version: 2.1.3
% 27.67/4.76 % (352258)Termination reason: Instruction limit
% 27.67/4.76 % (352258)Termination phase: Saturation
% 27.67/4.76 % (352258)Time elapsed: 0.603 s
% 27.67/4.76 % (352258)Peak memory usage: 97 MB
% 27.67/4.76 % (352258)Instructions burned: 592 (million)
% 27.67/4.76 % (352264)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=3133255657:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/125Mi)
% 27.67/4.76 % (352238)Refutation found. Thanks to Tanya!
% 27.67/4.76 % SZS status Theorem for theBenchmark
% 27.67/4.76 % SZS output start Proof for theBenchmark
% See solution above
% 28.51/5.01 % (352238)------------------------------
% 28.51/5.01 % (352238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.51/5.01 % (352238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.51/5.01 % (352238)CaDiCaL version: 2.1.3
% 28.51/5.01 % (352238)Termination reason: Refutation
% 28.51/5.01 % (352238)Time elapsed: 2.370 s
% 28.51/5.01 % (352238)Peak memory usage: 149 MB
% 28.51/5.01 % (352238)Instructions burned: 2201 (million)
% 28.51/5.01 % (352238)------------------------------
% 28.51/5.01 % (352238)------------------------------
% 28.51/5.01 % (352209)Success in time 4.013 s
% 28.51/5.01 % Vampire exiting
%------------------------------------------------------------------------------