%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SCT171+3 : TPTP v8.1.0. Released v5.3.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 : Mon Jul 18 22:11:13 EDT 2022
% Result : Theorem 1.29s 1.51s
% Output : Refutation 1.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 4
% Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 6 RR)
% Number of literals : 8 ( 1 equ; 3 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 45 ( 45 usr; 19 con; 0-2 aty)
% Number of variables : 3 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(191,axiom,
hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto) ).
cnf(192,axiom,
( hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p)))
| ~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(ord_less_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1644373103_mktop),p)),e))),hAPP_f1740414619t_bool(cOMBS_1064524443t_bool(hAPP_f1842612975t_bool(cOMBS_131695599t_bool(hAPP_f586238575t_bool(cOMBB_2107911302e_indi(if_fun2098446489t_bool),hAPP_n821919323i_bool(hAPP_f446868133i_bool(cOMBC_1996607964t_bool,hAPP_f224734595t_bool(cOMBB_1883918730e_indi(fequal_nat),h)),n))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_A1906441908t_bool(hAPP_f248867553t_bool(cOMBC_898791271t_bool,hAPP_f210227915t_bool(cOMBB_1769989562e_indi(arrow_230821333_above),p)),c)),e))),hAPP_A1805174428t_bool(hAPP_f1808153265t_bool(cOMBC_1353880399t_bool,hAPP_f721938099t_bool(cOMBB_2032668066e_indi(arrow_1495666017_mkbot),p)),e)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_PW) ).
cnf(193,plain,
hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))),
inference('REWRITE',[status(thm)],[192,191]) ).
cnf(1751,axiom,
hAPP_P606313927t_bool(hAPP_f515126293t_bool(hAPP_f49469479t_bool(cOMBC_864945570l_bool,X),Y),Z) = hAPP_f592646513l_bool(hAPP_P229966473l_bool(X,Z),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_COMBC_000tc__prod_Itc__Arrow____Order____Mirabelle____tpnfnnbpuu_) ).
cnf(1777,negated_conjecture,
~ hBOOL(hAPP_f592646513l_bool(hAPP_P229966473l_bool(member1441201108le_alt,hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d)),hAPP_f412050202t_bool(f,p))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
cnf(1778,plain,
~ hBOOL(hAPP_P606313927t_bool(hAPP_f515126293t_bool(hAPP_f49469479t_bool(cOMBC_864945570l_bool,member1441201108le_alt),hAPP_f412050202t_bool(f,p)),hAPP_A702847159le_alt(hAPP_A1505516597le_alt(produc1400112471le_alt,c),d))),
inference('REWRITE',[status(thm)],[1777,1751,theory(equality)]) ).
cnf(1881,plain,
$false,
inference('REWRITE',[status(thm)],[193,1778,1751,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SCT171+3 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jul 2 06:38:09 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.44 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 *
% 0.18/0.45 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-02T06:38:09
% 0.18/0.46 ; 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-07-02T06:38:09
% 0.59/0.80
% 0.68/0.85 ; Recognized left identity assertion (= (|hAPP_f800510211t_bool| |collect_nat| ?X) ?X).
% 0.68/0.85 ; Recognized left identity assertion (= (|hAPP_nat_nat| |size_size_nat| ?X) ?X).
% 1.29/1.51 ; Recognized left identity assertion (= (|hAPP_nat_nat| |cOMBI_nat| ?X) ?X).
% 1.29/1.51
% 1.29/1.51 #||
% 1.29/1.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.29/1.51 % SZS output start Refutation
% See solution above
% 1.29/1.51 ||#
% 1.29/1.51
% 1.29/1.51 ; Summary of computation:
% 1.29/1.51 ; 2750 formulas have been input or derived (from 1 formulas).
% 1.29/1.51 ; 1881 (68%) were retained. Of these,
% 1.29/1.51 ; 442 (23%) were simplified or subsumed later,
% 1.29/1.51 ; 1439 (77%) are still being kept.
% 1.29/1.51 ;
% 1.29/1.51 ; Run time in seconds excluding printing time:
% 1.29/1.51 ; 0.321 31% Read assertion file (1 call)
% 1.29/1.51 ; 0.053 5% Assert (1,415 calls)
% 1.29/1.51 ; 0.172 16% Process new row (2,436 calls)
% 1.29/1.51 ; 0.018 2% Condensing (2,053 calls)
% 1.29/1.51 ; 0.230 22% Forward subsumption (2,053 calls)
% 1.29/1.51 ; 0.077 7% Backward subsumption (1,486 calls)
% 1.29/1.51 ; 0.007 1% Clause clause subsumption (1,839 calls)
% 1.29/1.51 ; 0.045 4% Forward simplification (2,436 calls)
% 1.29/1.51 ; 0.031 3% Backward simplification (1,793 calls)
% 1.29/1.51 ; 0.052 5% Ordering (869 calls)
% 1.29/1.51 ; 0.000 0% Sortal reasoning (32 calls)
% 1.29/1.51 ; 0.003 0% Purity testing (1 call)
% 1.29/1.51 ; 0.036 3% Other
% 1.29/1.51 ; 1.045 Total
% 1.29/1.51 ; 1.046 Real time
% 1.29/1.51 ;
% 1.29/1.51 ; Term-hash-array has 7,014 terms in all.
% 1.29/1.51 ; Feature-vector-row-index has 1,165 entries (1,288 at peak, 1,486 added, 321 deleted).
% 1.29/1.51 ; Feature-vector-row-index has 16,807 nodes (19,001 at peak, 22,923 added, 6,116 deleted).
% 1.29/1.51 ; Retrieved 2,090 possibly forward subsuming rows in 2,053 calls.
% 1.29/1.51 ; Retrieved 358 possibly backward subsumed rows in 1,486 calls.
% 1.29/1.51 ; Path-index has 6,272 entries (6,643 at peak, 7,291 added, 1,019 deleted).
% 1.29/1.51 ; Path-index has 21,617 nodes (21,617 at peak, 23,037 added, 1,420 deleted).
% 1.29/1.51 ; Trie-index has 6,272 entries (6,643 at peak, 7,291 added, 1,019 deleted).
% 1.29/1.51 ; Trie-index has 17,229 nodes (18,016 at peak, 20,741 added, 3,512 deleted).
% 1.29/1.51 ; Retrieved 3,939 generalization terms in 9,857 calls.
% 1.29/1.51 ; Retrieved 922 instance terms in 349 calls.
% 1.29/1.51 ;
% 1.29/1.51 ; The agenda of backward simplifiable rows to process has 225 entries:
% 1.29/1.51 ; 225 with value 0
% 1.29/1.51 ; The agenda of input rows to give has 1438 entries:
% 1.29/1.51 ; 27 with value 3 47 with value 28 1 with value 60
% 1.29/1.51 ; 2 with value 4 11 with value 29 3 with value 61
% 1.29/1.51 ; 3 with value 5 8 with value 30 3 with value 62
% 1.29/1.51 ; 73 with value 6 6 with value 31 1 with value 64
% 1.29/1.51 ; 9 with value 7 34 with value 32 1 with value 65
% 1.29/1.51 ; 6 with value 8 3 with value 33 2 with value 68
% 1.29/1.51 ; 90 with value 9 29 with value 34 1 with value 69
% 1.29/1.51 ; 22 with value 10 27 with value 35 1 with value 70
% 1.29/1.51 ; 17 with value 11 81 with value 36 7 with value 72
% 1.29/1.51 ; 12 with value 12 3 with value 37 2 with value 73
% 1.29/1.51 ; 58 with value 13 83 with value 38 2 with value 74
% 1.29/1.51 ; 14 with value 14 4 with value 39 1 with value 76
% 1.29/1.51 ; 28 with value 15 2 with value 41 5 with value 77
% 1.29/1.51 ; 43 with value 16 3 with value 42 8 with value 84
% 1.29/1.51 ; 26 with value 17 80 with value 43 1 with value 85
% 1.29/1.51 ; 53 with value 18 81 with value 45 4 with value 89
% 1.29/1.51 ; 6 with value 19 3 with value 46 3 with value 92
% 1.29/1.51 ; 14 with value 20 87 with value 48 1 with value 96
% 1.29/1.51 ; 11 with value 21 2 with value 49 1 with value 101
% 1.29/1.51 ; 36 with value 22 85 with value 50 4 with value 110
% 1.29/1.51 ; 18 with value 23 1 with value 51 4 with value 112
% 1.29/1.51 ; 44 with value 24 1 with value 53 4 with value 123
% 1.29/1.51 ; 9 with value 25 7 with value 54 4 with value 124
% 1.29/1.51 ; 2 with value 26 2 with value 57 6 with value 132
% 1.29/1.51 ; 53 with value 27 2 with value 59
% 1.29/1.51 Evaluation took:
% 1.29/1.51 1.047 seconds of real time
% 1.29/1.51 0.997188 seconds of user run time
% 1.29/1.51 0.049534 seconds of system run time
% 1.29/1.51 [Run times include 0.107 seconds GC run time.]
% 1.29/1.51 0 calls to %EVAL
% 1.29/1.51 0 page faults and
% 1.29/1.51 104,889,112 bytes consed.
% 1.29/1.51 :PROOF-FOUND
% 1.29/1.51 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-02T06:38:10
% 1.29/1.51 :PROOF-FOUND
% 1.29/1.51 *
%------------------------------------------------------------------------------