%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW287+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:39:45 PM UTC 2026
% Result : Theorem 1.16s 0.34s
% Output : Refutation 1.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of formulae : 89 ( 23 unt; 9 def)
% Number of atoms : 205 ( 82 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 198 ( 82 ~; 92 |; 5 &)
% ( 11 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 10 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 22 ( 0 sgn 20 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
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(f3,axiom,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_dp) ).
fof(f4,axiom,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Nat_OSuc(v_n____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_n) ).
fof(f6,axiom,
! [X0] :
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))
=> ( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096_B_Bx_O_A_091_124_Ap_Advd_Aq_A_094_ASuc_An_059_Apoly_Ap_Ax_A_061_A0_059_Apoly_Aq_Ax_A_126_061_A0_A_124_093_A_061_061_062_AFalse_096) ).
fof(f7,axiom,
( ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
=> ( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096_091_124_AALL_Ax_O_Apoly_Ap_Ax_A_061_A0_A_N_N_062_Apoly_Aq_Ax_A_061_A0_059_Adegree_Ap_A_061_Adegree_Ap_059_Adegree_Ap_A_126_061_A0_A_124_093_061_061_062_Ap_Advd_Aq_A_094_Adegree_Ap_096) ).
fof(f317,axiom,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__eq__plus1__left) ).
fof(f392,axiom,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__add__commute) ).
fof(f1206,conjecture,
( ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
<=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
& v_q = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1207,negated_conjecture,
~ ( ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
<=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
& v_q = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1206]) ).
fof(f1257,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____)))) ),
inference(ennf_transformation,[],[f6]) ).
fof(f1258,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____)))) ),
inference(flattening,[],[f1257]) ).
fof(f1259,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ? [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)
& hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f1260,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ? [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)
& hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ),
inference(flattening,[],[f1259]) ).
fof(f2424,plain,
( ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
<~> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
& v_q = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ) ) ),
inference(ennf_transformation,[],[f1207]) ).
fof(f2426,plain,
v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[],[f2]) ).
fof(f2427,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[],[f3]) ).
fof(f2428,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Nat_OSuc(v_n____),
inference(cnf_transformation,[],[f4]) ).
fof(f2433,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ),
inference(cnf_transformation,[],[f1258]) ).
fof(f2434,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2)
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ),
inference(cnf_transformation,[],[f1260]) ).
fof(f2435,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2)
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ),
inference(cnf_transformation,[],[f1260]) ).
fof(f2847,plain,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
inference(cnf_transformation,[],[f317]) ).
fof(f2953,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1),
inference(cnf_transformation,[],[f392]) ).
fof(f3949,plain,
! [X0] :
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f3950,plain,
( ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f3951,plain,
( ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f3952,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),v_n____),
inference(definition_unfolding,[],[f2428,f2847]) ).
fof(f3953,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),v_n____))))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ),
inference(definition_unfolding,[],[f2433,f2847]) ).
fof(f4339,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),v_n____))))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ),
inference(consistent_polarity_flipping,[],[f3953]) ).
fof(f4340,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2)
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ),
inference(consistent_polarity_flipping,[],[f2435]) ).
fof(f4341,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2)
| c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ),
inference(consistent_polarity_flipping,[],[f2434]) ).
fof(f5302,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19) ),
inference(consistent_polarity_flipping,[],[f3951]) ).
fof(f5303,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19) ),
inference(consistent_polarity_flipping,[],[f3950]) ).
fof(f5304,plain,
! [X0] :
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ),
inference(consistent_polarity_flipping,[],[f3949]) ).
fof(f5309,definition,
( spl20_1
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f5311,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19)
| spl20_1 ),
inference(avatar_component_clause,[],[f5309]) ).
fof(f5313,definition,
( spl20_2
<=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f5322,definition,
( spl20_4
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f5324,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19)
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f5322]) ).
fof(f5327,definition,
( spl20_5
<=> ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f5328,plain,
( ! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0) )
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f5327]) ).
fof(f5330,definition,
( spl20_6
<=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f5332,plain,
( ~ hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| spl20_6 ),
inference(avatar_component_clause,[],[f5330]) ).
fof(f5334,plain,
( spl20_5
| ~ spl20_6
| spl20_2 ),
inference(avatar_split_clause,[],[f5304,f5313,f5330,f5327]) ).
fof(f5335,plain,
( spl20_4
| spl20_6 ),
inference(avatar_split_clause,[],[f5303,f5330,f5322]) ).
fof(f5336,plain,
( ~ spl20_1
| spl20_6 ),
inference(avatar_split_clause,[],[f5302,f5330,f5309]) ).
fof(f5352,definition,
( spl20_10
<=> c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f5366,definition,
( spl20_12
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f5368,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2)
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f5366]) ).
fof(f5369,plain,
( ~ spl20_6
| spl20_10
| spl20_12 ),
inference(avatar_split_clause,[],[f4341,f5366,f5352,f5330]) ).
fof(f5371,definition,
( spl20_13
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f5374,plain,
( ~ spl20_6
| spl20_10
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f4340,f5371,f5352,f5330]) ).
fof(f5376,definition,
( spl20_14
<=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),v_n____)))) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f5378,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),v_n____))))
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f5376]) ).
fof(f5379,plain,
( spl20_5
| spl20_14 ),
inference(avatar_split_clause,[],[f4339,f5376,f5327]) ).
fof(f5392,plain,
~ spl20_10,
inference(avatar_split_clause,[],[f2427,f5352]) ).
fof(f5393,plain,
~ spl20_2,
inference(avatar_split_clause,[],[f2426,f5313]) ).
fof(f5394,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19)
| ~ spl20_4
| ~ spl20_5 ),
inference(superposition,[],[f5328,f5324]) ).
fof(f5395,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19)
| ~ spl20_4
| ~ spl20_5 ),
inference(trivial_inequality_removal,[],[f5394]) ).
fof(f5396,plain,
( $false
| spl20_1
| ~ spl20_4
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f5395,f5311]) ).
fof(f5397,plain,
( spl20_1
| ~ spl20_4
| ~ spl20_5 ),
inference(avatar_contradiction_clause,[],[f5396]) ).
fof(f5430,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2)
| ~ spl20_5
| ~ spl20_12 ),
inference(superposition,[],[f5328,f5368]) ).
fof(f5431,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2)
| ~ spl20_5
| ~ spl20_12 ),
inference(trivial_inequality_removal,[],[f5430]) ).
fof(f5432,plain,
( spl20_13
| ~ spl20_5
| ~ spl20_12 ),
inference(avatar_split_clause,[],[f5431,f5366,f5327,f5371]) ).
fof(f5540,plain,
c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_n____,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(superposition,[],[f3952,f2953]) ).
fof(f14399,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_n____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))))
| ~ spl20_14 ),
inference(forward_demodulation,[],[f5378,f2953]) ).
fof(f14400,plain,
( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))
| ~ spl20_14 ),
inference(forward_demodulation,[],[f14399,f5540]) ).
fof(f14401,plain,
( $false
| spl20_6
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f14400,f5332]) ).
fof(f14402,plain,
( spl20_6
| ~ spl20_14 ),
inference(avatar_contradiction_clause,[],[f14401]) ).
cnf(s4,plain,
( spl20_2
| spl20_5
| ~ spl20_6 ),
inference(sat_conversion,[],[f5334]) ).
cnf(s5,plain,
( spl20_4
| spl20_6 ),
inference(sat_conversion,[],[f5335]) ).
cnf(s6,plain,
( ~ spl20_1
| spl20_6 ),
inference(sat_conversion,[],[f5336]) ).
cnf(s15,plain,
( ~ spl20_6
| spl20_10
| spl20_12 ),
inference(sat_conversion,[],[f5369]) ).
cnf(s16,plain,
( ~ spl20_6
| spl20_10
| ~ spl20_13 ),
inference(sat_conversion,[],[f5374]) ).
cnf(s17,plain,
( spl20_5
| spl20_14 ),
inference(sat_conversion,[],[f5379]) ).
cnf(s22,plain,
~ spl20_10,
inference(sat_conversion,[],[f5392]) ).
cnf(s23,plain,
~ spl20_2,
inference(sat_conversion,[],[f5393]) ).
cnf(s24,plain,
( spl20_1
| ~ spl20_4
| ~ spl20_5 ),
inference(sat_conversion,[],[f5397]) ).
cnf(s25,plain,
( ~ spl20_5
| ~ spl20_12
| spl20_13 ),
inference(sat_conversion,[],[f5432]) ).
cnf(s154,plain,
( spl20_6
| ~ spl20_14 ),
inference(sat_conversion,[],[f14402]) ).
cnf(s155,plain,
( ~ spl20_6
| ~ spl20_13 ),
inference(rat,[],[s16,s22]) ).
cnf(s156,plain,
( ~ spl20_6
| spl20_12 ),
inference(rat,[],[s15,s22]) ).
cnf(s158,plain,
( spl20_5
| ~ spl20_6 ),
inference(rat,[],[s4,s23]) ).
cnf(s159,plain,
~ spl20_6,
inference(rat,[],[s25,s158,s156,s155]) ).
cnf(s160,plain,
~ spl20_14,
inference(rat,[],[s154,s159]) ).
cnf(s161,plain,
spl20_4,
inference(rat,[],[s5,s159]) ).
cnf(s162,plain,
spl20_5,
inference(rat,[],[s17,s160]) ).
cnf(s163,plain,
spl20_1,
inference(rat,[],[s24,s161,s162]) ).
cnf(s164,plain,
$false,
inference(rat,[],[s6,s159,s163]) ).
fof(f14403,plain,
$false,
inference(avatar_sat_refutation,[],[s164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW287+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 13:29:49 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.12 Running first-order model finding
% 0.08/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.16/0.34 % (3377015)Will run a generic schedule for satisfiability detection.
% 1.16/0.34 % (3377021)% WARNING: option uhcvi not known.
% 1.16/0.34 % (3377025)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2254712909:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.16/0.34 % (3377022)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4141790496:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.16/0.34 % (3377021)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1794604053:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.16/0.34 % (3377020)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2151503423_2999 on theBenchmark for (2999ds/0Mi)
% 1.16/0.34 % (3377023)dis+10_1_sil=32000:sp=arity:random_seed=2170039765:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.16/0.34 % (3377024)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=11438158:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.16/0.34 % (3377026)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3669933112:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.16/0.34 % (3377023)Instruction limit reached!
% 1.16/0.34 % (3377023)------------------------------
% 1.16/0.34 % (3377023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377023)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377023)Termination reason: Instruction limit
% 1.16/0.34 % (3377023)Termination phase: Saturation
% 1.16/0.34 % (3377023)Time elapsed: 0.028 s
% 1.16/0.34 % (3377023)Peak memory usage: 14 MB
% 1.16/0.34 % (3377023)Instructions burned: 103 (million)
% 1.16/0.34 % (3377024)Instruction limit reached!
% 1.16/0.34 % (3377024)------------------------------
% 1.16/0.34 % (3377024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377024)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377024)Termination reason: Instruction limit
% 1.16/0.34 % (3377024)Termination phase: Saturation
% 1.16/0.34 % (3377024)Time elapsed: 0.030 s
% 1.16/0.34 % (3377024)Peak memory usage: 14 MB
% 1.16/0.34 % (3377024)Instructions burned: 116 (million)
% 1.16/0.34 % (3377025)Instruction limit reached!
% 1.16/0.34 % (3377025)------------------------------
% 1.16/0.34 % (3377025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377025)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377025)Termination reason: Instruction limit
% 1.16/0.34 % (3377025)Termination phase: Saturation
% 1.16/0.34 % (3377025)Time elapsed: 0.039 s
% 1.16/0.34 % (3377025)Peak memory usage: 15 MB
% 1.16/0.34 % (3377025)Instructions burned: 139 (million)
% 1.16/0.34 % (3377034)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1344184660:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.16/0.34 % (3377035)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1856167928:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.16/0.34 % (3377026)Instruction limit reached!
% 1.16/0.34 % (3377026)------------------------------
% 1.16/0.34 % (3377026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377026)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377026)Termination reason: Instruction limit
% 1.16/0.34 % (3377026)Termination phase: Saturation
% 1.16/0.34 % (3377026)Time elapsed: 0.049 s
% 1.16/0.34 % (3377026)Peak memory usage: 16 MB
% 1.16/0.34 % (3377026)Instructions burned: 160 (million)
% 1.16/0.34 % (3377036)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4184704303:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.16/0.34 % (3377039)ott-21_1_sil=16000:fs=off:random_seed=956148525:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.16/0.34 % (3377035)Instruction limit reached!
% 1.16/0.34 % (3377035)------------------------------
% 1.16/0.34 % (3377035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377035)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377035)Termination reason: Instruction limit
% 1.16/0.34 % (3377035)Termination phase: Saturation
% 1.16/0.34 % (3377035)Time elapsed: 0.033 s
% 1.16/0.34 % (3377035)Peak memory usage: 14 MB
% 1.16/0.34 % (3377035)Instructions burned: 131 (million)
% 1.16/0.34 % (3377042)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2064629317:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.16/0.34 % (3377039)Instruction limit reached!
% 1.16/0.34 % (3377039)------------------------------
% 1.16/0.34 % (3377039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377039)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377039)Termination reason: Instruction limit
% 1.16/0.34 % (3377039)Termination phase: Saturation
% 1.16/0.34 % (3377039)Time elapsed: 0.048 s
% 1.16/0.34 % (3377039)Peak memory usage: 15 MB
% 1.16/0.34 % (3377039)Instructions burned: 182 (million)
% 1.16/0.34 % (3377044)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=731781179:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.16/0.34 % (3377021) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3377015-3377021"...
% 1.16/0.34 % (3377021)...printing done.
% 1.16/0.34 % (3377021)Refutation found. Thanks to Tanya!
% 1.16/0.34 % SZS status Theorem for theBenchmark
% 1.16/0.34 % SZS output start Proof for theBenchmark
% See solution above
% 1.16/0.34 % (3377021)------------------------------
% 1.16/0.34 % (3377021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.34 % (3377021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.34 % (3377021)CaDiCaL version: 2.1.3
% 1.16/0.34 % (3377021)Termination reason: Refutation
% 1.16/0.34 % (3377021)Time elapsed: 0.156 s
% 1.16/0.34 % (3377021)Peak memory usage: 18 MB
% 1.16/0.34 % (3377021)Instructions burned: 468 (million)
% 1.16/0.34 % (3377015)Success in time 0.216 s
% 1.16/0.34 % Vampire exiting
%------------------------------------------------------------------------------