%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n018.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 : Tue Apr 1 02:16:16 AM UTC 2025
% Result : Theorem 10.25s 10.51s
% Output : Refutation 10.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 8
% Syntax : Number of clauses : 13 ( 8 unt; 0 nHn; 12 RR)
% Number of literals : 26 ( 6 equ; 15 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 17 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(22,axiom,
( times_succeeds(X,Y,Z)
| X != s(U)
| ~ times_succeeds(U,Y,V)
| ~ plus_succeeds(Y,V,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id15) ).
cnf(93,axiom,
( nat_succeeds(X)
| X != s(Y)
| ~ nat_succeeds(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id27) ).
cnf(102,axiom,
( ~ nat_succeeds(X)
| '@+'(X,Y) != Z
| plus_succeeds(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','(@+)/2') ).
cnf(104,axiom,
( ~ nat_succeeds(X)
| ~ nat_succeeds(Y)
| '@*'(X,Y) != Z
| times_succeeds(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','(@*)/2') ).
cnf(105,axiom,
( ~ nat_succeeds(X)
| ~ nat_succeeds(Y)
| '@*'(X,Y) = Z
| ~ times_succeeds(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','(@*)/2') ).
cnf(140,negated_conjecture,
nat_succeeds('SKOLEMAAAV36'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:successor)') ).
cnf(141,negated_conjecture,
nat_succeeds('SKOLEMAAAV37'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:successor)') ).
cnf(142,negated_conjecture,
'@*'(s('SKOLEMAAAV36'),'SKOLEMAAAV37') != '@+'('SKOLEMAAAV37','@*'('SKOLEMAAAV36','SKOLEMAAAV37')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(times:successor)') ).
cnf(175,plain,
nat_succeeds(s('SKOLEMAAAV36')),
inference('HYPERRESOLVE',[status(thm)],[93,140,theory(equality)]) ).
cnf(216,plain,
plus_succeeds('SKOLEMAAAV37',X,'@+'('SKOLEMAAAV37',X)),
inference('HYPERRESOLVE',[status(thm)],[102,141,theory(equality)]) ).
cnf(240,plain,
times_succeeds('SKOLEMAAAV36','SKOLEMAAAV37','@*'('SKOLEMAAAV36','SKOLEMAAAV37')),
inference('HYPERRESOLVE',[status(thm)],[104,140,141,theory(equality)]) ).
cnf(610,plain,
~ times_succeeds(s('SKOLEMAAAV36'),'SKOLEMAAAV37','@+'('SKOLEMAAAV37','@*'('SKOLEMAAAV36','SKOLEMAAAV37'))),
inference('UR-RESOLVE',[status(thm)],[105,175,141,142]) ).
cnf(13231,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[22,240,216,theory(equality)]),610]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SWX035+1 : TPTP v9.1.0. Released v9.1.0.
% 0.12/0.14 % Command : run-snark %s %d
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Mon Mar 31 14:28:17 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.20/0.48 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.49 *
% 0.20/0.49 *
% 0.20/0.50 #<PACKAGE "SNARK-USER">
% 0.20/0.50 *
% 0.20/0.50 SNARK-TPTP-OPTIONS
% 0.20/0.50 *
% 0.20/0.50 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.50 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.50 (USE-FACTORING :POS)
% 0.20/0.50 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.50 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.50 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.50 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.50 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.50 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.50 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.50 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.50 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.50 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.50 *
% 0.20/0.50 "."
% 0.20/0.50 *
% 0.20/0.50 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2025-03-31T14:28:17
% 0.20/0.50 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n018.cluster.edu at 2025-03-31T14:28:17
% 0.20/0.53
% 0.20/0.53 ; Recognized relation functionality assertion (OR (NOT (|plus_succeeds| ?X ?Y ?Z)) (NOT (|plus_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.20/0.53 ; Recognized left identity assertion (= (@+ |0| ?X) ?X).
% 10.25/10.51 ; Recognized relation functionality assertion (OR (NOT (|times_succeeds| ?X ?Y ?Z)) (NOT (|times_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 10.25/10.51
% 10.25/10.51 #||
% 10.25/10.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.25/10.51 % SZS output start Refutation
% See solution above
% 10.33/10.53 ||#
% 10.33/10.53
% 10.33/10.53 ; Summary of computation:
% 10.33/10.53 ; 44694 formulas have been input or derived (from 266 formulas).
% 10.33/10.53 ; 13231 (30%) were retained. Of these,
% 10.33/10.53 ; 2268 (17%) were simplified or subsumed later,
% 10.33/10.53 ; 10963 (83%) are still being kept.
% 10.33/10.53 ;
% 10.33/10.53 ; Run time in seconds excluding printing time:
% 10.33/10.53 ; 0.015 0% Read assertion file (1 call)
% 10.33/10.53 ; 0.007 0% Assert (62 calls)
% 10.33/10.53 ; 1.383 14% Process new row (44,257 calls)
% 10.33/10.53 ; 0.699 7% Resolution (530 calls)
% 10.33/10.53 ; 0.005 0% Paramodulation (265 calls)
% 10.33/10.53 ; 0.001 0% Factoring (22 calls)
% 10.33/10.53 ; 0.030 0% Condensing (13,478 calls)
% 10.33/10.53 ; 5.209 52% Forward subsumption (13,478 calls)
% 10.33/10.53 ; 0.103 1% Backward subsumption (1,926 calls)
% 10.33/10.53 ; 0.370 4% Clause clause subsumption (91,534 calls)
% 10.33/10.53 ; 1.644 16% Forward simplification (44,105 calls)
% 10.33/10.53 ; 0.280 3% Backward simplification (13,231 calls)
% 10.33/10.53 ; 0.068 1% Ordering (11,787 calls)
% 10.33/10.53 ; 0.000 0% Sortal reasoning (32 calls)
% 10.33/10.53 ; 0.001 0% Purity testing (1 call)
% 10.33/10.53 ; 0.195 2% Other
% 10.33/10.53 ; 10.010 Total
% 10.33/10.53 ; 10.030 Real time
% 10.33/10.53 ;
% 10.33/10.53 ; Term-hash-array has 27,597 terms in all.
% 10.33/10.53 ; Feature-vector-row-index has 1,862 entries (1,862 at peak, 1,926 added, 64 deleted).
% 10.33/10.53 ; Feature-vector-row-index has 7,654 nodes (7,654 at peak, 8,738 added, 1,084 deleted).
% 10.33/10.53 ; Retrieved 159,061 possibly forward subsuming rows in 13,478 calls.
% 10.33/10.53 ; Retrieved 3,573 possibly backward subsumed rows in 1,926 calls.
% 10.33/10.53 ; Path-index has 25,122 entries (25,122 at peak, 29,663 added, 4,541 deleted).
% 10.33/10.53 ; Path-index has 4,195 nodes (4,195 at peak, 4,455 added, 260 deleted).
% 10.33/10.53 ; Trie-index has 25,122 entries (25,122 at peak, 29,663 added, 4,541 deleted).
% 10.33/10.53 ; Trie-index has 118,294 nodes (118,294 at peak, 142,531 added, 24,237 deleted).
% 10.33/10.53 ; Retrieved 68,775 generalization terms in 450,993 calls.
% 10.33/10.53 ; Retrieved 11,521 instance terms in 11,304 calls.
% 10.33/10.53 ; Retrieved 855,819 unifiable terms in 26,362 calls.
% 10.33/10.53 ;
% 10.33/10.53 ; The agenda of rows to process has 9 entries:
% 10.33/10.53 ; 1 with value 16 1 with value 20 2 with value 23
% 10.33/10.53 ; 2 with value 19 2 with value 22 1 with value 26
% 10.33/10.53 ; The agenda of rows to give has 10707 entries:
% 10.33/10.53 ; 56 with value (4 9) 133 with value (4 19) 1548 with value (4 29)
% 10.33/10.53 ; 122 with value (4 10) 538 with value (4 20) 2579 with value (4 30)
% 10.33/10.53 ; 182 with value (4 11) 206 with value (4 21) 8 with value (4 32)
% 10.33/10.53 ; 192 with value (4 12) 306 with value (4 22) 2 with value (4 37)
% 10.33/10.53 ; 261 with value (4 13) 264 with value (4 23) 12 with value (4 38)
% 10.33/10.53 ; 269 with value (4 14) 528 with value (4 24) 2 with value (4 40)
% 10.33/10.53 ; 134 with value (4 15) 483 with value (4 25) 2 with value (4 41)
% 10.33/10.53 ; 240 with value (4 16) 1793 with value (4 26) 2 with value (4 46)
% 10.33/10.53 ; 95 with value (4 17) 334 with value (4 27) 2 with value (4 54)
% 10.33/10.53 ; 234 with value (4 18) 180 with value (4 28)
% 10.33/10.53 Evaluation took:
% 10.33/10.53 10.032 seconds of real time
% 10.33/10.53 9.433598 seconds of user run time
% 10.33/10.53 0.596133 seconds of system run time
% 10.33/10.53 [Run times include 1.499 seconds GC run time.]
% 10.33/10.53 0 calls to %EVAL
% 10.33/10.53 0 page faults and
% 10.33/10.53 1,033,380,168 bytes consed.
% 10.33/10.53 :PROOF-FOUND
% 10.33/10.53 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2025-03-31T14:28:27
% 10.33/10.53 :PROOF-FOUND
% 10.33/10.53 *
%------------------------------------------------------------------------------