%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : COM130+1 : TPTP v8.1.0. Released v6.4.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 : Fri Jul 15 01:43:05 EDT 2022
% Result : Theorem 18.57s 18.79s
% Output : Refutation 18.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 6
% Syntax : Number of clauses : 13 ( 9 unt; 2 nHn; 12 RR)
% Number of literals : 24 ( 11 equ; 13 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 27 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(19,axiom,
( X != Y
| Z != vabs(U,V,W)
| ~ visFreeVar(X,Z)
| Y != U ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',isFreeVar1) ).
cnf(92,axiom,
( X != Y
| Z != U
| V != vabs(W,X1,Y1)
| Y != W
| Z1 != vsubst(X,Z,V)
| Z1 = vabs(W,X1,Y1) ),
file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax',subst3) ).
cnf(23433,axiom,
( visFreeVar(X,Y)
| ~ vtcheck(vbind(X,Z,U),Y,V)
| vtcheck(U,Y,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-Strong') ).
cnf(23436,negated_conjecture,
'SKOLEMAAAV77' = 'SKOLEMAAAV79',
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-subst-abs-1') ).
cnf(23438,negated_conjecture,
vtcheck(vbind('SKOLEMAAAV77','SKOLEMAAAV75','SKOLEMAAAV76'),vabs('SKOLEMAAAV79','SKOLEMAAAV80','SKOLEMAAAV81'),'SKOLEMAAAV82'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-subst-abs-1') ).
cnf(23439,plain,
vtcheck(vbind('SKOLEMAAAV77','SKOLEMAAAV75','SKOLEMAAAV76'),vabs('SKOLEMAAAV77','SKOLEMAAAV80','SKOLEMAAAV81'),'SKOLEMAAAV82'),
inference('REWRITE',[status(thm)],[23438,23436,theory(equality)]) ).
cnf(23440,negated_conjecture,
~ vtcheck('SKOLEMAAAV76',vsubst('SKOLEMAAAV77','SKOLEMAAAV78',vabs('SKOLEMAAAV79','SKOLEMAAAV80','SKOLEMAAAV81')),'SKOLEMAAAV82'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','T-subst-abs-1') ).
cnf(23441,plain,
~ vtcheck('SKOLEMAAAV76',vsubst('SKOLEMAAAV77','SKOLEMAAAV78',vabs('SKOLEMAAAV77','SKOLEMAAAV80','SKOLEMAAAV81')),'SKOLEMAAAV82'),
inference('REWRITE',[status(thm)],[23440,23436,theory(equality)]) ).
cnf(23545,plain,
( visFreeVar('SKOLEMAAAV77',vabs('SKOLEMAAAV77','SKOLEMAAAV80','SKOLEMAAAV81'))
| vtcheck('SKOLEMAAAV76',vabs('SKOLEMAAAV77','SKOLEMAAAV80','SKOLEMAAAV81'),'SKOLEMAAAV82') ),
inference('HYPERRESOLVE',[status(thm)],[23433,23439]) ).
cnf(23549,plain,
~ visFreeVar(X,vabs(X,Y,Z)),
inference('UR-RESOLVE',[status(thm)],[19,theory(equality),theory(equality),theory(equality)]) ).
cnf(23550,plain,
vtcheck('SKOLEMAAAV76',vabs('SKOLEMAAAV77','SKOLEMAAAV80','SKOLEMAAAV81'),'SKOLEMAAAV82'),
inference('REWRITE',[status(thm)],[23545,23549]) ).
cnf(23619,plain,
vsubst(X,Y,vabs(X,Z,U)) = vabs(X,Z,U),
inference('HYPERRESOLVE',[status(thm)],[92,theory(equality),theory(equality),theory(equality),theory(equality),theory(equality)]) ).
cnf(23620,plain,
$false,
inference('REWRITE',[status(thm)],[23441,23550,23619,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : COM130+1 : TPTP v8.1.0. Released v6.4.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.14/0.34 % Computer : n011.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Thu Jun 16 18:41:51 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.20/0.46 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.47 *
% 0.20/0.47 *
% 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-16T18:41:51
% 0.20/0.48 ; 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-06-16T18:41:51
% 18.57/18.79
% 18.57/18.79
% 18.57/18.79 #||
% 18.57/18.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.57/18.79 % SZS output start Refutation
% See solution above
% 18.57/18.79 ||#
% 18.57/18.79
% 18.57/18.79 ; Summary of computation:
% 18.57/18.79 ; 24366 formulas have been input or derived (from 101 formulas).
% 18.57/18.79 ; 23620 (97%) were retained. Of these,
% 18.57/18.79 ; 622 ( 3%) were simplified or subsumed later,
% 18.57/18.79 ; 22998 (97%) are still being kept.
% 18.57/18.79 ;
% 18.57/18.79 ; Run time in seconds excluding printing time:
% 18.57/18.79 ; 0.024 0% Read assertion file (1 call)
% 18.57/18.79 ; 0.715 4% Assert (59 calls)
% 18.57/18.79 ; 2.797 15% Process new row (24,255 calls)
% 18.57/18.79 ; 4.185 23% Resolution (200 calls)
% 18.57/18.79 ; 0.002 0% Paramodulation (100 calls)
% 18.57/18.79 ; 0.795 4% Condensing (23,465 calls)
% 18.57/18.79 ; 5.526 30% Forward subsumption (23,465 calls)
% 18.57/18.79 ; 1.697 9% Backward subsumption (23,455 calls)
% 18.57/18.79 ; 1.092 6% Clause clause subsumption (121,421 calls)
% 18.57/18.79 ; 1.271 7% Forward simplification (24,255 calls)
% 18.57/18.79 ; 0.025 0% Backward simplification (23,618 calls)
% 18.57/18.79 ; 0.000 0% Ordering (250 calls)
% 18.57/18.79 ; 0.000 0% Sortal reasoning (32 calls)
% 18.57/18.79 ; 0.041 0% Purity testing (1 call)
% 18.57/18.79 ; 0.138 1% Other
% 18.57/18.79 ; 18.308 Total
% 18.57/18.79 ; 18.312 Real time
% 18.57/18.79 ;
% 18.57/18.80 ; Term-hash-array has 871 terms in all.
% 18.57/18.80 ; Feature-vector-row-index has 22,854 entries (22,854 at peak, 23,455 added, 601 deleted).
% 18.57/18.80 ; Feature-vector-row-index has 142,743 nodes (143,344 at peak, 156,164 added, 13,421 deleted).
% 18.57/18.80 ; Retrieved 127,055 possibly forward subsuming rows in 23,465 calls.
% 18.57/18.80 ; Retrieved 67,535 possibly backward subsumed rows in 23,455 calls.
% 18.57/18.80 ; Path-index has 829 entries (837 at peak, 885 added, 56 deleted).
% 18.57/18.80 ; Path-index has 3,928 nodes (3,938 at peak, 3,943 added, 15 deleted).
% 18.57/18.80 ; Trie-index has 829 entries (837 at peak, 885 added, 56 deleted).
% 18.57/18.80 ; Trie-index has 3,360 nodes (3,388 at peak, 3,524 added, 164 deleted).
% 18.57/18.80 ; Retrieved 757 generalization terms in 156,643 calls.
% 18.57/18.80 ; Retrieved 184 instance terms in 162 calls.
% 18.57/18.80 ; Retrieved 165,302 unifiable terms in 2,890 calls.
% 18.57/18.80 ;
% 18.57/18.80 ; The agenda of rows to process has 56 entries:
% 18.57/18.80 ; 41 with value 16 1 with value 18 1 with value 22
% 18.57/18.80 ; 10 with value 17 3 with value 20
% 18.57/18.80 ; The agenda of input rows to give has 22739 entries:
% 18.57/18.80 ; 10 with value 37 295 with value 81 192 with value 124
% 18.57/18.80 ; 7 with value 38 611 with value 82 128 with value 125
% 18.57/18.80 ; 8 with value 39 303 with value 83 138 with value 126
% 18.57/18.80 ; 6 with value 40 425 with value 84 99 with value 127
% 18.57/18.80 ; 3 with value 41 450 with value 85 161 with value 128
% 18.57/18.80 ; 4 with value 42 439 with value 86 89 with value 129
% 18.57/18.80 ; 10 with value 43 458 with value 87 148 with value 130
% 18.57/18.80 ; 7 with value 44 356 with value 88 87 with value 131
% 18.57/18.80 ; 6 with value 45 474 with value 89 148 with value 132
% 18.57/18.80 ; 4 with value 46 476 with value 90 73 with value 133
% 18.57/18.80 ; 10 with value 47 338 with value 91 136 with value 134
% 18.57/18.80 ; 6 with value 48 448 with value 92 49 with value 135
% 18.57/18.80 ; 6 with value 49 316 with value 93 129 with value 136
% 18.57/18.80 ; 5 with value 50 440 with value 94 49 with value 137
% 18.57/18.80 ; 7 with value 51 302 with value 95 105 with value 138
% 18.57/18.80 ; 6 with value 52 395 with value 96 43 with value 139
% 18.57/18.80 ; 4 with value 53 350 with value 97 79 with value 140
% 18.57/18.80 ; 3 with value 54 443 with value 98 37 with value 141
% 18.57/18.80 ; 3 with value 55 348 with value 99 84 with value 142
% 18.57/18.80 ; 3 with value 56 499 with value 100 33 with value 143
% 18.57/18.80 ; 3 with value 57 279 with value 101 72 with value 144
% 18.57/18.80 ; 1 with value 58 516 with value 102 27 with value 145
% 18.57/18.80 ; 2 with value 59 173 with value 103 80 with value 146
% 18.57/18.80 ; 7 with value 60 583 with value 104 17 with value 147
% 18.57/18.80 ; 2 with value 61 124 with value 105 60 with value 148
% 18.57/18.80 ; 98 with value 62 506 with value 106 19 with value 149
% 18.57/18.80 ; 3 with value 63 169 with value 107 41 with value 150
% 18.57/18.80 ; 137 with value 64 540 with value 108 18 with value 151
% 18.57/18.80 ; 17 with value 65 194 with value 109 15 with value 152
% 18.57/18.80 ; 362 with value 66 435 with value 110 14 with value 153
% 18.57/18.80 ; 372 with value 68 205 with value 111 29 with value 154
% 18.57/18.80 ; 73 with value 69 457 with value 112 6 with value 155
% 18.57/18.80 ; 525 with value 70 173 with value 113 32 with value 156
% 18.57/18.80 ; 90 with value 71 350 with value 114 2 with value 157
% 18.57/18.80 ; 380 with value 72 132 with value 115 34 with value 158
% 18.57/18.80 ; 184 with value 73 392 with value 116 20 with value 160
% 18.57/18.80 ; 542 with value 74 124 with value 117 11 with value 162
% 18.57/18.80 ; 235 with value 75 304 with value 118 3 with value 164
% 18.57/18.80 ; 453 with value 76 159 with value 119 13 with value 166
% 18.57/18.80 ; 260 with value 77 303 with value 120 16 with value 168
% 18.57/18.80 ; 669 with value 78 159 with value 121 14 with value 170
% 18.57/18.80 ; 236 with value 79 203 with value 122 6 with value 172
% 18.57/18.80 ; 624 with value 80 142 with value 123 2 with value 174
% 18.57/18.80 ; The agenda of rows to give has 159 entries:
% 18.57/18.80 ; 2 with value (4 4) 7 with value (4 17) 1 with value (4 32)
% 18.57/18.80 ; 3 with value (4 6) 10 with value (4 18) 2 with value (4 34)
% 18.57/18.80 ; 3 with value (4 7) 2 with value (4 19) 1 with value (4 35)
% 18.57/18.80 ; 4 with value (4 8) 5 with value (4 20) 4 with value (4 37)
% 18.57/18.80 ; 6 with value (4 9) 1 with value (4 21) 2 with value (4 38)
% 18.57/18.80 ; 8 with value (4 10) 3 with value (4 22) 1 with value (4 39)
% 18.57/18.80 ; 5 with value (4 11) 1 with value (4 23) 1 with value (4 40)
% 18.57/18.80 ; 16 with value (4 12) 1 with value (4 25) 1 with value (4 41)
% 18.57/18.80 ; 8 with value (4 13) 1 with value (4 27) 1 with value (4 42)
% 18.57/18.80 ; 24 with value (4 14) 1 with value (4 30) 1 with value (4 44)
% 18.57/18.80 ; 7 with value (4 15) 2 with value (4 31) 1 with value (4 45)
% 18.57/18.80 ; 23 with value (4 16)
% 18.57/18.80 Evaluation took:
% 18.57/18.80 18.325 seconds of real time
% 18.57/18.80 17.662308 seconds of user run time
% 18.57/18.80 0.660529 seconds of system run time
% 18.57/18.80 [Run times include 1.401 seconds GC run time.]
% 18.57/18.80 0 calls to %EVAL
% 18.57/18.80 0 page faults and
% 18.57/18.80 1,540,253,840 bytes consed.
% 18.57/18.80 :PROOF-FOUND
% 18.57/18.80 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-16T18:42:10
% 18.57/18.80 :PROOF-FOUND
% 18.57/18.80 *
%------------------------------------------------------------------------------