%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWX055+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n004.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 9.54s 9.70s
% Output : Refutation 9.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of clauses : 26 ( 16 unt; 4 nHn; 19 RR)
% Number of literals : 42 ( 6 equ; 20 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 26 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(23,axiom,
( ~ same_occ_succeeds(X,Y)
| ~ same_occ_fails(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id20) ).
cnf(50,axiom,
( member2_succeeds(X,Y,Z)
| ~ member_succeeds(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id46) ).
cnf(51,axiom,
( member2_succeeds(X,Y,Z)
| ~ member_succeeds(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id46) ).
cnf(117,axiom,
( not_same_occ_succeeds(X,Y)
| ~ member2_succeeds(Z,X,Y)
| ~ occ_succeeds(Z,X,U)
| ~ occ_succeeds(Z,Y,V)
| U = V ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id52) ).
cnf(135,axiom,
( same_occ_fails(X,Y)
| ~ not_same_occ_succeeds(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id56) ).
cnf(434,axiom,
( ~ list_succeeds(X)
| member_succeeds(Y,X)
| member_fails(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(member:termination)_014') ).
cnf(528,axiom,
( ~ list_succeeds(X)
| occ(Y,X) != Z
| occ_succeeds(Y,X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','occ/2') ).
cnf(557,axiom,
( ~ list_succeeds(X)
| ~ member_fails(Y,X)
| occ(Y,X) = '0' ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(occ:member)') ).
cnf(564,negated_conjecture,
list_succeeds('SKOLEMAAAU136'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(same_occ:success)') ).
cnf(565,negated_conjecture,
list_succeeds('SKOLEMAAAU137'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(same_occ:success)') ).
cnf(566,negated_conjecture,
same_occ_succeeds('SKOLEMAAAU136','SKOLEMAAAU137'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(same_occ:success)') ).
cnf(567,negated_conjecture,
occ('SKOLEMAAAU138','SKOLEMAAAU136') != occ('SKOLEMAAAU138','SKOLEMAAAU137'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(same_occ:success)') ).
cnf(591,plain,
~ same_occ_fails('SKOLEMAAAU136','SKOLEMAAAU137'),
inference('UR-RESOLVE',[status(thm)],[23,566]) ).
cnf(654,plain,
( member_succeeds(X,'SKOLEMAAAU137')
| member_fails(X,'SKOLEMAAAU137') ),
inference('HYPERRESOLVE',[status(thm)],[434,565]) ).
cnf(655,plain,
( member_succeeds(X,'SKOLEMAAAU136')
| member_fails(X,'SKOLEMAAAU136') ),
inference('HYPERRESOLVE',[status(thm)],[434,564]) ).
cnf(904,plain,
occ_succeeds(X,'SKOLEMAAAU137',occ(X,'SKOLEMAAAU137')),
inference('HYPERRESOLVE',[status(thm)],[528,565,theory(equality)]) ).
cnf(905,plain,
occ_succeeds(X,'SKOLEMAAAU136',occ(X,'SKOLEMAAAU136')),
inference('HYPERRESOLVE',[status(thm)],[528,564,theory(equality)]) ).
cnf(2416,plain,
~ not_same_occ_succeeds('SKOLEMAAAU136','SKOLEMAAAU137'),
inference('UR-RESOLVE',[status(thm)],[135,591]) ).
cnf(13128,plain,
~ member2_succeeds('SKOLEMAAAU138','SKOLEMAAAU136','SKOLEMAAAU137'),
inference('UR-RESOLVE',[status(thm)],[117,905,2416,904,567]) ).
cnf(13181,plain,
~ member_succeeds('SKOLEMAAAU138','SKOLEMAAAU136'),
inference('UR-RESOLVE',[status(thm)],[51,13128]) ).
cnf(13182,plain,
~ member_succeeds('SKOLEMAAAU138','SKOLEMAAAU137'),
inference('UR-RESOLVE',[status(thm)],[50,13128]) ).
cnf(13184,plain,
member_fails('SKOLEMAAAU138','SKOLEMAAAU136'),
inference('HYPERRESOLVE',[status(thm)],[13181,655]) ).
cnf(13207,plain,
member_fails('SKOLEMAAAU138','SKOLEMAAAU137'),
inference('HYPERRESOLVE',[status(thm)],[13182,654]) ).
cnf(19193,plain,
occ('SKOLEMAAAU138','SKOLEMAAAU136') = '0',
inference('HYPERRESOLVE',[status(thm)],[557,13184,564]) ).
cnf(19194,plain,
'0' != occ('SKOLEMAAAU138','SKOLEMAAAU137'),
inference('REWRITE',[status(thm)],[567,19193,theory(equality)]) ).
cnf(19254,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[557,19194,565]),13207]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SWX055+1 : TPTP v9.1.0. Released v9.1.0.
% 0.11/0.12 % Command : run-snark %s %d
% 0.13/0.33 % Computer : n004.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Mar 31 15:14:40 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.19/0.44 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 *
% 0.19/0.45 *
% 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/sandbox2/benchmark/theBenchmark.p 2025-03-31T15:14:40
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n004.cluster.edu at 2025-03-31T15:14:40
% 0.19/0.55
% 0.19/0.55 ; Recognized relation functionality assertion (OR (NOT (|plus_succeeds| ?X ?Y ?Z)) (NOT (|plus_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.19/0.55 ; Recognized left identity assertion (= (@+ |0| ?X) ?X).
% 0.19/0.55 ; Recognized relation functionality assertion (OR (NOT (|times_succeeds| ?X ?Y ?Z)) (NOT (|times_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.19/0.55 ; Recognized relation functionality assertion (OR (NOT (|append_succeeds| ?X ?Y ?Z)) (NOT (|append_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 0.19/0.56 ; Recognized left identity assertion (= (** |nil| ?X) ?X).
% 9.54/9.70 ; Recognized relation functionality assertion (OR (NOT (|occ_succeeds| ?X ?Y ?Z)) (NOT (|occ_succeeds| ?X ?Y ?U)) (= ?Z ?U)).
% 9.54/9.70
% 9.54/9.70 #||
% 9.54/9.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.54/9.70 % SZS output start Refutation
% See solution above
% 9.54/9.70 ||#
% 9.54/9.70
% 9.54/9.70 ; Summary of computation:
% 9.54/9.70 ; 68005 formulas have been input or derived (from 1464 formulas).
% 9.54/9.70 ; 19254 (28%) were retained. Of these,
% 9.54/9.70 ; 2654 (14%) were simplified or subsumed later,
% 9.54/9.70 ; 16600 (86%) are still being kept.
% 9.54/9.70 ;
% 9.54/9.70 ; Run time in seconds excluding printing time:
% 9.54/9.70 ; 0.068 1% Read assertion file (1 call)
% 9.54/9.70 ; 0.022 0% Assert (301 calls)
% 9.54/9.70 ; 1.693 18% Process new row (62,198 calls)
% 9.54/9.70 ; 4.402 48% Resolution (2,926 calls)
% 9.54/9.70 ; 0.057 1% Paramodulation (1,463 calls)
% 9.54/9.70 ; 0.000 0% Factoring (83 calls)
% 9.54/9.70 ; 0.092 1% Condensing (4,013 calls)
% 9.54/9.70 ; 0.416 5% Forward subsumption (4,013 calls)
% 9.54/9.70 ; 0.171 2% Backward subsumption (2,371 calls)
% 9.54/9.70 ; 0.024 0% Clause clause subsumption (3,600 calls)
% 9.54/9.70 ; 1.460 16% Forward simplification (61,329 calls)
% 9.54/9.70 ; 0.352 4% Backward simplification (19,254 calls)
% 9.54/9.70 ; 0.262 3% Ordering (101,315 calls)
% 9.54/9.70 ; 0.000 0% Sortal reasoning (32 calls)
% 9.54/9.70 ; 0.002 0% Purity testing (1 call)
% 9.54/9.70 ; 0.222 2% Other
% 9.54/9.70 ; 9.243 Total
% 9.54/9.70 ; 9.245 Real time
% 9.54/9.70 ;
% 9.54/9.71 ; Term-hash-array has 35,268 terms in all.
% 9.54/9.71 ; Feature-vector-row-index has 2,085 entries (2,085 at peak, 2,371 added, 286 deleted).
% 9.54/9.71 ; Feature-vector-row-index has 18,977 nodes (18,977 at peak, 21,808 added, 2,831 deleted).
% 9.54/9.71 ; Retrieved 4,446 possibly forward subsuming rows in 4,013 calls.
% 9.54/9.71 ; Retrieved 1,668 possibly backward subsumed rows in 2,371 calls.
% 9.54/9.71 ; Path-index has 31,033 entries (31,053 at peak, 36,202 added, 5,169 deleted).
% 9.54/9.71 ; Path-index has 24,458 nodes (24,458 at peak, 28,418 added, 3,960 deleted).
% 9.54/9.71 ; Trie-index has 31,033 entries (31,053 at peak, 36,202 added, 5,169 deleted).
% 9.54/9.71 ; Trie-index has 138,462 nodes (138,622 at peak, 163,828 added, 25,366 deleted).
% 9.54/9.71 ; Retrieved 175,470 generalization terms in 453,950 calls.
% 9.54/9.71 ; Retrieved 19,279 instance terms in 17,904 calls.
% 9.54/9.71 ; Retrieved 7,368,464 unifiable terms in 130,519 calls.
% 9.54/9.71 ;
% 9.54/9.71 ; The agenda of rows to process has 302 entries:
% 9.54/9.71 ; 1 with value 6 3 with value 14 4 with value 21
% 9.54/9.71 ; 1 with value 7 13 with value 15 6 with value 22
% 9.54/9.71 ; 9 with value 8 21 with value 16 4 with value 23
% 9.54/9.71 ; 27 with value 9 12 with value 17 6 with value 24
% 9.54/9.71 ; 40 with value 10 15 with value 18 1 with value 26
% 9.54/9.71 ; 43 with value 11 15 with value 19 1 with value 38
% 9.54/9.71 ; 38 with value 12 17 with value 20 1 with value 40
% 9.54/9.71 ; 24 with value 13
% 9.54/9.71 ; The agenda of rows to give has 15272 entries:
% 9.54/9.71 ; 1 with value (4 6) 7 with value (4 45) 11 with value (4 106)
% 9.54/9.71 ; 16 with value (4 9) 8 with value (4 46) 1 with value (4 108)
% 9.54/9.71 ; 471 with value (4 10) 11 with value (4 47) 2 with value (4 112)
% 9.54/9.71 ; 676 with value (4 11) 6 with value (4 48) 2 with value (4 115)
% 9.54/9.71 ; 643 with value (4 12) 7 with value (4 50) 2 with value (4 118)
% 9.54/9.71 ; 978 with value (4 13) 21 with value (4 51) 2 with value (4 120)
% 9.54/9.71 ; 723 with value (4 14) 17 with value (4 52) 2 with value (4 121)
% 9.54/9.71 ; 669 with value (4 15) 4 with value (4 53) 2 with value (4 123)
% 9.54/9.71 ; 576 with value (4 16) 9 with value (4 54) 2 with value (4 126)
% 9.54/9.71 ; 585 with value (4 17) 5 with value (4 55) 2 with value (4 129)
% 9.54/9.71 ; 642 with value (4 18) 1 with value (4 56) 2 with value (4 131)
% 9.54/9.71 ; 598 with value (4 19) 4 with value (4 57) 4 with value (4 134)
% 9.54/9.71 ; 551 with value (4 20) 5 with value (4 58) 4 with value (4 137)
% 9.54/9.71 ; 684 with value (4 21) 1 with value (4 59) 4 with value (4 139)
% 9.54/9.71 ; 917 with value (4 22) 5 with value (4 60) 9 with value (4 140)
% 9.54/9.71 ; 603 with value (4 23) 4 with value (4 61) 16 with value (4 142)
% 9.54/9.71 ; 451 with value (4 24) 2 with value (4 62) 24 with value (4 143)
% 9.54/9.71 ; 457 with value (4 25) 3 with value (4 64) 24 with value (4 145)
% 9.54/9.71 ; 498 with value (4 26) 1 with value (4 67) 30 with value (4 146)
% 9.54/9.71 ; 429 with value (4 27) 1 with value (4 68) 20 with value (4 148)
% 9.54/9.71 ; 440 with value (4 28) 1 with value (4 69) 20 with value (4 149)
% 9.54/9.71 ; 675 with value (4 29) 1 with value (4 70) 4 with value (4 151)
% 9.54/9.71 ; 338 with value (4 30) 2 with value (4 72) 5 with value (4 152)
% 9.54/9.71 ; 690 with value (4 31) 2 with value (4 74) 2 with value (4 153)
% 9.54/9.71 ; 469 with value (4 32) 1 with value (4 75) 2 with value (4 198)
% 9.54/9.71 ; 359 with value (4 33) 2 with value (4 76) 4 with value (4 201)
% 9.54/9.71 ; 123 with value (4 34) 1 with value (4 78) 2 with value (4 202)
% 9.54/9.71 ; 374 with value (4 35) 2 with value (4 79) 2 with value (4 203)
% 9.54/9.71 ; 17 with value (4 36) 4 with value (4 88) 4 with value (4 204)
% 9.54/9.71 ; 27 with value (4 37) 4 with value (4 91) 2 with value (4 205)
% 9.54/9.71 ; 33 with value (4 38) 4 with value (4 96) 4 with value (4 206)
% 9.54/9.71 ; 10 with value (4 39) 11 with value (4 97) 8 with value (4 207)
% 9.54/9.71 ; 6 with value (4 40) 12 with value (4 99) 4 with value (4 209)
% 9.54/9.71 ; 7 with value (4 41) 33 with value (4 100) 6 with value (4 210)
% 9.54/9.71 ; 10 with value (4 42) 12 with value (4 102) 6 with value (4 212)
% 9.54/9.71 ; 12 with value (4 43) 33 with value (4 103) 4 with value (4 215)
% 9.54/9.71 ; 19 with value (4 44) 4 with value (4 105)
% 9.54/9.71 Evaluation took:
% 9.54/9.71 9.248 seconds of real time
% 9.54/9.71 8.654059 seconds of user run time
% 9.54/9.71 0.594011 seconds of system run time
% 9.54/9.71 [Run times include 1.428 seconds GC run time.]
% 9.54/9.71 0 calls to %EVAL
% 9.54/9.71 0 page faults and
% 9.54/9.71 625,108,008 bytes consed.
% 9.54/9.71 :PROOF-FOUND
% 9.54/9.71 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2025-03-31T15:14:49
% 9.54/9.71 :PROOF-FOUND
% 9.54/9.71 *
%------------------------------------------------------------------------------