%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG370-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n029.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 : 600s
% DateTime : Thu Jul 14 18:00:39 EDT 2022
% Result : Unsatisfiable 0.60s 0.80s
% Output : Refutation 0.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 7
% Syntax : Number of clauses : 11 ( 9 unt; 0 nHn; 9 RR)
% Number of literals : 15 ( 2 equ; 6 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-3 aty)
% Number of variables : 9 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_xt1_I7_J_0,axiom,
( ~ class_Orderings_Oorder(X)
| c_HOL_Oord__class_Oless(Y,Z,X)
| ~ c_lessequals(Y,U,X)
| ~ c_HOL_Oord__class_Oless(U,Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I7_J_0) ).
cnf(cls_norm__mult_0,axiom,
( ~ class_RealVector_Oreal__normed__div__algebra(X)
| c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(Y,Z,X),X) = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(Y,X),c_RealVector_Onorm__class_Onorm(Z,X),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_norm__mult_0) ).
cnf(cls_CHAINED_0,axiom,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
cnf(cls_CHAINED_0_01,axiom,
c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
cnf(cls_conjecture_0,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(clsarity_RealDef__Oreal__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Oorder) ).
cnf(clsarity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra) ).
cnf(1004,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X,Y,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(Y,tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference('HYPERRESOLVE',[status(thm)],[cls_norm__mult_0,clsarity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra]) ).
cnf(1005,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference('REWRITE',[status(thm)],[cls_CHAINED_0_01,1004,theory(equality)]) ).
cnf(1006,plain,
~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal),
inference('REWRITE',[status(thm)],[cls_conjecture_0,1004,theory(equality)]) ).
cnf(1028,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[cls_xt1_I7_J_0,1006,clsarity_RealDef__Oreal__Orderings_Oorder,cls_CHAINED_0]),1005]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG370-1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n029.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 : 600
% 0.13/0.34 % DateTime : Wed Jun 8 21:59:51 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T21:59:51
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n029.cluster.edu at 2022-06-08T21:59:51
% 0.37/0.60 WARNING:
% 0.37/0.60 |class_OrderedGroup_Oab__semigroup__idem__mult| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.60/0.80
% 0.60/0.80
% 0.60/0.80 #||
% 0.60/0.80 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.60/0.80 % SZS output start Refutation
% See solution above
% 0.60/0.80 ||#
% 0.60/0.80
% 0.60/0.80 ; Summary of computation:
% 0.60/0.80 ; 2462 formulas have been input or derived (from 395 formulas).
% 0.60/0.80 ; 1028 (42%) were retained. Of these,
% 0.60/0.80 ; 33 ( 3%) were simplified or subsumed later,
% 0.60/0.80 ; 995 (97%) are still being kept.
% 0.60/0.80 ;
% 0.60/0.80 ; Run time in seconds excluding printing time:
% 0.60/0.80 ; 0.113 33% Read assertion file (1 call)
% 0.60/0.80 ; 0.010 3% Assert (614 calls)
% 0.60/0.80 ; 0.059 17% Process new row (2,173 calls)
% 0.60/0.80 ; 0.044 13% Resolution (788 calls)
% 0.60/0.80 ; 0.003 1% Paramodulation (394 calls)
% 0.60/0.80 ; 0.000 0% Factoring (2 calls)
% 0.60/0.80 ; 0.010 3% Condensing (654 calls)
% 0.60/0.80 ; 0.013 4% Forward subsumption (654 calls)
% 0.60/0.80 ; 0.009 3% Backward subsumption (454 calls)
% 0.60/0.80 ; 0.004 1% Clause clause subsumption (732 calls)
% 0.60/0.80 ; 0.028 8% Forward simplification (2,171 calls)
% 0.60/0.80 ; 0.007 2% Backward simplification (1,028 calls)
% 0.60/0.80 ; 0.004 1% Ordering (1,173 calls)
% 0.60/0.80 ; 0.001 0% Sortal reasoning (32 calls)
% 0.60/0.80 ; 0.001 0% Purity testing (1 call)
% 0.60/0.80 ; 0.033 10% Other
% 0.60/0.80 ; 0.339 Total
% 0.60/0.80 ; 0.341 Real time
% 0.60/0.80 ;
% 0.60/0.80 ; Term-hash-array has 1,564 terms in all.
% 0.60/0.80 ; Feature-vector-row-index has 447 entries (447 at peak, 454 added, 7 deleted).
% 0.60/0.80 ; Feature-vector-row-index has 1,418 nodes (1,418 at peak, 1,504 added, 86 deleted).
% 0.60/0.80 ; Retrieved 759 possibly forward subsuming rows in 654 calls.
% 0.60/0.80 ; Retrieved 349 possibly backward subsumed rows in 454 calls.
% 0.60/0.81 ; Path-index has 1,522 entries (1,522 at peak, 1,584 added, 62 deleted).
% 0.60/0.81 ; Path-index has 3,350 nodes (3,350 at peak, 3,472 added, 122 deleted).
% 0.60/0.81 ; Trie-index has 1,522 entries (1,522 at peak, 1,584 added, 62 deleted).
% 0.60/0.81 ; Trie-index has 5,034 nodes (5,034 at peak, 5,385 added, 351 deleted).
% 0.60/0.81 ; Retrieved 2,287 generalization terms in 4,275 calls.
% 0.60/0.81 ; Retrieved 801 instance terms in 619 calls.
% 0.60/0.81 ; Retrieved 50,972 unifiable terms in 3,023 calls.
% 0.60/0.81 ;
% 0.60/0.81 ; The agenda of rows to process has 4 entries:
% 0.60/0.81 ; 1 with value 27 1 with value 29 2 with value 31
% 0.60/0.81 ; The agenda of input rows to give has 160 entries:
% 0.60/0.81 ; 26 with value 24 1 with value 31 1 with value 37
% 0.60/0.81 ; 12 with value 25 3 with value 32 1 with value 38
% 0.60/0.81 ; 11 with value 26 3 with value 33 14 with value 39
% 0.60/0.81 ; 69 with value 27 6 with value 34 1 with value 47
% 0.60/0.81 ; 2 with value 29 5 with value 35 2 with value 52
% 0.60/0.81 ; 2 with value 30 1 with value 36
% 0.60/0.81 ; The agenda of rows to give has 441 entries:
% 0.60/0.81 ; 123 with value (4 6) 21 with value (4 15) 2 with value (4 23)
% 0.60/0.81 ; 12 with value (4 8) 14 with value (4 16) 2 with value (4 24)
% 0.60/0.81 ; 10 with value (4 9) 17 with value (4 17) 3 with value (4 25)
% 0.60/0.81 ; 32 with value (4 10) 19 with value (4 18) 5 with value (4 26)
% 0.60/0.81 ; 47 with value (4 11) 34 with value (4 19) 3 with value (4 27)
% 0.60/0.81 ; 20 with value (4 12) 13 with value (4 20) 2 with value (4 30)
% 0.60/0.81 ; 34 with value (4 13) 6 with value (4 21) 2 with value (4 32)
% 0.60/0.81 ; 18 with value (4 14) 2 with value (4 22)
% 0.60/0.81 Evaluation took:
% 0.60/0.81 0.342 seconds of real time
% 0.60/0.81 0.318573 seconds of user run time
% 0.60/0.81 0.023008 seconds of system run time
% 0.60/0.81 [Run times include 0.011 seconds GC run time.]
% 0.60/0.81 0 calls to %EVAL
% 0.60/0.81 0 page faults and
% 0.60/0.81 21,022,280 bytes consed.
% 0.60/0.81 :PROOF-FOUND
% 0.60/0.81 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T21:59:52
% 0.60/0.81 :PROOF-FOUND
% 0.60/0.81 *
%------------------------------------------------------------------------------