%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP397_1 : TPTP v8.1.0. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n018.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 00:35:14 EDT 2022
% Result : Theorem 8.61s 8.78s
% Output : Refutation 8.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 20
% Syntax : Number of formulae : 37 ( 28 unt; 0 typ; 0 def)
% Number of atoms : 229 ( 34 equ)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 25 ( 13 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 180 ( 180 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 44 ( 42 usr; 18 prp; 0-3 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 51 ( 0 sgn 51 !; 0 ?; 51 :)
% Comments :
%------------------------------------------------------------------------------
tff(3,negated_conjecture,
'fun_app$a'('comp$'('f$'),'i$') != 'g$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture1) ).
tff(7,axiom,
! [X: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Z: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'('fun_app$a'('comp$'(X),Y),Z) = 'fun_app$c'(X,'fun_app$d'(Y,Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom5) ).
tff(9,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',Z: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'('fun_app$i'('comp$b'(X),Y),Z) = 'fun_app$d'(X,'fun_app$g'(Y,Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom7) ).
tff(19,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',Z: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( 'comp$j'(X,'fun_app$f'('comp$a'(Y),Z)) = 'fun_app$a'('comp$'('comp$k'(X,Y)),Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom18) ).
tff(81,axiom,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X) = 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$c'('f$',X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom96) ).
tff(82,axiom,
'image$'('f$','top$') = 'image$a'('g$','top$a'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom97) ).
tff(114,axiom,
! [X: 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Z: 'B_ell2_b_ell2_cblinfun_set$'] :
( ( 'fun_app$n'(X,'fun_app$b'(Y,'SKOLEMAAAV12.B_ell2_b_ell2_cblinfun$'(Z,X,Y))) != 'SKOLEMAAAV12.B_ell2_b_ell2_cblinfun$'(Z,X,Y) )
| 'inj_on$a'(Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom111) ).
tff(170,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'C_ell2_c_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X,'top$a')
| ~ 'member$'(Y,'image$a'(X,'top$a'))
| ( Y = 'fun_app$b'(X,'SKOLEMAAAV30.B_ell2_b_ell2_cblinfun$'(Y,X)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom139) ).
tff(205,axiom,
! [X: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun$'] : 'member$'('fun_app$c'(X,Y),'image$'(X,'top$')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom171) ).
tff(219,axiom,
! [X: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Z: 'B_ell2_b_ell2_cblinfun_set$'] :
( ~ 'inj_on$c'('fun_app$f'('comp$a'(X),Y),Z)
| 'inj_on$e'(Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom185) ).
tff(313,axiom,
! [X: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Z: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'(X,'SKOLEMAAAV80.A_ell2_a_ell2_cblinfun$'(Y,X,Z)) != 'fun_app$c'(Z,'SKOLEMAAAV80.A_ell2_a_ell2_cblinfun$'(Y,X,Z)) )
| ( 'fun_app$a'('comp$'(X),Y) = 'fun_app$a'('comp$'(Z),Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom259) ).
tff(338,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ~ 'inj_on$e'(X,'top$a')
| ( 'fun_app$a'('comp$'('comp$k'(Y,'inv_into$c'('top$a',X))),X) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom289) ).
tff(393,axiom,
'inj_on$a'('g$','top$a'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom336) ).
tff(438,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'C_ell2_c_ell2_cblinfun$',Z: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X,'top$a')
| ( Y != 'fun_app$b'(X,Z) )
| ( 'fun_app$n'('inv_into$a'('top$a',X),Y) = Z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom377) ).
tff(440,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X,'top$a')
| ( 'fun_app$n'('inv_into$a'('top$a',X),'fun_app$b'(X,Y)) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom379) ).
tff(452,axiom,
'fun_app$f'('comp$a'('j$'),'i$') = 'id$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom388) ).
tff(453,axiom,
'fun_app$i'('comp$b'('i$'),'j$') = 'id$a',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom389) ).
tff(477,axiom,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'('id$a',X) = X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom424) ).
tff(509,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_set$'] : 'inj_on$c'('id$',X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom454) ).
tff(526,axiom,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'fun_app$i'('comp$b'(X),Y) != 'id$a' )
| ( 'fun_app$f'('comp$a'(Y),X) != 'id$' )
| ( 'inv_into$c'('top$a',X) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom480) ).
tff(782,plain,
! [X: 'B_ell2_b_ell2_cblinfun_set$'] : 'inj_on$e'('i$',X),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[219,452,theory(equality)]),509]) ).
tff(816,plain,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( X = 'fun_app$d'('i$','fun_app$g'('j$',X)) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[9,453,theory(equality)]),477,theory(equality)]) ).
tff(894,plain,
! [X: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$b'('g$',X)) = X ),
inference('HYPERRESOLVE',[status(thm)],[440,393]) ).
tff(906,plain,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$j'(X,'id$') = 'fun_app$a'('comp$'('comp$k'(X,'j$')),'i$') ),
inference('PARAMODULATE',[status(thm)],[19,452,theory(equality)]) ).
tff(1230,plain,
! [X: 'C_ell2_c_ell2_cblinfun$'] :
( ~ 'member$'(X,'image$'('f$','top$'))
| ( X = 'fun_app$b'('g$','SKOLEMAAAV30.B_ell2_b_ell2_cblinfun$'(X,'g$')) ) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[170,82,theory(equality)]),393]) ).
tff(1456,plain,
'inv_into$c'('top$a','i$') = 'j$',
inference('HYPERRESOLVE',[status(thm)],[526,453,452]) ).
tff(1964,plain,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$j'(X,'id$') = X ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[338,782]),906,1456,theory(equality)]) ).
tff(1969,plain,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( X = 'fun_app$a'('comp$'('comp$k'(X,'j$')),'i$') ),
inference('REWRITE',[status(thm)],[906,1964,theory(equality)]) ).
tff(2901,plain,
! [X: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$b'('fun_app$a'('comp$'(X),'i$'),'fun_app$g'('j$',Y)) = 'fun_app$c'(X,Y) ),
inference('PARAMODULATE',[status(thm)],[7,816,theory(equality)]) ).
tff(3439,plain,
! [X: 'B_ell2_b_ell2_cblinfun_set$'] : 'inj_on$a'('g$',X),
inference('HYPERRESOLVE',[status(thm)],[114,894]) ).
tff(4778,plain,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X) = 'fun_app$b'('g$','SKOLEMAAAV30.B_ell2_b_ell2_cblinfun$'('fun_app$c'('f$',X),'g$')) ),
inference('HYPERRESOLVE',[status(thm)],[1230,205]) ).
tff(4783,plain,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X) = 'SKOLEMAAAV30.B_ell2_b_ell2_cblinfun$'('fun_app$c'('f$',X),'g$') ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[438,4778,3439]),81,theory(equality)]) ).
tff(4784,plain,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X) = 'fun_app$b'('g$','fun_app$g'('j$',X)) ),
inference('REWRITE',[status(thm)],[4778,4783,theory(equality)]) ).
tff(5064,plain,
! [X: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',Y: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$b'(X,'fun_app$g'('j$',Y)) = 'fun_app$c'('comp$k'(X,'j$'),Y) ),
inference('PARAMODULATE',[status(thm)],[2901,1969,theory(equality)]) ).
tff(5065,plain,
! [X: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X) = 'fun_app$c'('comp$k'('g$','j$'),X) ),
inference('REWRITE',[status(thm)],[4784,5064,theory(equality)]) ).
tff(5190,plain,
! [X: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( 'fun_app$a'('comp$'('f$'),X) = 'fun_app$a'('comp$'('comp$k'('g$','j$')),X) ),
inference('HYPERRESOLVE',[status(thm)],[313,5065]) ).
cnf(6104,plain,
$false,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[1969,5190,theory(equality)]),3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP397_1 : TPTP v8.1.0. Released v8.0.0.
% 0.07/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n018.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 3 05:56:46 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.20/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.47 *
% 0.20/0.47 *
% 0.20/0.47 #<PACKAGE "SNARK-USER">
% 0.20/0.47 *
% 0.20/0.47 SNARK-TPTP-OPTIONS
% 0.20/0.47 *
% 0.20/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.47 (USE-FACTORING :POS)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.47 *
% 0.20/0.47 "."
% 0.20/0.47 *
% 0.20/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T05:56:46
% 0.20/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n018.cluster.edu at 2022-06-03T05:56:46
% 0.47/0.68 WARNING:
% 0.47/0.68 |clinear$f| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |bijection$a| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |bijection$| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$f| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |bijection$b| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$k| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$j| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$n| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |iso_register$h| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |inj_on$j| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$q| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$p| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$r| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |inj_on$k| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$l| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$m| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |inj_on$h| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$o| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |inj_on$i| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.47/0.68 WARNING:
% 0.47/0.68 |register$i| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 8.61/8.78
% 8.61/8.78
% 8.61/8.78 #||
% 8.61/8.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.61/8.78 % SZS output start Refutation
% See solution above
% 8.62/8.78 ||#
% 8.62/8.78
% 8.62/8.78 ; Summary of computation:
% 8.62/8.78 ; 47780 formulas have been input or derived (from 1064 formulas).
% 8.62/8.78 ; 6104 (13%) were retained. Of these,
% 8.62/8.78 ; 2183 (36%) were simplified or subsumed later,
% 8.62/8.78 ; 3921 (64%) are still being kept.
% 8.62/8.78 ;
% 8.62/8.78 ; Run time in seconds excluding printing time:
% 8.62/8.78 ; 0.168 2% Read assertion file (1 call)
% 8.62/8.78 ; 0.021 0% Assert (640 calls)
% 8.62/8.78 ; 0.772 9% Process new row (41,747 calls)
% 8.62/8.78 ; 3.453 42% Resolution (2,126 calls)
% 8.62/8.78 ; 0.085 1% Paramodulation (1,063 calls)
% 8.62/8.78 ; 0.000 0% Factoring (53 calls)
% 8.62/8.78 ; 0.118 1% Condensing (7,611 calls)
% 8.62/8.78 ; 0.618 7% Forward subsumption (7,611 calls)
% 8.62/8.78 ; 0.239 3% Backward subsumption (3,740 calls)
% 8.62/8.78 ; 0.045 1% Clause clause subsumption (9,711 calls)
% 8.62/8.78 ; 1.503 18% Forward simplification (39,717 calls)
% 8.62/8.78 ; 0.190 2% Backward simplification (6,050 calls)
% 8.62/8.78 ; 0.657 8% Ordering (153,544 calls)
% 8.62/8.78 ; 0.295 4% Sortal reasoning (396,265 calls)
% 8.62/8.78 ; 0.003 0% Purity testing (1 call)
% 8.62/8.78 ; 0.138 2% Other
% 8.62/8.78 ; 8.305 Total
% 8.62/8.78 ; 8.309 Real time
% 8.62/8.78 ;
% 8.62/8.79 ; Term-hash-array has 16,435 terms in all.
% 8.62/8.79 ; Feature-vector-row-index has 3,121 entries (3,121 at peak, 3,740 added, 619 deleted).
% 8.62/8.79 ; Feature-vector-row-index has 31,913 nodes (31,913 at peak, 38,419 added, 6,506 deleted).
% 8.62/8.79 ; Retrieved 12,755 possibly forward subsuming rows in 7,611 calls.
% 8.62/8.79 ; Retrieved 1,540 possibly backward subsumed rows in 3,740 calls.
% 8.62/8.79 ; Path-index has 11,711 entries (11,711 at peak, 17,131 added, 5,420 deleted).
% 8.62/8.79 ; Path-index has 38,583 nodes (38,583 at peak, 43,132 added, 4,549 deleted).
% 8.62/8.79 ; Trie-index has 11,711 entries (11,711 at peak, 17,131 added, 5,420 deleted).
% 8.62/8.79 ; Trie-index has 53,516 nodes (53,516 at peak, 90,906 added, 37,390 deleted).
% 8.62/8.79 ; Retrieved 139,991 generalization terms in 270,341 calls.
% 8.62/8.79 ; Retrieved 6,290 instance terms in 2,821 calls.
% 8.62/8.79 ; Retrieved 6,270,631 unifiable terms in 40,037 calls.
% 8.62/8.79 ;
% 8.62/8.79 ; The agenda of rows to process has 100 entries:
% 8.62/8.79 ; 1 with value 16 2 with value 23 2 with value 33
% 8.62/8.79 ; 1 with value 17 12 with value 24 4 with value 38
% 8.62/8.79 ; 1 with value 18 36 with value 26 1 with value 39
% 8.62/8.79 ; 2 with value 19 1 with value 27 4 with value 40
% 8.62/8.79 ; 3 with value 20 4 with value 28 2 with value 45
% 8.62/8.79 ; 1 with value 21 9 with value 29 2 with value 47
% 8.62/8.79 ; 4 with value 22 8 with value 31
% 8.62/8.79 ; The agenda of rows to give has 3007 entries:
% 8.62/8.79 ; 3 with value (4 18) 57 with value (4 43) 3 with value (4 68)
% 8.62/8.79 ; 56 with value (4 19) 45 with value (4 44) 14 with value (4 69)
% 8.62/8.79 ; 67 with value (4 20) 22 with value (4 45) 6 with value (4 70)
% 8.62/8.79 ; 113 with value (4 21) 64 with value (4 46) 9 with value (4 71)
% 8.62/8.79 ; 69 with value (4 22) 75 with value (4 47) 6 with value (4 72)
% 8.62/8.79 ; 142 with value (4 23) 34 with value (4 48) 8 with value (4 73)
% 8.62/8.79 ; 137 with value (4 24) 43 with value (4 49) 9 with value (4 74)
% 8.62/8.79 ; 132 with value (4 25) 16 with value (4 50) 4 with value (4 75)
% 8.62/8.79 ; 107 with value (4 26) 24 with value (4 51) 4 with value (4 76)
% 8.62/8.79 ; 129 with value (4 27) 19 with value (4 52) 8 with value (4 77)
% 8.62/8.79 ; 112 with value (4 28) 23 with value (4 53) 12 with value (4 78)
% 8.62/8.79 ; 145 with value (4 29) 13 with value (4 54) 2 with value (4 79)
% 8.62/8.79 ; 105 with value (4 30) 23 with value (4 55) 2 with value (4 80)
% 8.62/8.79 ; 115 with value (4 31) 9 with value (4 56) 10 with value (4 81)
% 8.62/8.79 ; 95 with value (4 32) 11 with value (4 57) 8 with value (4 82)
% 8.62/8.79 ; 89 with value (4 33) 14 with value (4 58) 2 with value (4 83)
% 8.62/8.79 ; 103 with value (4 34) 10 with value (4 59) 2 with value (4 84)
% 8.62/8.79 ; 76 with value (4 35) 8 with value (4 60) 1 with value (4 85)
% 8.62/8.79 ; 76 with value (4 36) 11 with value (4 61) 6 with value (4 86)
% 8.62/8.79 ; 52 with value (4 37) 11 with value (4 62) 4 with value (4 87)
% 8.62/8.79 ; 77 with value (4 38) 8 with value (4 63) 2 with value (4 88)
% 8.62/8.79 ; 65 with value (4 39) 10 with value (4 64) 2 with value (4 89)
% 8.62/8.79 ; 91 with value (4 40) 14 with value (4 65) 2 with value (4 94)
% 8.62/8.79 ; 73 with value (4 41) 7 with value (4 66) 2 with value (4 95)
% 8.62/8.79 ; 66 with value (4 42) 13 with value (4 67)
% 8.62/8.79 Evaluation took:
% 8.62/8.79 8.312 seconds of real time
% 8.62/8.79 7.478819 seconds of user run time
% 8.62/8.79 0.833066 seconds of system run time
% 8.62/8.79 [Run times include 0.957 seconds GC run time.]
% 8.62/8.79 0 calls to %EVAL
% 8.62/8.79 0 page faults and
% 8.62/8.79 540,757,040 bytes consed.
% 8.62/8.79 :PROOF-FOUND
% 8.62/8.79 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T05:56:54
% 8.62/8.79 :PROOF-FOUND
% 8.62/8.79 *
%------------------------------------------------------------------------------