%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP055^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Wed Oct 7 10:23:52 AM UTC 2026
% Result : Theorem 2.42s 0.63s
% Output : CNFRefutation 2.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 6
% Syntax : Number of formulae : 41 ( 28 unt; 0 typ; 0 def)
% Number of atoms : 172 ( 49 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 274 ( 21 ~; 29 |; 0 &; 212 @)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Number of types : 15 ( 14 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 61 ( 58 usr; 16 con; 0-4 aty)
% Number of variables : 60 ( 0 ^; 60 !; 0 ?; 60 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_config256849571t_unit,type,
config256849571t_unit: $tType ).
thf(tp_int,type,
int: $tType ).
thf(tp_list_c1059388851t_unit,type,
list_c1059388851t_unit: $tType ).
thf(tp_list_l1341496881ge_p_v,type,
list_l1341496881ge_p_v: $tType ).
thf(tp_list_l1584713811t_unit,type,
list_l1584713811t_unit: $tType ).
thf(tp_list_l1619404459ge_p_v,type,
list_l1619404459ge_p_v: $tType ).
thf(tp_list_l611321411t_unit,type,
list_l611321411t_unit: $tType ).
thf(tp_list_message_p_v,type,
list_message_p_v: $tType ).
thf(tp_messageValue_v,type,
messageValue_v: $tType ).
thf(tp_message_p_v,type,
message_p_v: $tType ).
thf(tp_nat,type,
nat: $tType ).
thf(tp_p,type,
p: $tType ).
thf(tp_s,type,
s: $tType ).
thf(tp_set_nat,type,
set_nat: $tType ).
thf(tp_cfg,type,
cfg: config256849571t_unit ).
thf(tp_collect_nat,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(tp_cons_c1162654829t_unit,type,
cons_c1162654829t_unit: config256849571t_unit > list_c1059388851t_unit > list_c1059388851t_unit ).
thf(tp_cons_l1083444861t_unit,type,
cons_l1083444861t_unit: list_c1059388851t_unit > list_l611321411t_unit > list_l611321411t_unit ).
thf(tp_cons_l1383421281ge_p_v,type,
cons_l1383421281ge_p_v: list_l1619404459ge_p_v > list_l1341496881ge_p_v > list_l1341496881ge_p_v ).
thf(tp_cons_l1777019405t_unit,type,
cons_l1777019405t_unit: list_l611321411t_unit > list_l1584713811t_unit > list_l1584713811t_unit ).
thf(tp_cons_l233104475ge_p_v,type,
cons_l233104475ge_p_v: list_message_p_v > list_l1619404459ge_p_v > list_l1619404459ge_p_v ).
thf(tp_cons_message_p_v,type,
cons_message_p_v: message_p_v > list_message_p_v > list_message_p_v ).
thf(tp_fLPThe1519354920_p_v_s,type,
fLPThe1519354920_p_v_s: config256849571t_unit > ( list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit ) > ( list_c1059388851t_unit > list_message_p_v > list_message_p_v ) > nat > list_c1059388851t_unit ).
thf(tp_fLPThe536531371_p_v_s,type,
fLPThe536531371_p_v_s: config256849571t_unit > ( list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit ) > ( list_c1059388851t_unit > list_message_p_v > list_message_p_v ) > nat > list_message_p_v ).
thf(tp_fLPThe9398366_p_s_v,type,
fLPThe9398366_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > ( p > s ) > $o ).
thf(tp_fe,type,
fe: nat > list_c1059388851t_unit ).
thf(tp_gen_le193291088t_unit,type,
gen_le193291088t_unit: nat > list_c1059388851t_unit > nat ).
thf(tp_gen_le697204914ge_p_v,type,
gen_le697204914ge_p_v: nat > list_message_p_v > nat ).
thf(tp_insert1308755079t_unit,type,
insert1308755079t_unit: config256849571t_unit > list_c1059388851t_unit > list_c1059388851t_unit ).
thf(tp_insert_message_p_v,type,
insert_message_p_v: message_p_v > list_message_p_v > list_message_p_v ).
thf(tp_list_e1598815642t_unit,type,
list_e1598815642t_unit: ( config256849571t_unit > $o ) > list_c1059388851t_unit > $o ).
thf(tp_list_ex1_message_p_v,type,
list_ex1_message_p_v: ( message_p_v > $o ) > list_message_p_v > $o ).
thf(tp_m,type,
m: nat ).
thf(tp_member_nat,type,
member_nat: nat > set_nat > $o ).
thf(tp_n,type,
n: nat ).
thf(tp_n_list1987762709t_unit,type,
n_list1987762709t_unit: nat > list_c1059388851t_unit > list_l611321411t_unit ).
thf(tp_n_lists_message_p_v,type,
n_lists_message_p_v: nat > list_message_p_v > list_l1619404459ge_p_v ).
thf(tp_na,type,
na: nat ).
thf(tp_nat2,type,
nat2: int > nat ).
thf(tp_nil_co1338500125t_unit,type,
nil_co1338500125t_unit: list_c1059388851t_unit ).
thf(tp_nil_li2108369341t_unit,type,
nil_li2108369341t_unit: list_l1584713811t_unit ).
thf(tp_nil_li307996205t_unit,type,
nil_li307996205t_unit: list_l611321411t_unit ).
thf(tp_nil_li835338673ge_p_v,type,
nil_li835338673ge_p_v: list_l1341496881ge_p_v ).
thf(tp_nil_list_message_p_v,type,
nil_list_message_p_v: list_l1619404459ge_p_v ).
thf(tp_nil_message_p_v,type,
nil_message_p_v: list_message_p_v ).
thf(tp_nths_c890550943t_unit,type,
nths_c890550943t_unit: list_c1059388851t_unit > set_nat > list_c1059388851t_unit ).
thf(tp_nths_message_p_v,type,
nths_message_p_v: list_message_p_v > set_nat > list_message_p_v ).
thf(tp_one_one_int,type,
one_one_int: int ).
thf(tp_one_one_nat,type,
one_one_nat: nat ).
thf(tp_ord_less_eq_int,type,
ord_less_eq_int: int > int > $o ).
thf(tp_ord_less_eq_nat,type,
ord_less_eq_nat: nat > nat > $o ).
thf(tp_ord_less_int,type,
ord_less_int: int > int > $o ).
thf(tp_ord_less_nat,type,
ord_less_nat: nat > nat > $o ).
thf(tp_prefix1465223476ge_p_v,type,
prefix1465223476ge_p_v: list_l1619404459ge_p_v > list_l1619404459ge_p_v > $o ).
thf(tp_prefix1615116500t_unit,type,
prefix1615116500t_unit: list_c1059388851t_unit > list_c1059388851t_unit > $o ).
thf(tp_prefix47729710ge_p_v,type,
prefix47729710ge_p_v: list_message_p_v > list_message_p_v > $o ).
thf(tp_prefix747844452t_unit,type,
prefix747844452t_unit: list_l611321411t_unit > list_l611321411t_unit > $o ).
thf(tp_produc1505827982ge_p_v,type,
produc1505827982ge_p_v: list_l1619404459ge_p_v > list_l1619404459ge_p_v ).
thf(tp_produc663212148t_unit,type,
produc663212148t_unit: list_l611321411t_unit > list_l611321411t_unit ).
thf(tp_ring_1_of_int_int,type,
ring_1_of_int_int: int > int ).
thf(tp_semiri1382578993at_nat,type,
semiri1382578993at_nat: nat > nat ).
thf(tp_semiri2019852685at_int,type,
semiri2019852685at_int: nat > int ).
thf(tp_size_s1168481041ge_p_v,type,
size_s1168481041ge_p_v: list_message_p_v > nat ).
thf(tp_size_s1406904903t_unit,type,
size_s1406904903t_unit: list_c1059388851t_unit > nat ).
thf(tp_size_s1809856791ge_p_v,type,
size_s1809856791ge_p_v: list_l1619404459ge_p_v > nat ).
thf(tp_size_s503142615t_unit,type,
size_s503142615t_unit: list_l611321411t_unit > nat ).
thf(tp_subseq1144048270t_unit,type,
subseq1144048270t_unit: list_c1059388851t_unit > list_l611321411t_unit ).
thf(tp_subseqs_message_p_v,type,
subseqs_message_p_v: list_message_p_v > list_l1619404459ge_p_v ).
thf(tp_suc,type,
suc: nat > nat ).
thf(tp_uminus_uminus_int,type,
uminus_uminus_int: int > int ).
thf(tp_zero_zero_int,type,
zero_zero_int: int ).
thf(tp_zero_zero_nat,type,
zero_zero_nat: nat ).
thf(330,axiom,
! [Xa: list_c1059388851t_unit,Xb: list_c1059388851t_unit,X: config256849571t_unit] :
( ( prefix1615116500t_unit @ Xa @ Xb )
=> ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ X @ Xa ) @ ( cons_c1162654829t_unit @ X @ Xb ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_prefixList_Ointros_I2_J) ).
thf(335,axiom,
! [L1: list_c1059388851t_unit,L2: list_c1059388851t_unit,L3: list_c1059388851t_unit] :
( ( prefix1615116500t_unit @ L1 @ L2 )
=> ( ( prefix1615116500t_unit @ L2 @ L3 )
=> ( prefix1615116500t_unit @ L1 @ L3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_PrefixListTransitive) ).
thf(338,axiom,
( ( m = na )
| ( ord_less_nat @ m @ na ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__092_060open_062m_A_061_An_A_092_060or_062_Am_A_060_An_092_060close_062) ).
thf(339,axiom,
( ( ord_less_nat @ m @ na )
=> ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_IA_I1_J) ).
thf(341,axiom,
ord_less_nat @ m @ na,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062m_A_060_An_092_060close_062) ).
thf(342,conjecture,
prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(343,negated_conjecture,
( ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) )
= $false ),
inference(negate_conjecture,[status(cth)],[342]) ).
thf(344,plain,
( ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) )
= $false ),
inference(unfold_def,[status(thm)],[343]) ).
thf(345,plain,
( ( ! [Xa: list_c1059388851t_unit,Xb: list_c1059388851t_unit,X: config256849571t_unit] :
( ( prefix1615116500t_unit @ Xa @ Xb )
=> ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ X @ Xa ) @ ( cons_c1162654829t_unit @ X @ Xb ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[330]) ).
thf(346,plain,
( ( ! [L1: list_c1059388851t_unit,L2: list_c1059388851t_unit,L3: list_c1059388851t_unit] :
( ( prefix1615116500t_unit @ L1 @ L2 )
=> ( ( prefix1615116500t_unit @ L2 @ L3 )
=> ( prefix1615116500t_unit @ L1 @ L3 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[335]) ).
thf(347,plain,
( ( ( m = na )
| ( ord_less_nat @ m @ na ) )
= $true ),
inference(unfold_def,[status(thm)],[338]) ).
thf(348,plain,
( ( ( ord_less_nat @ m @ na )
=> ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) )
= $true ),
inference(unfold_def,[status(thm)],[339]) ).
thf(349,plain,
( ( ord_less_nat @ m @ na )
= $true ),
inference(unfold_def,[status(thm)],[341]) ).
thf(350,plain,
( ( ~ ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[344]) ).
thf(351,plain,
( ( ord_less_nat @ m @ na )
= $true ),
inference(copy,[status(thm)],[349]) ).
thf(352,plain,
( ( ( ord_less_nat @ m @ na )
=> ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) )
= $true ),
inference(copy,[status(thm)],[348]) ).
thf(353,plain,
( ( ( m = na )
| ( ord_less_nat @ m @ na ) )
= $true ),
inference(copy,[status(thm)],[347]) ).
thf(354,plain,
( ( ! [L1: list_c1059388851t_unit,L2: list_c1059388851t_unit,L3: list_c1059388851t_unit] :
( ( prefix1615116500t_unit @ L1 @ L2 )
=> ( ( prefix1615116500t_unit @ L2 @ L3 )
=> ( prefix1615116500t_unit @ L1 @ L3 ) ) ) )
= $true ),
inference(copy,[status(thm)],[346]) ).
thf(355,plain,
( ( ! [Xa: list_c1059388851t_unit,Xb: list_c1059388851t_unit,X: config256849571t_unit] :
( ( prefix1615116500t_unit @ Xa @ Xb )
=> ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ X @ Xa ) @ ( cons_c1162654829t_unit @ X @ Xb ) ) ) )
= $true ),
inference(copy,[status(thm)],[345]) ).
thf(356,plain,
( ( ~ ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) )
= $true ),
inference(copy,[status(thm)],[350]) ).
thf(357,plain,
( ( ~ ( ord_less_nat @ m @ na )
| ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) ) )
= $true ),
inference(unfold_def,[status(thm)],[352]) ).
thf(358,plain,
( ( ! [SX0: list_c1059388851t_unit,SX1: list_c1059388851t_unit,SX2: config256849571t_unit] :
( ~ ( prefix1615116500t_unit @ SX0 @ SX1 )
| ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SX2 @ SX0 ) @ ( cons_c1162654829t_unit @ SX2 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[355]) ).
thf(359,plain,
( ( ! [SX0: list_c1059388851t_unit,SX1: list_c1059388851t_unit,SX2: list_c1059388851t_unit] :
( ~ ( prefix1615116500t_unit @ SX0 @ SX1 )
| ~ ( prefix1615116500t_unit @ SX1 @ SX2 )
| ( prefix1615116500t_unit @ SX0 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(360,plain,
( ( ( m = na )
= $true )
| ( ( ord_less_nat @ m @ na )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[353]) ).
thf(361,plain,
( ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[356]) ).
thf(362,plain,
( ( ( ~ ( ord_less_nat @ m @ na ) )
= $true )
| ( ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[357]) ).
thf(363,plain,
! [SV1: list_c1059388851t_unit] :
( ( ! [SY6: list_c1059388851t_unit,SY7: config256849571t_unit] :
( ~ ( prefix1615116500t_unit @ SV1 @ SY6 )
| ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SY7 @ SV1 ) @ ( cons_c1162654829t_unit @ SY7 @ SY6 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[358]) ).
thf(364,plain,
! [SV2: list_c1059388851t_unit] :
( ( ! [SY8: list_c1059388851t_unit,SY9: list_c1059388851t_unit] :
( ~ ( prefix1615116500t_unit @ SV2 @ SY8 )
| ~ ( prefix1615116500t_unit @ SY8 @ SY9 )
| ( prefix1615116500t_unit @ SV2 @ SY9 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[359]) ).
thf(365,plain,
( ( ( ord_less_nat @ m @ na )
= $false )
| ( ( prefix1615116500t_unit @ ( fe @ m ) @ ( fe @ na ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[362]) ).
thf(366,plain,
! [SV3: list_c1059388851t_unit,SV1: list_c1059388851t_unit] :
( ( ! [SY10: config256849571t_unit] :
( ~ ( prefix1615116500t_unit @ SV1 @ SV3 )
| ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SY10 @ SV1 ) @ ( cons_c1162654829t_unit @ SY10 @ SV3 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[363]) ).
thf(367,plain,
! [SV4: list_c1059388851t_unit,SV2: list_c1059388851t_unit] :
( ( ! [SY11: list_c1059388851t_unit] :
( ~ ( prefix1615116500t_unit @ SV2 @ SV4 )
| ~ ( prefix1615116500t_unit @ SV4 @ SY11 )
| ( prefix1615116500t_unit @ SV2 @ SY11 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[364]) ).
thf(368,plain,
! [SV5: config256849571t_unit,SV3: list_c1059388851t_unit,SV1: list_c1059388851t_unit] :
( ( ~ ( prefix1615116500t_unit @ SV1 @ SV3 )
| ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SV5 @ SV1 ) @ ( cons_c1162654829t_unit @ SV5 @ SV3 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[366]) ).
thf(369,plain,
! [SV6: list_c1059388851t_unit,SV4: list_c1059388851t_unit,SV2: list_c1059388851t_unit] :
( ( ~ ( prefix1615116500t_unit @ SV2 @ SV4 )
| ~ ( prefix1615116500t_unit @ SV4 @ SV6 )
| ( prefix1615116500t_unit @ SV2 @ SV6 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[367]) ).
thf(370,plain,
! [SV5: config256849571t_unit,SV3: list_c1059388851t_unit,SV1: list_c1059388851t_unit] :
( ( ( ~ ( prefix1615116500t_unit @ SV1 @ SV3 ) )
= $true )
| ( ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SV5 @ SV1 ) @ ( cons_c1162654829t_unit @ SV5 @ SV3 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[368]) ).
thf(371,plain,
! [SV6: list_c1059388851t_unit,SV4: list_c1059388851t_unit,SV2: list_c1059388851t_unit] :
( ( ( ~ ( prefix1615116500t_unit @ SV2 @ SV4 ) )
= $true )
| ( ( ~ ( prefix1615116500t_unit @ SV4 @ SV6 )
| ( prefix1615116500t_unit @ SV2 @ SV6 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[369]) ).
thf(372,plain,
! [SV5: config256849571t_unit,SV3: list_c1059388851t_unit,SV1: list_c1059388851t_unit] :
( ( ( prefix1615116500t_unit @ SV1 @ SV3 )
= $false )
| ( ( prefix1615116500t_unit @ ( cons_c1162654829t_unit @ SV5 @ SV1 ) @ ( cons_c1162654829t_unit @ SV5 @ SV3 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[370]) ).
thf(373,plain,
! [SV6: list_c1059388851t_unit,SV4: list_c1059388851t_unit,SV2: list_c1059388851t_unit] :
( ( ( prefix1615116500t_unit @ SV2 @ SV4 )
= $false )
| ( ( ~ ( prefix1615116500t_unit @ SV4 @ SV6 )
| ( prefix1615116500t_unit @ SV2 @ SV6 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[371]) ).
thf(374,plain,
! [SV2: list_c1059388851t_unit,SV6: list_c1059388851t_unit,SV4: list_c1059388851t_unit] :
( ( ( ~ ( prefix1615116500t_unit @ SV4 @ SV6 ) )
= $true )
| ( ( prefix1615116500t_unit @ SV2 @ SV6 )
= $true )
| ( ( prefix1615116500t_unit @ SV2 @ SV4 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[373]) ).
thf(375,plain,
! [SV2: list_c1059388851t_unit,SV6: list_c1059388851t_unit,SV4: list_c1059388851t_unit] :
( ( ( prefix1615116500t_unit @ SV4 @ SV6 )
= $false )
| ( ( prefix1615116500t_unit @ SV2 @ SV6 )
= $true )
| ( ( prefix1615116500t_unit @ SV2 @ SV4 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[374]) ).
thf(376,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[351,375,372,365,361,360]) ).
thf(377,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP055^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.16 % Computer : n014.cluster.edu
% 0.11/0.16 % Model : x86_64 x86_64
% 0.11/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.16 % Memory : 8046.5625MB
% 0.11/0.16 % OS : Linux 6.8.0-71-generic
% 0.11/0.16 % CPULimit : 300
% 0.11/0.16 % WCLimit : 300
% 0.11/0.16 % DateTime : Tue Oct 6 11:14:56 UTC 2026
% 0.11/0.16 % CPUTime :
% 0.11/0.16 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.42/0.63 ...
% 2.42/0.63
% 2.42/0.63 No.of.Axioms: 5
% 2.42/0.63
% 2.42/0.63 Length.of.Defs: 0
% 2.42/0.63
% 2.42/0.63 Contains.Choice.Funs: false
% 2.42/0.63 ...
% 2.42/0.63
% 2.42/0.63 ********************************
% 2.42/0.63 * All subproblems solved! *
% 2.42/0.63 ********************************
% 2.42/0.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:5,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:376,loop_count:0,foatp_calls:1,translation:fof_full)
% 2.42/0.63
% 2.42/0.63 %**** Beginning of derivation protocol ****
% 2.42/0.63 % SZS output start CNFRefutation
% See solution above
% 2.42/0.63
% 2.42/0.63 %**** End of derivation protocol ****
% 2.42/0.63 %**** no. of clauses in derivation: 41 ****
% 2.42/0.63 %**** clause counter: 376 ****
% 2.42/0.63
% 2.42/0.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:5,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:376,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------