%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP001_1 : TPTP v8.1.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n025.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 00:35:13 EDT 2022
% Result : Theorem 54.74s 54.95s
% Output : Refutation 54.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 4
% Syntax : Number of formulae : 7 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 38 ( 7 equ)
% Maximal formula atoms : 2 ( 5 avg)
% Number of connectives : 4 ( 3 ~; 1 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 30 ( 30 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 15 usr; 8 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 7 ( 0 sgn 7 !; 0 ?; 7 :)
% Comments :
%------------------------------------------------------------------------------
tff(5,axiom,
! [X: 'B_ell2$',Y: 'A_ell2$'] : ( 'fun_app$d'('uuf$'(X),Y) = 'fun_app$e'('tensor_ell2$'(Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom2) ).
tff(57,negated_conjecture,
'fun_app$n'('image$'('tensor_ell2$'('psi$')),'top$a') != 'top$b',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture24) ).
tff(58,axiom,
! [X: 'A_b_prod_ell2$'] : ( 'fun_app$e'('tensor_ell2$'('psi$'),'SKOLEMAAAV1.B_ell2$'(X)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom25) ).
tff(59,plain,
! [X: 'A_b_prod_ell2$'] : ( 'fun_app$d'('uuf$'('SKOLEMAAAV1.B_ell2$'(X)),'psi$') = X ),
inference('REWRITE',[status(thm)],[58,5,theory(equality)]) ).
tff(232,axiom,
! [X: 'B_ell2_a_b_prod_ell2_fun$',Y: 'B_ell2$'] :
( ( 'fun_app$n'('image$'(X),'top$a') = 'top$b' )
| ( 'SKOLEMAAAV67.A_b_prod_ell2$'(X) != 'fun_app$e'(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom134) ).
tff(1386,plain,
! [X: 'B_ell2$'] : ( 'SKOLEMAAAV67.A_b_prod_ell2$'('tensor_ell2$'('psi$')) != 'fun_app$d'('uuf$'(X),'psi$') ),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[232,57]),5,theory(equality)]) ).
cnf(29325,plain,
$false,
inference('HYPERRESOLVE',[status(thm)],[1386,59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : ITP001_1 : TPTP v8.1.0. Released v8.1.0.
% 0.10/0.12 % Command : run-snark %s %d
% 0.13/0.33 % Computer : n025.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 : 600
% 0.13/0.33 % DateTime : Thu Jun 2 11:53:44 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.20/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 *
% 0.20/0.46 *
% 0.20/0.46 #<PACKAGE "SNARK-USER">
% 0.20/0.46 *
% 0.20/0.46 SNARK-TPTP-OPTIONS
% 0.20/0.46 *
% 0.20/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.46 (USE-FACTORING :POS)
% 0.20/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.46 *
% 0.20/0.46 "."
% 0.20/0.46 *
% 0.20/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-02T11:53:45
% 0.20/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n025.cluster.edu at 2022-06-02T11:53:45
% 0.49/0.66 WARNING:
% 0.49/0.66 |member$d| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |inj_on$o| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |inj_on$h| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |inj_on$n| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |inj_on$m| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |less_eq$f| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.49/0.66 WARNING:
% 0.49/0.66 |inj_on$f| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 54.74/54.95
% 54.74/54.95
% 54.74/54.95 #||
% 54.74/54.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 54.74/54.95 % SZS output start Refutation
% See solution above
% 54.74/54.95 ||#
% 54.74/54.95
% 54.74/54.95 ; Summary of computation:
% 54.74/54.95 ; 158855 formulas have been input or derived (from 1125 formulas).
% 54.74/54.95 ; 29325 (18%) were retained. Of these,
% 54.74/54.95 ; 1063 ( 4%) were simplified or subsumed later,
% 54.74/54.95 ; 28262 (96%) are still being kept.
% 54.74/54.95 ;
% 54.74/54.95 ; Run time in seconds excluding printing time:
% 54.74/54.95 ; 0.154 0% Read assertion file (1 call)
% 54.74/54.95 ; 0.021 0% Assert (662 calls)
% 54.74/54.95 ; 3.425 6% Process new row (151,478 calls)
% 54.74/54.95 ; 7.326 13% Resolution (2,248 calls)
% 54.74/54.95 ; 0.050 0% Paramodulation (1,124 calls)
% 54.74/54.95 ; 0.001 0% Factoring (77 calls)
% 54.74/54.95 ; 1.064 2% Condensing (52,482 calls)
% 54.74/54.95 ; 18.459 34% Forward subsumption (52,482 calls)
% 54.74/54.95 ; 3.547 7% Backward subsumption (25,505 calls)
% 54.74/54.95 ; 7.857 14% Clause clause subsumption (997,749 calls)
% 54.74/54.95 ; 9.593 18% Forward simplification (142,812 calls)
% 54.74/54.95 ; 0.138 0% Backward simplification (29,094 calls)
% 54.74/54.95 ; 0.292 1% Ordering (121,349 calls)
% 54.74/54.95 ; 0.010 0% Ordering ac (1,018 calls)
% 54.74/54.95 ; 1.997 4% Sortal reasoning (2,930,100 calls)
% 54.74/54.95 ; 0.003 0% Purity testing (1 call)
% 54.74/54.95 ; 0.540 1% Other
% 54.74/54.95 ; 54.477 Total
% 54.74/54.95 ; 54.485 Real time
% 54.74/54.95 ;
% 54.81/54.97 ; Term-hash-array has 30,382 terms in all.
% 54.81/54.97 ; Feature-vector-row-index has 24,896 entries (24,896 at peak, 25,505 added, 609 deleted).
% 54.81/54.97 ; Feature-vector-row-index has 231,524 nodes (231,524 at peak, 238,153 added, 6,629 deleted).
% 54.81/54.97 ; Retrieved 1,534,543 possibly forward subsuming rows in 52,482 calls.
% 54.81/54.97 ; Retrieved 140,046 possibly backward subsumed rows in 25,505 calls.
% 54.81/54.97 ; Path-index has 29,678 entries (29,678 at peak, 31,028 added, 1,350 deleted).
% 54.81/54.97 ; Path-index has 38,902 nodes (38,902 at peak, 39,418 added, 516 deleted).
% 54.81/54.97 ; Trie-index has 29,678 entries (29,678 at peak, 31,028 added, 1,350 deleted).
% 54.81/54.97 ; Trie-index has 138,224 nodes (138,224 at peak, 143,526 added, 5,302 deleted).
% 54.81/54.97 ; Retrieved 4,662,120 generalization terms in 1,333,311 calls.
% 54.81/54.97 ; Retrieved 7,130 instance terms in 3,678 calls.
% 54.81/54.97 ; Retrieved 8,825,436 unifiable terms in 90,696 calls.
% 54.81/54.97 ;
% 54.81/54.97 ; The agenda of rows to process has 2 entries:
% 54.81/54.97 ; 2 with value 10
% 54.81/54.97 ; The agenda of rows to give has 27161 entries:
% 54.81/54.97 ; 259 with value (4 12) 765 with value (4 43) 54 with value (4 74)
% 54.81/54.97 ; 166 with value (4 13) 376 with value (4 44) 31 with value (4 75)
% 54.81/54.97 ; 218 with value (4 14) 390 with value (4 45) 24 with value (4 76)
% 54.81/54.97 ; 312 with value (4 15) 293 with value (4 46) 6 with value (4 77)
% 54.81/54.97 ; 394 with value (4 16) 295 with value (4 47) 22 with value (4 78)
% 54.81/54.97 ; 384 with value (4 17) 428 with value (4 48) 35 with value (4 79)
% 54.81/54.97 ; 490 with value (4 18) 360 with value (4 49) 60 with value (4 80)
% 54.81/54.97 ; 541 with value (4 19) 211 with value (4 50) 30 with value (4 81)
% 54.81/54.97 ; 446 with value (4 20) 147 with value (4 51) 124 with value (4 82)
% 54.81/54.97 ; 535 with value (4 21) 81 with value (4 52) 118 with value (4 83)
% 54.81/54.97 ; 638 with value (4 22) 96 with value (4 53) 29 with value (4 84)
% 54.81/54.97 ; 826 with value (4 23) 91 with value (4 54) 2 with value (4 85)
% 54.81/54.97 ; 918 with value (4 24) 53 with value (4 55) 27 with value (4 86)
% 54.81/54.97 ; 815 with value (4 25) 60 with value (4 56) 17 with value (4 87)
% 54.81/54.97 ; 821 with value (4 26) 65 with value (4 57) 12 with value (4 88)
% 54.81/54.97 ; 794 with value (4 27) 28 with value (4 58) 58 with value (4 89)
% 54.81/54.97 ; 839 with value (4 28) 57 with value (4 59) 2 with value (4 90)
% 54.81/54.97 ; 947 with value (4 29) 42 with value (4 60) 21 with value (4 91)
% 54.81/54.97 ; 846 with value (4 30) 39 with value (4 61) 28 with value (4 92)
% 54.81/54.97 ; 789 with value (4 31) 21 with value (4 62) 20 with value (4 93)
% 54.81/54.97 ; 692 with value (4 32) 28 with value (4 63) 16 with value (4 94)
% 54.81/54.97 ; 719 with value (4 33) 47 with value (4 64) 8 with value (4 95)
% 54.81/54.97 ; 951 with value (4 34) 32 with value (4 65) 8 with value (4 96)
% 54.81/54.97 ; 1030 with value (4 35) 39 with value (4 66) 5 with value (4 97)
% 54.81/54.97 ; 1035 with value (4 36) 22 with value (4 67) 18 with value (4 98)
% 54.81/54.97 ; 759 with value (4 37) 53 with value (4 68) 40 with value (4 99)
% 54.81/54.97 ; 710 with value (4 38) 78 with value (4 69) 42 with value (4 100)
% 54.81/54.97 ; 814 with value (4 39) 62 with value (4 70) 8 with value (4 101)
% 54.81/54.97 ; 1023 with value (4 40) 44 with value (4 71) 4 with value (4 103)
% 54.81/54.97 ; 1053 with value (4 41) 68 with value (4 72) 4 with value (4 105)
% 54.81/54.97 ; 1068 with value (4 42) 69 with value (4 73) 16 with value (4 106)
% 54.81/54.97 Evaluation took:
% 54.81/54.97 54.507 seconds of real time
% 54.81/54.97 48.86865 seconds of user run time
% 54.81/54.97 5.631271 seconds of system run time
% 54.81/54.97 [Run times include 7.367 seconds GC run time.]
% 54.81/54.97 0 calls to %EVAL
% 54.81/54.97 0 page faults and
% 54.81/54.97 4,657,298,368 bytes consed.
% 54.81/54.97 :PROOF-FOUND
% 54.81/54.97 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-02T11:54:39
% 54.81/54.97 :PROOF-FOUND
% 54.81/54.97 *
%------------------------------------------------------------------------------