%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP386_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:37:48 AM UTC 2026
% Result : Theorem 9.84s 3.64s
% Output : Refutation 10.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 38
% Syntax : Number of formulae : 78 ( 34 unt; 0 typ; 0 def)
% Number of atoms : 175 ( 147 equ; 0 cnn)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 667 ( 22 ~; 0 |; 35 &; 548 @)
% ( 14 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Number of types : 92 ( 91 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 27 usr; 8 con; 0-2 aty)
% Number of variables : 204 ( 0 ^; 180 !; 24 ?; 204 :)
% Comments :
%------------------------------------------------------------------------------
thf('B_b_option_fun_b_b_option_fun_fun$_type',type,
'B_b_option_fun_b_b_option_fun_fun$': $tType ).
thf('B_b_option_fun_b_option_fun$_type',type,
'B_b_option_fun_b_option_fun$': $tType ).
thf('A_option_c_option_fun$_type',type,
'A_option_c_option_fun$': $tType ).
thf('A_a_option_fun_c_c_option_fun_fun$_type',type,
'A_a_option_fun_c_c_option_fun_fun$': $tType ).
thf('A_c_fun$_type',type,
'A_c_fun$': $tType ).
thf('C_c_option_fun$_type',type,
'C_c_option_fun$': $tType ).
thf('C_option$_type',type,
'C_option$': $tType ).
thf('C_c_option_fun_a_a_option_fun_fun$_type',type,
'C_c_option_fun_a_a_option_fun_fun$': $tType ).
thf('B_option$_type',type,
'B_option$': $tType ).
thf('B_option_c_option_bool_fun_fun$_type',type,
'B_option_c_option_bool_fun_fun$': $tType ).
thf('B_b_fun$_type',type,
'B_b_fun$': $tType ).
thf('B_c_c_option_fun_fun$_type',type,
'B_c_c_option_fun_fun$': $tType ).
thf('C_c_c_fun_fun$_type',type,
'C_c_c_fun_fun$': $tType ).
thf('C_c_fun$_type',type,
'C_c_fun$': $tType ).
thf('B_option_b_option_fun$_type',type,
'B_option_b_option_fun$': $tType ).
thf('B_c_option_fun$_type',type,
'B_c_option_fun$': $tType ).
thf('C_a_option_fun$_type',type,
'C_a_option_fun$': $tType ).
thf('C_option_set$_type',type,
'C_option_set$': $tType ).
thf('C_a_fun$_type',type,
'C_a_fun$': $tType ).
thf('C_option_c_option_bool_fun_fun$_type',type,
'C_option_c_option_bool_fun_fun$': $tType ).
thf('A_option_bool_fun$_type',type,
'A_option_bool_fun$': $tType ).
thf('B_option_b_fun$_type',type,
'B_option_b_fun$': $tType ).
thf('C_option_c_fun$_type',type,
'C_option_c_fun$': $tType ).
thf('C_option_a_option_bool_fun_fun$_type',type,
'C_option_a_option_bool_fun_fun$': $tType ).
thf('B_b_b_option_fun_fun$_type',type,
'B_b_b_option_fun_fun$': $tType ).
thf('C_b_option_fun$_type',type,
'C_b_option_fun$': $tType ).
thf('B$_type',type,
'B$': $tType ).
thf('C_c_option_fun_b_b_option_fun_fun$_type',type,
'C_c_option_fun_b_b_option_fun_fun$': $tType ).
thf('C_option_b_option_bool_fun_fun$_type',type,
'C_option_b_option_bool_fun_fun$': $tType ).
thf('A_a_option_fun_b_b_option_fun_fun$_type',type,
'A_a_option_fun_b_b_option_fun_fun$': $tType ).
thf('A_a_sum_a_fun$_type',type,
'A_a_sum_a_fun$': $tType ).
thf('C$_type',type,
'C$': $tType ).
thf('A_option_b_option_fun$_type',type,
'A_option_b_option_fun$': $tType ).
thf('B_option_c_option_fun$_type',type,
'B_option_c_option_fun$': $tType ).
thf('C_b_b_fun_fun$_type',type,
'C_b_b_fun_fun$': $tType ).
thf('C_c_c_option_fun_fun$_type',type,
'C_c_c_option_fun_fun$': $tType ).
thf('C_b_fun$_type',type,
'C_b_fun$': $tType ).
thf('B_b_sum_c_option_fun$_type',type,
'B_b_sum_c_option_fun$': $tType ).
thf('A_option$_type',type,
'A_option$': $tType ).
thf('A_a_option_fun_a_a_option_fun_fun$_type',type,
'A_a_option_fun_a_a_option_fun_fun$': $tType ).
thf('A_option_c_option_bool_fun_fun$_type',type,
'A_option_c_option_bool_fun_fun$': $tType ).
thf('B_a_fun$_type',type,
'B_a_fun$': $tType ).
thf('C_option_b_option_fun$_type',type,
'C_option_b_option_fun$': $tType ).
thf(tlbool_type,type,
tlbool: $tType ).
thf('A_option_a_fun$_type',type,
'A_option_a_fun$': $tType ).
thf('A_a_option_fun$_type',type,
'A_a_option_fun$': $tType ).
thf('A_option_a_option_fun$_type',type,
'A_option_a_option_fun$': $tType ).
thf('A_bool_fun$_type',type,
'A_bool_fun$': $tType ).
thf('C_option_a_option_fun$_type',type,
'C_option_a_option_fun$': $tType ).
thf('A_set$_type',type,
'A_set$': $tType ).
thf('B_b_option_fun_c_c_option_fun_fun$_type',type,
'B_b_option_fun_c_c_option_fun_fun$': $tType ).
thf('C_bool_fun$_type',type,
'C_bool_fun$': $tType ).
thf('A_b_fun$_type',type,
'A_b_fun$': $tType ).
thf('B_c_c_fun_fun$_type',type,
'B_c_c_fun_fun$': $tType ).
thf('B_set$_type',type,
'B_set$': $tType ).
thf('B_option_a_option_bool_fun_fun$_type',type,
'B_option_a_option_bool_fun_fun$': $tType ).
thf('Bool_c_option_fun$_type',type,
'Bool_c_option_fun$': $tType ).
thf('A$_type',type,
'A$': $tType ).
thf('B_option_option$_type',type,
'B_option_option$': $tType ).
thf('Bool_b_option_fun$_type',type,
'Bool_b_option_fun$': $tType ).
thf('A_b_b_option_fun_fun$_type',type,
'A_b_b_option_fun_fun$': $tType ).
thf('A_b_option_fun$_type',type,
'A_b_option_fun$': $tType ).
thf('C_c_sum_c_option_fun$_type',type,
'C_c_sum_c_option_fun$': $tType ).
thf('Bool_bool_fun$_type',type,
'Bool_bool_fun$': $tType ).
thf('B_a_option_fun$_type',type,
'B_a_option_fun$': $tType ).
thf('A_a_a_fun_fun$_type',type,
'A_a_a_fun_fun$': $tType ).
thf('B_b_option_fun_a_a_option_fun_fun$_type',type,
'B_b_option_fun_a_a_option_fun_fun$': $tType ).
thf('C_option_c_option_fun$_type',type,
'C_option_c_option_fun$': $tType ).
thf('A_a_fun$_type',type,
'A_a_fun$': $tType ).
thf('B_b_sum_b_option_fun$_type',type,
'B_b_sum_b_option_fun$': $tType ).
thf('B_b_b_fun_fun$_type',type,
'B_b_b_fun_fun$': $tType ).
thf('B_b_option_fun$_type',type,
'B_b_option_fun$': $tType ).
thf('C_option_option$_type',type,
'C_option_option$': $tType ).
thf('A_option_b_option_bool_fun_fun$_type',type,
'A_option_b_option_bool_fun_fun$': $tType ).
thf('C_c_sum_c_fun$_type',type,
'C_c_sum_c_fun$': $tType ).
thf('A_a_sum_b_option_fun$_type',type,
'A_a_sum_b_option_fun$': $tType ).
thf('A_a_option_fun_a_option_fun$_type',type,
'A_a_option_fun_a_option_fun$': $tType ).
thf('C_option_bool_fun$_type',type,
'C_option_bool_fun$': $tType ).
thf('A_option_a_option_bool_fun_fun$_type',type,
'A_option_a_option_bool_fun_fun$': $tType ).
thf('C_c_option_fun_c_option_fun$_type',type,
'C_c_option_fun_c_option_fun$': $tType ).
thf('A_b_b_fun_fun$_type',type,
'A_b_b_fun_fun$': $tType ).
thf('C_c_option_fun_c_c_option_fun_fun$_type',type,
'C_c_option_fun_c_c_option_fun_fun$': $tType ).
thf('B_option_bool_fun$_type',type,
'B_option_bool_fun$': $tType ).
thf('B_option_a_option_fun$_type',type,
'B_option_a_option_fun$': $tType ).
thf('B_c_fun$_type',type,
'B_c_fun$': $tType ).
thf('C_set$_type',type,
'C_set$': $tType ).
thf('B_option_b_option_bool_fun_fun$_type',type,
'B_option_b_option_bool_fun_fun$': $tType ).
thf('B_bool_fun$_type',type,
'B_bool_fun$': $tType ).
thf('A_c_option_fun$_type',type,
'A_c_option_fun$': $tType ).
thf('B_option_set$_type',type,
'B_option_set$': $tType ).
thf('B_b_sum_b_fun$_type',type,
'B_b_sum_b_fun$': $tType ).
thf('none$a_decl',type,
'none$a': 'B_option$' ).
thf('some$a_decl',type,
'some$a': 'C_c_option_fun$' ).
thf('bind$b_decl',type,
'bind$b': 'B_option$' > 'B_c_option_fun$' > 'C_option$' ).
thf('g$_decl',type,
'g$': 'B_b_option_fun_c_c_option_fun_fun$' ).
thf('none$_decl',type,
'none$': 'C_option$' ).
thf('map_option$d_decl',type,
'map_option$d': 'B_c_fun$' > 'B_option_c_option_fun$' ).
thf('fun_app$an_decl',type,
'fun_app$an': 'B_option_c_option_fun$' > 'B_option$' > 'C_option$' ).
thf('some$_decl',type,
'some$': 'B_b_option_fun$' ).
thf('uvg$_decl',type,
'uvg$': 'B_c_fun$' > 'B_c_option_fun$' ).
thf('thesis$_decl',type,
'thesis$': $o ).
thf('uwc$_decl',type,
'uwc$': 'C_c_option_fun$' ).
thf('preregister$b_decl',type,
'preregister$b': 'B_b_option_fun_c_c_option_fun_fun$' > $o ).
thf('fun_app$k_decl',type,
'fun_app$k': 'C_c_fun$' > 'C$' > 'C$' ).
thf('fun_app$n_decl',type,
'fun_app$n': 'B_c_option_fun$' > 'B$' > 'C_option$' ).
thf('fun_app$am_decl',type,
'fun_app$am': 'B_b_option_fun_c_c_option_fun_fun$' > 'B_b_option_fun$' > 'C_c_option_fun$' ).
thf('valid_getter_setter$_decl',type,
'valid_getter_setter$': 'C_b_fun$' > 'B_c_c_fun_fun$' > $o ).
thf('case_option$c_decl',type,
'case_option$c': 'C_option$' > 'B_c_option_fun$' > 'B_option_c_option_fun$' ).
thf('register_from_getter_setter$a_decl',type,
'register_from_getter_setter$a': 'C_b_fun$' > 'B_c_c_fun_fun$' > 'B_b_option_fun_c_c_option_fun_fun$' ).
thf('register$a_decl',type,
'register$a': 'B_b_option_fun_c_c_option_fun_fun$' > $o ).
thf('fun_app$y_decl',type,
'fun_app$y': 'B_c_c_fun_fun$' > 'B$' > 'C_c_fun$' ).
thf('fun_app$m_decl',type,
'fun_app$m': 'C_b_fun$' > 'C$' > 'B$' ).
thf('uuu$_decl',type,
'uuu$': 'B_c_c_option_fun_fun$' > 'C$' > 'B_c_option_fun$' ).
thf('uu$_decl',type,
'uu$': 'B_c_c_fun_fun$' > 'C$' > 'B_c_option_fun$' ).
thf('fun_app$w_decl',type,
'fun_app$w': 'B_c_c_option_fun_fun$' > 'B$' > 'C_c_option_fun$' ).
thf('fun_app$j_decl',type,
'fun_app$j': 'C_c_option_fun$' > 'C$' > 'C_option$' ).
thf('fun_app$g_decl',type,
'fun_app$g': 'B_b_option_fun$' > 'B$' > 'B_option$' ).
thf('fun_app$o_decl',type,
'fun_app$o': 'B_c_fun$' > 'B$' > 'C$' ).
thf(23,axiom,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'register$a' )
=> ( A @ 'preregister$b' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom313) ).
thf(170,plain,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'register$a' )
=> ( A @ 'preregister$b' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(5,axiom,
! [A: 'B$',B: 'B_c_option_fun$'] :
( ( B @ ( A @ ( 'some$' @ 'fun_app$g' ) @ 'bind$b' ) )
= ( A @ ( B @ 'fun_app$n' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom424) ).
thf(52,plain,
! [A: 'B$',B: 'B_c_option_fun$'] :
( ( B @ ( A @ ( 'some$' @ 'fun_app$g' ) @ 'bind$b' ) )
= ( A @ ( B @ 'fun_app$n' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(29,axiom,
! [A: 'C_option$',B: 'B_c_option_fun$',C: 'B$'] :
( ( C @ ( 'some$' @ 'fun_app$g' ) @ ( B @ ( A @ 'case_option$c' ) @ 'fun_app$an' ) )
= ( C @ ( B @ 'fun_app$n' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom102) ).
thf(189,plain,
! [A: 'C_option$',B: 'B_c_option_fun$',C: 'B$'] :
( ( C @ ( 'some$' @ 'fun_app$g' ) @ ( B @ ( A @ 'case_option$c' ) @ 'fun_app$an' ) )
= ( C @ ( B @ 'fun_app$n' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(34,axiom,
! [A: 'C_b_fun$',B: 'B_c_c_fun_fun$',C: 'B_b_option_fun$',D: 'C$'] :
( ( D @ ( C @ ( B @ ( A @ 'register_from_getter_setter$a' ) @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( D @ ( A @ 'fun_app$m' ) @ ( C @ 'fun_app$g' ) @ ( D @ ( B @ 'uu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom94) ).
thf(211,plain,
! [A: 'C_b_fun$',B: 'B_c_c_fun_fun$',C: 'B_b_option_fun$',D: 'C$'] :
( ( D @ ( C @ ( B @ ( A @ 'register_from_getter_setter$a' ) @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( D @ ( A @ 'fun_app$m' ) @ ( C @ 'fun_app$g' ) @ ( D @ ( B @ 'uu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(7,axiom,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( 'none$'
= ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) ) )
<=> ( B = 'none$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom223) ).
thf(60,plain,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( ( B = 'none$a' )
=> ( 'none$'
= ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) ) ) )
& ( ( 'none$'
= ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) ) )
=> ( B = 'none$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(27,axiom,
! [A: 'C$'] :
( 'none$'
!= ( A @ ( 'some$a' @ 'fun_app$j' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom111) ).
thf(182,plain,
! [A: 'C$'] :
( 'none$'
!= ( A @ ( 'some$a' @ 'fun_app$j' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(32,axiom,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( A @ 'uvg$' @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom194) ).
thf(203,plain,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( A @ 'uvg$' @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(20,axiom,
! [A: 'B_option$'] :
( ( A != 'none$a' )
<=> ? [B: 'B$'] :
( A
= ( B @ ( 'some$' @ 'fun_app$g' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom80) ).
thf(151,plain,
! [A: 'B_option$'] :
( ( ? [B: 'B$'] :
( A
= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( A != 'none$a' ) )
& ( ( A != 'none$a' )
=> ? [B: 'B$'] :
( A
= ( B @ ( 'some$' @ 'fun_app$g' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(14,axiom,
! [A: 'B_c_fun$'] :
( ( 'none$a' @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom278) ).
thf(116,plain,
! [A: 'B_c_fun$'] :
( ( 'none$a' @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(33,axiom,
! [A: 'C_option$',B: 'C$'] :
( ( A
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ( A != 'none$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom114) ).
thf(206,plain,
! [A: 'C_option$',B: 'C$'] :
( ( A
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ( A != 'none$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(30,axiom,
! [A: 'C_option$'] :
( ! [B: 'C$'] :
( A
!= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
<=> ( A = 'none$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom82) ).
thf(192,plain,
! [A: 'C_option$'] :
( ( ( A = 'none$' )
=> ! [B: 'C$'] :
( A
!= ( B @ ( 'some$a' @ 'fun_app$j' ) ) ) )
& ( ! [B: 'C$'] :
( A
!= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ( A = 'none$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(17,axiom,
! [A: 'B_c_c_fun_fun$',B: 'C$',C: 'B$'] :
( ( C @ ( B @ ( A @ 'uu$' ) @ 'fun_app$n' ) )
= ( B @ ( C @ ( A @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom49) ).
thf(137,plain,
! [A: 'B_c_c_fun_fun$',B: 'C$',C: 'B$'] :
( ( C @ ( B @ ( A @ 'uu$' ) @ 'fun_app$n' ) )
= ( B @ ( C @ ( A @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(16,axiom,
! [A: 'B_option$'] :
( ! [B: 'B$'] :
( A
!= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
<=> ( A = 'none$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom83) ).
thf(129,plain,
! [A: 'B_option$'] :
( ( ( A = 'none$a' )
=> ! [B: 'B$'] :
( A
!= ( B @ ( 'some$' @ 'fun_app$g' ) ) ) )
& ( ! [B: 'B$'] :
( A
!= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( A = 'none$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(3,axiom,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_option_fun$',D: 'B_c_option_fun$'] :
( ( ! [E: 'B$'] :
( ( B
= ( E @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( ( E @ ( C @ 'fun_app$n' ) )
= ( E @ ( D @ 'fun_app$n' ) ) ) )
& ( A = B ) )
=> ( ( C @ ( A @ 'bind$b' ) )
= ( D @ ( B @ 'bind$b' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom420) ).
thf(41,plain,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_option_fun$',D: 'B_c_option_fun$'] :
( ( ! [E: 'B$'] :
( ( B
= ( E @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( ( E @ ( C @ 'fun_app$n' ) )
= ( E @ ( D @ 'fun_app$n' ) ) ) )
& ( A = B ) )
=> ( ( C @ ( A @ 'bind$b' ) )
= ( D @ ( B @ 'bind$b' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(9,axiom,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' )
<=> ( B = 'none$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom205) ).
thf(73,plain,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( ( B = 'none$a' )
=> ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' ) )
& ( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' )
=> ( B = 'none$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(38,axiom,
! [A: 'C_option$'] :
( ( A != 'none$' )
<=> ? [B: 'C$'] :
( A
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom79) ).
thf(237,plain,
! [A: 'C_option$'] :
( ( ? [B: 'C$'] :
( A
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ( A != 'none$' ) )
& ( ( A != 'none$' )
=> ? [B: 'C$'] :
( A
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(4,axiom,
! [A: 'B_c_option_fun$'] :
( ( A @ ( 'none$a' @ 'bind$b' ) )
= 'none$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom406) ).
thf(49,plain,
! [A: 'B_c_option_fun$'] :
( ( A @ ( 'none$a' @ 'bind$b' ) )
= 'none$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(21,axiom,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_fun$',D: 'B_c_fun$'] :
( ( ! [E: 'B$'] :
( ( B
= ( E @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( ( E @ ( C @ 'fun_app$o' ) )
= ( E @ ( D @ 'fun_app$o' ) ) ) )
& ( A = B ) )
=> ( ( A @ ( C @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( D @ 'map_option$d' @ 'fun_app$an' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom290) ).
thf(159,plain,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_fun$',D: 'B_c_fun$'] :
( ( ! [E: 'B$'] :
( ( B
= ( E @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( ( E @ ( C @ 'fun_app$o' ) )
= ( E @ ( D @ 'fun_app$o' ) ) ) )
& ( A = B ) )
=> ( ( A @ ( C @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( D @ 'map_option$d' @ 'fun_app$an' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(24,axiom,
! [A: 'B_c_fun$',B: 'B$'] :
( ( B @ ( A @ 'uvg$' @ 'fun_app$n' ) )
= ( B @ ( A @ 'fun_app$o' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom15) ).
thf(172,plain,
! [A: 'B_c_fun$',B: 'B$'] :
( ( B @ ( A @ 'uvg$' @ 'fun_app$n' ) )
= ( B @ ( A @ 'fun_app$o' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(10,axiom,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'register$a' )
<=> ? [B: 'C_b_fun$',C: 'B_c_c_fun_fun$'] :
( ( C @ ( B @ 'valid_getter_setter$' ) )
& ( A
= ( C @ ( B @ 'register_from_getter_setter$a' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom136) ).
thf(81,plain,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( ? [B: 'C_b_fun$',C: 'B_c_c_fun_fun$'] :
( ( C @ ( B @ 'valid_getter_setter$' ) )
& ( A
= ( C @ ( B @ 'register_from_getter_setter$a' ) ) ) )
=> ( A @ 'register$a' ) )
& ( ( A @ 'register$a' )
=> ? [B: 'C_b_fun$',C: 'B_c_c_fun_fun$'] :
( ( C @ ( B @ 'valid_getter_setter$' ) )
& ( A
= ( C @ ( B @ 'register_from_getter_setter$a' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(39,axiom,
! [A: 'B_c_c_fun_fun$',B: 'C_b_fun$'] :
( ( ( A @ ( B @ 'valid_getter_setter$' ) )
& ! [C: 'B_b_option_fun$',D: 'C$'] :
( ( D @ ( C @ ( 'g$' @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( D @ ( B @ 'fun_app$m' ) @ ( C @ 'fun_app$g' ) @ ( D @ ( A @ 'uu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ) )
=> 'thesis$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hypothesis73) ).
thf(245,plain,
! [A: 'B_c_c_fun_fun$',B: 'C_b_fun$'] :
( ( ( A @ ( B @ 'valid_getter_setter$' ) )
& ! [C: 'B_b_option_fun$',D: 'C$'] :
( ( D @ ( C @ ( 'g$' @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( D @ ( B @ 'fun_app$m' ) @ ( C @ 'fun_app$g' ) @ ( D @ ( A @ 'uu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ) )
=> 'thesis$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(18,axiom,
! [A: 'B_c_fun$',B: 'B$'] :
( ( B @ ( 'some$' @ 'fun_app$g' ) @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( A @ 'fun_app$o' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom287) ).
thf(140,plain,
! [A: 'B_c_fun$',B: 'B$'] :
( ( B @ ( 'some$' @ 'fun_app$g' ) @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( B @ ( A @ 'fun_app$o' ) @ ( 'some$a' @ 'fun_app$j' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(13,axiom,
! [A: 'B$',B: 'B$'] :
( ( ( A @ ( 'some$' @ 'fun_app$g' ) )
= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom97) ).
thf(108,plain,
! [A: 'B$',B: 'B$'] :
( ( ( A = B )
=> ( ( A @ ( 'some$' @ 'fun_app$g' ) )
= ( B @ ( 'some$' @ 'fun_app$g' ) ) ) )
& ( ( ( A @ ( 'some$' @ 'fun_app$g' ) )
= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(37,axiom,
! [A: 'C_b_fun$',B: 'B_c_c_fun_fun$'] :
( ( B @ ( A @ 'valid_getter_setter$' ) )
<=> ( ! [C: 'B$',D: 'B$',E: 'C$'] :
( ( E @ ( D @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) )
= ( E @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) )
& ! [C: 'B$',D: 'C$'] :
( ( D @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( A @ 'fun_app$m' ) )
= C )
& ! [C: 'C$'] :
( C
= ( C @ ( C @ ( A @ 'fun_app$m' ) @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom76) ).
thf(223,plain,
! [A: 'C_b_fun$',B: 'B_c_c_fun_fun$'] :
( ( ( ! [C: 'B$',D: 'B$',E: 'C$'] :
( ( E @ ( D @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) )
= ( E @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) )
& ! [C: 'B$',D: 'C$'] :
( ( D @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( A @ 'fun_app$m' ) )
= C )
& ! [C: 'C$'] :
( C
= ( C @ ( C @ ( A @ 'fun_app$m' ) @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) ) )
=> ( B @ ( A @ 'valid_getter_setter$' ) ) )
& ( ( B @ ( A @ 'valid_getter_setter$' ) )
=> ( ! [C: 'B$',D: 'B$',E: 'C$'] :
( ( E @ ( D @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) )
= ( E @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) )
& ! [C: 'B$',D: 'C$'] :
( ( D @ ( C @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) @ ( A @ 'fun_app$m' ) )
= C )
& ! [C: 'C$'] :
( C
= ( C @ ( C @ ( A @ 'fun_app$m' ) @ ( B @ 'fun_app$y' ) @ 'fun_app$k' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(22,axiom,
! [A: 'B_c_c_option_fun_fun$',B: 'C$',C: 'B$'] :
( ( C @ ( B @ ( A @ 'uuu$' ) @ 'fun_app$n' ) )
= ( B @ ( C @ ( A @ 'fun_app$w' ) @ 'fun_app$j' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom23) ).
thf(167,plain,
! [A: 'B_c_c_option_fun_fun$',B: 'C$',C: 'B$'] :
( ( C @ ( B @ ( A @ 'uuu$' ) @ 'fun_app$n' ) )
= ( B @ ( C @ ( A @ 'fun_app$w' ) @ 'fun_app$j' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(25,axiom,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'register$a' )
=> ( ( 'some$' @ ( A @ 'fun_app$am' ) )
= 'some$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom92) ).
thf(175,plain,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'register$a' )
=> ( ( 'some$' @ ( A @ 'fun_app$am' ) )
= 'some$a' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(19,axiom,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' )
<=> ( B = 'none$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom214) ).
thf(143,plain,
! [A: 'B_c_fun$',B: 'B_option$'] :
( ( ( B = 'none$a' )
=> ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' ) )
& ( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= 'none$' )
=> ( B = 'none$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(1,conjecture,
'thesis$',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture72) ).
thf(2,negated_conjecture,
~ 'thesis$',
inference(neg_conjecture,[status(cth)],[1]) ).
thf(40,plain,
~ 'thesis$',
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(28,axiom,
! [A: 'C$'] :
( ( A @ ( 'uwc$' @ 'fun_app$j' ) )
= 'none$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom60) ).
thf(186,plain,
! [A: 'C$'] :
( ( A @ ( 'uwc$' @ 'fun_app$j' ) )
= 'none$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(6,axiom,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_option_fun$'] :
( ( A = B )
=> ( ( C @ ( A @ 'bind$b' ) )
= ( C @ ( B @ 'bind$b' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom387) ).
thf(55,plain,
! [A: 'B_option$',B: 'B_option$',C: 'B_c_option_fun$'] :
( ( A = B )
=> ( ( C @ ( A @ 'bind$b' ) )
= ( C @ ( B @ 'bind$b' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(15,axiom,
! [A: 'B_c_fun$',B: 'B_option$',C: 'C$'] :
( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
<=> ? [D: 'B$'] :
( ( ( D @ ( A @ 'fun_app$o' ) )
= C )
& ( B
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom232) ).
thf(119,plain,
! [A: 'B_c_fun$',B: 'B_option$',C: 'C$'] :
( ( ? [D: 'B$'] :
( ( ( D @ ( A @ 'fun_app$o' ) )
= C )
& ( B
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) )
=> ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) ) )
& ( ( ( B @ ( A @ 'map_option$d' @ 'fun_app$an' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ? [D: 'B$'] :
( ( ( D @ ( A @ 'fun_app$o' ) )
= C )
& ( B
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(35,axiom,
'g$' @ 'register$a',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom75) ).
thf(214,plain,
'g$' @ 'register$a',
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(31,axiom,
! [A: 'C_option$',B: 'B_c_option_fun$'] :
( ( 'none$a' @ ( B @ ( A @ 'case_option$c' ) @ 'fun_app$an' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom108) ).
thf(200,plain,
! [A: 'C_option$',B: 'B_c_option_fun$'] :
( ( 'none$a' @ ( B @ ( A @ 'case_option$c' ) @ 'fun_app$an' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(8,axiom,
! [A: 'B_option$',B: 'B$'] :
( ( A
= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( A != 'none$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom115) ).
thf(68,plain,
! [A: 'B_option$',B: 'B$'] :
( ( A
= ( B @ ( 'some$' @ 'fun_app$g' ) ) )
=> ( A != 'none$a' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(26,axiom,
! [A: 'B$'] :
( 'none$a'
!= ( A @ ( 'some$' @ 'fun_app$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom112) ).
thf(178,plain,
! [A: 'B$'] :
( 'none$a'
!= ( A @ ( 'some$' @ 'fun_app$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(11,axiom,
! [A: 'B_option$',B: 'B_c_option_fun$',C: 'C$'] :
( ( ( B @ ( A @ 'bind$b' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
<=> ? [D: 'B$'] :
( ( ( D @ ( B @ 'fun_app$n' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
& ( A
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom414) ).
thf(90,plain,
! [A: 'B_option$',B: 'B_c_option_fun$',C: 'C$'] :
( ( ? [D: 'B$'] :
( ( ( D @ ( B @ 'fun_app$n' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
& ( A
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) )
=> ( ( B @ ( A @ 'bind$b' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) ) )
& ( ( ( B @ ( A @ 'bind$b' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ? [D: 'B$'] :
( ( ( D @ ( B @ 'fun_app$n' ) )
= ( C @ ( 'some$a' @ 'fun_app$j' ) ) )
& ( A
= ( D @ ( 'some$' @ 'fun_app$g' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(36,axiom,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( A @ 'preregister$b' )
<=> ? [B: 'C_b_fun$',C: 'B_c_c_option_fun_fun$'] :
! [D: 'B_b_option_fun$',E: 'C$'] :
( ( E @ ( D @ ( A @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( E @ ( B @ 'fun_app$m' ) @ ( D @ 'fun_app$g' ) @ ( E @ ( C @ 'uuu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom173) ).
thf(215,plain,
! [A: 'B_b_option_fun_c_c_option_fun_fun$'] :
( ( ? [B: 'C_b_fun$',C: 'B_c_c_option_fun_fun$'] :
! [D: 'B_b_option_fun$',E: 'C$'] :
( ( E @ ( D @ ( A @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( E @ ( B @ 'fun_app$m' ) @ ( D @ 'fun_app$g' ) @ ( E @ ( C @ 'uuu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) )
=> ( A @ 'preregister$b' ) )
& ( ( A @ 'preregister$b' )
=> ? [B: 'C_b_fun$',C: 'B_c_c_option_fun_fun$'] :
! [D: 'B_b_option_fun$',E: 'C$'] :
( ( E @ ( D @ ( A @ 'fun_app$am' ) @ 'fun_app$j' ) )
= ( E @ ( B @ 'fun_app$m' ) @ ( D @ 'fun_app$g' ) @ ( E @ ( C @ 'uuu$' ) @ ( 'none$' @ 'case_option$c' ) @ 'fun_app$an' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(12,axiom,
! [A: 'C$',B: 'C$'] :
( ( ( A @ ( 'some$a' @ 'fun_app$j' ) )
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom96) ).
thf(100,plain,
! [A: 'C$',B: 'C$'] :
( ( ( A = B )
=> ( ( A @ ( 'some$a' @ 'fun_app$j' ) )
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) ) )
& ( ( ( A @ ( 'some$a' @ 'fun_app$j' ) )
= ( B @ ( 'some$a' @ 'fun_app$j' ) ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(249,plain,
$false,
inference(e,[status(thm)],[170,52,189,211,60,182,203,151,116,206,192,137,129,41,73,237,49,159,172,81,245,140,108,223,167,175,143,40,186,55,119,214,200,68,178,90,215,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP386_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.40 % Computer : n006.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Fri Sep 25 19:09:25 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.86/0.99 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 3.26/1.66 % [INFO] Parsing done (665ms).
% 3.26/1.67 % [INFO] Running in sequential loop mode.
% 4.39/2.07 % [INFO] eprover registered as external prover.
% 4.39/2.07 % [INFO] Scanning for conjecture ...
% 5.00/2.35 % [INFO] Found a conjecture (or negated_conjecture) and 734 axioms. Running axiom selection ...
% 5.77/2.50 % [INFO] Axiom selection finished. Selected 37 axioms (removed 697 axioms).
% 5.77/2.59 % [INFO] Problem is typed first-order (TPTP TFF).
% 6.22/2.60 % [INFO] Type checking passed.
% 6.22/2.60 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 9.84/3.64 % External prover 'e' found a proof!
% 9.84/3.64 % [INFO] Killing All external provers ...
% 9.84/3.64 % Time passed: 3092ms (effective reasoning time: 1957ms)
% 9.84/3.64 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 9.84/3.64 % Axioms used in derivation (37): axiom76, axiom214, axiom173, axiom112, axiom82, axiom232, axiom111, axiom223, hypothesis73, axiom49, axiom92, axiom424, axiom406, axiom115, axiom278, axiom94, axiom83, axiom60, axiom290, axiom108, axiom387, axiom75, axiom80, axiom97, axiom205, axiom79, axiom96, axiom23, axiom313, axiom102, axiom15, axiom114, axiom287, axiom136, axiom414, axiom420, axiom194
% 9.84/3.64 % No. of inferences in proof: 78
% 9.84/3.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3092 ms resp. 1957 ms w/o parsing
% 10.38/3.72 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 10.38/3.72 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------