%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n021.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 23:18:32 EDT 2022
% Result : Theorem 0.48s 0.66s
% Output : Refutation 0.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 34
% Syntax : Number of clauses : 64 ( 62 unt; 0 nHn; 64 RR)
% Number of literals : 68 ( 0 equ; 9 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 6 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(7,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just7) ).
cnf(9,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just9) ).
cnf(11,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just11) ).
cnf(13,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just13) ).
cnf(15,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just15) ).
cnf(17,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just17) ).
cnf(19,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just19) ).
cnf(21,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just21) ).
cnf(23,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just23) ).
cnf(25,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just25) ).
cnf(27,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just27) ).
cnf(29,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just29) ).
cnf(31,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just31) ).
cnf(33,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just33) ).
cnf(35,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just35) ).
cnf(37,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just37) ).
cnf(39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just39) ).
cnf(41,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just41) ).
cnf(43,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just43) ).
cnf(45,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just45) ).
cnf(47,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just47) ).
cnf(49,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just49) ).
cnf(51,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just51) ).
cnf(53,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just53) ).
cnf(55,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just55) ).
cnf(57,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just57) ).
cnf(59,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just59) ).
cnf(61,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just61) ).
cnf(63,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just63) ).
cnf(65,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just65) ).
cnf(67,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just67) ).
cnf(78,axiom,
( ~ disjointwith(X,Y)
| ~ genls(Z,Y)
| disjointwith(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just85) ).
cnf(145,axiom,
( ~ genls(X,Y)
| ~ genls(Y,Z)
| genls(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just155) ).
cnf(159,negated_conjecture,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query49) ).
cnf(201,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference('HYPERRESOLVE',[status(thm)],[78,67,7]) ).
cnf(202,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference('UR-RESOLVE',[status(thm)],[78,65,159]) ).
cnf(205,plain,
genls(c_tptpcol_15_92268,c_tptpcol_13_92263),
inference('HYPERRESOLVE',[status(thm)],[145,63,61]) ).
cnf(207,plain,
genls(c_tptpcol_13_92263,c_tptpcol_11_92230),
inference('HYPERRESOLVE',[status(thm)],[145,59,57]) ).
cnf(209,plain,
genls(c_tptpcol_11_92230,c_tptpcol_9_92165),
inference('HYPERRESOLVE',[status(thm)],[145,55,53]) ).
cnf(211,plain,
genls(c_tptpcol_9_92165,c_tptpcol_7_92163),
inference('HYPERRESOLVE',[status(thm)],[145,51,49]) ).
cnf(213,plain,
genls(c_tptpcol_7_92163,c_tptpcol_5_90114),
inference('HYPERRESOLVE',[status(thm)],[145,47,45]) ).
cnf(215,plain,
genls(c_tptpcol_5_90114,c_tptpcol_3_81921),
inference('HYPERRESOLVE',[status(thm)],[145,43,41]) ).
cnf(217,plain,
genls(c_tptpcol_3_81921,c_tptpcol_1_65536),
inference('HYPERRESOLVE',[status(thm)],[145,39,37]) ).
cnf(218,plain,
genls(c_tptpcol_16_26926,c_tptpcol_14_26921),
inference('HYPERRESOLVE',[status(thm)],[145,35,33]) ).
cnf(220,plain,
genls(c_tptpcol_14_26921,c_tptpcol_12_26919),
inference('HYPERRESOLVE',[status(thm)],[145,31,29]) ).
cnf(222,plain,
genls(c_tptpcol_12_26919,c_tptpcol_10_26886),
inference('HYPERRESOLVE',[status(thm)],[145,27,25]) ).
cnf(224,plain,
genls(c_tptpcol_10_26886,c_tptpcol_8_26629),
inference('HYPERRESOLVE',[status(thm)],[145,23,21]) ).
cnf(226,plain,
genls(c_tptpcol_8_26629,c_tptpcol_6_26627),
inference('HYPERRESOLVE',[status(thm)],[145,19,17]) ).
cnf(228,plain,
genls(c_tptpcol_6_26627,c_tptpcol_4_24578),
inference('HYPERRESOLVE',[status(thm)],[145,15,13]) ).
cnf(230,plain,
genls(c_tptpcol_4_24578,c_tptpcol_2_2),
inference('HYPERRESOLVE',[status(thm)],[145,11,9]) ).
cnf(286,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_13_92263),
inference('UR-RESOLVE',[status(thm)],[78,205,202]) ).
cnf(294,plain,
genls(c_tptpcol_13_92263,c_tptpcol_9_92165),
inference('HYPERRESOLVE',[status(thm)],[145,209,207]) ).
cnf(302,plain,
genls(c_tptpcol_9_92165,c_tptpcol_5_90114),
inference('HYPERRESOLVE',[status(thm)],[145,213,211]) ).
cnf(311,plain,
genls(c_tptpcol_5_90114,c_tptpcol_1_65536),
inference('HYPERRESOLVE',[status(thm)],[145,217,215]) ).
cnf(317,plain,
genls(c_tptpcol_16_26926,c_tptpcol_12_26919),
inference('HYPERRESOLVE',[status(thm)],[145,220,218]) ).
cnf(325,plain,
genls(c_tptpcol_12_26919,c_tptpcol_8_26629),
inference('HYPERRESOLVE',[status(thm)],[145,224,222]) ).
cnf(333,plain,
genls(c_tptpcol_8_26629,c_tptpcol_4_24578),
inference('HYPERRESOLVE',[status(thm)],[145,228,226]) ).
cnf(336,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_4_24578),
inference('HYPERRESOLVE',[status(thm)],[78,230,201]) ).
cnf(378,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_9_92165),
inference('UR-RESOLVE',[status(thm)],[78,294,286]) ).
cnf(413,plain,
genls(c_tptpcol_9_92165,c_tptpcol_1_65536),
inference('HYPERRESOLVE',[status(thm)],[145,311,302]) ).
cnf(441,plain,
genls(c_tptpcol_16_26926,c_tptpcol_8_26629),
inference('HYPERRESOLVE',[status(thm)],[145,325,317]) ).
cnf(465,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_8_26629),
inference('HYPERRESOLVE',[status(thm)],[78,336,333]) ).
cnf(592,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),
inference('UR-RESOLVE',[status(thm)],[78,413,378]) ).
cnf(710,plain,
$false,
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[78,465,441]),592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR049+1 : TPTP v8.1.0. Released v3.4.0.
% 0.12/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n021.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 : Fri Jun 10 13:39:24 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.21/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.46 *
% 0.21/0.46 *
% 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/sandbox/benchmark/theBenchmark.p 2022-06-10T13:39:24
% 0.21/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n021.cluster.edu at 2022-06-10T13:39:24
% 0.21/0.51
% 0.21/0.51 ; Recognized commutativity assertion (OR (NOT (|disjointwith| ?X ?Y)) (|disjointwith| ?Y ?X)).
% 0.21/0.51 WARNING:
% 0.21/0.51 |binarypredicate| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.21/0.51 WARNING:
% 0.21/0.51 |thing| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.48/0.66 ; Declaring disjointwith to be commutative.
% 0.48/0.66
% 0.48/0.66 #||
% 0.48/0.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.48/0.66 % SZS output start Refutation
% See solution above
% 0.48/0.66 ||#
% 0.48/0.66
% 0.48/0.66 ; Summary of computation:
% 0.48/0.66 ; 5726 formulas have been input or derived (from 466 formulas).
% 0.48/0.66 ; 710 (12%) were retained. Of these,
% 0.48/0.66 ; 710 (100%) are still being kept.
% 0.48/0.66 ;
% 0.48/0.66 ; Run time in seconds excluding printing time:
% 0.48/0.66 ; 0.023 12% Read assertion file (1 call)
% 0.48/0.66 ; 0.005 3% Assert (177 calls)
% 0.48/0.66 ; 0.038 21% Process new row (5,524 calls)
% 0.48/0.66 ; 0.043 23% Resolution (930 calls)
% 0.48/0.66 ; 0.002 1% Paramodulation (465 calls)
% 0.48/0.66 ; 0.002 1% Condensing (132 calls)
% 0.48/0.66 ; 0.001 1% Forward subsumption (132 calls)
% 0.48/0.66 ; 0.001 1% Backward subsumption (118 calls)
% 0.48/0.66 ; 0.001 1% Clause clause subsumption (22 calls)
% 0.48/0.66 ; 0.023 12% Forward simplification (5,520 calls)
% 0.48/0.66 ; 0.002 1% Backward simplification (710 calls)
% 0.48/0.66 ; 0.001 1% Sortal reasoning (32 calls)
% 0.48/0.66 ; 0.001 1% Purity testing (1 call)
% 0.48/0.66 ; 0.042 23% Other
% 0.48/0.66 ; 0.185 Total
% 0.48/0.66 ; 0.189 Real time
% 0.48/0.66 ;
% 0.48/0.66 ; Term-hash-array has 688 terms in all.
% 0.48/0.66 ; Feature-vector-row-index has 118 entries (118 at peak, 118 added, 0 deleted).
% 0.48/0.66 ; Feature-vector-row-index has 96 nodes (96 at peak, 96 added, 0 deleted).
% 0.48/0.66 ; Retrieved 207 possibly forward subsuming rows in 132 calls.
% 0.48/0.66 ; Retrieved 190 possibly backward subsumed rows in 118 calls.
% 0.48/0.66 ; Path-index has 728 entries (728 at peak, 728 added, 0 deleted).
% 0.48/0.66 ; Path-index has 333 nodes (333 at peak, 333 added, 0 deleted).
% 0.48/0.66 ; Trie-index has 728 entries (728 at peak, 728 added, 0 deleted).
% 0.48/0.66 ; Trie-index has 829 nodes (829 at peak, 829 added, 0 deleted).
% 0.48/0.66 ; Retrieved 4,796 generalization terms in 5,418 calls.
% 0.48/0.66 ; Retrieved 591 instance terms in 591 calls.
% 0.48/0.66 ; Retrieved 23,317 unifiable terms in 7,554 calls.
% 0.48/0.66 ;
% 0.48/0.66 ; The agenda of rows to process has 27 entries:
% 0.48/0.66 ; 27 with value 8
% 0.48/0.66 ; The agenda of rows to give has 244 entries:
% 0.48/0.66 ; 11 with value (4 7) 233 with value (4 8)
% 0.48/0.66 Evaluation took:
% 0.48/0.66 0.189 seconds of real time
% 0.48/0.66 0.145233 seconds of user run time
% 0.48/0.66 0.044147 seconds of system run time
% 0.48/0.66 0 calls to %EVAL
% 0.48/0.66 0 page faults and
% 0.48/0.66 12,210,392 bytes consed.
% 0.48/0.66 :PROOF-FOUND
% 0.48/0.66 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-10T13:39:24
% 0.48/0.66 :PROOF-FOUND
% 0.48/0.66 *
%------------------------------------------------------------------------------