%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWW269+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 : Thu Sep 24 03:10:11 PM UTC 2026
% Result : Theorem 13.63s 2.72s
% Output : CNFRefutation 13.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 38
% Syntax : Number of formulae : 154 ( 49 unt; 0 def)
% Number of atoms : 288 ( 183 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 232 ( 98 ~; 96 |; 5 &)
% ( 3 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-3 aty)
% Number of variables : 227 ( 6 sgn 117 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_diff__0,axiom,
! [X9,X5] :
( class_Groups_Ogroup__add(X5)
=> c_Groups_Ominus__class_Ominus(X5,c_Groups_Ozero__class_Ozero(X5),X9) = c_Groups_Ouminus__class_Ouminus(X5,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__0) ).
fof(fact_inverse__minus__eq,axiom,
! [X9,X5] :
( class_Rings_Odivision__ring__inverse__zero(X5)
=> c_Rings_Oinverse__class_Oinverse(X5,c_Groups_Ouminus__class_Ouminus(X5,X9)) = c_Groups_Ouminus__class_Ouminus(X5,c_Rings_Oinverse__class_Oinverse(X5,X9)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__minus__eq) ).
fof(arity_Complex__Ocomplex__Groups_Ogroup__add,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ogroup__add) ).
fof(fact__096d_A_061_A0_096,axiom,
v_d____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096d_A_061_A0_096) ).
fof(fact_inverse__nonzero__iff__nonzero,axiom,
! [X7,X5] :
( class_Rings_Odivision__ring__inverse__zero(X5)
=> ( c_Rings_Oinverse__class_Oinverse(X5,X7) = c_Groups_Ozero__class_Ozero(X5)
<=> X7 = c_Groups_Ozero__class_Ozero(X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__nonzero__iff__nonzero) ).
fof(arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero,axiom,
class_Rings_Odivision__ring__inverse__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero) ).
fof(fact_inverse__inverse__eq,axiom,
! [X9,X5] :
( class_Rings_Odivision__ring__inverse__zero(X5)
=> c_Rings_Oinverse__class_Oinverse(X5,c_Rings_Oinverse__class_Oinverse(X5,X9)) = X9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__inverse__eq) ).
fof(fact_eq__iff__diff__eq__0,axiom,
! [X12,X7,X5] :
( class_Groups_Oab__group__add(X5)
=> ( X7 = X12
<=> c_Groups_Ominus__class_Ominus(X5,X7,X12) = c_Groups_Ozero__class_Ozero(X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__iff__diff__eq__0) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,axiom,
! [X9,X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> c_Groups_Otimes__class_Otimes(X5,c_Groups_Ozero__class_Ozero(X5),X9) = c_Groups_Ozero__class_Ozero(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
! [X30,X9,X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> c_Groups_Otimes__class_Otimes(X5,X9,X30) = c_Groups_Otimes__class_Otimes(X5,X30,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(fact_diff__add__cancel,axiom,
! [X30,X9,X5] :
( class_Groups_Ogroup__add(X5)
=> c_Groups_Oplus__class_Oplus(X5,c_Groups_Ominus__class_Ominus(X5,X9,X30),X30) = X9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
! [X19,X9,X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> c_Groups_Oplus__class_Oplus(X5,X9,X19) = c_Groups_Oplus__class_Oplus(X5,X19,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(fact_inverse__mult__distrib,axiom,
! [X30,X9,X5] :
( class_Fields_Ofield__inverse__zero(X5)
=> c_Rings_Oinverse__class_Oinverse(X5,c_Groups_Otimes__class_Otimes(X5,X9,X30)) = c_Groups_Otimes__class_Otimes(X5,c_Rings_Oinverse__class_Oinverse(X5,X9),c_Rings_Oinverse__class_Oinverse(X5,X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__mult__distrib) ).
fof(arity_Complex__Ocomplex__Groups_Oab__group__add,axiom,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Oab__group__add) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__1) ).
fof(fact_field__divide__inverse,axiom,
! [X30,X9,X5] :
( class_Fields_Ofield(X5)
=> c_Rings_Oinverse__class_Odivide(X5,X9,X30) = c_Groups_Otimes__class_Otimes(X5,X9,c_Rings_Oinverse__class_Oinverse(X5,X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_field__divide__inverse) ).
fof(fact_inverse__divide,axiom,
! [X30,X9,X5] :
( class_Fields_Ofield__inverse__zero(X5)
=> c_Rings_Oinverse__class_Oinverse(X5,c_Rings_Oinverse__class_Odivide(X5,X9,X30)) = c_Rings_Oinverse__class_Odivide(X5,X30,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__divide) ).
fof(fact_add__diff__cancel,axiom,
! [X30,X9,X5] :
( class_Groups_Ogroup__add(X5)
=> c_Groups_Ominus__class_Ominus(X5,c_Groups_Oplus__class_Oplus(X5,X9,X30),X30) = X9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__diff__cancel) ).
fof(fact_diff__poly__code_I1_J,axiom,
! [X21,X5] :
( class_Groups_Oab__group__add(X5)
=> c_Groups_Ominus__class_Ominus(tc_Polynomial_Opoly(X5),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5)),X21) = c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X5),X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__poly__code_I1_J) ).
fof(fact_minus__zero,axiom,
! [X5] :
( class_Groups_Ogroup__add(X5)
=> c_Groups_Ouminus__class_Ouminus(X5,c_Groups_Ozero__class_Ozero(X5)) = c_Groups_Ozero__class_Ozero(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_minus__zero) ).
fof(arity_Polynomial__Opoly__Groups_Ogroup__add,axiom,
! [X87] :
( class_Groups_Oab__group__add(X87)
=> class_Groups_Ogroup__add(tc_Polynomial_Opoly(X87)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Polynomial__Opoly__Groups_Ogroup__add) ).
fof(arity_Complex__Ocomplex__Fields_Ofield__inverse__zero,axiom,
class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Fields_Ofield__inverse__zero) ).
fof(arity_Complex__Ocomplex__Fields_Ofield,axiom,
class_Fields_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Fields_Ofield) ).
fof(arity_Polynomial__Opoly__Groups_Oab__group__add,axiom,
! [X87] :
( class_Groups_Oab__group__add(X87)
=> class_Groups_Oab__group__add(tc_Polynomial_Opoly(X87)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Polynomial__Opoly__Groups_Oab__group__add) ).
fof(fact_minus__poly__code_I2_J,axiom,
! [X20,X9,X14] :
( class_Groups_Oab__group__add(X14)
=> c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X14),c_Polynomial_OpCons(X14,X9,X20)) = c_Polynomial_OpCons(X14,c_Groups_Ouminus__class_Ouminus(X14,X9),c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X14),X20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_minus__poly__code_I2_J) ).
fof(fact_field__class_Onormalizing__field__rules_I2_J,axiom,
! [X9,X5] :
( class_Fields_Ofield(X5)
=> c_Rings_Oinverse__class_Oinverse(X5,X9) = c_Rings_Oinverse__class_Odivide(X5,c_Groups_Oone__class_Oone(X5),X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_field__class_Onormalizing__field__rules_I2_J) ).
fof(fact_pCons__0__0,axiom,
! [X5] :
( class_Groups_Ozero(X5)
=> c_Polynomial_OpCons(X5,c_Groups_Ozero__class_Ozero(X5),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_pCons__0__0) ).
fof(fact_pCons_Oprems,axiom,
! [X4] :
( X4 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X4) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_pCons_Oprems) ).
fof(fact_pCons_Ohyps,axiom,
( ! [X4] :
( X4 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),X4) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
=> v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_pCons_Ohyps) ).
fof(arity_Complex__Ocomplex__Groups_Ozero,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ozero) ).
fof(fact_add__0,axiom,
! [X9,X5] :
( class_Groups_Ocomm__monoid__add(X5)
=> c_Groups_Oplus__class_Oplus(X5,c_Groups_Ozero__class_Ozero(X5),X9) = X9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__0) ).
fof(conj_0,conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(fact_poly__pCons,axiom,
! [X16,X20,X9,X5] :
( class_Rings_Ocomm__semiring__0(X5)
=> hAPP(c_Polynomial_Opoly(X5,c_Polynomial_OpCons(X5,X9,X20)),X16) = c_Groups_Oplus__class_Oplus(X5,X9,c_Groups_Otimes__class_Otimes(X5,X16,hAPP(c_Polynomial_Opoly(X5,X20),X16))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_poly__pCons) ).
fof(arity_Complex__Ocomplex__Groups_Ocomm__monoid__add,axiom,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Groups_Ocomm__monoid__add) ).
fof(fact_mult__eq__0__iff,axiom,
! [X12,X7,X5] :
( class_Rings_Oring__no__zero__divisors(X5)
=> ( c_Groups_Otimes__class_Otimes(X5,X7,X12) = c_Groups_Ozero__class_Ozero(X5)
<=> ( X12 = c_Groups_Ozero__class_Ozero(X5)
| X7 = c_Groups_Ozero__class_Ozero(X5) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mult__eq__0__iff) ).
fof(arity_Complex__Ocomplex__Rings_Ocomm__semiring__0,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Ocomm__semiring__0) ).
fof(fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J,axiom,
! [X29,X5] :
( class_Rings_Ocomm__semiring__1(X5)
=> c_Groups_Oplus__class_Oplus(X5,X29,X29) = c_Groups_Otimes__class_Otimes(X5,c_Groups_Oplus__class_Oplus(X5,c_Groups_Oone__class_Oone(X5),c_Groups_Oone__class_Oone(X5)),X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J) ).
fof(arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors,axiom,
class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors) ).
fof(c_0_38,plain,
! [X2093,X2094] :
( c_Groups_Ominus__class_Ominus(X2094,c_Groups_Ozero__class_Ozero(X2094),X2093) = c_Groups_Ouminus__class_Ouminus(X2094,X2093)
| ~ class_Groups_Ogroup__add(X2094) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_diff__0])])]) ).
fof(c_0_39,plain,
! [X2826,X2827] :
( c_Rings_Oinverse__class_Oinverse(X2827,c_Groups_Ouminus__class_Ouminus(X2827,X2826)) = c_Groups_Ouminus__class_Ouminus(X2827,c_Rings_Oinverse__class_Oinverse(X2827,X2826))
| ~ class_Rings_Odivision__ring__inverse__zero(X2827) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__minus__eq])])]) ).
cnf(c_0_40,plain,
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ominus__class_Ominus(X1,c_Groups_Ozero__class_Ozero(X1),X2) = c_Groups_Ouminus__class_Ouminus(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_41,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Groups_Ogroup__add]) ).
cnf(c_0_42,plain,
v_d____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[fact__096d_A_061_A0_096]) ).
fof(c_0_43,plain,
! [X2777,X2778] :
( ( ~ class_Rings_Odivision__ring__inverse__zero(X2778)
| c_Rings_Oinverse__class_Oinverse(X2778,X2777) = c_Groups_Ozero__class_Ozero(X2778)
| X2777 != c_Groups_Ozero__class_Ozero(X2778) )
& ( ~ class_Rings_Odivision__ring__inverse__zero(X2778)
| X2777 = c_Groups_Ozero__class_Ozero(X2778)
| c_Rings_Oinverse__class_Oinverse(X2778,X2777) != c_Groups_Ozero__class_Ozero(X2778) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__nonzero__iff__nonzero])])])]) ).
cnf(c_0_44,plain,
( ~ class_Rings_Odivision__ring__inverse__zero(X1)
| c_Rings_Oinverse__class_Oinverse(X1,c_Groups_Ouminus__class_Ouminus(X1,X2)) = c_Groups_Ouminus__class_Ouminus(X1,c_Rings_Oinverse__class_Oinverse(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_45,plain,
class_Rings_Odivision__ring__inverse__zero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero]) ).
cnf(c_0_46,plain,
c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_42]) ).
fof(c_0_47,plain,
! [X2766,X2767] :
( c_Rings_Oinverse__class_Oinverse(X2767,c_Rings_Oinverse__class_Oinverse(X2767,X2766)) = X2766
| ~ class_Rings_Odivision__ring__inverse__zero(X2767) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__inverse__eq])])]) ).
cnf(c_0_48,plain,
( ~ class_Rings_Odivision__ring__inverse__zero(X1)
| c_Rings_Oinverse__class_Oinverse(X1,X2) != c_Groups_Ozero__class_Ozero(X1)
| X2 = c_Groups_Ozero__class_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_49,plain,
c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1)) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_46]),c_0_46]) ).
cnf(c_0_50,plain,
( ~ class_Rings_Odivision__ring__inverse__zero(X1)
| c_Rings_Oinverse__class_Oinverse(X1,c_Rings_Oinverse__class_Oinverse(X1,X2)) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
fof(c_0_51,plain,
! [X1576,X1577,X1578] :
( ( ~ class_Groups_Oab__group__add(X1578)
| X1577 = X1576
| c_Groups_Ominus__class_Ominus(X1578,X1577,X1576) != c_Groups_Ozero__class_Ozero(X1578) )
& ( ~ class_Groups_Oab__group__add(X1578)
| c_Groups_Ominus__class_Ominus(X1578,X1577,X1576) = c_Groups_Ozero__class_Ozero(X1578)
| X1577 != X1576 ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_eq__iff__diff__eq__0])])])]) ).
cnf(c_0_52,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)) != v_d____
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_42]),c_0_42]),c_0_45])]) ).
cnf(c_0_53,plain,
c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)) = X1,
inference(spm,[status(thm)],[c_0_50,c_0_45]) ).
fof(c_0_54,plain,
! [X516,X517] :
( c_Groups_Otimes__class_Otimes(X517,c_Groups_Ozero__class_Ozero(X517),X516) = c_Groups_Ozero__class_Ozero(X517)
| ~ class_Rings_Ocomm__semiring__1(X517) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J])])]) ).
fof(c_0_55,plain,
! [X487,X488,X489] :
( c_Groups_Otimes__class_Otimes(X489,X488,X487) = c_Groups_Otimes__class_Otimes(X489,X487,X488)
| ~ class_Rings_Ocomm__semiring__1(X489) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J])])]) ).
fof(c_0_56,plain,
! [X1613,X1614,X1615] :
( c_Groups_Oplus__class_Oplus(X1615,c_Groups_Ominus__class_Ominus(X1615,X1614,X1613),X1613) = X1614
| ~ class_Groups_Ogroup__add(X1615) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_diff__add__cancel])])]) ).
fof(c_0_57,plain,
! [X395,X396,X397] :
( c_Groups_Oplus__class_Oplus(X397,X396,X395) = c_Groups_Oplus__class_Oplus(X397,X395,X396)
| ~ class_Rings_Ocomm__semiring__1(X397) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J])])]) ).
fof(c_0_58,plain,
! [X2786,X2787,X2788] :
( c_Rings_Oinverse__class_Oinverse(X2788,c_Groups_Otimes__class_Otimes(X2788,X2787,X2786)) = c_Groups_Otimes__class_Otimes(X2788,c_Rings_Oinverse__class_Oinverse(X2788,X2787),c_Rings_Oinverse__class_Oinverse(X2788,X2786))
| ~ class_Fields_Ofield__inverse__zero(X2788) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__mult__distrib])])]) ).
cnf(c_0_59,plain,
( ~ class_Groups_Oab__group__add(X1)
| c_Groups_Ominus__class_Ominus(X1,X2,X3) != c_Groups_Ozero__class_Ozero(X1)
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_60,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1) != v_d____
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)) = v_d____ ),
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_61,plain,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Groups_Oab__group__add]) ).
cnf(c_0_62,plain,
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Otimes__class_Otimes(X1,c_Groups_Ozero__class_Ozero(X1),X2) = c_Groups_Ozero__class_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
cnf(c_0_63,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__1]) ).
fof(c_0_64,plain,
! [X2819,X2820,X2821] :
( c_Rings_Oinverse__class_Odivide(X2821,X2820,X2819) = c_Groups_Otimes__class_Otimes(X2821,X2820,c_Rings_Oinverse__class_Oinverse(X2821,X2819))
| ~ class_Fields_Ofield(X2821) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_field__divide__inverse])])]) ).
cnf(c_0_65,plain,
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Otimes__class_Otimes(X1,X2,X3) = c_Groups_Otimes__class_Otimes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
fof(c_0_66,plain,
! [X2816,X2817,X2818] :
( c_Rings_Oinverse__class_Oinverse(X2818,c_Rings_Oinverse__class_Odivide(X2818,X2817,X2816)) = c_Rings_Oinverse__class_Odivide(X2818,X2816,X2817)
| ~ class_Fields_Ofield__inverse__zero(X2818) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__divide])])]) ).
fof(c_0_67,plain,
! [X1610,X1611,X1612] :
( c_Groups_Ominus__class_Ominus(X1612,c_Groups_Oplus__class_Oplus(X1612,X1611,X1610),X1610) = X1611
| ~ class_Groups_Ogroup__add(X1612) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_add__diff__cancel])])]) ).
cnf(c_0_68,plain,
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ominus__class_Ominus(X1,X2,X3),X3) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_69,plain,
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oplus__class_Oplus(X1,X2,X3) = c_Groups_Oplus__class_Oplus(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
fof(c_0_70,plain,
! [X1959,X1960] :
( c_Groups_Ominus__class_Ominus(tc_Polynomial_Opoly(X1960),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1960)),X1959) = c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1960),X1959)
| ~ class_Groups_Oab__group__add(X1960) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_diff__poly__code_I1_J])])]) ).
fof(c_0_71,plain,
! [X2056] :
( c_Groups_Ouminus__class_Ouminus(X2056,c_Groups_Ozero__class_Ozero(X2056)) = c_Groups_Ozero__class_Ozero(X2056)
| ~ class_Groups_Ogroup__add(X2056) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_minus__zero])])]) ).
fof(c_0_72,plain,
! [X3140] :
( class_Groups_Ogroup__add(tc_Polynomial_Opoly(X3140))
| ~ class_Groups_Oab__group__add(X3140) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arity_Polynomial__Opoly__Groups_Ogroup__add])])]) ).
cnf(c_0_73,plain,
( ~ class_Fields_Ofield__inverse__zero(X1)
| c_Rings_Oinverse__class_Oinverse(X1,c_Groups_Otimes__class_Otimes(X1,X2,X3)) = c_Groups_Otimes__class_Otimes(X1,c_Rings_Oinverse__class_Oinverse(X1,X2),c_Rings_Oinverse__class_Oinverse(X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_74,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1) != v_d____
| c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_42]),c_0_61])]) ).
cnf(c_0_75,plain,
c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,v_d____,X1) = v_d____,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63]),c_0_42]),c_0_42]) ).
cnf(c_0_76,plain,
class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Fields_Ofield__inverse__zero]) ).
cnf(c_0_77,plain,
( ~ class_Fields_Ofield(X1)
| c_Rings_Oinverse__class_Odivide(X1,X2,X3) = c_Groups_Otimes__class_Otimes(X1,X2,c_Rings_Oinverse__class_Oinverse(X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_78,plain,
c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X2,X1),
inference(spm,[status(thm)],[c_0_65,c_0_63]) ).
cnf(c_0_79,plain,
class_Fields_Ofield(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Fields_Ofield]) ).
cnf(c_0_80,plain,
( ~ class_Fields_Ofield__inverse__zero(X1)
| c_Rings_Oinverse__class_Oinverse(X1,c_Rings_Oinverse__class_Odivide(X1,X2,X3)) = c_Rings_Oinverse__class_Odivide(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_81,plain,
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ominus__class_Ominus(X1,c_Groups_Oplus__class_Oplus(X1,X2,X3),X3) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_82,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X2),X2) = X1,
inference(spm,[status(thm)],[c_0_68,c_0_41]) ).
cnf(c_0_83,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X2) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X2,X1),
inference(spm,[status(thm)],[c_0_69,c_0_63]) ).
cnf(c_0_84,plain,
( ~ class_Groups_Oab__group__add(X1)
| c_Groups_Ominus__class_Ominus(tc_Polynomial_Opoly(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2) = c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1),X2) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_85,plain,
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ozero__class_Ozero(X1)) = c_Groups_Ozero__class_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_86,plain,
( ~ class_Groups_Oab__group__add(X1)
| class_Groups_Ogroup__add(tc_Polynomial_Opoly(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_87,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1) != v_d____
| c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2)) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_75]),c_0_76])]) ).
cnf(c_0_88,plain,
c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1),X2) = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X2,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78]),c_0_79])]) ).
cnf(c_0_89,plain,
c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X2)) = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X2,X1),
inference(spm,[status(thm)],[c_0_80,c_0_76]) ).
cnf(c_0_90,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X2),X2) = X1,
inference(spm,[status(thm)],[c_0_81,c_0_41]) ).
cnf(c_0_91,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X2,X1)) = X2,
inference(rw,[status(thm)],[c_0_82,c_0_83]) ).
cnf(c_0_92,plain,
c_Groups_Ominus__class_Ominus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1) = c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1),
inference(spm,[status(thm)],[c_0_84,c_0_61]) ).
fof(c_0_93,plain,
! [X3131] :
( class_Groups_Oab__group__add(tc_Polynomial_Opoly(X3131))
| ~ class_Groups_Oab__group__add(X3131) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arity_Polynomial__Opoly__Groups_Oab__group__add])])]) ).
fof(c_0_94,plain,
! [X1967,X1968,X1969] :
( c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1969),c_Polynomial_OpCons(X1969,X1968,X1967)) = c_Polynomial_OpCons(X1969,c_Groups_Ouminus__class_Ouminus(X1969,X1968),c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1969),X1967))
| ~ class_Groups_Oab__group__add(X1969) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_minus__poly__code_I2_J])])]) ).
cnf(c_0_95,plain,
( ~ class_Groups_Oab__group__add(X1)
| c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
inference(spm,[status(thm)],[c_0_85,c_0_86]) ).
cnf(c_0_96,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)) != v_d____
| c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X2) = v_d____ ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_88]),c_0_89]) ).
cnf(c_0_97,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X2)) = X2,
inference(spm,[status(thm)],[c_0_90,c_0_91]) ).
cnf(c_0_98,plain,
( ~ class_Groups_Oab__group__add(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1 ),
inference(spm,[status(thm)],[c_0_59,c_0_92]) ).
cnf(c_0_99,plain,
( ~ class_Groups_Oab__group__add(X1)
| class_Groups_Oab__group__add(tc_Polynomial_Opoly(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_93]) ).
cnf(c_0_100,plain,
( ~ class_Groups_Oab__group__add(X1)
| c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1),c_Polynomial_OpCons(X1,X2,X3)) = c_Polynomial_OpCons(X1,c_Groups_Ouminus__class_Ouminus(X1,X2),c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(X1),X3)) ),
inference(split_conjunct,[status(thm)],[c_0_94]) ).
cnf(c_0_101,plain,
c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spm,[status(thm)],[c_0_95,c_0_61]) ).
fof(c_0_102,plain,
! [X2750,X2751] :
( c_Rings_Oinverse__class_Oinverse(X2751,X2750) = c_Rings_Oinverse__class_Odivide(X2751,c_Groups_Oone__class_Oone(X2751),X2750)
| ~ class_Fields_Ofield(X2751) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_field__class_Onormalizing__field__rules_I2_J])])]) ).
cnf(c_0_103,plain,
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X2,X1) != v_d____
| c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X2) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_89]),c_0_42]),c_0_42]),c_0_45])]) ).
cnf(c_0_104,plain,
( c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1) != v_d____
| c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1),X2) = v_d____ ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_49]),c_0_97]) ).
fof(c_0_105,plain,
! [X93] :
( c_Polynomial_OpCons(X93,c_Groups_Ozero__class_Ozero(X93),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X93))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X93))
| ~ class_Groups_Ozero(X93) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_pCons__0__0])])]) ).
fof(c_0_106,plain,
! [X4] :
( X4 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X4) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(fof_simplification,[status(thm)],[fact_pCons_Oprems]) ).
fof(c_0_107,plain,
( ! [X4] :
( X4 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),X4) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
=> v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(fof_simplification,[status(thm)],[fact_pCons_Ohyps]) ).
cnf(c_0_108,plain,
( c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_99]),c_0_61])]) ).
cnf(c_0_109,plain,
c_Groups_Ouminus__class_Ouminus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) = c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100,c_0_101]),c_0_46]),c_0_61])]) ).
cnf(c_0_110,plain,
( ~ class_Fields_Ofield(X1)
| c_Rings_Oinverse__class_Oinverse(X1,X2) = c_Rings_Oinverse__class_Odivide(X1,c_Groups_Oone__class_Oone(X1),X2) ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
cnf(c_0_111,plain,
( c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X2) != v_d____
| c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X2)) = v_d____ ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_112,plain,
( ~ class_Groups_Ozero(X1)
| c_Polynomial_OpCons(X1,c_Groups_Ozero__class_Ozero(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_105]) ).
cnf(c_0_113,plain,
class_Groups_Ozero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Groups_Ozero]) ).
fof(c_0_114,plain,
! [X92] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X92) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| X92 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_106])]) ).
fof(c_0_115,plain,
! [X303,X304] :
( c_Groups_Oplus__class_Oplus(X304,c_Groups_Ozero__class_Ozero(X304),X303) = X303
| ~ class_Groups_Ocomm__monoid__add(X304) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_add__0])])]) ).
fof(c_0_116,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(c_0_117,plain,
( ( v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),esk2_0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )
& ( v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| esk2_0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_107])])])])]) ).
cnf(c_0_118,plain,
( c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_108,c_0_109]) ).
cnf(c_0_119,plain,
( c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1) != v_d____
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_d____,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1)) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_111]),c_0_49]),c_0_79])]) ).
cnf(c_0_120,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(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_112,c_0_42]),c_0_113])]) ).
cnf(c_0_121,plain,
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X1) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| X1 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(split_conjunct,[status(thm)],[c_0_114]) ).
fof(c_0_122,plain,
! [X708,X709,X710,X711] :
( hAPP(c_Polynomial_Opoly(X711,c_Polynomial_OpCons(X711,X710,X709)),X708) = c_Groups_Oplus__class_Oplus(X711,X710,c_Groups_Otimes__class_Otimes(X711,X708,hAPP(c_Polynomial_Opoly(X711,X709),X708)))
| ~ class_Rings_Ocomm__semiring__0(X711) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_poly__pCons])])]) ).
cnf(c_0_123,plain,
( ~ class_Groups_Ocomm__monoid__add(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X2) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_115]) ).
cnf(c_0_124,plain,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Groups_Ocomm__monoid__add]) ).
fof(c_0_125,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(fof_simplification,[status(thm)],[c_0_116]) ).
cnf(c_0_126,plain,
( esk2_0 != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
cnf(c_0_127,plain,
( c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1) != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(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_118,c_0_119]),c_0_120])]) ).
fof(c_0_128,plain,
! [X795,X796,X797] :
( ( ~ class_Rings_Oring__no__zero__divisors(X797)
| c_Groups_Otimes__class_Otimes(X797,X796,X795) = c_Groups_Ozero__class_Ozero(X797)
| X795 != c_Groups_Ozero__class_Ozero(X797) )
& ( ~ class_Rings_Oring__no__zero__divisors(X797)
| c_Groups_Otimes__class_Otimes(X797,X796,X795) = c_Groups_Ozero__class_Ozero(X797)
| X796 != c_Groups_Ozero__class_Ozero(X797) )
& ( ~ class_Rings_Oring__no__zero__divisors(X797)
| X795 = c_Groups_Ozero__class_Ozero(X797)
| X796 = c_Groups_Ozero__class_Ozero(X797)
| c_Groups_Otimes__class_Otimes(X797,X796,X795) != c_Groups_Ozero__class_Ozero(X797) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_mult__eq__0__iff])])])]) ).
cnf(c_0_129,plain,
( X1 = v_d____
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X1) = v_d____ ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_121,c_0_42]),c_0_42]) ).
cnf(c_0_130,plain,
( ~ class_Rings_Ocomm__semiring__0(X1)
| hAPP(c_Polynomial_Opoly(X1,c_Polynomial_OpCons(X1,X2,X3)),X4) = c_Groups_Oplus__class_Oplus(X1,X2,c_Groups_Otimes__class_Otimes(X1,X4,hAPP(c_Polynomial_Opoly(X1,X3),X4))) ),
inference(split_conjunct,[status(thm)],[c_0_122]) ).
cnf(c_0_131,plain,
c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_d____,X1) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_124]),c_0_42]) ).
cnf(c_0_132,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Ocomm__semiring__0]) ).
fof(c_0_133,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(fof_nnf,[status(thm)],[c_0_125]) ).
cnf(c_0_134,plain,
( esk2_0 != v_d____
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_ds____ ),
inference(rw,[status(thm)],[c_0_126,c_0_42]) ).
cnf(c_0_135,plain,
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X2) != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_127,c_0_89]) ).
cnf(c_0_136,plain,
c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X1,c_Rings_Oinverse__class_Oinverse(tc_Complex_Ocomplex,X2)) = c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_53]),c_0_79])]) ).
fof(c_0_137,plain,
! [X1777,X1778] :
( c_Groups_Oplus__class_Oplus(X1778,X1777,X1777) = c_Groups_Otimes__class_Otimes(X1778,c_Groups_Oplus__class_Oplus(X1778,c_Groups_Oone__class_Oone(X1778),c_Groups_Oone__class_Oone(X1778)),X1777)
| ~ class_Rings_Ocomm__semiring__1(X1778) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J])])]) ).
cnf(c_0_138,plain,
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),esk2_0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| v_ds____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
cnf(c_0_139,plain,
( ~ class_Rings_Oring__no__zero__divisors(X1)
| c_Groups_Otimes__class_Otimes(X1,X2,X3) != c_Groups_Ozero__class_Ozero(X1)
| X3 = c_Groups_Ozero__class_Ozero(X1)
| X2 = c_Groups_Ozero__class_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_128]) ).
cnf(c_0_140,plain,
( X1 = v_d____
| c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),X1)) = v_d____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_130]),c_0_131]),c_0_132])]) ).
cnf(c_0_141,plain,
class_Rings_Oring__no__zero__divisors(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors]) ).
cnf(c_0_142,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(split_conjunct,[status(thm)],[c_0_133]) ).
cnf(c_0_143,plain,
( esk2_0 != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) = v_ds____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112,c_0_134]),c_0_42]),c_0_113])]) ).
cnf(c_0_144,plain,
( c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2) != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex,X1,X2),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(spm,[status(thm)],[c_0_135,c_0_136]) ).
cnf(c_0_145,plain,
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oplus__class_Oplus(X1,X2,X2) = c_Groups_Otimes__class_Otimes(X1,c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Oone__class_Oone(X1)),X2) ),
inference(split_conjunct,[status(thm)],[c_0_137]) ).
cnf(c_0_146,plain,
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),esk2_0) != v_d____
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_ds____ ),
inference(rw,[status(thm)],[c_0_138,c_0_42]) ).
cnf(c_0_147,plain,
( X1 = v_d____
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_ds____),X1) = v_d____ ),
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_139,c_0_140]),c_0_42]),c_0_42]),c_0_42]),c_0_141])]) ).
cnf(c_0_148,negated_conjecture,
esk2_0 != v_d____,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_143]),c_0_134]) ).
cnf(c_0_149,plain,
( c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X1) != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(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_144,c_0_145]),c_0_63])]) ).
cnf(c_0_150,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_ds____,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_146,c_0_147]),c_0_148]) ).
cnf(c_0_151,plain,
( c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X1) != v_d____
| c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X1),v_ds____) = v_ds____ ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_149,c_0_150]),c_0_150]) ).
cnf(c_0_152,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != v_ds____,
inference(rw,[status(thm)],[c_0_142,c_0_150]) ).
cnf(c_0_153,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_151,c_0_131]),c_0_152]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW269+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:44:32 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.63/2.72 % Version: 3.5.1
% 13.63/2.72 % Preprocessing class: FMLMSMSMSSSNFFN.
% 13.63/2.72 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.63/2.72 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 13.63/2.72 % Starting new_bool_3 with 300s (1) cores
% 13.63/2.72 % Starting new_bool_1 with 300s (1) cores
% 13.63/2.72 % Starting sh5l with 300s (1) cores
% 13.63/2.72 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 3149308 completed with status 0
% 13.63/2.72 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 13.63/2.72 % Preprocessing class: FMLMSMSMSSSNFFN.
% 13.63/2.72 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.63/2.72 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 13.63/2.72 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.63/2.72 % No SInE strategy applied
% 13.63/2.72 % Search class: FGHSM-SMLM32-DFFFFFNN
% 13.63/2.72 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 13.63/2.72 % Starting SubtermCWHack with 136s (1) cores
% 13.63/2.72 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 13.63/2.72 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 113s (1) cores
% 13.63/2.72 % Starting G-E--_207_C01_F1_SE_CS_SP_PI_S5PRR_S0Y with 113s (1) cores
% 13.63/2.72 % Starting G-E--_208_B07CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 113s (1) cores
% 13.63/2.72 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 3149347 completed with status 0
% 13.63/2.72 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 13.63/2.72 % Preprocessing class: FMLMSMSMSSSNFFN.
% 13.63/2.72 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.63/2.72 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 13.63/2.72 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.63/2.72 % No SInE strategy applied
% 13.63/2.72 % Search class: FGHSM-SMLM32-DFFFFFNN
% 13.63/2.72 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 13.63/2.72 % Starting SubtermCWHack with 136s (1) cores
% 13.63/2.72 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 13.63/2.72 % Preprocessing time : 0.022 s
% 13.63/2.72 % Presaturation interreduction done
% 13.63/2.72
% 13.63/2.72 % Proof found!
% 13.63/2.72 % SZS status Theorem
% 13.63/2.72 % SZS output start CNFRefutation
% See solution above
% 13.63/2.72 % Parsed axioms : 1159
% 13.63/2.72 % Removed by relevancy pruning/SinE : 0
% 13.63/2.72 % Initial clauses : 1649
% 13.63/2.72 % Removed in clause preprocessing : 82
% 13.63/2.72 % Initial clauses in saturation : 1567
% 13.63/2.72 % Processed clauses : 8707
% 13.63/2.72 % ...of these trivial : 136
% 13.63/2.72 % ...subsumed : 4641
% 13.63/2.72 % ...remaining for further processing : 3930
% 13.63/2.72 % Other redundant clauses eliminated : 930
% 13.63/2.72 % Clauses deleted for lack of memory : 0
% 13.63/2.72 % Backward-subsumed : 64
% 13.63/2.72 % Backward-rewritten : 249
% 13.63/2.72 % Generated clauses : 64206
% 13.63/2.72 % ...of the previous two non-redundant : 56035
% 13.63/2.72 % ...aggressively subsumed : 0
% 13.63/2.72 % Contextual simplify-reflections : 25
% 13.63/2.72 % Paramodulations : 63275
% 13.63/2.72 % Factorizations : 4
% 13.63/2.72 % NegExts : 0
% 13.63/2.72 % Equation resolutions : 960
% 13.63/2.72 % Disequality decompositions : 0
% 13.63/2.72 % Total rewrite steps : 42542
% 13.63/2.72 % ...of those cached : 38445
% 13.63/2.72 % Propositional unsat checks : 0
% 13.63/2.72 % Propositional check models : 0
% 13.63/2.72 % Propositional check unsatisfiable : 0
% 13.63/2.72 % Propositional clauses : 0
% 13.63/2.72 % Propositional clauses after purity: 0
% 13.63/2.72 % Propositional unsat core size : 0
% 13.63/2.72 % Propositional preprocessing time : 0.000
% 13.63/2.72 % Propositional encoding time : 0.000
% 13.63/2.72 % Propositional solver time : 0.000
% 13.63/2.72 % Success case prop preproc time : 0.000
% 13.63/2.72 % Success case prop encoding time : 0.000
% 13.63/2.72 % Success case prop solver time : 0.000
% 13.63/2.72 % Current number of processed clauses : 2200
% 13.63/2.72 % Positive orientable unit clauses : 350
% 13.63/2.72 % Positive unorientable unit clauses: 18
% 13.63/2.72 % Negative unit clauses : 76
% 13.63/2.72 % Non-unit-clauses : 1756
% 13.63/2.72 % Current number of unprocessed clauses: 50020
% 13.63/2.72 % ...number of literals in the above : 142099
% 13.63/2.72 % Current number of archived formulas : 0
% 13.63/2.72 % Current number of archived clauses : 1568
% 13.63/2.72 % Clause-clause subsumption calls (NU) : 551009
% 13.63/2.72 % Rec. Clause-clause subsumption calls : 345126
% 13.63/2.72 % Non-unit clause-clause subsumptions : 2880
% 13.63/2.72 % Unit Clause-clause subsumption calls : 11676
% 13.63/2.72 % Rewrite failures with RHS unbound : 0
% 13.63/2.72 % BW rewrite match attempts : 4512
% 13.63/2.72 % BW rewrite match successes : 293
% 13.63/2.72 % Condensation attempts : 0
% 13.63/2.72 % Condensation successes : 0
% 13.63/2.72 % Termbank termtop insertions : 1318473
% 13.63/2.72 % Search garbage collected termcells : 22569
% 13.63/2.72
% 13.63/2.72 % -------------------------------------------------
% 13.63/2.72 % User time : 1.958 s
% 13.63/2.72 % System time : 0.075 s
% 13.63/2.72 % Total time : 2.033 s
% 13.63/2.72 % Maximum resident set size: 10116 pages
% 13.63/2.72
% 13.63/2.72 % -------------------------------------------------
% 13.63/2.72 % User time : 8.619 s
% 13.63/2.72 % System time : 0.348 s
% 13.63/2.72 % Total time : 8.968 s
% 13.63/2.72 % Maximum resident set size: 6144 pages
% 13.63/2.72 % E exiting
%------------------------------------------------------------------------------