%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP386_1 : TPTP v8.1.0. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n026.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:12 EDT 2022
% Result : Theorem 30.29s 30.46s
% Output : Refutation 30.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of formulae : 20 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 134 ( 13 equ)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 19 ( 11 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 106 ( 106 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 28 usr; 11 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 18 ( 0 sgn 18 !; 0 ?; 18 :)
% Comments :
%------------------------------------------------------------------------------
cnf(97,negated_conjecture,
~ 'thesis$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture72) ).
tff(98,hypothesis,
! [X: 'B_c_c_fun_fun$',Y: 'C_b_fun$'] :
( ( 'fun_app$j'('fun_app$am'('g$','SKOLEMAAAV1.B_b_option_fun$'(X,Y)),'SKOLEMAAAV2.C$'(X,Y)) != 'fun_app$an'('case_option$c'('none$','uu$'(X,'SKOLEMAAAV2.C$'(X,Y))),'fun_app$g'('SKOLEMAAAV1.B_b_option_fun$'(X,Y),'fun_app$m'(Y,'SKOLEMAAAV2.C$'(X,Y)))) )
| ~ 'valid_getter_setter$'(Y,X)
| 'thesis$' ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis73) ).
tff(99,plain,
! [X: 'B_c_c_fun_fun$',Y: 'C_b_fun$'] :
( ( 'fun_app$j'('fun_app$am'('g$','SKOLEMAAAV1.B_b_option_fun$'(X,Y)),'SKOLEMAAAV2.C$'(X,Y)) != 'fun_app$an'('case_option$c'('none$','uu$'(X,'SKOLEMAAAV2.C$'(X,Y))),'fun_app$g'('SKOLEMAAAV1.B_b_option_fun$'(X,Y),'fun_app$m'(Y,'SKOLEMAAAV2.C$'(X,Y)))) )
| ~ 'valid_getter_setter$'(Y,X) ),
inference('REWRITE',[status(thm)],[98,97]) ).
tff(101,axiom,
'register$a'('g$'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom75) ).
tff(125,axiom,
! [X: 'C_b_fun$',Y: 'B_c_c_fun_fun$',Z: 'B_b_option_fun$',U: 'C$'] : ( 'fun_app$j'('fun_app$am'('register_from_getter_setter$a'(X,Y),Z),U) = 'fun_app$an'('case_option$c'('none$','uu$'(Y,U)),'fun_app$g'(Z,'fun_app$m'(X,U))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom94) ).
tff(199,axiom,
! [X: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ~ 'register$a'(X)
| ( X = 'register_from_getter_setter$a'('SKOLEMAAAV41.C_b_fun$'(X),'SKOLEMAAAV42.B_c_c_fun_fun$'(X)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom136) ).
tff(200,axiom,
! [X: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ~ 'register$a'(X)
| 'valid_getter_setter$'('SKOLEMAAAV41.C_b_fun$'(X),'SKOLEMAAAV42.B_c_c_fun_fun$'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom136) ).
tff(247,axiom,
! [X: 'C_b_fun$',Y: 'B_c_c_fun_fun$'] :
( ~ 'valid_getter_setter$'(X,Y)
| ( 'getter$'('register_from_getter_setter$a'(X,Y)) = X ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom163) ).
tff(250,axiom,
! [X: 'C_b_fun$',Y: 'B_c_c_fun_fun$'] :
( ~ 'valid_getter_setter$'(X,Y)
| ( 'setter$'('register_from_getter_setter$a'(X,Y)) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom166) ).
tff(699,axiom,
! [X: 'C$',Y: 'C_c_option_fun$'] : ( 'fun_app$ab'('bind$'('fun_app$j'('some$a',X)),Y) = 'fun_app$j'(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom422) ).
tff(1326,plain,
! [X: 'B_c_c_fun_fun$',Y: 'C_b_fun$'] :
( ( 'fun_app$ab'('bind$'('fun_app$j'('some$a','SKOLEMAAAV2.C$'(X,Y))),'fun_app$am'('g$','SKOLEMAAAV1.B_b_option_fun$'(X,Y))) != 'fun_app$ab'('bind$'('fun_app$j'('some$a','SKOLEMAAAV2.C$'(X,Y))),'fun_app$am'('register_from_getter_setter$a'(Y,X),'SKOLEMAAAV1.B_b_option_fun$'(X,Y))) )
| ~ 'valid_getter_setter$'(Y,X) ),
inference('REWRITE',[status(thm)],[99,699,125,theory(equality)]) ).
tff(1366,plain,
'valid_getter_setter$'('SKOLEMAAAV41.C_b_fun$'('g$'),'SKOLEMAAAV42.B_c_c_fun_fun$'('g$')),
inference('HYPERRESOLVE',[status(thm)],[200,101]) ).
tff(1684,plain,
'g$' = 'register_from_getter_setter$a'('SKOLEMAAAV41.C_b_fun$'('g$'),'SKOLEMAAAV42.B_c_c_fun_fun$'('g$')),
inference('HYPERRESOLVE',[status(thm)],[199,101]) ).
tff(13360,plain,
'setter$'('g$') = 'SKOLEMAAAV42.B_c_c_fun_fun$'('g$'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[250,1366]),1684,theory(equality)]) ).
tff(13361,plain,
'valid_getter_setter$'('SKOLEMAAAV41.C_b_fun$'('g$'),'setter$'('g$')),
inference('REWRITE',[status(thm)],[1366,13360,theory(equality)]) ).
tff(13362,plain,
'g$' = 'register_from_getter_setter$a'('SKOLEMAAAV41.C_b_fun$'('g$'),'setter$'('g$')),
inference('REWRITE',[status(thm)],[1684,13360,theory(equality)]) ).
tff(14121,plain,
'getter$'('g$') = 'SKOLEMAAAV41.C_b_fun$'('g$'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[247,13361]),13362,theory(equality)]) ).
tff(14122,plain,
'valid_getter_setter$'('getter$'('g$'),'setter$'('g$')),
inference('REWRITE',[status(thm)],[13361,14121,theory(equality)]) ).
tff(14123,plain,
'g$' = 'register_from_getter_setter$a'('getter$'('g$'),'setter$'('g$')),
inference('REWRITE',[status(thm)],[13362,14121,theory(equality)]) ).
cnf(14130,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[1326,14122]),14123,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ITP386_1 : TPTP v8.1.0. Released v8.0.0.
% 0.06/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jun 2 17:31:27 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.21/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.47 *
% 0.21/0.47 *
% 0.21/0.47 #<PACKAGE "SNARK-USER">
% 0.21/0.47 *
% 0.21/0.47 SNARK-TPTP-OPTIONS
% 0.21/0.47 *
% 0.21/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.47 (USE-FACTORING :POS)
% 0.21/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.47 *
% 0.21/0.47 "."
% 0.21/0.47 *
% 0.21/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-02T17:31:27
% 0.21/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n026.cluster.edu at 2022-06-02T17:31:27
% 0.48/0.70 WARNING:
% 0.48/0.70 |register$c| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |register$e| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |register$b| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |register$d| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |preregister$e| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |inj_on$| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |preregister$d| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 DECLARE-PROPOSITION is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |preregister$f| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.70 WARNING:
% 0.48/0.70 |inj_on$a| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 30.29/30.46
% 30.29/30.46
% 30.29/30.46 #||
% 30.29/30.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.29/30.46 % SZS output start Refutation
% See solution above
% 30.29/30.46 ||#
% 30.29/30.46
% 30.29/30.46 ; Summary of computation:
% 30.29/30.46 ; 60428 formulas have been input or derived (from 1340 formulas).
% 30.29/30.46 ; 14130 (23%) were retained. Of these,
% 30.29/30.46 ; 3680 (26%) were simplified or subsumed later,
% 30.29/30.46 ; 10450 (74%) are still being kept.
% 30.29/30.46 ;
% 30.29/30.46 ; Run time in seconds excluding printing time:
% 30.29/30.46 ; 0.181 1% Read assertion file (1 call)
% 30.29/30.46 ; 0.027 0% Assert (736 calls)
% 30.29/30.46 ; 2.791 9% Process new row (52,083 calls)
% 30.29/30.46 ; 12.090 40% Resolution (2,678 calls)
% 30.29/30.46 ; 0.284 1% Paramodulation (1,339 calls)
% 30.29/30.46 ; 0.000 0% Factoring (138 calls)
% 30.29/30.46 ; 0.351 1% Condensing (20,475 calls)
% 30.29/30.46 ; 5.941 20% Forward subsumption (20,475 calls)
% 30.29/30.46 ; 1.708 6% Backward subsumption (10,594 calls)
% 30.29/30.46 ; 0.245 1% Clause clause subsumption (21,515 calls)
% 30.29/30.46 ; 3.205 11% Forward simplification (47,132 calls)
% 30.29/30.46 ; 0.574 2% Backward simplification (14,039 calls)
% 30.29/30.46 ; 1.820 6% Ordering (259,289 calls)
% 30.29/30.46 ; 0.527 2% Sortal reasoning (643,930 calls)
% 30.29/30.46 ; 0.002 0% Purity testing (1 call)
% 30.29/30.46 ; 0.237 1% Other
% 30.29/30.46 ; 29.983 Total
% 30.29/30.46 ; 29.985 Real time
% 30.29/30.46 ;
% 30.29/30.47 ; Term-hash-array has 41,770 terms in all.
% 30.29/30.47 ; Feature-vector-row-index has 8,059 entries (8,059 at peak, 10,594 added, 2,535 deleted).
% 30.29/30.47 ; Feature-vector-row-index has 103,968 nodes (103,968 at peak, 142,583 added, 38,615 deleted).
% 30.29/30.47 ; Retrieved 38,806 possibly forward subsuming rows in 20,475 calls.
% 30.29/30.47 ; Retrieved 2,593 possibly backward subsumed rows in 10,594 calls.
% 30.29/30.47 ; Path-index has 34,933 entries (34,933 at peak, 47,596 added, 12,663 deleted).
% 30.29/30.47 ; Path-index has 167,641 nodes (167,641 at peak, 188,667 added, 21,026 deleted).
% 30.29/30.47 ; Trie-index has 34,933 entries (34,933 at peak, 47,596 added, 12,663 deleted).
% 30.29/30.47 ; Trie-index has 210,535 nodes (210,535 at peak, 286,638 added, 76,103 deleted).
% 30.29/30.47 ; Retrieved 244,653 generalization terms in 400,303 calls.
% 30.29/30.47 ; Retrieved 11,651 instance terms in 5,816 calls.
% 30.29/30.47 ; Retrieved 17,996,138 unifiable terms in 42,489 calls.
% 30.29/30.47 ;
% 30.29/30.47 ; The agenda of rows to give has 9349 entries:
% 30.29/30.47 ; 1 with value (4 8) 108 with value (4 51) 10 with value (4 93)
% 30.29/30.47 ; 44 with value (4 9) 111 with value (4 52) 29 with value (4 94)
% 30.29/30.47 ; 90 with value (4 10) 111 with value (4 53) 4 with value (4 95)
% 30.29/30.47 ; 114 with value (4 11) 75 with value (4 54) 10 with value (4 96)
% 30.29/30.47 ; 161 with value (4 12) 97 with value (4 55) 7 with value (4 97)
% 30.29/30.47 ; 89 with value (4 13) 89 with value (4 56) 12 with value (4 98)
% 30.29/30.47 ; 79 with value (4 14) 77 with value (4 57) 11 with value (4 99)
% 30.29/30.47 ; 69 with value (4 15) 76 with value (4 58) 2 with value (4 100)
% 30.29/30.47 ; 130 with value (4 16) 89 with value (4 59) 13 with value (4 101)
% 30.29/30.47 ; 131 with value (4 17) 88 with value (4 60) 3 with value (4 102)
% 30.29/30.47 ; 142 with value (4 18) 62 with value (4 61) 10 with value (4 103)
% 30.29/30.47 ; 166 with value (4 19) 53 with value (4 62) 2 with value (4 104)
% 30.29/30.47 ; 187 with value (4 20) 74 with value (4 63) 10 with value (4 106)
% 30.29/30.47 ; 130 with value (4 21) 52 with value (4 64) 5 with value (4 107)
% 30.29/30.47 ; 189 with value (4 22) 55 with value (4 65) 7 with value (4 108)
% 30.29/30.47 ; 217 with value (4 23) 72 with value (4 66) 4 with value (4 109)
% 30.29/30.47 ; 270 with value (4 24) 50 with value (4 67) 4 with value (4 110)
% 30.29/30.47 ; 301 with value (4 25) 48 with value (4 68) 10 with value (4 111)
% 30.29/30.47 ; 273 with value (4 26) 39 with value (4 69) 3 with value (4 112)
% 30.29/30.47 ; 228 with value (4 27) 37 with value (4 70) 3 with value (4 114)
% 30.29/30.47 ; 227 with value (4 28) 44 with value (4 71) 2 with value (4 115)
% 30.29/30.47 ; 236 with value (4 29) 31 with value (4 72) 2 with value (4 116)
% 30.29/30.47 ; 240 with value (4 30) 50 with value (4 73) 4 with value (4 117)
% 30.29/30.47 ; 217 with value (4 31) 40 with value (4 74) 12 with value (4 118)
% 30.29/30.47 ; 217 with value (4 32) 25 with value (4 75) 4 with value (4 119)
% 30.29/30.47 ; 190 with value (4 33) 35 with value (4 76) 2 with value (4 120)
% 30.29/30.47 ; 199 with value (4 34) 44 with value (4 77) 2 with value (4 121)
% 30.29/30.47 ; 197 with value (4 35) 25 with value (4 78) 2 with value (4 124)
% 30.29/30.47 ; 158 with value (4 36) 22 with value (4 79) 6 with value (4 126)
% 30.29/30.47 ; 172 with value (4 37) 31 with value (4 80) 10 with value (4 129)
% 30.29/30.47 ; 163 with value (4 38) 19 with value (4 81) 4 with value (4 130)
% 30.29/30.47 ; 139 with value (4 39) 22 with value (4 82) 2 with value (4 132)
% 30.29/30.47 ; 152 with value (4 40) 21 with value (4 83) 6 with value (4 135)
% 30.29/30.47 ; 207 with value (4 41) 50 with value (4 84) 2 with value (4 137)
% 30.29/30.47 ; 152 with value (4 42) 14 with value (4 85) 2 with value (4 146)
% 30.29/30.47 ; 174 with value (4 43) 16 with value (4 86) 4 with value (4 149)
% 30.29/30.47 ; 156 with value (4 44) 33 with value (4 87) 2 with value (4 154)
% 30.29/30.47 ; 163 with value (4 45) 22 with value (4 88) 8 with value (4 170)
% 30.29/30.47 ; 146 with value (4 46) 14 with value (4 89) 4 with value (4 177)
% 30.29/30.47 ; 122 with value (4 47) 7 with value (4 90) 2 with value (4 184)
% 30.29/30.47 ; 127 with value (4 48) 22 with value (4 91) 4 with value (4 192)
% 30.29/30.47 ; 137 with value (4 49) 13 with value (4 92) 2 with value (4 196)
% 30.29/30.47 ; 137 with value (4 50)
% 30.29/30.47 Evaluation took:
% 30.29/30.47 29.999 seconds of real time
% 30.29/30.47 27.93142 seconds of user run time
% 30.29/30.47 2.068037 seconds of system run time
% 30.29/30.47 [Run times include 6.114 seconds GC run time.]
% 30.29/30.47 0 calls to %EVAL
% 30.29/30.47 0 page faults and
% 30.29/30.47 1,627,980,400 bytes consed.
% 30.29/30.47 :PROOF-FOUND
% 30.29/30.47 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-02T17:31:57
% 30.29/30.47 :PROOF-FOUND
% 30.29/30.47 *
%------------------------------------------------------------------------------