%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG348-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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 : Fri Sep 25 12:52:21 PM UTC 2026
% Result : Unsatisfiable 34.91s 4.98s
% Output : Proof 34.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 27
% Syntax : Number of formulae : 147 ( 79 unt; 0 def)
% Number of atoms : 247 ( 79 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 271 ( 171 ~; 100 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-4 aty)
% Number of variables : 186 ( 4 sgn 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t168,axiom,
sF5 = ifeq(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true),
introduced(definition) ).
cnf(t163,axiom,
sF0 = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t193,plain,
c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex) = sF0,
inference(orient,[status(thm)],[t163]) ).
cnf(t4061,plain,
sF5 = ifeq(c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true),
inference(step,[status(thm)],[t168,t193]) ).
cnf(t164,axiom,
sF1 = c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t3526,plain,
sF1 = c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t164,t193]) ).
cnf(t197,plain,
c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex) = sF1,
inference(orient,[status(thm)],[t3526]) ).
cnf(t4062,plain,
sF5 = ifeq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true),
inference(step,[status(thm)],[t4061,t197]) ).
cnf(f782,axiom,
( c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__commute_0) ).
fof(f782_nnf,plain,
! [T_a,V_a,V_b] :
( c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(nnf_transformation,[status(thm)],[f782]) ).
fof(f782_sk,plain,
! [T_a,V_a,V_b] :
( c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(skolemisation,[status(esa)],[f782_nnf]) ).
cnf(c782,plain,
( c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(esa)],[f782_sk]) ).
cnf(t62,plain,
ifeq(class_OrderedGroup_Ocomm__monoid__add(X1),true,c_HOL_Oplus__class_Oplus(X2,X3,X1),c_HOL_Oplus__class_Oplus(X3,X2,X1)) = c_HOL_Oplus__class_Oplus(X3,X2,X1),
inference(equality_encoding,[status(esa)],[c782]) ).
cnf(t682,plain,
ifeq(class_OrderedGroup_Ocomm__monoid__add(X1),true,c_HOL_Oplus__class_Oplus(X2,X3,X1),c_HOL_Oplus__class_Oplus(X3,X2,X1)) = c_HOL_Oplus__class_Oplus(X3,X2,X1),
inference(orient,[status(thm)],[t62]) ).
cnf(f916,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Ocomm__monoid__add) ).
fof(f916_nnf,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f916]) ).
cnf(c916,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f916_nnf]) ).
cnf(t4,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c916]) ).
cnf(t172,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t683,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_Complex_Ocomplex) = ifeq(true,true,c_HOL_Oplus__class_Oplus(X2,X1,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,X2,tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t682,t172]) ).
cnf(t25,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t195,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t3714,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X2,X1,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t683,t195]) ).
cnf(t705,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X2,X1,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t3714]) ).
cnf(t4063,plain,
sF5 = ifeq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true),
inference(step,[status(thm)],[t4062,t705]) ).
cnf(t165,axiom,
sF2 = c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t194,plain,
c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex) = sF2,
inference(orient,[status(thm)],[t165]) ).
cnf(t685,plain,
c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex) = ifeq(class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),true,sF2,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t682,t194]) ).
cnf(t3712,plain,
c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex) = ifeq(true,true,sF2,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t685,t172]) ).
cnf(t3713,plain,
c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex) = sF2,
inference(step,[status(thm)],[t3712,t195]) ).
cnf(t704,plain,
c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex) = sF2,
inference(orient,[status(thm)],[t3713]) ).
cnf(t4064,plain,
sF5 = ifeq(sF1,c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex),false,true),
inference(step,[status(thm)],[t4063,t704]) ).
cnf(t166,axiom,
sF3 = c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t3527,plain,
sF3 = c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t166,t194]) ).
cnf(t198,plain,
c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex) = sF3,
inference(orient,[status(thm)],[t3527]) ).
cnf(t4065,plain,
sF5 = ifeq(sF1,sF3,false,true),
inference(step,[status(thm)],[t4064,t198]) ).
cnf(t167,axiom,
sF4 = eq(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
introduced(definition) ).
cnf(t3870,plain,
sF4 = eq(c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t167,t193]) ).
cnf(t3871,plain,
sF4 = eq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t3870,t197]) ).
cnf(t3872,plain,
sF4 = eq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t3871,t705]) ).
cnf(t3873,plain,
sF4 = eq(sF1,c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t3872,t704]) ).
cnf(t3874,plain,
sF4 = eq(sF1,sF3),
inference(step,[status(thm)],[t3873,t198]) ).
cnf(f801,negated_conjecture,
c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f801_nnf,plain,
c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f801]) ).
fof(f801_sk,plain,
c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f801_nnf]) ).
cnf(c801,plain,
c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f801_sk]) ).
cnf(t61,plain,
eq(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)) = false,
inference(equality_encoding,[status(esa)],[c801]) ).
cnf(t3771,plain,
eq(c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t61,t193]) ).
cnf(t3772,plain,
eq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t3771,t197]) ).
cnf(t3773,plain,
eq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t3772,t705]) ).
cnf(t3774,plain,
eq(sF1,c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t3773,t704]) ).
cnf(t3775,plain,
eq(sF1,sF3) = false,
inference(step,[status(thm)],[t3774,t198]) ).
cnf(t908,plain,
eq(sF1,sF3) = false,
inference(orient,[status(thm)],[t3775]) ).
cnf(t3875,plain,
sF4 = false,
inference(step,[status(thm)],[t3874,t908]) ).
cnf(t1262,plain,
false = sF4,
inference(orient,[status(thm)],[t3875]) ).
cnf(t4066,plain,
sF5 = ifeq(sF1,sF3,sF4,true),
inference(step,[status(thm)],[t4065,t1262]) ).
cnf(t69,plain,
ifeq(c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(v_p,v_a,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true) = true,
inference(equality_encoding,[status(esa)],[c801]) ).
cnf(t3804,plain,
ifeq(c_Polynomial_Opoly(sF0,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true) = true,
inference(step,[status(thm)],[t69,t193]) ).
cnf(t3805,plain,
ifeq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_a,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true) = true,
inference(step,[status(thm)],[t3804,t197]) ).
cnf(t3806,plain,
ifeq(sF1,c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_x,v_a,tc_Complex_Ocomplex),tc_Complex_Ocomplex),false,true) = true,
inference(step,[status(thm)],[t3805,t705]) ).
cnf(t3807,plain,
ifeq(sF1,c_Polynomial_Opoly(v_p,sF2,tc_Complex_Ocomplex),false,true) = true,
inference(step,[status(thm)],[t3806,t704]) ).
cnf(t3808,plain,
ifeq(sF1,sF3,false,true) = true,
inference(step,[status(thm)],[t3807,t198]) ).
cnf(t1016,plain,
ifeq(sF1,sF3,false,true) = true,
inference(orient,[status(thm)],[t3808]) ).
cnf(t3890,plain,
ifeq(sF1,sF3,sF4,true) = true,
inference(step,[status(thm)],[t1016,t1262]) ).
cnf(t1277,plain,
ifeq(sF1,sF3,sF4,true) = true,
inference(rw,[status(thm)],[t3890]) ).
cnf(t1300,plain,
ifeq(sF1,sF3,sF4,true) = true,
inference(orient,[status(thm)],[t1277]) ).
cnf(t4067,plain,
sF5 = true,
inference(step,[status(thm)],[t4066,t1300]) ).
cnf(t1854,plain,
true = sF5,
inference(orient,[status(thm)],[t4067]) ).
cnf(t3885,plain,
eq(sF1,sF3) = sF4,
inference(step,[status(thm)],[t908,t1262]) ).
cnf(t1272,plain,
eq(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t3885]) ).
cnf(t2933,plain,
eq(sF1,sF1) = sF4,
inference(rw,[status(thm)],[t1272]) ).
cnf(t20,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t188,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t4106,plain,
eq(X1,X1) = sF5,
inference(step,[status(thm)],[t188,t1854]) ).
cnf(t1893,plain,
eq(X1,X1) = sF5,
inference(orient,[status(thm)],[t4106]) ).
cnf(t4750,plain,
sF5 = sF4,
inference(step,[status(thm)],[t2933,t1893]) ).
cnf(t2944,plain,
sF5 = sF4,
inference(orient,[status(thm)],[t4750]) ).
cnf(t5295,plain,
true = sF4,
inference(step,[status(thm)],[t1854,t2944]) ).
cnf(t3489,plain,
true = sF4,
inference(orient,[status(thm)],[t5295]) ).
cnf(f99,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f99_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f99_nnf]) ).
cnf(c99,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f159,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f159_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(f261,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f261_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f261]) ).
fof(f261_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f261_nnf]) ).
cnf(c261,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
cnf(f364,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f364_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f364]) ).
fof(f364_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f364_nnf]) ).
cnf(c364,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f364_sk]) ).
cnf(f366,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f366_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f366]) ).
fof(f366_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f366_nnf]) ).
cnf(c366,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f366_sk]) ).
cnf(f368,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f368_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c368,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
cnf(f371,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f371_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f371]) ).
fof(f371_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f371_nnf]) ).
cnf(c371,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f371_sk]) ).
cnf(f610,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f610_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f610]) ).
fof(f610_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f610_nnf]) ).
cnf(c610,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f610_sk]) ).
cnf(f611,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f611_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f611]) ).
fof(f611_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f611_nnf]) ).
cnf(c611,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f611_sk]) ).
cnf(f612,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f612_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f612]) ).
fof(f612_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f612_nnf]) ).
cnf(c612,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f612_sk]) ).
cnf(f629,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f629_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f629]) ).
fof(f629_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f629_nnf]) ).
cnf(c629,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f629_sk]) ).
cnf(f655,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f655_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(X0),X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(f695,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f695_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f695]) ).
fof(f695_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f695_nnf]) ).
cnf(c695,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f695_sk]) ).
cnf(f696,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f696_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f696]) ).
fof(f696_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f696_nnf]) ).
cnf(c696,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f696_sk]) ).
cnf(f699,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f699_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f699]) ).
fof(f699_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f699_nnf]) ).
cnf(c699,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f699_sk]) ).
cnf(f700,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f700_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f700]) ).
fof(f700_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f700_nnf]) ).
cnf(c700,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f700_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c99,c159,c261,c364,c366,c368,c371,c610,c611,c612,c629,c655,c695,c696,c699,c700,c801]) ).
cnf(g0_0,plain,
sF4 != false,
inference(rw,[status(thm)],[goal_0,t3489]) ).
cnf(g0_1,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_0,t1262]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG348-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n019.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 05:26:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.91/4.98 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.91/4.98 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------