%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : NUM603+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n011.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 : Mon Jul 18 14:12:06 EDT 2022
% Result : Theorem 68.24s 68.42s
% Output : Refutation 68.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 7
% Syntax : Number of clauses : 9 ( 7 unt; 0 nHn; 9 RR)
% Number of literals : 14 ( 1 equ; 6 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 4 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(42,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroNum) ).
cnf(49,axiom,
( ~ aElementOf0(X,szNzAzT0)
| sdtlseqdt0(sz00,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroLess) ).
cnf(2559,hypothesis,
sdtlpdtrp0(xN,sz00) = xS,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3623) ).
cnf(2597,hypothesis,
( ~ aElementOf0(X,szNzAzT0)
| ~ aElementOf0(Y,szNzAzT0)
| ~ sdtlseqdt0(Y,X)
| ~ aElementOf0(Z,sdtlpdtrp0(xN,X))
| aElementOf0(Z,sdtlpdtrp0(xN,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3754) ).
cnf(2854,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5034) ).
cnf(2856,negated_conjecture,
aElementOf0('SKOLEMAAAV48',sdtlpdtrp0(xN,xi)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
cnf(2857,negated_conjecture,
~ aElementOf0('SKOLEMAAAV48',xS),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
cnf(2873,plain,
sdtlseqdt0(sz00,xi),
inference('HYPERRESOLVE',[status(thm)],[49,2854]) ).
cnf(12878,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[2597,2873,2854,42,2856]),2857,2559,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NUM603+3 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.15 % Command : run-snark %s %d
% 0.14/0.36 % Computer : n011.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Thu Jul 7 00:02:38 EDT 2022
% 0.14/0.37 % CPUTime :
% 0.22/0.50 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.51 *
% 0.22/0.51 *
% 0.22/0.51 #<PACKAGE "SNARK-USER">
% 0.22/0.51 *
% 0.22/0.51 SNARK-TPTP-OPTIONS
% 0.22/0.51 *
% 0.22/0.52 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.22/0.52 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.22/0.52 (USE-FACTORING :POS)
% 0.22/0.52 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.22/0.52 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.22/0.52 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.22/0.52 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.22/0.52 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.22/0.52 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.22/0.52 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.22/0.52 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.22/0.52 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.22/0.52 (DECLARE-TPTP-SYMBOLS2))
% 0.22/0.52 *
% 0.22/0.52 "."
% 0.22/0.52 *
% 0.22/0.52 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-07T00:02:38
% 0.22/0.52 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n011.cluster.edu at 2022-07-07T00:02:38
% 68.24/68.42
% 68.24/68.42
% 68.24/68.42 #||
% 68.24/68.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.24/68.42 % SZS output start Refutation
% See solution above
% 68.24/68.42 ||#
% 68.24/68.42
% 68.24/68.42 ; Summary of computation:
% 68.24/68.42 ; 16404 formulas have been input or derived (from 2770 formulas).
% 68.24/68.42 ; 12878 (79%) were retained. Of these,
% 68.24/68.42 ; 430 ( 3%) were simplified or subsumed later,
% 68.24/68.42 ; 12448 (97%) are still being kept.
% 68.24/68.42 ;
% 68.24/68.42 ; Run time in seconds excluding printing time:
% 68.24/68.42 ; 0.044 0% Read assertion file (1 call)
% 68.24/68.42 ; 0.126 0% Assert (100 calls)
% 68.24/68.42 ; 1.725 3% Process new row (16,239 calls)
% 68.24/68.42 ; 56.043 83% Resolution (5,538 calls)
% 68.24/68.42 ; 0.754 1% Paramodulation (2,769 calls)
% 68.24/68.42 ; 0.346 1% Condensing (14,242 calls)
% 68.24/68.42 ; 6.467 10% Forward subsumption (14,242 calls)
% 68.24/68.42 ; 0.928 1% Backward subsumption (11,910 calls)
% 68.24/68.42 ; 0.101 0% Clause clause subsumption (13,417 calls)
% 68.24/68.42 ; 1.117 2% Forward simplification (16,239 calls)
% 68.24/68.42 ; 0.027 0% Backward simplification (12,836 calls)
% 68.24/68.42 ; 0.029 0% Ordering (17,242 calls)
% 68.24/68.42 ; 0.000 0% Sortal reasoning (32 calls)
% 68.24/68.42 ; 0.024 0% Purity testing (1 call)
% 68.24/68.42 ; 0.169 0% Other
% 68.24/68.42 ; 67.900 Total
% 68.24/68.42 ; 67.901 Real time
% 68.24/68.42 ;
% 68.24/68.44 ; Term-hash-array has 9,226 terms in all.
% 68.24/68.44 ; Feature-vector-row-index has 11,556 entries (11,616 at peak, 11,910 added, 354 deleted).
% 68.24/68.44 ; Feature-vector-row-index has 177,296 nodes (177,315 at peak, 181,102 added, 3,806 deleted).
% 68.24/68.44 ; Retrieved 23,635 possibly forward subsuming rows in 14,242 calls.
% 68.24/68.44 ; Retrieved 2,555 possibly backward subsumed rows in 11,910 calls.
% 68.24/68.44 ; Path-index has 9,162 entries (9,162 at peak, 9,549 added, 387 deleted).
% 68.24/68.44 ; Path-index has 3,566 nodes (3,566 at peak, 3,627 added, 61 deleted).
% 68.24/68.44 ; Trie-index has 9,162 entries (9,162 at peak, 9,549 added, 387 deleted).
% 68.24/68.44 ; Trie-index has 18,874 nodes (18,874 at peak, 19,574 added, 700 deleted).
% 68.24/68.44 ; Retrieved 14,955 generalization terms in 181,413 calls.
% 68.24/68.44 ; Retrieved 925 instance terms in 925 calls.
% 68.24/68.44 ; Retrieved 20,749,799 unifiable terms in 955,252 calls.
% 68.24/68.44 ;
% 68.24/68.44 ; The agenda of rows to process has 4 entries:
% 68.24/68.44 ; 3 with value 9 1 with value 11
% 68.24/68.44 ; The agenda of rows to give has 9678 entries:
% 68.24/68.44 ; 12 with value (4 5) 19 with value (4 40) 150 with value (4 75)
% 68.24/68.44 ; 33 with value (4 6) 215 with value (4 41) 169 with value (4 76)
% 68.24/68.44 ; 69 with value (4 7) 202 with value (4 42) 146 with value (4 77)
% 68.24/68.44 ; 170 with value (4 8) 126 with value (4 43) 157 with value (4 78)
% 68.24/68.44 ; 242 with value (4 9) 43 with value (4 44) 191 with value (4 79)
% 68.24/68.44 ; 73 with value (4 10) 80 with value (4 45) 132 with value (4 80)
% 68.24/68.44 ; 55 with value (4 11) 65 with value (4 46) 141 with value (4 81)
% 68.24/68.44 ; 77 with value (4 12) 105 with value (4 47) 165 with value (4 82)
% 68.24/68.44 ; 56 with value (4 13) 34 with value (4 48) 149 with value (4 83)
% 68.24/68.44 ; 79 with value (4 14) 70 with value (4 49) 139 with value (4 84)
% 68.24/68.44 ; 35 with value (4 15) 68 with value (4 50) 98 with value (4 85)
% 68.24/68.44 ; 45 with value (4 16) 95 with value (4 51) 119 with value (4 86)
% 68.24/68.44 ; 133 with value (4 17) 57 with value (4 52) 110 with value (4 87)
% 68.24/68.44 ; 69 with value (4 18) 88 with value (4 53) 83 with value (4 88)
% 68.24/68.44 ; 16 with value (4 19) 78 with value (4 54) 93 with value (4 89)
% 68.24/68.44 ; 42 with value (4 20) 157 with value (4 55) 52 with value (4 90)
% 68.24/68.44 ; 21 with value (4 21) 137 with value (4 56) 85 with value (4 91)
% 68.24/68.44 ; 22 with value (4 22) 86 with value (4 57) 96 with value (4 92)
% 68.24/68.44 ; 21 with value (4 23) 97 with value (4 58) 64 with value (4 93)
% 68.24/68.44 ; 250 with value (4 24) 63 with value (4 59) 55 with value (4 94)
% 68.24/68.44 ; 225 with value (4 25) 139 with value (4 60) 76 with value (4 95)
% 68.24/68.44 ; 119 with value (4 26) 139 with value (4 61) 98 with value (4 96)
% 68.24/68.44 ; 41 with value (4 27) 155 with value (4 62) 31 with value (4 97)
% 68.24/68.44 ; 103 with value (4 28) 121 with value (4 63) 38 with value (4 98)
% 68.24/68.44 ; 45 with value (4 29) 96 with value (4 64) 83 with value (4 99)
% 68.24/68.44 ; 35 with value (4 30) 154 with value (4 65) 44 with value (4 100)
% 68.24/68.44 ; 45 with value (4 31) 144 with value (4 66) 15 with value (4 101)
% 68.24/68.44 ; 10 with value (4 32) 164 with value (4 67) 48 with value (4 102)
% 68.24/68.44 ; 124 with value (4 33) 135 with value (4 68) 52 with value (4 103)
% 68.24/68.44 ; 74 with value (4 34) 115 with value (4 69) 9 with value (4 104)
% 68.28/68.44 ; 106 with value (4 35) 134 with value (4 70) 15 with value (4 105)
% 68.28/68.44 ; 72 with value (4 36) 173 with value (4 71) 30 with value (4 106)
% 68.28/68.44 ; 47 with value (4 37) 175 with value (4 72) 12 with value (4 107)
% 68.28/68.44 ; 55 with value (4 38) 138 with value (4 73) 6 with value (4 109)
% 68.28/68.44 ; 102 with value (4 39) 131 with value (4 74) 6 with value (4 110)
% 68.28/68.44 Evaluation took:
% 68.28/68.44 67.92 seconds of real time
% 68.28/68.44 67.18097 seconds of user run time
% 68.28/68.44 0.739014 seconds of system run time
% 68.28/68.44 [Run times include 1.814 seconds GC run time.]
% 68.28/68.44 0 calls to %EVAL
% 68.28/68.44 0 page faults and
% 68.28/68.44 1,693,213,072 bytes consed.
% 68.28/68.44 :PROOF-FOUND
% 68.28/68.44 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-07-07T00:03:46
% 68.28/68.44 :PROOF-FOUND
% 68.28/68.44 *
%------------------------------------------------------------------------------