%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWB021+2 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n027.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 : Tue Jul 19 19:20:20 EDT 2022
% Result : Theorem 2.17s 2.41s
% Output : Refutation 2.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 37
% Syntax : Number of clauses : 56 ( 36 unt; 10 nHn; 56 RR)
% Number of literals : 151 ( 22 equ; 77 neg)
% Maximal clause size : 11 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 22 con; 0-2 aty)
% Number of variables : 76 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ iext(uri_owl_oneOf,X,Y)
| ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_oneof_ext) ).
cnf(3,axiom,
( ~ iext(uri_owl_unionOf,X,Y)
| ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_unionof_ext) ).
cnf(7,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,V,X)
| ~ icext(V,W)
| icext(Y,W)
| icext(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_bool_unionof_class_002) ).
cnf(8,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,V,X)
| icext(V,W)
| ~ icext(Y,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_bool_unionof_class_002) ).
cnf(9,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,V,X)
| icext(V,W)
| ~ icext(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_bool_unionof_class_002) ).
cnf(13,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,V,X)
| ~ icext(V,W)
| W = Y
| W = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_002) ).
cnf(14,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,V,X)
| icext(V,W)
| W != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_002) ).
cnf(15,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,V,X)
| icext(V,W)
| W != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_002) ).
cnf(19,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,V)
| ~ iext(uri_rdf_first,V,W)
| ~ iext(uri_rdf_rest,V,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,X1,X)
| ~ icext(X1,Y1)
| Y1 = Y
| Y1 = U
| Y1 = W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_003) ).
cnf(20,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,V)
| ~ iext(uri_rdf_first,V,W)
| ~ iext(uri_rdf_rest,V,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,X1,X)
| icext(X1,Y1)
| Y1 != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_003) ).
cnf(21,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,V)
| ~ iext(uri_rdf_first,V,W)
| ~ iext(uri_rdf_rest,V,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,X1,X)
| icext(X1,Y1)
| Y1 != U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_003) ).
cnf(22,axiom,
( ~ iext(uri_rdf_first,X,Y)
| ~ iext(uri_rdf_rest,X,Z)
| ~ iext(uri_rdf_first,Z,U)
| ~ iext(uri_rdf_rest,Z,V)
| ~ iext(uri_rdf_first,V,W)
| ~ iext(uri_rdf_rest,V,uri_rdf_nil)
| ~ iext(uri_owl_oneOf,X1,X)
| icext(X1,Y1)
| Y1 != W ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_enum_class_003) ).
cnf(31,axiom,
( iext(uri_owl_equivalentClass,X,Y)
| ~ ic(X)
| ~ ic(Y)
| ~ icext(X,'SKOLEMAAAV4'(X,Y))
| ~ icext(Y,'SKOLEMAAAV4'(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_eqdis_equivalentclass) ).
cnf(32,axiom,
( iext(uri_owl_equivalentClass,X,Y)
| ~ ic(X)
| ~ ic(Y)
| icext(X,'SKOLEMAAAV4'(X,Y))
| icext(Y,'SKOLEMAAAV4'(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_eqdis_equivalentclass) ).
cnf(33,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_021_Composite_Enumerations) ).
cnf(34,axiom,
iext(uri_owl_oneOf,uri_ex_c1,'SKOLEMAAAV5'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(35,axiom,
iext(uri_rdf_first,'SKOLEMAAAV5',uri_ex_w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(36,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV5','SKOLEMAAAV6'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(37,axiom,
iext(uri_rdf_first,'SKOLEMAAAV6',uri_ex_w2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(38,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV6',uri_rdf_nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(39,axiom,
iext(uri_owl_oneOf,uri_ex_c2,'SKOLEMAAAV7'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(40,axiom,
iext(uri_rdf_first,'SKOLEMAAAV7',uri_ex_w2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(41,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV7','SKOLEMAAAV8'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(42,axiom,
iext(uri_rdf_first,'SKOLEMAAAV8',uri_ex_w3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(43,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV8',uri_rdf_nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(44,axiom,
iext(uri_owl_oneOf,uri_ex_c3,'SKOLEMAAAV9'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(45,axiom,
iext(uri_rdf_first,'SKOLEMAAAV9',uri_ex_w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(46,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV9','SKOLEMAAAV10'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(47,axiom,
iext(uri_rdf_first,'SKOLEMAAAV10',uri_ex_w2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(48,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV10','SKOLEMAAAV11'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(49,axiom,
iext(uri_rdf_first,'SKOLEMAAAV11',uri_ex_w3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(50,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV11',uri_rdf_nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(51,axiom,
iext(uri_owl_unionOf,uri_ex_c4,'SKOLEMAAAV12'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(52,axiom,
iext(uri_rdf_first,'SKOLEMAAAV12',uri_ex_c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(53,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV12','SKOLEMAAAV13'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(54,axiom,
iext(uri_rdf_first,'SKOLEMAAAV13',uri_ex_c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(55,axiom,
iext(uri_rdf_rest,'SKOLEMAAAV13',uri_rdf_nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
cnf(58,plain,
ic(uri_ex_c3),
inference('HYPERRESOLVE',[status(thm)],[1,44]) ).
cnf(59,plain,
ic(uri_ex_c4),
inference('HYPERRESOLVE',[status(thm)],[3,51]) ).
cnf(64,plain,
icext(uri_ex_c1,uri_ex_w1),
inference('HYPERRESOLVE',[status(thm)],[14,35,36,37,38,34,theory(equality)]) ).
cnf(65,plain,
icext(uri_ex_c2,uri_ex_w2),
inference('HYPERRESOLVE',[status(thm)],[14,40,41,42,43,39,theory(equality)]) ).
cnf(67,plain,
icext(uri_ex_c2,uri_ex_w3),
inference('HYPERRESOLVE',[status(thm)],[15,40,41,42,43,39,theory(equality)]) ).
cnf(68,plain,
icext(uri_ex_c3,uri_ex_w1),
inference('HYPERRESOLVE',[status(thm)],[20,45,46,47,48,49,50,44,theory(equality)]) ).
cnf(69,plain,
icext(uri_ex_c3,uri_ex_w2),
inference('HYPERRESOLVE',[status(thm)],[21,45,46,47,48,49,50,44,theory(equality)]) ).
cnf(70,plain,
icext(uri_ex_c3,uri_ex_w3),
inference('HYPERRESOLVE',[status(thm)],[22,45,46,47,48,49,50,44,theory(equality)]) ).
cnf(101,plain,
( icext(uri_ex_c3,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c4,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4)) ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[32,59,58]),33]) ).
cnf(107,plain,
icext(uri_ex_c4,uri_ex_w1),
inference('HYPERRESOLVE',[status(thm)],[8,64,52,53,54,55,51]) ).
cnf(108,plain,
icext(uri_ex_c4,uri_ex_w2),
inference('HYPERRESOLVE',[status(thm)],[9,65,52,53,54,55,51]) ).
cnf(109,plain,
icext(uri_ex_c4,uri_ex_w3),
inference('HYPERRESOLVE',[status(thm)],[9,67,52,53,54,55,51]) ).
cnf(110,plain,
( icext(uri_ex_c3,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c2,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4)) ),
inference('HYPERRESOLVE',[status(thm)],[7,101,52,53,54,55,51]) ).
cnf(226,plain,
( icext(uri_ex_c1,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c2,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w3 ),
inference('HYPERRESOLVE',[status(thm)],[19,110,45,46,47,48,49,50,44]) ).
cnf(1579,plain,
( icext(uri_ex_c1,'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4))
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w3 ),
inference('HYPERRESOLVE',[status(thm)],[13,226,40,41,42,43,39]) ).
cnf(1580,plain,
( 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w3 ),
inference('HYPERRESOLVE',[status(thm)],[13,1579,35,36,37,38,34]) ).
cnf(1583,plain,
( 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| 'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[31,1580,theory(equality)]),109,70,59,58,33]) ).
cnf(1587,plain,
'SKOLEMAAAV4'(uri_ex_c3,uri_ex_c4) = uri_ex_w1,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[31,1583,theory(equality)]),108,69,59,58,33]) ).
cnf(1588,plain,
$false,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[31,1587,theory(equality)]),107,68,59,58,33]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB021+2 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n027.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 : Wed Jun 1 10:17:48 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-01T10:17:48
% 0.18/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n027.cluster.edu at 2022-06-01T10:17:48
% 2.17/2.41
% 2.17/2.41
% 2.17/2.41 #||
% 2.17/2.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.17/2.41 % SZS output start Refutation
% See solution above
% 2.17/2.42 ||#
% 2.17/2.42
% 2.17/2.42 ; Summary of computation:
% 2.17/2.42 ; 5886 formulas have been input or derived (from 424 formulas).
% 2.17/2.42 ; 1588 (27%) were retained. Of these,
% 2.17/2.42 ; 492 (31%) were simplified or subsumed later,
% 2.17/2.42 ; 1096 (69%) are still being kept.
% 2.17/2.42 ;
% 2.17/2.42 ; Run time in seconds excluding printing time:
% 2.17/2.42 ; 0.005 0% Read assertion file (1 call)
% 2.17/2.42 ; 0.003 0% Assert (8 calls)
% 2.17/2.42 ; 0.161 8% Process new row (5,473 calls)
% 2.17/2.42 ; 0.343 18% Resolution (846 calls)
% 2.17/2.42 ; 0.019 1% Paramodulation (423 calls)
% 2.17/2.42 ; 0.002 0% Factoring (337 calls)
% 2.17/2.42 ; 0.010 1% Condensing (3,923 calls)
% 2.17/2.42 ; 1.012 52% Forward subsumption (3,923 calls)
% 2.17/2.42 ; 0.126 6% Backward subsumption (1,545 calls)
% 2.17/2.42 ; 0.058 3% Clause clause subsumption (25,136 calls)
% 2.17/2.42 ; 0.136 7% Forward simplification (4,799 calls)
% 2.17/2.42 ; 0.006 0% Backward simplification (1,588 calls)
% 2.17/2.42 ; 0.027 1% Ordering (21,795 calls)
% 2.17/2.42 ; 0.000 0% Sortal reasoning (32 calls)
% 2.17/2.42 ; 0.000 0% Purity testing (1 call)
% 2.17/2.42 ; 0.045 2% Other
% 2.17/2.42 ; 1.953 Total
% 2.17/2.42 ; 1.958 Real time
% 2.17/2.42 ;
% 2.17/2.42 ; Term-hash-array has 426 terms in all.
% 2.17/2.42 ; Feature-vector-row-index has 1,053 entries (1,185 at peak, 1,545 added, 492 deleted).
% 2.17/2.42 ; Feature-vector-row-index has 5,458 nodes (6,024 at peak, 8,896 added, 3,438 deleted).
% 2.17/2.42 ; Retrieved 77,514 possibly forward subsuming rows in 3,923 calls.
% 2.17/2.42 ; Retrieved 6,373 possibly backward subsumed rows in 1,545 calls.
% 2.17/2.42 ; Path-index has 440 entries (449 at peak, 464 added, 24 deleted).
% 2.17/2.42 ; Path-index has 263 nodes (263 at peak, 266 added, 3 deleted).
% 2.17/2.42 ; Trie-index has 440 entries (449 at peak, 464 added, 24 deleted).
% 2.17/2.42 ; Trie-index has 714 nodes (723 at peak, 749 added, 35 deleted).
% 2.17/2.42 ; Retrieved 937 generalization terms in 15,060 calls.
% 2.17/2.42 ; Retrieved 42 instance terms in 42 calls.
% 2.17/2.42 ; Retrieved 115,575 unifiable terms in 74,626 calls.
% 2.17/2.42 ;
% 2.17/2.42 ; The agenda of rows to process has 3 entries:
% 2.17/2.42 ; 3 with value 40
% 2.17/2.42 ; The agenda of rows to give has 757 entries:
% 2.17/2.42 ; 7 with value (4 39) 65 with value (4 51) 19 with value (4 61)
% 2.17/2.42 ; 9 with value (4 40) 36 with value (4 52) 13 with value (4 62)
% 2.17/2.42 ; 5 with value (4 42) 41 with value (4 53) 4 with value (4 63)
% 2.17/2.42 ; 17 with value (4 43) 21 with value (4 54) 26 with value (4 64)
% 2.17/2.42 ; 23 with value (4 44) 12 with value (4 55) 27 with value (4 65)
% 2.17/2.42 ; 24 with value (4 45) 23 with value (4 56) 9 with value (4 66)
% 2.17/2.42 ; 64 with value (4 46) 2 with value (4 57) 82 with value (4 68)
% 2.17/2.42 ; 39 with value (4 47) 1 with value (4 58) 40 with value (4 69)
% 2.17/2.42 ; 18 with value (4 48) 10 with value (4 59) 4 with value (4 70)
% 2.17/2.42 ; 13 with value (4 49) 21 with value (4 60) 10 with value (4 71)
% 2.17/2.42 ; 72 with value (4 50)
% 2.17/2.42 Evaluation took:
% 2.17/2.42 1.959 seconds of real time
% 2.17/2.42 1.848898 seconds of user run time
% 2.17/2.42 0.109672 seconds of system run time
% 2.17/2.42 [Run times include 0.08 seconds GC run time.]
% 2.17/2.42 0 calls to %EVAL
% 2.17/2.42 0 page faults and
% 2.17/2.42 220,132,696 bytes consed.
% 2.17/2.42 :PROOF-FOUND
% 2.17/2.42 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-01T10:17:50
% 2.17/2.42 :PROOF-FOUND
% 2.17/2.42 *
%------------------------------------------------------------------------------