%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW278+1 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:31:02 PM UTC 2026
% Result : Theorem 8.70s 6.12s
% Output : CNFRefutation 8.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 49 ( 26 unt; 0 def)
% Number of atoms : 91 ( 56 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 71 ( 29 ~; 29 |; 4 &)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-3 aty)
% Number of variables : 75 ( 9 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_smult__eq__0__iff,axiom,
! [X7,X9,X5] :
( class_Rings_Oidom(X5)
=> ( c_Polynomial_Osmult(X5,X9,X7) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5))
<=> ( X9 = c_Groups_Ozero__class_Ozero(X5)
| X7 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_smult__eq__0__iff) ).
fof(fact_add__poly__code_I2_J,axiom,
! [X12,X5] :
( class_Groups_Ocomm__monoid__add(X5)
=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X5),X12,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5))) = X12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__poly__code_I2_J) ).
fof(fact_synthetic__div__unique,axiom,
! [X52,X11,X24,X12,X5] :
( class_Rings_Ocomm__semiring__0(X5)
=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X5),X12,c_Polynomial_Osmult(X5,X24,X11)) = c_Polynomial_OpCons(X5,X52,X11)
=> ( X52 = hAPP(c_Polynomial_Opoly(X5,X12),X24)
& X11 = c_Polynomial_Osynthetic__div(X5,X12,X24) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_synthetic__div__unique) ).
fof(arity_Complex__Ocomplex__Rings_Oidom,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oidom) ).
fof(arity_Complex__Ocomplex__Groups_Ocomm__monoid__add,axiom,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ocomm__monoid__add) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__0,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(fact_one__poly__def,axiom,
! [X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X5)) = c_Polynomial_OpCons(X5,c_Groups_Oone__class_Oone(X5),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_one__poly__def) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,axiom,
! [X15,X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X5),X15),c_Groups_Ozero__class_Ozero(X5)) = c_Groups_Ozero__class_Ozero(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
fof(fact_synthetic__div__correct,axiom,
! [X24,X12,X5] :
( class_Rings_Ocomm__semiring__0(X5)
=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X5),X12,c_Polynomial_Osmult(X5,X24,c_Polynomial_Osynthetic__div(X5,X12,X24))) = c_Polynomial_OpCons(X5,hAPP(c_Polynomial_Opoly(X5,X12),X24),c_Polynomial_Osynthetic__div(X5,X12,X24)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_synthetic__div__correct) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(fact_poly__mult,axiom,
! [X4,X11,X12,X5] :
( class_Rings_Ocomm__semiring__0(X5)
=> hAPP(c_Polynomial_Opoly(X5,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X5)),X12),X11)),X4) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X5),hAPP(c_Polynomial_Opoly(X5,X12),X4)),hAPP(c_Polynomial_Opoly(X5,X11),X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_poly__mult) ).
fof(fact_h,axiom,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_h) ).
fof(fact_s,axiom,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_s) ).
fof(conj_0,conjecture,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(c_0_14,plain,
! [X3139,X3140,X3141] :
( ( c_Polynomial_Osmult(X3141,X3140,X3139) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3141))
| X3140 = c_Groups_Ozero__class_Ozero(X3141)
| X3139 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3141))
| ~ class_Rings_Oidom(X3141) )
& ( X3140 != c_Groups_Ozero__class_Ozero(X3141)
| c_Polynomial_Osmult(X3141,X3140,X3139) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3141))
| ~ class_Rings_Oidom(X3141) )
& ( X3139 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3141))
| c_Polynomial_Osmult(X3141,X3140,X3139) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3141))
| ~ class_Rings_Oidom(X3141) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_smult__eq__0__iff])])]) ).
cnf(c_0_15,plain,
( c_Polynomial_Osmult(X2,X1,X3) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| X1 != c_Groups_Ozero__class_Ozero(X2)
| ~ class_Rings_Oidom(X2) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
fof(c_0_16,plain,
! [X4504,X4505] :
( ~ class_Groups_Ocomm__monoid__add(X4505)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4505),X4504,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4505))) = X4504 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_add__poly__code_I2_J])]) ).
fof(c_0_17,plain,
! [X4728,X4729,X4730,X4731,X4732] :
( ( X4728 = hAPP(c_Polynomial_Opoly(X4732,X4731),X4730)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4732),X4731,c_Polynomial_Osmult(X4732,X4730,X4729)) != c_Polynomial_OpCons(X4732,X4728,X4729)
| ~ class_Rings_Ocomm__semiring__0(X4732) )
& ( X4729 = c_Polynomial_Osynthetic__div(X4732,X4731,X4730)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4732),X4731,c_Polynomial_Osmult(X4732,X4730,X4729)) != c_Polynomial_OpCons(X4732,X4728,X4729)
| ~ class_Rings_Ocomm__semiring__0(X4732) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_synthetic__div__unique])])]) ).
cnf(c_0_18,plain,
( c_Polynomial_Osmult(X1,c_Groups_Ozero__class_Ozero(X1),X2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| ~ class_Rings_Oidom(X1) ),
inference(er,[status(thm)],[c_0_15]) ).
cnf(c_0_19,plain,
class_Rings_Oidom(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Oidom]) ).
cnf(c_0_20,plain,
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = X2
| ~ class_Groups_Ocomm__monoid__add(X1) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_21,plain,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Groups_Ocomm__monoid__add]) ).
cnf(c_0_22,plain,
( X1 = c_Polynomial_Osynthetic__div(X2,X3,X4)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),X3,c_Polynomial_Osmult(X2,X4,X1)) != c_Polynomial_OpCons(X2,X5,X1)
| ~ class_Rings_Ocomm__semiring__0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_23,plain,
c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X1) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_24,plain,
c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = X1,
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_25,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__0]) ).
fof(c_0_26,plain,
! [X3368] :
( ~ class_Rings_Ocomm__semiring__1(X3368)
| c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X3368)) = c_Polynomial_OpCons(X3368,c_Groups_Oone__class_Oone(X3368),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3368))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_one__poly__def])]) ).
cnf(c_0_27,plain,
( X1 = hAPP(c_Polynomial_Opoly(X2,X3),X4)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X2),X3,c_Polynomial_Osmult(X2,X4,X5)) != c_Polynomial_OpCons(X2,X1,X5)
| ~ class_Rings_Ocomm__semiring__0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
fof(c_0_28,plain,
! [X3746,X3747] :
( ~ class_Rings_Ocomm__semiring__1(X3747)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3747),X3746),c_Groups_Ozero__class_Ozero(X3747)) = c_Groups_Ozero__class_Ozero(X3747) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J])]) ).
fof(c_0_29,plain,
! [X4725,X4726,X4727] :
( ~ class_Rings_Ocomm__semiring__0(X4727)
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X4727),X4726,c_Polynomial_Osmult(X4727,X4725,c_Polynomial_Osynthetic__div(X4727,X4726,X4725))) = c_Polynomial_OpCons(X4727,hAPP(c_Polynomial_Opoly(X4727,X4726),X4725),c_Polynomial_Osynthetic__div(X4727,X4726,X4725)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_synthetic__div__correct])]) ).
cnf(c_0_30,plain,
c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X2,
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_23]),c_0_24]),c_0_25])])]) ).
cnf(c_0_31,plain,
( c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(X1)) = c_Polynomial_OpCons(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)))
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_32,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__1]) ).
cnf(c_0_33,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X1,
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_23]),c_0_24]),c_0_25])])]) ).
fof(c_0_34,plain,
! [X3748,X3749,X3750,X3751] :
( ~ class_Rings_Ocomm__semiring__0(X3751)
| hAPP(c_Polynomial_Opoly(X3751,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X3751)),X3750),X3749)),X3748) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X3751),hAPP(c_Polynomial_Opoly(X3751,X3750),X3748)),hAPP(c_Polynomial_Opoly(X3751,X3749),X3748)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_poly__mult])]) ).
cnf(c_0_35,plain,
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X2),c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_36,plain,
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),X2,c_Polynomial_Osmult(X1,X3,c_Polynomial_Osynthetic__div(X1,X2,X3))) = c_Polynomial_OpCons(X1,hAPP(c_Polynomial_Opoly(X1,X2),X3),c_Polynomial_Osynthetic__div(X1,X2,X3))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_37,plain,
c_Polynomial_Osynthetic__div(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_31]),c_0_32])]) ).
cnf(c_0_38,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_31]),c_0_32])]) ).
cnf(c_0_39,plain,
( hAPP(c_Polynomial_Opoly(X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X1)),X2),X3)),X4) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),hAPP(c_Polynomial_Opoly(X1,X2),X4)),hAPP(c_Polynomial_Opoly(X1,X3),X4))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_40,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[fact_h]) ).
cnf(c_0_41,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X1),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(spm,[status(thm)],[c_0_35,c_0_32]) ).
cnf(c_0_42,plain,
v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____),
inference(split_conjunct,[status(thm)],[fact_s]) ).
cnf(c_0_43,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_38]),c_0_23]),c_0_24]),c_0_25])]) ).
fof(c_0_44,negated_conjecture,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
cnf(c_0_45,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1),v_s____)),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_40]),c_0_41]),c_0_25])]) ).
cnf(c_0_46,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Groups_Oone__class_Oone(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____) = v_pa____,
inference(rw,[status(thm)],[c_0_42,c_0_43]) ).
cnf(c_0_47,negated_conjecture,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_48,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWW278+1 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n025.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 06:31:58 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 8.70/6.12 % Version : CSE_E---1.7
% 8.70/6.12 % Problem : theBenchmark.p
% 8.70/6.12 % SZS status Theorem for theBenchmark.p
% 8.70/6.12 % SZS output start CNFRefutation
% See solution above
% 8.80/6.15 % Total time : 4.548s
%------------------------------------------------------------------------------