%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP303_1 : TPTP v8.1.0. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n022.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:03 EDT 2022
% Result : Theorem 1.46s 1.66s
% Output : Refutation 1.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 6
% Syntax : Number of formulae : 9 ( 8 unt; 0 typ; 0 def)
% Number of atoms : 55 ( 7 equ)
% Maximal formula atoms : 2 ( 6 avg)
% Number of connectives : 4 ( 3 ~; 1 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 45 ( 45 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 11 prp; 0-3 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 10 ( 0 sgn 10 !; 0 ?; 10 :)
% Comments :
%------------------------------------------------------------------------------
tff(50,negated_conjecture,
'nTCatDom$'('yFtorNT$'('c$','f$')) != 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture27) ).
tff(55,axiom,
'functor_abbrev$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom32) ).
tff(61,axiom,
! [X: 'A_b_b_c_LSCategory_ext_Category_ext$',Y: 'B$'] : ( 'nTCatDom$'('fun_app$t'('yFtorNT$a'(X),Y)) = 'fun_app$s'('oppositeCategory$',X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom38) ).
tff(63,axiom,
! [X: 'A_b_b_c_LSCategory_ext_Category_ext$',Y: 'B$'] : ( 'fun_app$t'('yFtorNT$a'(X),Y) = 'makeNT$'('yFtorNT$'(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom40) ).
tff(87,axiom,
! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : ( 'nTCatDom$'(X) = 'nTCatDom$'('makeNT$'(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom58) ).
tff(111,axiom,
! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',Y: 'A_b_b_c_LSCategory_ext_Category_ext$',Z: 'ZF_ZF_unit_Category_ext$'] :
( ~ 'functor_abbrev$'(X,Y,Z)
| ( 'catDom$'(X) = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom72) ).
tff(2671,plain,
! [X: 'A_b_b_c_LSCategory_ext_Category_ext$',Y: 'B$'] : ( 'nTCatDom$'('yFtorNT$'(X,Y)) = 'fun_app$s'('oppositeCategory$',X) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[87,63,theory(equality)]),61,theory(equality)]) ).
tff(2672,plain,
'fun_app$s'('oppositeCategory$','c$') != 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$'))),
inference('REWRITE',[status(thm)],[50,2671,theory(equality)]) ).
cnf(2683,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[111,55]),2672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP303_1 : TPTP v8.1.0. Released v8.0.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.12/0.34 % Computer : n022.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jun 2 11:27:36 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.20/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 *
% 0.20/0.46 *
% 0.20/0.47 #<PACKAGE "SNARK-USER">
% 0.20/0.47 *
% 0.20/0.47 SNARK-TPTP-OPTIONS
% 0.20/0.47 *
% 0.20/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.47 (USE-FACTORING :POS)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.47 *
% 0.20/0.47 "."
% 0.20/0.47 *
% 0.20/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-02T11:27:37
% 0.20/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n022.cluster.edu at 2022-06-02T11:27:37
% 0.48/0.73 WARNING:
% 0.48/0.73 |member$l| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nt_abbrev$c| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nTCompDefined$d| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nTCompDefined$c| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |natTrans$f| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |natTrans$d| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |natTrans$c| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nt_abbrev$b| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |natTrans$e| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nTCompDefined$e| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |nTCompDefined$b| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |equivalence$| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |category$b| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |compDefined$c| is a 3-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |category_axioms$b| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |natTrans$b| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |preFunctor$a| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.73 WARNING:
% 0.48/0.73 |member$k| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 1.46/1.66
% 1.46/1.66
% 1.46/1.66 #||
% 1.46/1.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.46/1.66 % SZS output start Refutation
% See solution above
% 1.46/1.67 ||#
% 1.46/1.67
% 1.46/1.67 ; Summary of computation:
% 1.46/1.67 ; 2948 formulas have been input or derived (from 229 formulas).
% 1.46/1.67 ; 2683 (91%) were retained. Of these,
% 1.46/1.67 ; 636 (24%) were simplified or subsumed later,
% 1.46/1.67 ; 2047 (76%) are still being kept.
% 1.46/1.67 ;
% 1.46/1.67 ; Run time in seconds excluding printing time:
% 1.46/1.67 ; 0.190 16% Read assertion file (1 call)
% 1.46/1.67 ; 0.047 4% Assert (589 calls)
% 1.46/1.67 ; 0.247 21% Process new row (2,309 calls)
% 1.46/1.67 ; 0.014 1% Resolution (456 calls)
% 1.46/1.67 ; 0.001 0% Paramodulation (228 calls)
% 1.46/1.67 ; 0.042 4% Condensing (2,033 calls)
% 1.46/1.67 ; 0.310 26% Forward subsumption (2,033 calls)
% 1.46/1.67 ; 0.087 7% Backward subsumption (1,899 calls)
% 1.46/1.67 ; 0.007 1% Clause clause subsumption (1,091 calls)
% 1.46/1.67 ; 0.110 9% Forward simplification (2,276 calls)
% 1.46/1.67 ; 0.006 1% Backward simplification (2,064 calls)
% 1.46/1.67 ; 0.094 8% Ordering (6,175 calls)
% 1.46/1.67 ; 0.000 0% Sortal reasoning (444 calls)
% 1.46/1.67 ; 0.010 1% Purity testing (1 call)
% 1.46/1.67 ; 0.029 2% Other
% 1.46/1.67 ; 1.194 Total
% 1.46/1.67 ; 1.196 Real time
% 1.46/1.67 ;
% 1.46/1.67 ; Term-hash-array has 2,813 terms in all.
% 1.46/1.67 ; Feature-vector-row-index has 1,886 entries (1,887 at peak, 1,899 added, 13 deleted).
% 1.46/1.67 ; Feature-vector-row-index has 42,113 nodes (42,121 at peak, 42,214 added, 101 deleted).
% 1.46/1.67 ; Retrieved 3,806 possibly forward subsuming rows in 2,033 calls.
% 1.46/1.67 ; Retrieved 53 possibly backward subsumed rows in 1,899 calls.
% 1.46/1.67 ; Path-index has 2,810 entries (2,810 at peak, 2,851 added, 41 deleted).
% 1.46/1.67 ; Path-index has 10,051 nodes (10,051 at peak, 10,129 added, 78 deleted).
% 1.46/1.67 ; Trie-index has 2,810 entries (2,810 at peak, 2,851 added, 41 deleted).
% 1.46/1.67 ; Trie-index has 11,238 nodes (11,238 at peak, 11,417 added, 179 deleted).
% 1.46/1.67 ; Retrieved 3,938 generalization terms in 20,296 calls.
% 1.46/1.67 ; Retrieved 193 instance terms in 178 calls.
% 1.46/1.67 ; Retrieved 12,301 unifiable terms in 931 calls.
% 1.46/1.67 ;
% 1.46/1.67 ; The agenda of rows to process has 2 entries:
% 1.46/1.67 ; 2 with value 15
% 1.46/1.67 ; The agenda of input rows to give has 1777 entries:
% 1.46/1.67 ; 10 with value 13 7 with value 49 16 with value 91
% 1.46/1.67 ; 29 with value 14 4 with value 50 48 with value 92
% 1.46/1.67 ; 14 with value 15 3 with value 51 12 with value 93
% 1.46/1.67 ; 17 with value 16 20 with value 53 40 with value 94
% 1.46/1.67 ; 31 with value 17 2 with value 54 34 with value 96
% 1.46/1.67 ; 12 with value 18 3 with value 55 8 with value 97
% 1.46/1.67 ; 28 with value 19 1 with value 56 40 with value 98
% 1.46/1.67 ; 17 with value 20 3 with value 57 16 with value 99
% 1.46/1.67 ; 28 with value 21 5 with value 59 32 with value 100
% 1.46/1.67 ; 21 with value 22 22 with value 60 4 with value 101
% 1.46/1.67 ; 19 with value 23 4 with value 61 28 with value 102
% 1.46/1.67 ; 7 with value 24 2 with value 62 32 with value 103
% 1.46/1.67 ; 14 with value 25 1 with value 63 32 with value 104
% 1.46/1.67 ; 21 with value 26 38 with value 64 16 with value 106
% 1.46/1.67 ; 15 with value 27 2 with value 66 26 with value 107
% 1.46/1.67 ; 20 with value 28 2 with value 67 24 with value 108
% 1.46/1.67 ; 8 with value 29 24 with value 68 16 with value 109
% 1.46/1.67 ; 28 with value 30 20 with value 69 4 with value 110
% 1.46/1.67 ; 12 with value 31 2 with value 70 16 with value 111
% 1.46/1.67 ; 19 with value 32 18 with value 72 16 with value 112
% 1.46/1.67 ; 12 with value 33 32 with value 73 32 with value 113
% 1.46/1.67 ; 11 with value 34 2 with value 74 16 with value 115
% 1.46/1.67 ; 18 with value 35 32 with value 75 8 with value 116
% 1.46/1.67 ; 16 with value 36 12 with value 76 24 with value 117
% 1.46/1.67 ; 6 with value 37 24 with value 77 16 with value 119
% 1.46/1.67 ; 23 with value 38 68 with value 79 16 with value 121
% 1.46/1.67 ; 6 with value 39 4 with value 80 12 with value 123
% 1.46/1.67 ; 6 with value 40 16 with value 81 8 with value 124
% 1.46/1.67 ; 7 with value 41 50 with value 83 8 with value 125
% 1.46/1.67 ; 9 with value 42 32 with value 84 8 with value 127
% 1.46/1.67 ; 4 with value 43 16 with value 85 16 with value 128
% 1.46/1.67 ; 2 with value 44 34 with value 87 4 with value 131
% 1.46/1.67 ; 2 with value 45 66 with value 88 12 with value 132
% 1.46/1.67 ; 10 with value 46 16 with value 89 8 with value 136
% 1.46/1.67 ; 3 with value 47 18 with value 90 4 with value 140
% 1.46/1.67 ; 15 with value 48
% 1.46/1.67 ; The agenda of rows to give has 42 entries:
% 1.46/1.67 ; 4 with value (4 4) 2 with value (4 9) 6 with value (4 12)
% 1.46/1.67 ; 3 with value (4 6) 3 with value (4 10) 6 with value (4 13)
% 1.46/1.67 ; 3 with value (4 7) 10 with value (4 11) 3 with value (4 15)
% 1.46/1.67 ; 2 with value (4 8)
% 1.46/1.67 Evaluation took:
% 1.46/1.67 1.2 seconds of real time
% 1.46/1.67 1.135871 seconds of user run time
% 1.46/1.67 0.063995 seconds of system run time
% 1.46/1.67 [Run times include 0.114 seconds GC run time.]
% 1.46/1.67 0 calls to %EVAL
% 1.46/1.67 0 page faults and
% 1.46/1.67 112,129,680 bytes consed.
% 1.46/1.67 :PROOF-FOUND
% 1.46/1.67 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-02T11:27:38
% 1.46/1.67 :PROOF-FOUND
% 1.46/1.67 *
%------------------------------------------------------------------------------