%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KLE026+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n016.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 : Sun Jul 17 02:26:14 EDT 2022
% Result : Theorem 14.23s 14.43s
% Output : Refutation 14.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of clauses : 21 ( 17 unt; 0 nHn; 12 RR)
% Number of literals : 25 ( 12 equ; 5 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 23 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
addition(X,X) = X,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
cnf(3,plain,
addition(X,addition(X,Y)) = addition(X,Y),
inference('EMBED',[status(thm)],[2]) ).
cnf(4,axiom,
multiplication(X,multiplication(Y,Z)) = multiplication(multiplication(X,Y),Z),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
cnf(6,axiom,
multiplication(one,X) = X,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
cnf(8,axiom,
multiplication(addition(X,Y),Z) = addition(multiplication(X,Z),multiplication(Y,Z)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
cnf(11,axiom,
( ~ leq(X,Y)
| addition(X,Y) = Y ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',order) ).
cnf(12,axiom,
( leq(X,Y)
| addition(X,Y) != Y ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',order) ).
cnf(13,axiom,
( ~ test(X)
| complement('SKOLEMAAAV1'(X),X) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_1) ).
cnf(17,axiom,
( ~ complement(X,Y)
| addition(X,Y) = one ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+1.ax',test_2) ).
cnf(22,negated_conjecture,
test('SKOLEMAAAV3'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(24,negated_conjecture,
multiplication('SKOLEMAAAV3','SKOLEMAAAV2') = multiplication(multiplication('SKOLEMAAAV3','SKOLEMAAAV2'),'SKOLEMAAAV4'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(25,negated_conjecture,
~ leq(multiplication('SKOLEMAAAV3','SKOLEMAAAV2'),multiplication('SKOLEMAAAV2','SKOLEMAAAV4')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(27,plain,
complement('SKOLEMAAAV1'('SKOLEMAAAV3'),'SKOLEMAAAV3'),
inference('HYPERRESOLVE',[status(thm)],[13,22]) ).
cnf(31,plain,
leq(X,addition(X,Y)),
inference('HYPERRESOLVE',[status(thm)],[12,3]) ).
cnf(89,plain,
addition('SKOLEMAAAV1'('SKOLEMAAAV3'),'SKOLEMAAAV3') = one,
inference('HYPERRESOLVE',[status(thm)],[17,27]) ).
cnf(141,plain,
leq('SKOLEMAAAV3',one),
inference('PARAMODULATE',[status(thm)],[31,89,theory(equality)]) ).
cnf(150,plain,
addition('SKOLEMAAAV3',one) = one,
inference('HYPERRESOLVE',[status(thm)],[11,141]) ).
cnf(232,plain,
X = addition(multiplication('SKOLEMAAAV3',X),X),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[8,150,theory(equality)]),6,theory(equality)]) ).
cnf(445,plain,
leq(multiplication('SKOLEMAAAV3',X),X),
inference('HYPERRESOLVE',[status(thm)],[12,232]) ).
cnf(463,plain,
leq(multiplication(multiplication('SKOLEMAAAV3',X),Y),multiplication(X,Y)),
inference('PARAMODULATE',[status(thm)],[445,4,theory(equality)]) ).
cnf(3215,plain,
$false,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[463,24,theory(equality)]),25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KLE026+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n016.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 : Thu Jun 16 15:17:34 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.47 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.48 *
% 0.20/0.48 *
% 0.20/0.48 #<PACKAGE "SNARK-USER">
% 0.20/0.48 *
% 0.20/0.48 SNARK-TPTP-OPTIONS
% 0.20/0.48 *
% 0.20/0.48 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.48 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.48 (USE-FACTORING :POS)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.48 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.48 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.48 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.48 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.48 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.48 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.48 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.48 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.48 *
% 0.20/0.48 "."
% 0.20/0.48 *
% 0.20/0.48 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-16T15:17:34
% 0.20/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n016.cluster.edu at 2022-06-16T15:17:34
% 0.20/0.50
% 0.20/0.50 ; Recognized commutativity assertion (= (|addition| ?X ?Y) (|addition| ?Y ?X)).
% 0.20/0.50 ; Recognized associativity assertion (= (|addition| ?X (|addition| ?Y ?Z)) (|addition| (|addition| ?X ?Y) ?Z)).
% 0.20/0.50 ; Recognized right identity assertion (= (|addition| ?X |zero|) ?X).
% 0.20/0.50 ; Recognized associativity assertion (= (|multiplication| ?X (|multiplication| ?Y ?Z)) (|multiplication| (|multiplication| ?X ?Y) ?Z)).
% 0.20/0.50 ; Recognized right identity assertion (= (|multiplication| ?X |one|) ?X).
% 0.20/0.50 ; Recognized left identity assertion (= (|multiplication| |one| ?X) ?X).
% 0.20/0.50 ; Declaring addition to be commutative.
% 14.23/14.43 ; Declaring addition to be associative-commutative.
% 14.23/14.43
% 14.23/14.43 #||
% 14.23/14.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.23/14.43 % SZS output start Refutation
% See solution above
% 14.23/14.43 ||#
% 14.23/14.43
% 14.23/14.43 ; Summary of computation:
% 14.23/14.43 ; 30787 formulas have been input or derived (from 363 formulas).
% 14.23/14.43 ; 3215 (10%) were retained. Of these,
% 14.23/14.43 ; 322 (10%) were simplified or subsumed later,
% 14.23/14.43 ; 2893 (90%) are still being kept.
% 14.23/14.43 ;
% 14.23/14.43 ; Run time in seconds excluding printing time:
% 14.23/14.43 ; 0.005 0% Read assertion file (1 call)
% 14.23/14.43 ; 0.001 0% Assert (17 calls)
% 14.23/14.43 ; 0.394 3% Process new row (29,767 calls)
% 14.23/14.43 ; 0.106 1% Resolution (724 calls)
% 14.23/14.43 ; 0.375 3% Paramodulation (362 calls)
% 14.23/14.43 ; 0.000 0% Factoring (39 calls)
% 14.23/14.43 ; 0.001 0% Embedding (199 calls)
% 14.23/14.43 ; 0.106 1% Condensing (3,811 calls)
% 14.23/14.43 ; 0.165 1% Forward subsumption (3,811 calls)
% 14.23/14.43 ; 0.035 0% Backward subsumption (1,071 calls)
% 14.23/14.43 ; 0.050 0% Clause clause subsumption (12,754 calls)
% 14.23/14.43 ; 12.402 89% Forward simplification (29,531 calls)
% 14.23/14.43 ; 0.073 1% Backward simplification (3,019 calls)
% 14.23/14.43 ; 0.076 1% Ordering (31,244 calls)
% 14.23/14.43 ; 0.017 0% Ordering ac (2,751 calls)
% 14.23/14.43 ; 0.000 0% Sortal reasoning (32 calls)
% 14.23/14.43 ; 0.000 0% Purity testing (1 call)
% 14.23/14.43 ; 0.135 1% Other
% 14.23/14.43 ; 13.941 Total
% 14.23/14.43 ; 13.942 Real time
% 14.23/14.43 ;
% 14.23/14.43 ; Term-hash-array has 6,421 terms in all.
% 14.23/14.43 ; Feature-vector-row-index has 1,008 entries (1,008 at peak, 1,071 added, 63 deleted).
% 14.23/14.43 ; Feature-vector-row-index has 4,677 nodes (4,677 at peak, 5,236 added, 559 deleted).
% 14.23/14.43 ; Retrieved 16,746 possibly forward subsuming rows in 3,811 calls.
% 14.23/14.43 ; Retrieved 1,804 possibly backward subsumed rows in 1,071 calls.
% 14.23/14.43 ; Path-index has 5,901 entries (5,901 at peak, 6,459 added, 558 deleted).
% 14.23/14.43 ; Path-index has 1,328 nodes (1,328 at peak, 1,448 added, 120 deleted).
% 14.23/14.43 ; Trie-index has 5,901 entries (5,901 at peak, 6,459 added, 558 deleted).
% 14.23/14.43 ; Trie-index has 2,777 nodes (2,777 at peak, 3,135 added, 358 deleted).
% 14.23/14.43 ; Retrieved 17,746,599 generalization terms in 204,106 calls.
% 14.23/14.43 ; Retrieved 7,881 instance terms in 1,971 calls.
% 14.23/14.43 ; Retrieved 132,060 unifiable terms in 3,800 calls.
% 14.23/14.43 ;
% 14.23/14.43 ; The agenda of rows to process has 66 entries:
% 14.23/14.43 ; 8 with value 17 15 with value 22 3 with value 26
% 14.23/14.43 ; 5 with value 18 5 with value 23 4 with value 27
% 14.23/14.43 ; 5 with value 19 3 with value 24 3 with value 29
% 14.23/14.43 ; 5 with value 20 10 with value 25
% 14.23/14.43 ; The agenda of rows to give has 2556 entries:
% 14.23/14.43 ; 97 with value (4 19) 14 with value (4 37) 4 with value (4 63)
% 14.23/14.43 ; 163 with value (4 20) 25 with value (4 38) 8 with value (4 64)
% 14.23/14.43 ; 148 with value (4 21) 26 with value (4 39) 8 with value (4 65)
% 14.23/14.43 ; 172 with value (4 22) 10 with value (4 40) 8 with value (4 67)
% 14.23/14.43 ; 206 with value (4 23) 12 with value (4 41) 8 with value (4 68)
% 14.23/14.43 ; 184 with value (4 24) 8 with value (4 42) 8 with value (4 70)
% 14.23/14.43 ; 203 with value (4 25) 8 with value (4 43) 8 with value (4 71)
% 14.23/14.43 ; 127 with value (4 26) 8 with value (4 44) 4 with value (4 73)
% 14.23/14.43 ; 151 with value (4 27) 8 with value (4 45) 8 with value (4 77)
% 14.23/14.43 ; 129 with value (4 28) 4 with value (4 46) 8 with value (4 78)
% 14.23/14.43 ; 113 with value (4 29) 8 with value (4 47) 2 with value (4 79)
% 14.23/14.43 ; 94 with value (4 30) 2 with value (4 51) 8 with value (4 85)
% 14.23/14.43 ; 81 with value (4 31) 12 with value (4 53) 4 with value (4 91)
% 14.23/14.43 ; 102 with value (4 32) 4 with value (4 55) 8 with value (4 93)
% 14.23/14.43 ; 86 with value (4 33) 8 with value (4 56) 8 with value (4 97)
% 14.23/14.43 ; 82 with value (4 34) 4 with value (4 58) 8 with value (4 105)
% 14.23/14.43 ; 62 with value (4 35) 13 with value (4 59) 1 with value (4 107)
% 14.23/14.43 ; 54 with value (4 36) 13 with value (4 61) 4 with value (4 111)
% 14.23/14.43 Evaluation took:
% 14.23/14.43 13.943 seconds of real time
% 14.23/14.43 13.706734 seconds of user run time
% 14.23/14.43 0.236845 seconds of system run time
% 14.23/14.43 [Run times include 0.6 seconds GC run time.]
% 14.23/14.43 0 calls to %EVAL
% 14.23/14.43 0 page faults and
% 14.23/14.43 1,359,261,864 bytes consed.
% 14.23/14.43 :PROOF-FOUND
% 14.23/14.43 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-16T15:17:48
% 14.23/14.43 :PROOF-FOUND
% 14.23/14.43 *
%------------------------------------------------------------------------------