%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.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 03:28:31 EDT 2022
% Result : Unsatisfiable 6.58s 6.79s
% Output : Refutation 6.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 26
% Syntax : Number of clauses : 66 ( 32 unt; 10 nHn; 66 RR)
% Number of literals : 154 ( 78 equ; 63 neg)
% Maximal clause size : 16 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(5,axiom,
( X != Y
| ~ cp1(X)
| cp1(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp1_substitution_1) ).
cnf(6,axiom,
( X != Y
| ~ cp2(X)
| cp2(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp2_substitution_1) ).
cnf(8,axiom,
( X != Y
| ~ cp4(X)
| cp4(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp4_substitution_1) ).
cnf(9,axiom,
( X != Y
| ~ cp5(X)
| cp5(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp5_substitution_1) ).
cnf(18,axiom,
( ~ cUnsatisfiable(X)
| rr(X,'SKOLEMAAAV1'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(19,axiom,
( ~ cUnsatisfiable(X)
| cp3('SKOLEMAAAV1'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(20,axiom,
( ~ cUnsatisfiable(X)
| rr(X,'SKOLEMAAAV2'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(21,axiom,
( ~ cUnsatisfiable(X)
| cp4('SKOLEMAAAV2'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(25,axiom,
( ~ cUnsatisfiable(X)
| rr(X,'SKOLEMAAAV4'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(26,axiom,
( ~ cUnsatisfiable(X)
| cp2('SKOLEMAAAV4'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(28,axiom,
( ~ cUnsatisfiable(X)
| rr(X,'SKOLEMAAAV5'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(29,axiom,
( ~ cUnsatisfiable(X)
| cp5('SKOLEMAAAV5'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(35,axiom,
( ~ cUnsatisfiable(X)
| ~ rr(X,Y)
| ~ rr(X,Z)
| ~ rr(X,U)
| ~ rr(X,V)
| ~ rr(X,W)
| Y = Z
| Y = U
| Y = V
| Y = W
| Z = U
| Z = V
| Z = W
| U = V
| U = W
| V = W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(36,axiom,
( ~ cUnsatisfiable(X)
| rr(X,'SKOLEMAAAV8'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(37,axiom,
( ~ cUnsatisfiable(X)
| cp1('SKOLEMAAAV8'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(71,axiom,
( ~ cp1(X)
| ~ cp2(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(72,axiom,
( ~ cp1(X)
| ~ cp4(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(73,axiom,
( ~ cp1(X)
| ~ cp5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(74,axiom,
( ~ cp1(X)
| ~ cp3(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(75,axiom,
( ~ cp2(X)
| ~ cp4(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
cnf(76,axiom,
( ~ cp2(X)
| ~ cp5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
cnf(77,axiom,
( ~ cp2(X)
| ~ cp3(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
cnf(78,axiom,
( ~ cp3(X)
| ~ cp4(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
cnf(79,axiom,
( ~ cp3(X)
| ~ cp5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
cnf(80,axiom,
( ~ cp4(X)
| ~ cp5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
cnf(81,axiom,
cUnsatisfiable(i2003_11_14_17_19_24236),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
cnf(82,plain,
cp3('SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[19,81]) ).
cnf(83,plain,
cp4('SKOLEMAAAV2'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[21,81]) ).
cnf(86,plain,
cp2('SKOLEMAAAV4'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[26,81]) ).
cnf(88,plain,
cp5('SKOLEMAAAV5'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[29,81]) ).
cnf(92,plain,
cp1('SKOLEMAAAV8'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[37,81]) ).
cnf(95,plain,
rr(i2003_11_14_17_19_24236,'SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[18,81]) ).
cnf(96,plain,
rr(i2003_11_14_17_19_24236,'SKOLEMAAAV2'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[20,81]) ).
cnf(98,plain,
rr(i2003_11_14_17_19_24236,'SKOLEMAAAV4'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[25,81]) ).
cnf(99,plain,
rr(i2003_11_14_17_19_24236,'SKOLEMAAAV5'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[28,81]) ).
cnf(102,plain,
rr(i2003_11_14_17_19_24236,'SKOLEMAAAV8'(i2003_11_14_17_19_24236)),
inference('HYPERRESOLVE',[status(thm)],[36,81]) ).
cnf(104,plain,
~ cp5('SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[79,82]) ).
cnf(105,plain,
~ cp4('SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[78,82]) ).
cnf(106,plain,
~ cp2('SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[77,82]) ).
cnf(107,plain,
~ cp1('SKOLEMAAAV1'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[74,82]) ).
cnf(108,plain,
~ cp5('SKOLEMAAAV2'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[80,83]) ).
cnf(110,plain,
~ cp2('SKOLEMAAAV2'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[75,83]) ).
cnf(111,plain,
~ cp1('SKOLEMAAAV2'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[72,83]) ).
cnf(117,plain,
~ cp5('SKOLEMAAAV4'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[76,86]) ).
cnf(119,plain,
~ cp1('SKOLEMAAAV4'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[71,86]) ).
cnf(123,plain,
~ cp1('SKOLEMAAAV5'(i2003_11_14_17_19_24236)),
inference('UR-RESOLVE',[status(thm)],[73,88]) ).
cnf(165,plain,
( 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV8'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('HYPERRESOLVE',[status(thm)],[35,102,81,95,96,98,99]) ).
cnf(266,plain,
'SKOLEMAAAV1'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV5'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[9,104,88]) ).
cnf(278,plain,
( 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV8'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[165,266]) ).
cnf(338,plain,
'SKOLEMAAAV1'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV2'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[8,105,83]) ).
cnf(352,plain,
( 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV8'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[278,338]) ).
cnf(410,plain,
'SKOLEMAAAV1'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV4'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[6,106,86]) ).
cnf(426,plain,
( 'SKOLEMAAAV1'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV8'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[352,410]) ).
cnf(446,plain,
'SKOLEMAAAV1'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV8'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[5,107,92]) ).
cnf(475,plain,
( 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[426,446]) ).
cnf(518,plain,
'SKOLEMAAAV5'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV2'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[9,108,88]) ).
cnf(528,plain,
( 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV2'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[475,518]) ).
cnf(566,plain,
'SKOLEMAAAV2'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV4'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[6,110,86]) ).
cnf(571,plain,
( 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV2'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[528,566]) ).
cnf(582,plain,
'SKOLEMAAAV8'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV2'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[5,111,92]) ).
cnf(595,plain,
( 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[571,582]) ).
cnf(656,plain,
'SKOLEMAAAV5'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV4'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[9,117,88]) ).
cnf(658,plain,
( 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV4'(i2003_11_14_17_19_24236)
| 'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236) ),
inference('REWRITE',[status(thm)],[595,656]) ).
cnf(662,plain,
'SKOLEMAAAV8'(i2003_11_14_17_19_24236) != 'SKOLEMAAAV4'(i2003_11_14_17_19_24236),
inference('UR-RESOLVE',[status(thm)],[5,119,92]) ).
cnf(666,plain,
'SKOLEMAAAV8'(i2003_11_14_17_19_24236) = 'SKOLEMAAAV5'(i2003_11_14_17_19_24236),
inference('REWRITE',[status(thm)],[658,662]) ).
cnf(667,plain,
$false,
inference('REWRITE',[status(thm)],[92,123,666,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n022.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 : Tue Jun 7 11:47:20 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.44 /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p 2022-06-07T11:47:20
% 0.18/0.46 ; 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-07T11:47:20
% 6.58/6.79
% 6.58/6.79
% 6.58/6.79 #||
% 6.58/6.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.58/6.79 % SZS output start Refutation
% See solution above
% 6.58/6.79 ||#
% 6.58/6.79
% 6.58/6.79 ; Summary of computation:
% 6.58/6.79 ; 77403 formulas have been input or derived (from 103 formulas).
% 6.58/6.79 ; 667 ( 1%) were retained. Of these,
% 6.58/6.79 ; 535 (80%) were simplified or subsumed later,
% 6.58/6.79 ; 132 (20%) are still being kept.
% 6.58/6.79 ;
% 6.58/6.79 ; Run time in seconds excluding printing time:
% 6.58/6.79 ; 0.006 0% Read assertion file (1 call)
% 6.58/6.79 ; 0.006 0% Assert (21 calls)
% 6.58/6.79 ; 0.218 3% Process new row (75,384 calls)
% 6.58/6.79 ; 2.571 41% Resolution (204 calls)
% 6.58/6.79 ; 0.000 0% Paramodulation (102 calls)
% 6.58/6.79 ; 0.000 0% Factoring (1 call)
% 6.58/6.79 ; 0.104 2% Condensing (15,442 calls)
% 6.58/6.79 ; 0.890 14% Forward subsumption (15,442 calls)
% 6.58/6.79 ; 0.034 1% Backward subsumption (566 calls)
% 6.58/6.79 ; 0.323 5% Clause clause subsumption (15,128 calls)
% 6.58/6.79 ; 1.947 31% Forward simplification (75,384 calls)
% 6.58/6.79 ; 0.025 0% Backward simplification (652 calls)
% 6.58/6.79 ; 0.000 0% Ordering (13 calls)
% 6.58/6.79 ; 0.000 0% Sortal reasoning (32 calls)
% 6.58/6.79 ; 0.001 0% Purity testing (1 call)
% 6.58/6.79 ; 0.204 3% Other
% 6.58/6.79 ; 6.329 Total
% 6.58/6.79 ; 6.336 Real time
% 6.58/6.79 ;
% 6.58/6.79 ; Term-hash-array has 203 terms in all.
% 6.58/6.79 ; Feature-vector-row-index has 69 entries (187 at peak, 566 added, 497 deleted).
% 6.58/6.79 ; Feature-vector-row-index has 157 nodes (781 at peak, 2,463 added, 2,306 deleted).
% 6.58/6.79 ; Retrieved 14,879 possibly forward subsuming rows in 15,442 calls.
% 6.58/6.79 ; Retrieved 253 possibly backward subsumed rows in 566 calls.
% 6.58/6.79 ; Path-index has 176 entries (202 at peak, 206 added, 30 deleted).
% 6.58/6.79 ; Path-index has 233 nodes (246 at peak, 246 added, 13 deleted).
% 6.58/6.79 ; Trie-index has 176 entries (202 at peak, 206 added, 30 deleted).
% 6.58/6.79 ; Trie-index has 291 nodes (342 at peak, 346 added, 55 deleted).
% 6.58/6.79 ; Retrieved 72 generalization terms in 2,579 calls.
% 6.58/6.79 ; Retrieved 87 instance terms in 85 calls.
% 6.58/6.79 ; Retrieved 1,437,098 unifiable terms in 355,247 calls.
% 6.58/6.79 ;
% 6.58/6.79 ; The agenda of backward simplifiable rows to process has 15 entries:
% 6.58/6.79 ; 15 with value 0
% 6.58/6.79 ; The agenda of rows to process has 1 entry:
% 6.58/6.79 ; 1 with value 10
% 6.58/6.79 ; The agenda of rows to give has 38 entries:
% 6.58/6.79 ; 16 with value (4 7) 12 with value (4 10) 4 with value (4 23)
% 6.58/6.79 ; 2 with value (4 9) 3 with value (4 16) 1 with value (4 30)
% 6.58/6.79 Evaluation took:
% 6.58/6.79 6.336 seconds of real time
% 6.58/6.79 6.043104 seconds of user run time
% 6.58/6.79 0.291296 seconds of system run time
% 6.58/6.79 [Run times include 0.25 seconds GC run time.]
% 6.58/6.79 0 calls to %EVAL
% 6.58/6.79 0 page faults and
% 6.58/6.79 487,463,584 bytes consed.
% 6.58/6.79 :PROOF-FOUND
% 6.58/6.79 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-07T11:47:26
% 6.58/6.79 :PROOF-FOUND
% 6.58/6.79 *
%------------------------------------------------------------------------------