%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : ALG384-1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:15:17 EDT 2024
% Result : Unsatisfiable 6.76s 6.93s
% Output : Refutation 6.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 6
% Syntax : Number of clauses : 11 ( 7 unt; 2 nHn; 9 RR)
% Number of literals : 17 ( 4 equ; 6 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 7 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_CHAINED_0,axiom,
v_c____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
cnf(clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
cnf(clsarity_RealDef__Oreal__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Olinorder) ).
cnf(cls_not__leE_0,axiom,
( ~ class_Orderings_Olinorder(X592)
| c_HOL_Oord__class_Oless(X594,X593,X592)
| c_lessequals(X593,X594,X592) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__leE_0) ).
cnf(c1053,plain,
( c_HOL_Oord__class_Oless(X603,X604,tc_RealDef_Oreal)
| c_lessequals(X604,X603,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[cls_not__leE_0,clsarity_RealDef__Oreal__Orderings_Olinorder]) ).
cnf(cls_conjecture_0,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(v_c____,tc_Complex_Ocomplex),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(c1729,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(v_c____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[cls_conjecture_0,c1053]) ).
cnf(cls_norm__le__zero__iff_0,axiom,
( ~ class_RealVector_Oreal__normed__vector(X2065)
| X2066 = c_HOL_Ozero__class_Ozero(X2065)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(X2066,X2065),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_norm__le__zero__iff_0) ).
cnf(c11030,plain,
( ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| v_c____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[cls_norm__le__zero__iff_0,c1729]) ).
cnf(c11048,plain,
v_c____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[c11030,clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector]) ).
cnf(c11101,plain,
$false,
inference(resolution,[status(thm)],[c11048,cls_CHAINED_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ALG384-1 : TPTP v8.1.2. Released v4.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:35:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 6.76/6.93 % Version: 1.5
% 6.76/6.93 % SZS status Unsatisfiable
% 6.76/6.93 % SZS output start CNFRefutation
% See solution above
% 6.76/6.93
% 6.76/6.93 % Initial clauses : 653
% 6.76/6.93 % Processed clauses : 2200
% 6.76/6.93 % Factors computed : 98
% 6.76/6.93 % Resolvents computed: 10928
% 6.76/6.93 % Tautologies deleted: 48
% 6.76/6.93 % Forward subsumed : 333
% 6.76/6.93 % Backward subsumed : 16
% 6.76/6.93 % -------- CPU Time ---------
% 6.76/6.93 % User time : 6.540 s
% 6.76/6.93 % System time : 0.042 s
% 6.76/6.93 % Total time : 6.582 s
%------------------------------------------------------------------------------