%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWX057+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n019.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:18 AM UTC 2025
% Result : Theorem 7.12s 7.37s
% Output : Refutation 7.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 14 unt; 0 nHn; 13 RR)
% Number of literals : 28 ( 7 equ; 10 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 16 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(449,axiom,
( ~ list_succeeds(X)
| ~ list_succeeds(Y)
| list_succeeds('**'(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(app:types:1)') ).
cnf(530,axiom,
( ~ permutation_succeeds(X,Y)
| list_succeeds(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(permutation:types)') ).
cnf(547,axiom,
( ~ list_succeeds(X)
| ~ list_succeeds(Y)
| occ(Z,'**'(X,Y)) = '@+'(occ(Z,X),occ(Z,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(occ:app)') ).
cnf(550,axiom,
( ~ permutation_succeeds(X,Y)
| occ(Z,X) = occ(Z,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(permutation:occ)') ).
cnf(555,axiom,
( ~ list_succeeds(X)
| ~ list_succeeds(Y)
| occ('SKOLEMAAAV130'(Y,X),Y) != occ('SKOLEMAAAV130'(Y,X),X)
| permutation_succeeds(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(occ:permutation)') ).
cnf(571,negated_conjecture,
permutation_succeeds('SKOLEMAAAV138','SKOLEMAAAV140'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(permutation:app)') ).
cnf(572,negated_conjecture,
permutation_succeeds('SKOLEMAAAV139','SKOLEMAAAV141'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(permutation:app)') ).
cnf(573,negated_conjecture,
~ permutation_succeeds('**'('SKOLEMAAAV138','SKOLEMAAAV139'),'**'('SKOLEMAAAV140','SKOLEMAAAV141')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(permutation:app)') ).
cnf(584,plain,
list_succeeds('SKOLEMAAAV139'),
inference('HYPERRESOLVE',[status(thm)],[530,572]) ).
cnf(585,plain,
list_succeeds('SKOLEMAAAV141'),
inference('HYPERRESOLVE',[status(thm)],[530,572]) ).
cnf(586,plain,
list_succeeds('SKOLEMAAAV138'),
inference('HYPERRESOLVE',[status(thm)],[530,571]) ).
cnf(587,plain,
list_succeeds('SKOLEMAAAV140'),
inference('HYPERRESOLVE',[status(thm)],[530,571]) ).
cnf(786,plain,
occ(X,'SKOLEMAAAV139') = occ(X,'SKOLEMAAAV141'),
inference('HYPERRESOLVE',[status(thm)],[550,572]) ).
cnf(787,plain,
occ(X,'SKOLEMAAAV138') = occ(X,'SKOLEMAAAV140'),
inference('HYPERRESOLVE',[status(thm)],[550,571]) ).
cnf(2201,plain,
list_succeeds('**'('SKOLEMAAAV138','SKOLEMAAAV139')),
inference('HYPERRESOLVE',[status(thm)],[449,586,584]) ).
cnf(2261,plain,
occ(X,'**'('SKOLEMAAAV138','SKOLEMAAAV139')) = '@+'(occ(X,'SKOLEMAAAV138'),occ(X,'SKOLEMAAAV139')),
inference('HYPERRESOLVE',[status(thm)],[547,586,584]) ).
cnf(2320,plain,
list_succeeds('**'('SKOLEMAAAV140','SKOLEMAAAV141')),
inference('HYPERRESOLVE',[status(thm)],[449,587,585]) ).
cnf(2390,plain,
occ(X,'**'('SKOLEMAAAV140','SKOLEMAAAV141')) = '@+'(occ(X,'SKOLEMAAAV138'),occ(X,'SKOLEMAAAV139')),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[547,587,585]),786,787,theory(equality)]) ).
cnf(12487,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[555,2320,2201,573]),2390,2261,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWX057+1 : TPTP v9.1.0. Released v9.1.0.
% 0.06/0.13 % Command : run-snark %s %d
% 0.12/0.35 % Computer : n019.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Mon Mar 31 15:19:02 EDT 2025
% 0.12/0.35 % CPUTime :
% 0.20/0.47 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.48 *
% 0.20/0.48 *
% 0.20/0.49 #<PACKAGE "SNARK-USER">
% 0.20/0.49 *
% 0.20/0.49 SNARK-TPTP-OPTIONS
% 0.20/0.49 *
% 0.20/0.49 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.49 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.49 (USE-FACTORING :POS)
% 0.20/0.49 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.49 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.49 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.49 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.49 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.49 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.49 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.49 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.49 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.49 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.49 *
% 0.20/0.49 "."
% 0.20/0.49 *
% 0.20/0.49 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2025-03-31T15:19:03
% 0.20/0.49 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n019.cluster.edu at 2025-03-31T15:19:03
% 0.20/0.58
% 0.20/0.58 ; Recognized relation functionality assertion (OR (NOT (|plus_succeeds| ?X ?Y ?Z)) (NOT (|plus_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.20/0.58 ; Recognized left identity assertion (= (@+ |0| ?X) ?X).
% 0.20/0.58 ; Recognized relation functionality assertion (OR (NOT (|times_succeeds| ?X ?Y ?Z)) (NOT (|times_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.20/0.58 ; Recognized relation functionality assertion (OR (NOT (|append_succeeds| ?X ?Y ?Z)) (NOT (|append_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.20/0.59 ; Recognized left identity assertion (= (** |nil| ?X) ?X).
% 0.20/0.59 ; Recognized relation functionality assertion (OR (NOT (|occ_succeeds| ?X ?Y ?Z)) (NOT (|occ_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.20/0.59 ; Recognized commutativity assertion (OR (NOT (|permutation_succeeds| ?X ?Y)) (|permutation_succeeds| ?Y ?X)).
% 7.12/7.37 ; Declaring permutation_succeeds to be commutative.
% 7.12/7.37
% 7.12/7.37 #||
% 7.12/7.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.12/7.37 % SZS output start Refutation
% See solution above
% 7.12/7.37 ||#
% 7.12/7.37
% 7.12/7.37 ; Summary of computation:
% 7.12/7.37 ; 43665 formulas have been input or derived (from 1040 formulas).
% 7.12/7.37 ; 12487 (29%) were retained. Of these,
% 7.12/7.37 ; 2020 (16%) were simplified or subsumed later,
% 7.12/7.37 ; 10467 (84%) are still being kept.
% 7.12/7.37 ;
% 7.12/7.37 ; Run time in seconds excluding printing time:
% 7.12/7.37 ; 0.071 1% Read assertion file (1 call)
% 7.12/7.37 ; 0.018 0% Assert (306 calls)
% 7.12/7.37 ; 0.954 14% Process new row (39,967 calls)
% 7.12/7.37 ; 3.324 48% Resolution (2,078 calls)
% 7.12/7.37 ; 0.031 0% Paramodulation (1,039 calls)
% 7.12/7.37 ; 0.000 0% Factoring (81 calls)
% 7.12/7.37 ; 0.047 1% Condensing (8,790 calls)
% 7.12/7.37 ; 0.733 11% Forward subsumption (8,790 calls)
% 7.12/7.37 ; 0.145 2% Backward subsumption (2,423 calls)
% 7.12/7.37 ; 0.057 1% Clause clause subsumption (17,345 calls)
% 7.12/7.37 ; 0.970 14% Forward simplification (39,512 calls)
% 7.12/7.37 ; 0.160 2% Backward simplification (12,487 calls)
% 7.12/7.37 ; 0.199 3% Ordering (66,329 calls)
% 7.12/7.37 ; 0.000 0% Sortal reasoning (32 calls)
% 7.12/7.37 ; 0.002 0% Purity testing (1 call)
% 7.12/7.37 ; 0.171 2% Other
% 7.12/7.37 ; 6.882 Total
% 7.12/7.37 ; 6.882 Real time
% 7.12/7.37 ;
% 7.12/7.37 ; Term-hash-array has 22,231 terms in all.
% 7.12/7.37 ; Feature-vector-row-index has 1,861 entries (1,861 at peak, 2,423 added, 562 deleted).
% 7.12/7.37 ; Feature-vector-row-index has 18,142 nodes (18,142 at peak, 22,738 added, 4,596 deleted).
% 7.12/7.37 ; Retrieved 32,368 possibly forward subsuming rows in 8,790 calls.
% 7.12/7.37 ; Retrieved 1,471 possibly backward subsumed rows in 2,423 calls.
% 7.12/7.37 ; Path-index has 19,202 entries (19,296 at peak, 23,530 added, 4,328 deleted).
% 7.12/7.37 ; Path-index has 19,396 nodes (19,446 at peak, 23,324 added, 3,928 deleted).
% 7.12/7.37 ; Trie-index has 19,202 entries (19,296 at peak, 23,530 added, 4,328 deleted).
% 7.12/7.37 ; Trie-index has 77,814 nodes (78,403 at peak, 100,570 added, 22,756 deleted).
% 7.12/7.37 ; Retrieved 98,214 generalization terms in 279,696 calls.
% 7.12/7.37 ; Retrieved 11,894 instance terms in 10,755 calls.
% 7.12/7.37 ; Retrieved 5,228,603 unifiable terms in 90,643 calls.
% 7.12/7.37 ;
% 7.12/7.37 ; The agenda of rows to process has 35 entries:
% 7.12/7.37 ; 6 with value 30 2 with value 34 4 with value 44
% 7.12/7.37 ; 4 with value 31 4 with value 38 4 with value 46
% 7.12/7.37 ; 4 with value 32 4 with value 43 1 with value 52
% 7.12/7.37 ; 2 with value 33
% 7.12/7.37 ; The agenda of rows to give has 9510 entries:
% 7.12/7.37 ; 178 with value (4 8) 9 with value (4 36) 1 with value (4 70)
% 7.12/7.37 ; 242 with value (4 9) 10 with value (4 37) 2 with value (4 72)
% 7.12/7.37 ; 342 with value (4 10) 13 with value (4 38) 2 with value (4 74)
% 7.12/7.37 ; 478 with value (4 11) 13 with value (4 39) 1 with value (4 75)
% 7.12/7.37 ; 435 with value (4 12) 8 with value (4 40) 2 with value (4 76)
% 7.12/7.37 ; 529 with value (4 13) 7 with value (4 41) 1 with value (4 78)
% 7.12/7.37 ; 404 with value (4 14) 10 with value (4 42) 2 with value (4 79)
% 7.12/7.37 ; 286 with value (4 15) 19 with value (4 44) 4 with value (4 88)
% 7.12/7.37 ; 518 with value (4 16) 9 with value (4 45) 4 with value (4 91)
% 7.12/7.37 ; 230 with value (4 17) 8 with value (4 46) 24 with value (4 97)
% 7.12/7.37 ; 513 with value (4 18) 7 with value (4 47) 76 with value (4 100)
% 7.12/7.37 ; 467 with value (4 19) 4 with value (4 48) 80 with value (4 103)
% 7.12/7.37 ; 429 with value (4 20) 5 with value (4 50) 28 with value (4 106)
% 7.12/7.37 ; 876 with value (4 21) 10 with value (4 51) 1 with value (4 108)
% 7.12/7.37 ; 374 with value (4 22) 25 with value (4 52) 2 with value (4 112)
% 7.12/7.37 ; 383 with value (4 23) 6 with value (4 54) 2 with value (4 115)
% 7.12/7.37 ; 264 with value (4 24) 9 with value (4 55) 2 with value (4 118)
% 7.12/7.37 ; 280 with value (4 25) 1 with value (4 56) 2 with value (4 120)
% 7.12/7.37 ; 514 with value (4 26) 5 with value (4 57) 2 with value (4 121)
% 7.12/7.37 ; 152 with value (4 27) 5 with value (4 58) 2 with value (4 123)
% 7.12/7.37 ; 188 with value (4 28) 1 with value (4 59) 2 with value (4 126)
% 7.12/7.37 ; 230 with value (4 29) 5 with value (4 60) 2 with value (4 129)
% 7.12/7.37 ; 74 with value (4 30) 2 with value (4 61) 16 with value (4 140)
% 7.12/7.37 ; 133 with value (4 31) 2 with value (4 62) 64 with value (4 143)
% 7.12/7.37 ; 136 with value (4 32) 1 with value (4 64) 96 with value (4 146)
% 7.12/7.37 ; 95 with value (4 33) 1 with value (4 67) 64 with value (4 149)
% 7.12/7.37 ; 46 with value (4 34) 1 with value (4 68) 16 with value (4 152)
% 7.12/7.37 ; 17 with value (4 35) 1 with value (4 69)
% 7.12/7.37 Evaluation took:
% 7.12/7.37 6.885 seconds of real time
% 7.12/7.37 6.466283 seconds of user run time
% 7.12/7.37 0.419737 seconds of system run time
% 7.12/7.37 [Run times include 0.819 seconds GC run time.]
% 7.12/7.37 0 calls to %EVAL
% 7.12/7.37 0 page faults and
% 7.12/7.37 482,805,336 bytes consed.
% 7.12/7.37 :PROOF-FOUND
% 7.12/7.37 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2025-03-31T15:19:09
% 7.12/7.37 :PROOF-FOUND
% 7.12/7.37 *
%------------------------------------------------------------------------------