%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP384_1 : TPTP v8.1.0. Released v8.0.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 00:35:12 EDT 2022
% Result : Theorem 1.09s 1.29s
% Output : Refutation 1.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 15
% Syntax : Number of formulae : 29 ( 22 unt; 0 typ; 0 def)
% Number of atoms : 177 ( 28 equ)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 20 ( 11 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 139 ( 139 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 42 ( 40 usr; 21 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 36 ( 0 sgn 36 !; 0 ?; 36 :)
% Comments :
%------------------------------------------------------------------------------
tff(45,negated_conjecture,
'comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) != 'id$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture29) ).
tff(58,axiom,
'fun_app$ae'('fun_app$af'('comp$d','g$'),'g$a') = 'id$',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom42) ).
tff(89,axiom,
'fun_app$ac'('fun_app$ad'('comp$c','SKOLEMAAAU4.B_update_a_update_fun$'),'f$a') = 'id$b',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom66) ).
tff(92,axiom,
'fun_app$aj'('fun_app$ak'('comp$e','f$a'),'f$') = 'id$a',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom67) ).
tff(94,axiom,
'fun_app$ac'('fun_app$ad'('comp$c','f$'),'f$a') = 'id$b',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom69) ).
tff(212,axiom,
! [X: 'A_update_c_update_fun$',Y: 'B_update_a_update_fun$',Z: 'A_update_b_update_fun$'] : ( 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X),Y),Z) = 'comp$ab'(X,'fun_app$ac'('fun_app$ad'('comp$c',Y),Z)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom169) ).
tff(223,axiom,
! [X: 'B_update_c_update_fun$',Y: 'A_update_b_update_fun$',Z: 'C_update_a_update_fun$'] : ( 'comp$'(X,'fun_app$x'('fun_app$y'('comp$b',Y),Z)) = 'fun_app$ae'('fun_app$af'('comp$d','comp$aj'(X,Y)),Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom187) ).
tff(264,axiom,
! [X: 'A_update_b_update_fun$',Y: 'B_update_a_update_fun$'] : ( 'fcomp$'(X,Y) = 'fun_app$ac'('fun_app$ad'('comp$c',Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom229) ).
tff(265,axiom,
! [X: 'C_update_a_update_fun$',Y: 'A_update_c_update_fun$'] : ( 'fcomp$a'(X,Y) = 'fun_app$ae'('fun_app$af'('comp$d',Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom230) ).
tff(266,axiom,
! [X: 'B_update_a_update_fun$',Y: 'A_update_c_update_fun$'] : ( 'fcomp$b'(X,Y) = 'fun_app$v'('fun_app$w'('comp$a',Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom231) ).
tff(268,axiom,
! [X: 'B_update_a_update_fun$',Y: 'A_update_b_update_fun$'] : ( 'fcomp$d'(X,Y) = 'fun_app$aj'('fun_app$ak'('comp$e',Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom233) ).
tff(453,axiom,
! [X: 'A_update_b_update_fun$',Y: 'B_update_a_update_fun$'] :
( ( 'fun_app$aj'('fun_app$ak'('comp$e',X),Y) != 'id$a' )
| ( 'fun_app$ac'('fun_app$ad'('comp$c',Y),X) != 'id$b' )
| ( 'inv_into$b'('top$',X) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom455) ).
tff(454,plain,
! [X: 'B_update_a_update_fun$',Y: 'A_update_b_update_fun$'] :
( ( 'fcomp$d'(X,Y) != 'id$a' )
| ( 'fcomp$'(Y,X) != 'id$b' )
| ( 'inv_into$b'('top$',Y) = X ) ),
inference('REWRITE',[status(thm)],[453,264,268,theory(equality)]) ).
tff(486,axiom,
! [X: 'A_update_b_update_fun$',Y: 'A_update_c_update_fun$'] :
( ~ 'inj_on$'(X,'top$')
| ( 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',Y),'inv_into$b'('top$',X)),X) = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom479) ).
tff(487,plain,
! [X: 'A_update_b_update_fun$',Y: 'A_update_c_update_fun$'] :
( ~ 'inj_on$'(X,'top$')
| ( 'comp$aj'('fcomp$b'('inv_into$b'('top$',X),Y),X) = Y ) ),
inference('REWRITE',[status(thm)],[486,266,theory(equality)]) ).
tff(568,axiom,
! [X: 'B_update_a_update_fun$',Y: 'A_update_b_update_fun$',Z: 'A_update_set$'] :
( ~ 'inj_on$i'('fun_app$ac'('fun_app$ad'('comp$c',X),Y),Z)
| 'inj_on$'(Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom526) ).
tff(569,plain,
! [X: 'A_update_b_update_fun$',Y: 'B_update_a_update_fun$',Z: 'A_update_set$'] :
( ~ 'inj_on$i'('fcomp$'(X,Y),Z)
| 'inj_on$'(X,Z) ),
inference('REWRITE',[status(thm)],[568,264,theory(equality)]) ).
tff(580,axiom,
! [X: 'A_update_set$'] : 'inj_on$i'('id$b',X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom533) ).
tff(766,plain,
'fcomp$d'('f$','f$a') = 'id$a',
inference('REWRITE',[status(thm)],[92,268,theory(equality)]) ).
tff(833,plain,
'fcomp$a'('g$a','g$') = 'id$',
inference('REWRITE',[status(thm)],[58,265,theory(equality)]) ).
tff(848,plain,
! [X: 'B_update_a_update_fun$',Y: 'A_update_c_update_fun$',Z: 'A_update_b_update_fun$'] : ( 'comp$aj'('fcomp$b'(X,Y),Z) = 'comp$ab'(Y,'fcomp$'(Z,X)) ),
inference('REWRITE',[status(thm)],[212,266,264,theory(equality)]) ).
tff(849,plain,
! [X: 'A_update_b_update_fun$',Y: 'A_update_c_update_fun$'] :
( ~ 'inj_on$'(X,'top$')
| ( 'comp$ab'(Y,'fcomp$'(X,'inv_into$b'('top$',X))) = Y ) ),
inference('REWRITE',[status(thm)],[487,848,theory(equality)]) ).
tff(863,plain,
'fcomp$'('f$a','f$') = 'id$b',
inference('REWRITE',[status(thm)],[94,264,theory(equality)]) ).
tff(864,plain,
'fcomp$'('f$a','SKOLEMAAAU4.B_update_a_update_fun$') = 'id$b',
inference('REWRITE',[status(thm)],[89,264,theory(equality)]) ).
tff(872,plain,
'fcomp$a'('g$a','comp$ab'('g$','id$b')) != 'id$',
inference('REWRITE',[status(thm)],[45,265,863,848,266,223,theory(equality)]) ).
tff(915,plain,
! [X: 'A_update_set$'] : 'inj_on$'('f$a',X),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[569,864,theory(equality)]),580]) ).
tff(1271,plain,
'inv_into$b'('top$','f$a') = 'f$',
inference('HYPERRESOLVE',[status(thm)],[454,766,863]) ).
tff(1734,plain,
! [X: 'A_update_c_update_fun$'] : ( 'comp$ab'(X,'id$b') = X ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[849,915]),863,1271,theory(equality)]) ).
cnf(1739,plain,
$false,
inference('REWRITE',[status(thm)],[872,833,1734,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : ITP384_1 : TPTP v8.1.0. Released v8.0.0.
% 0.08/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n022.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 01:25:21 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.47 #<PACKAGE "SNARK-USER">
% 0.19/0.47 *
% 0.19/0.47 SNARK-TPTP-OPTIONS
% 0.19/0.47 *
% 0.19/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.47 (USE-FACTORING :POS)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.47 *
% 0.19/0.47 "."
% 0.19/0.47 *
% 0.19/0.47 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T01:25:22
% 0.19/0.47 ; 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-03T01:25:22
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$a| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_surjective_proof_assist$b| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$b| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$f| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$c| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$g| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$b| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |bijection$b| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$e| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$c| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$f| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$h| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$d| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |bijection$| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$g| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$e| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$d| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$e| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$h| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |bijection$a| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$f| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$h| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_update_accessor_cong_assist$e| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$e| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_surjective_proof_assist$| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$c| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$c| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$d| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$f| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$g| is a 2-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$f| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |type_definition$d| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |iso_tuple_surjective_proof_assist$a| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |inj_on$d| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$h| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$au| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |fun_app$bw| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$m| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$be| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |fun_app$ca| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$z| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$s| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$ba| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$w| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |inj_on$h| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$bh| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$o| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$f| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$v| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |inj_on$e| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$j| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$b| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$j| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$br| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$ae| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$bx| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |fun_app$by| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$an| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$ar| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$n| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$e| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$aj| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$u| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$m| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$g| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$bu| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$by| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$k| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$q| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$d| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$p| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$bk| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$s| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$bn| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$o| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$r| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$n| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$e| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$l| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$i| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |compatible$t| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$w| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |rel_fun$ax| is a 4-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$a| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |register$g| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |inj_on$g| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |inj_on$f| is a 2-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$g| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |quotient3$h| is a 3-ary relation that occurs only negatively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$c| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 0.50/0.72 WARNING:
% 0.50/0.72 |preregister$d| is a 1-ary relation that occurs only positively; disabling rows that contain it.
% 1.09/1.29
% 1.09/1.29
% 1.09/1.29 #||
% 1.09/1.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.09/1.29 % SZS output start Refutation
% See solution above
% 1.09/1.31 ||#
% 1.09/1.31
% 1.09/1.31 ; Summary of computation:
% 1.09/1.31 ; 4317 formulas have been input or derived (from 534 formulas).
% 1.09/1.31 ; 1739 (40%) were retained. Of these,
% 1.09/1.31 ; 511 (29%) were simplified or subsumed later,
% 1.09/1.31 ; 1228 (71%) are still being kept.
% 1.09/1.31 ;
% 1.09/1.31 ; Run time in seconds excluding printing time:
% 1.09/1.31 ; 0.213 26% Read assertion file (1 call)
% 1.09/1.31 ; 0.021 3% Assert (669 calls)
% 1.09/1.31 ; 0.169 21% Process new row (3,674 calls)
% 1.09/1.31 ; 0.157 19% Resolution (1,066 calls)
% 1.09/1.31 ; 0.027 3% Paramodulation (533 calls)
% 1.09/1.31 ; 0.000 0% Factoring (8 calls)
% 1.09/1.31 ; 0.014 2% Condensing (1,062 calls)
% 1.09/1.31 ; 0.032 4% Forward subsumption (1,062 calls)
% 1.09/1.31 ; 0.032 4% Backward subsumption (972 calls)
% 1.09/1.31 ; 0.006 1% Clause clause subsumption (1,009 calls)
% 1.09/1.31 ; 0.048 6% Forward simplification (3,441 calls)
% 1.09/1.31 ; 0.020 2% Backward simplification (1,513 calls)
% 1.09/1.31 ; 0.011 1% Ordering (3,310 calls)
% 1.09/1.31 ; 0.028 3% Sortal reasoning (32,923 calls)
% 1.09/1.31 ; 0.006 1% Purity testing (1 call)
% 1.09/1.31 ; 0.036 4% Other
% 1.09/1.31 ; 0.820 Total
% 1.09/1.31 ; 0.838 Real time
% 1.09/1.31 ;
% 1.09/1.31 ; Term-hash-array has 5,408 terms in all.
% 1.09/1.31 ; Feature-vector-row-index has 817 entries (817 at peak, 972 added, 155 deleted).
% 1.09/1.31 ; Feature-vector-row-index has 5,815 nodes (5,852 at peak, 7,569 added, 1,754 deleted).
% 1.09/1.31 ; Retrieved 1,345 possibly forward subsuming rows in 1,062 calls.
% 1.09/1.31 ; Retrieved 314 possibly backward subsumed rows in 972 calls.
% 1.09/1.31 ; Path-index has 4,727 entries (4,739 at peak, 5,762 added, 1,035 deleted).
% 1.09/1.31 ; Path-index has 18,098 nodes (18,135 at peak, 19,460 added, 1,362 deleted).
% 1.09/1.31 ; Trie-index has 4,727 entries (4,739 at peak, 5,762 added, 1,035 deleted).
% 1.09/1.31 ; Trie-index has 17,326 nodes (17,400 at peak, 20,825 added, 3,499 deleted).
% 1.09/1.31 ; Retrieved 4,327 generalization terms in 15,675 calls.
% 1.09/1.31 ; Retrieved 921 instance terms in 685 calls.
% 1.09/1.31 ; Retrieved 205,479 unifiable terms in 4,203 calls.
% 1.09/1.31 ;
% 1.09/1.31 ; The agenda of backward simplifiable rows to process has 2 entries:
% 1.09/1.31 ; 2 with value 0
% 1.09/1.31 ; The agenda of rows to process has 13 entries:
% 1.09/1.31 ; 6 with value 15 2 with value 30 4 with value 34
% 1.09/1.31 ; 1 with value 16
% 1.09/1.31 ; The agenda of rows to give has 718 entries:
% 1.09/1.31 ; 4 with value (4 5) 9 with value (4 22) 1 with value (4 39)
% 1.09/1.31 ; 5 with value (4 6) 24 with value (4 23) 16 with value (4 40)
% 1.09/1.31 ; 6 with value (4 7) 36 with value (4 24) 3 with value (4 41)
% 1.09/1.31 ; 23 with value (4 8) 26 with value (4 25) 10 with value (4 42)
% 1.09/1.31 ; 2 with value (4 9) 21 with value (4 26) 16 with value (4 43)
% 1.09/1.31 ; 7 with value (4 10) 9 with value (4 27) 11 with value (4 44)
% 1.09/1.31 ; 6 with value (4 11) 11 with value (4 28) 4 with value (4 46)
% 1.09/1.31 ; 3 with value (4 12) 16 with value (4 29) 4 with value (4 50)
% 1.09/1.31 ; 15 with value (4 13) 35 with value (4 30) 2 with value (4 53)
% 1.09/1.31 ; 14 with value (4 14) 46 with value (4 31) 2 with value (4 55)
% 1.09/1.31 ; 13 with value (4 15) 14 with value (4 32) 2 with value (4 58)
% 1.09/1.31 ; 7 with value (4 16) 16 with value (4 33) 2 with value (4 64)
% 1.09/1.31 ; 31 with value (4 17) 22 with value (4 34) 2 with value (4 65)
% 1.09/1.31 ; 22 with value (4 18) 57 with value (4 35) 7 with value (4 68)
% 1.09/1.31 ; 12 with value (4 19) 31 with value (4 36) 1 with value (4 69)
% 1.09/1.31 ; 66 with value (4 20) 4 with value (4 37) 2 with value (4 70)
% 1.09/1.31 ; 10 with value (4 21) 10 with value (4 38)
% 1.09/1.31 Evaluation took:
% 1.09/1.31 0.838 seconds of real time
% 1.09/1.31 0.77853 seconds of user run time
% 1.09/1.31 0.0598 seconds of system run time
% 1.09/1.31 [Run times include 0.056 seconds GC run time.]
% 1.09/1.31 0 calls to %EVAL
% 1.09/1.31 0 page faults and
% 1.09/1.31 64,568,720 bytes consed.
% 1.09/1.31 :PROOF-FOUND
% 1.09/1.31 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T01:25:22
% 1.09/1.31 :PROOF-FOUND
% 1.09/1.31 *
%------------------------------------------------------------------------------