%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWW230+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 : n018.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:07 PM UTC 2026
% Result : Theorem 232.66s 34.48s
% Output : CNFRefutation 232.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 16
% Syntax : Number of formulae : 61 ( 51 unt; 0 def)
% Number of atoms : 77 ( 53 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 36 ( 20 ~; 9 |; 1 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 11 con; 0-3 aty)
% Number of variables : 70 ( 0 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_0,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(fact_number__of__is__id,axiom,
! [X21] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X21) = X21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_number__of__is__id) ).
fof(fact_real__mult__1,axiom,
! [X15] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X15) = X15,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__mult__1) ).
fof(fact_real__mult__commute,axiom,
! [X23,X15] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X15,X23) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X23,X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__mult__commute) ).
fof(fact_one__is__num__one,axiom,
c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_one__is__num__one) ).
fof(fact_real__norm__def,axiom,
! [X52] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X52) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(fact_abs__minus__add__cancel,axiom,
! [X37,X11] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X11,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X37))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X37,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X11))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_abs__minus__add__cancel) ).
fof(fact_real__diff__def,axiom,
! [X54,X52] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X52,X54) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X52,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X54)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__diff__def) ).
fof(fact_divide__real__def,axiom,
! [X37,X11] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X11,X37) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X11,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X37)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_divide__real__def) ).
fof(fact_inverse__1,axiom,
! [X16] :
( class_Rings_Odivision__ring(X16)
=> c_Rings_Oinverse__class_Oinverse(X16,c_Groups_Oone__class_Oone(X16)) = c_Groups_Oone__class_Oone(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inverse__1) ).
fof(fact_add__num__frac,axiom,
! [X11,X15,X37,X16] :
( class_Fields_Ofield__inverse__zero(X16)
=> ( X37 != c_Groups_Ozero__class_Ozero(X16)
=> c_Groups_Oplus__class_Oplus(X16,X15,c_Rings_Oinverse__class_Odivide(X16,X11,X37)) = c_Rings_Oinverse__class_Odivide(X16,c_Groups_Oplus__class_Oplus(X16,X11,c_Groups_Otimes__class_Otimes(X16,X15,X37)),X37) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__num__frac) ).
fof(fact_real__zero__not__eq__one,axiom,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__zero__not__eq__one) ).
fof(arity_RealDef__Oreal__Rings_Odivision__ring,axiom,
class_Rings_Odivision__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Odivision__ring) ).
fof(fact_eq__divide__2__times__iff,axiom,
! [X12,X13,X14] :
( X14 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X13,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X12))
<=> c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X14) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X13,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__divide__2__times__iff) ).
fof(arity_RealDef__Oreal__Fields_Ofield__inverse__zero,axiom,
class_Fields_Ofield__inverse__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Fields_Ofield__inverse__zero) ).
fof(fact__096abs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_060_061_Aabs_A_Icmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_J_A_N_A_N_As_J_A_L_Acmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_A_N_Apoly_Ap_Az_J_096,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096abs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_060_061_Aabs_A_Icmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_J_A_N_A_N_As_J_A_L_Acmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_A_N_Apoly_Ap_Az_J_096) ).
fof(c_0_16,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(c_0_17,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(fof_simplification,[status(thm)],[c_0_16]) ).
fof(c_0_18,plain,
! [X1438] : c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X1438) = X1438,
inference(variable_rename,[status(thm)],[fact_number__of__is__id]) ).
fof(c_0_19,plain,
! [X1166] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1166) = X1166,
inference(variable_rename,[status(thm)],[fact_real__mult__1]) ).
fof(c_0_20,plain,
! [X1160,X1161] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1161,X1160) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1160,X1161),
inference(variable_rename,[status(thm)],[fact_real__mult__commute]) ).
fof(c_0_21,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(fof_nnf,[status(thm)],[c_0_17]) ).
cnf(c_0_22,plain,
c_Groups_Oone__class_Oone(tc_Int_Oint) = c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit1(c_Int_OPls)),
inference(split_conjunct,[status(thm)],[fact_one__is__num__one]) ).
cnf(c_0_23,plain,
c_Int_Onumber__class_Onumber__of(tc_Int_Oint,X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_18]) ).
fof(c_0_24,plain,
! [X737] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X737) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X737),
inference(variable_rename,[status(thm)],[fact_real__norm__def]) ).
fof(c_0_25,plain,
! [X532,X533] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X533,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X532))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X532,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X533))),
inference(variable_rename,[status(thm)],[fact_abs__minus__add__cancel]) ).
fof(c_0_26,plain,
! [X528,X529] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X529,X528) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X529,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X528)),
inference(variable_rename,[status(thm)],[fact_real__diff__def]) ).
fof(c_0_27,plain,
! [X1167,X1168] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1168,X1167) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1168,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X1167)),
inference(variable_rename,[status(thm)],[fact_divide__real__def]) ).
fof(c_0_28,plain,
! [X1504] :
( c_Rings_Oinverse__class_Oinverse(X1504,c_Groups_Oone__class_Oone(X1504)) = c_Groups_Oone__class_Oone(X1504)
| ~ class_Rings_Odivision__ring(X1504) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inverse__1])])]) ).
cnf(c_0_29,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_30,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X2) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
fof(c_0_31,plain,
! [X11,X15,X37,X16] :
( class_Fields_Ofield__inverse__zero(X16)
=> ( X37 != c_Groups_Ozero__class_Ozero(X16)
=> c_Groups_Oplus__class_Oplus(X16,X15,c_Rings_Oinverse__class_Odivide(X16,X11,X37)) = c_Rings_Oinverse__class_Odivide(X16,c_Groups_Oplus__class_Oplus(X16,X11,c_Groups_Otimes__class_Otimes(X16,X15,X37)),X37) ) ),
inference(fof_simplification,[status(thm)],[fact_add__num__frac]) ).
fof(c_0_32,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(fof_simplification,[status(thm)],[fact_real__zero__not__eq__one]) ).
cnf(c_0_33,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_34,plain,
c_Int_OBit1(c_Int_OPls) = c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(rw,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_35,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_36,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_37,plain,
c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2)),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_38,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X2) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2)),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_39,plain,
( ~ class_Rings_Odivision__ring(X1)
| c_Rings_Oinverse__class_Oinverse(X1,c_Groups_Oone__class_Oone(X1)) = c_Groups_Oone__class_Oone(X1) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_40,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = X1,
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_41,plain,
class_Rings_Odivision__ring(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Rings_Odivision__ring]) ).
fof(c_0_42,plain,
! [X1747,X1748,X1749,X1750] :
( c_Groups_Oplus__class_Oplus(X1750,X1748,c_Rings_Oinverse__class_Odivide(X1750,X1747,X1749)) = c_Rings_Oinverse__class_Odivide(X1750,c_Groups_Oplus__class_Oplus(X1750,X1747,c_Groups_Otimes__class_Otimes(X1750,X1748,X1749)),X1749)
| X1749 = c_Groups_Ozero__class_Ozero(X1750)
| ~ class_Fields_Ofield__inverse__zero(X1750) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_31])])]) ).
fof(c_0_43,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(fof_nnf,[status(thm)],[c_0_32]) ).
fof(c_0_44,plain,
! [X1143,X1144,X1145] :
( ( X1145 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1144,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1143))
| c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1145) != c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1144,X1143) )
& ( c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1145) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1144,X1143)
| X1145 != c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1144,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1143)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_eq__divide__2__times__iff])])]) ).
cnf(c_0_45,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_34]),c_0_35]),c_0_34]),c_0_35]) ).
cnf(c_0_46,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2)) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X2,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_37]),c_0_35]),c_0_37]),c_0_35]) ).
cnf(c_0_47,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40]),c_0_41])]) ).
cnf(c_0_48,plain,
( ~ class_Fields_Ofield__inverse__zero(X1)
| c_Groups_Oplus__class_Oplus(X1,X3,c_Rings_Oinverse__class_Odivide(X1,X4,X2)) = c_Rings_Oinverse__class_Odivide(X1,c_Groups_Oplus__class_Oplus(X1,X4,c_Groups_Otimes__class_Otimes(X1,X3,X2)),X2)
| X2 = c_Groups_Ozero__class_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_49,plain,
class_Fields_Ofield__inverse__zero(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Fields_Ofield__inverse__zero]) ).
cnf(c_0_50,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_51,plain,
( X1 != c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X2,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X3))
| c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_52,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(split_conjunct,[status(thm)],[fact__096abs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_060_061_Aabs_A_Icmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_J_A_N_A_N_As_J_A_L_Acmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_A_N_Apoly_Ap_Az_J_096]) ).
cnf(c_0_53,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45,c_0_46]),c_0_46]) ).
cnf(c_0_54,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_48]),c_0_47]),c_0_40]),c_0_49])]),c_0_50]) ).
cnf(c_0_55,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),X2))) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X2),
inference(er,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_51,c_0_34]),c_0_34])]) ).
cnf(c_0_56,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_52,c_0_35]),c_0_46]),c_0_35]),c_0_46]) ).
cnf(c_0_57,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))))),
inference(rw,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_58,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Groups_Oone__class_Oone(tc_Int_Oint))))) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_40]),c_0_47]) ).
cnf(c_0_59,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))))),
inference(rw,[status(thm)],[c_0_56,c_0_54]) ).
cnf(c_0_60,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_57,c_0_58]),c_0_59])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW230+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.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 09:44:15 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.43 Running first-order theorem proving
% 0.14/0.43 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
% 232.66/34.48 % Version: 3.5.1
% 232.66/34.48 % Preprocessing class: FMLSSMSMSSSNFFN.
% 232.66/34.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 232.66/34.48 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 232.66/34.48 % Starting new_bool_3 with 600s (2) cores
% 232.66/34.48 % Starting new_bool_1 with 600s (2) cores
% 232.66/34.48 % Starting sh5l with 300s (1) cores
% 232.66/34.48 % sh5l with pid 1577353 completed with status 0
% 232.66/34.48 % Result found by sh5l
% 232.66/34.48 % Preprocessing class: FMLSSMSMSSSNFFN.
% 232.66/34.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 232.66/34.48 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 232.66/34.48 % Starting new_bool_3 with 600s (2) cores
% 232.66/34.48 % Starting new_bool_1 with 600s (2) cores
% 232.66/34.48 % Starting sh5l with 300s (1) cores
% 232.66/34.48 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 232.66/34.48 % SinE strategy is gf500_gu_R04_F100_L20000
% 232.66/34.48 % Search class: FGHSM-SSLM31-DFFFFFNN
% 232.66/34.48 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 232.66/34.48 % Starting SubtermCWHack with 28s (1) cores
% 232.66/34.48 % SubtermCWHack with pid 1577361 completed with status 8
% 232.66/34.48 % Starting sh5l with 31s (1) cores
% 232.66/34.48 % sh5l with pid 1577365 completed with status 0
% 232.66/34.48 % Result found by sh5l
% 232.66/34.48 % Preprocessing class: FMLSSMSMSSSNFFN.
% 232.66/34.48 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 232.66/34.48 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 232.66/34.48 % Starting new_bool_3 with 600s (2) cores
% 232.66/34.48 % Starting new_bool_1 with 600s (2) cores
% 232.66/34.48 % Starting sh5l with 300s (1) cores
% 232.66/34.48 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 232.66/34.48 % SinE strategy is gf500_gu_R04_F100_L20000
% 232.66/34.48 % Search class: FGHSM-SSLM31-DFFFFFNN
% 232.66/34.48 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 232.66/34.48 % Starting SubtermCWHack with 28s (1) cores
% 232.66/34.48 % SubtermCWHack with pid 1577361 completed with status 8
% 232.66/34.48 % Starting sh5l with 31s (1) cores
% 232.66/34.48 % Preprocessing time : 0.032 s
% 232.66/34.48 % Presaturation interreduction done
% 232.66/34.48
% 232.66/34.48 % Proof found!
% 232.66/34.48 % SZS status Theorem
% 232.66/34.48 % SZS output start CNFRefutation
% See solution above
% 232.66/34.48 % Parsed axioms : 1171
% 232.66/34.48 % Removed by relevancy pruning/SinE : 329
% 232.66/34.48 % Initial clauses : 1315
% 232.66/34.48 % Removed in clause preprocessing : 60
% 232.66/34.48 % Initial clauses in saturation : 1255
% 232.66/34.48 % Processed clauses : 17232
% 232.66/34.48 % ...of these trivial : 372
% 232.66/34.48 % ...subsumed : 12354
% 232.66/34.48 % ...remaining for further processing : 4506
% 232.66/34.48 % Other redundant clauses eliminated : 943
% 232.66/34.48 % Clauses deleted for lack of memory : 0
% 232.66/34.48 % Backward-subsumed : 228
% 232.66/34.48 % Backward-rewritten : 95
% 232.66/34.48 % Generated clauses : 129183
% 232.66/34.48 % ...of the previous two non-redundant : 114953
% 232.66/34.48 % ...aggressively subsumed : 0
% 232.66/34.48 % Contextual simplify-reflections : 7
% 232.66/34.48 % Paramodulations : 128217
% 232.66/34.48 % Factorizations : 12
% 232.66/34.48 % NegExts : 0
% 232.66/34.48 % Equation resolutions : 972
% 232.66/34.48 % Disequality decompositions : 0
% 232.66/34.48 % Total rewrite steps : 110366
% 232.66/34.48 % ...of those cached : 101137
% 232.66/34.48 % Propositional unsat checks : 0
% 232.66/34.48 % Propositional check models : 0
% 232.66/34.48 % Propositional check unsatisfiable : 0
% 232.66/34.48 % Propositional clauses : 0
% 232.66/34.48 % Propositional clauses after purity: 0
% 232.66/34.48 % Propositional unsat core size : 0
% 232.66/34.48 % Propositional preprocessing time : 0.000
% 232.66/34.48 % Propositional encoding time : 0.000
% 232.66/34.48 % Propositional solver time : 0.000
% 232.66/34.48 % Success case prop preproc time : 0.000
% 232.66/34.48 % Success case prop encoding time : 0.000
% 232.66/34.48 % Success case prop solver time : 0.000
% 232.66/34.48 % Current number of processed clauses : 3155
% 232.66/34.48 % Positive orientable unit clauses : 545
% 232.66/34.48 % Positive unorientable unit clauses: 24
% 232.66/34.48 % Negative unit clauses : 590
% 232.66/34.48 % Non-unit-clauses : 1996
% 232.66/34.48 % Current number of unprocessed clauses: 99625
% 232.66/34.48 % ...number of literals in the above : 270519
% 232.66/34.48 % Current number of archived formulas : 0
% 232.66/34.48 % Current number of archived clauses : 1242
% 232.66/34.48 % Clause-clause subsumption calls (NU) : 643195
% 232.66/34.48 % Rec. Clause-clause subsumption calls : 393747
% 232.66/34.48 % Non-unit clause-clause subsumptions : 4625
% 232.66/34.48 % Unit Clause-clause subsumption calls : 44969
% 232.66/34.48 % Rewrite failures with RHS unbound : 0
% 232.66/34.48 % BW rewrite match attempts : 14525
% 232.66/34.48 % BW rewrite match successes : 503
% 232.66/34.48 % Condensation attempts : 17232
% 232.66/34.48 % Condensation successes : 403
% 232.66/34.48 % Termbank termtop insertions : 2199347
% 232.66/34.48 % Search garbage collected termcells : 16959
% 232.66/34.48
% 232.66/34.48 % -------------------------------------------------
% 232.66/34.48 % User time : 32.413 s
% 232.66/34.48 % System time : 0.910 s
% 232.66/34.48 % Total time : 33.323 s
% 232.66/34.48 % Maximum resident set size: 8516 pages
% 232.66/34.48
% 232.66/34.48 % -------------------------------------------------
% 232.66/34.48 % User time : 32.453 s
% 232.66/34.48 % System time : 0.919 s
% 232.66/34.48 % Total time : 33.372 s
% 232.66/34.48 % Maximum resident set size: 5888 pages
% 232.66/34.48 % E exiting
%------------------------------------------------------------------------------