%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n020.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:29:04 EDT 2022
% Result : Theorem 0.42s 0.62s
% Output : Refutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 31
% Syntax : Number of clauses : 72 ( 30 unt; 3 nHn; 70 RR)
% Number of literals : 316 ( 0 equ; 243 neg)
% Maximal clause size : 19 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 25 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
cowlThing(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
cnf(2,axiom,
~ cowlNothing(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
cnf(3,axiom,
( ~ xsd_string(X)
| ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
cnf(4,axiom,
( xsd_string(X)
| xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
cnf(7,axiom,
( cC10(X)
| ~ cC4(X)
| ~ cC8(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(15,axiom,
( cC14(X)
| ~ rR1(X,Y)
| ~ cTOP(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
cnf(34,axiom,
( cC20(X)
| ~ rR1(X,Y)
| ~ cC2xcomp(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
cnf(73,axiom,
( cC34(X)
| ~ rR1(X,Y)
| ~ cC32xcomp(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
cnf(88,axiom,
( cC4(X)
| ~ rR1(X,Y)
| ~ cC2xcomp(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_35) ).
cnf(111,axiom,
( cC48(X)
| ~ rR1(X,Y)
| ~ cC2xcomp(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_44) ).
cnf(142,axiom,
( cC58(X)
| ~ rR1(X,Y)
| ~ cC2(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
cnf(152,axiom,
( cC60(X)
| ~ cC2xcomp(X)
| ~ cC58(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
cnf(155,axiom,
( cC62(X)
| ~ rR1(X,Y)
| ~ cC60(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_62) ).
cnf(198,axiom,
( cC8(X)
| ~ rR1(X,Y)
| ~ cC6xcomp(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
cnf(201,axiom,
( cC80(X)
| ~ cC78xcomp(X)
| ~ cC2xcomp(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_80) ).
cnf(206,axiom,
( cC82(X)
| ~ rR1(X,Y)
| ~ cC80(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
cnf(247,axiom,
rR1(iV8467,iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_103) ).
cnf(248,axiom,
rR1(iV8467,iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_104) ).
cnf(249,axiom,
rR1(iV8467,iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_105) ).
cnf(250,axiom,
rR1(iV8467,iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_106) ).
cnf(254,axiom,
rR1(iV8467,iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_110) ).
cnf(256,axiom,
cC6xcomp(iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
cnf(258,axiom,
cTOP(iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_116) ).
cnf(259,axiom,
cC78xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_118) ).
cnf(260,axiom,
cC2xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_119) ).
cnf(262,axiom,
cC2xcomp(iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_122) ).
cnf(263,axiom,
rR1(iV8472,iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_124) ).
cnf(265,axiom,
cC32xcomp(iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_127) ).
cnf(268,axiom,
cC2(iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_132) ).
cnf(269,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV80')
| cowlNothing('SKOLEMAAAV80')
| ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(270,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[269,2,1]) ).
cnf(271,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV80')
| cowlNothing('SKOLEMAAAV80')
| xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(272,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[271,2,1]) ).
cnf(306,plain,
cC80(iV8471),
inference('HYPERRESOLVE',[status(thm)],[201,259,260]) ).
cnf(307,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[270,306]) ).
cnf(308,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[272,306]) ).
cnf(314,plain,
cC14(iV8467),
inference('HYPERRESOLVE',[status(thm)],[15,248,258]) ).
cnf(315,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[307,314]) ).
cnf(316,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[308,314]) ).
cnf(317,plain,
cC20(iV8467),
inference('HYPERRESOLVE',[status(thm)],[34,254,262]) ).
cnf(318,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[315,317]) ).
cnf(319,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[316,317]) ).
cnf(322,plain,
cC34(iV8467),
inference('HYPERRESOLVE',[status(thm)],[73,250,265]) ).
cnf(323,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[318,322]) ).
cnf(324,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[319,322]) ).
cnf(326,plain,
cC4(iV8467),
inference('HYPERRESOLVE',[status(thm)],[88,254,262]) ).
cnf(327,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[323,326]) ).
cnf(328,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[324,326]) ).
cnf(329,plain,
cC48(iV8467),
inference('HYPERRESOLVE',[status(thm)],[111,254,262]) ).
cnf(330,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[327,329]) ).
cnf(331,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[328,329]) ).
cnf(333,plain,
cC58(iV8472),
inference('HYPERRESOLVE',[status(thm)],[142,263,268]) ).
cnf(334,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[330,333]) ).
cnf(335,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[331,333]) ).
cnf(339,plain,
cC8(iV8467),
inference('HYPERRESOLVE',[status(thm)],[198,249,256]) ).
cnf(340,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[334,339]) ).
cnf(341,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[335,339]) ).
cnf(343,plain,
cC82(iV8467),
inference('HYPERRESOLVE',[status(thm)],[206,306,247]) ).
cnf(344,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[340,343]) ).
cnf(345,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467)
| ~ cC10(iV8467)
| ~ cC60(iV8472) ),
inference('REWRITE',[status(thm)],[341,343]) ).
cnf(371,plain,
cC60(iV8472),
inference('HYPERRESOLVE',[status(thm)],[152,333,262]) ).
cnf(372,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467)
| ~ cC10(iV8467) ),
inference('REWRITE',[status(thm)],[344,371]) ).
cnf(373,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467)
| ~ cC10(iV8467) ),
inference('REWRITE',[status(thm)],[345,371]) ).
cnf(385,plain,
cC10(iV8467),
inference('HYPERRESOLVE',[status(thm)],[7,339,326]) ).
cnf(386,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467) ),
inference('REWRITE',[status(thm)],[372,385]) ).
cnf(387,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81')
| ~ cC62(iV8467) ),
inference('REWRITE',[status(thm)],[373,385]) ).
cnf(405,plain,
cC62(iV8467),
inference('HYPERRESOLVE',[status(thm)],[155,371,254]) ).
cnf(406,plain,
( ~ xsd_string('SKOLEMAAAV81')
| xsd_integer('SKOLEMAAAV81') ),
inference('REWRITE',[status(thm)],[386,405]) ).
cnf(407,plain,
( xsd_string('SKOLEMAAAV81')
| ~ xsd_integer('SKOLEMAAAV81') ),
inference('REWRITE',[status(thm)],[387,405]) ).
cnf(408,plain,
xsd_integer('SKOLEMAAAV81'),
inference('HYPERRESOLVE',[status(thm)],[406,4]) ).
cnf(409,plain,
xsd_string('SKOLEMAAAV81'),
inference('REWRITE',[status(thm)],[407,408]) ).
cnf(410,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[3,409]),408]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% 0.13/0.14 % Command : run-snark %s %d
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Tue Jun 7 14:53:36 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.21/0.49 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.50 *
% 0.21/0.50 *
% 0.21/0.51 #<PACKAGE "SNARK-USER">
% 0.21/0.51 *
% 0.21/0.51 SNARK-TPTP-OPTIONS
% 0.21/0.51 *
% 0.21/0.51 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.21/0.51 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.21/0.51 (USE-FACTORING :POS)
% 0.21/0.51 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.21/0.51 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.21/0.51 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.21/0.51 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.21/0.51 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.21/0.51 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.21/0.51 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.21/0.51 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.21/0.51 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.21/0.51 (DECLARE-TPTP-SYMBOLS2))
% 0.21/0.51 *
% 0.21/0.51 "."
% 0.21/0.51 *
% 0.21/0.51 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-07T14:53:37
% 0.21/0.51 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n020.cluster.edu at 2022-06-07T14:53:37
% 0.42/0.62
% 0.42/0.62
% 0.42/0.62 #||
% 0.42/0.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.62 % SZS output start Refutation
% See solution above
% 0.42/0.63 ||#
% 0.42/0.63
% 0.42/0.63 ; Summary of computation:
% 0.42/0.63 ; 580 formulas have been input or derived (from 306 formulas).
% 0.42/0.63 ; 410 (71%) were retained. Of these,
% 0.42/0.63 ; 28 ( 7%) were simplified or subsumed later,
% 0.42/0.63 ; 382 (93%) are still being kept.
% 0.42/0.63 ;
% 0.42/0.63 ; Run time in seconds excluding printing time:
% 0.42/0.63 ; 0.021 19% Read assertion file (1 call)
% 0.42/0.63 ; 0.008 7% Assert (135 calls)
% 0.42/0.63 ; 0.027 24% Process new row (472 calls)
% 0.42/0.63 ; 0.008 7% Resolution (610 calls)
% 0.42/0.63 ; 0.001 1% Paramodulation (305 calls)
% 0.42/0.63 ; 0.000 0% Factoring (25 calls)
% 0.42/0.63 ; 0.000 0% Condensing (292 calls)
% 0.42/0.63 ; 0.002 2% Forward subsumption (292 calls)
% 0.42/0.63 ; 0.006 5% Backward subsumption (292 calls)
% 0.42/0.63 ; 0.002 2% Forward simplification (472 calls)
% 0.42/0.63 ; 0.005 4% Backward simplification (408 calls)
% 0.42/0.63 ; 0.000 0% Ordering (76 calls)
% 0.42/0.63 ; 0.000 0% Sortal reasoning (32 calls)
% 0.42/0.63 ; 0.000 0% Purity testing (1 call)
% 0.42/0.63 ; 0.033 29% Other
% 0.42/0.63 ; 0.113 Total
% 0.42/0.63 ; 0.120 Real time
% 0.42/0.63 ;
% 0.42/0.63 ; Term-hash-array has 454 terms in all.
% 0.42/0.63 ; Feature-vector-row-index has 266 entries (268 at peak, 292 added, 26 deleted).
% 0.42/0.63 ; Feature-vector-row-index has 281 nodes (310 at peak, 571 added, 290 deleted).
% 0.42/0.63 ; Retrieved 225 possibly forward subsuming rows in 292 calls.
% 0.42/0.63 ; Retrieved 137 possibly backward subsumed rows in 292 calls.
% 0.42/0.63 ; Path-index has 466 entries (466 at peak, 569 added, 103 deleted).
% 0.42/0.63 ; Path-index has 826 nodes (826 at peak, 929 added, 103 deleted).
% 0.42/0.63 ; Trie-index has 466 entries (466 at peak, 569 added, 103 deleted).
% 0.42/0.63 ; Trie-index has 820 nodes (820 at peak, 923 added, 103 deleted).
% 0.42/0.63 ; Retrieved 75 generalization terms in 147 calls.
% 0.42/0.63 ; Retrieved 115 instance terms in 115 calls.
% 0.42/0.63 ; Retrieved 4,966 unifiable terms in 1,749 calls.
% 0.42/0.63 ;
% 0.42/0.63 ; The agenda of rows to give has 85 entries:
% 0.42/0.63 ; 1 with value (4 4) 5 with value (4 6) 22 with value (4 8)
% 0.42/0.63 ; 11 with value (4 5) 45 with value (4 7) 1 with value (4 9)
% 0.42/0.63 Evaluation took:
% 0.42/0.63 0.12 seconds of real time
% 0.42/0.63 0.102891 seconds of user run time
% 0.42/0.63 0.017012 seconds of system run time
% 0.42/0.63 0 calls to %EVAL
% 0.42/0.63 0 page faults and
% 0.42/0.63 11,571,920 bytes consed.
% 0.42/0.63 :PROOF-FOUND
% 0.42/0.63 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-07T14:53:37
% 0.42/0.63 :PROOF-FOUND
% 0.42/0.63 *
%------------------------------------------------------------------------------