%------------------------------------------------------------------------------
% File : Lash---1.13
% Problem : ITP057^1 : TPTP v9.2.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : lash -P picomus -M modes -p tstp -t %d %s
% Computer : n007.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 : 300s
% DateTime : Sat Feb 28 09:29:45 AM UTC 2026
% Result : Theorem 0.22s 0.45s
% Output : Proof 0.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
thf(ty_config256849571t_unit,type,
config256849571t_unit: $tType ).
thf(ty_p,type,
p: $tType ).
thf(ty_message_p_v,type,
message_p_v: $tType ).
thf(ty_list_message_p_v,type,
list_message_p_v: $tType ).
thf(ty_s,type,
s: $tType ).
thf(ty_nat,type,
nat: $tType ).
thf(ty_list_c1059388851t_unit,type,
list_c1059388851t_unit: $tType ).
thf(ty_messageValue_v,type,
messageValue_v: $tType ).
thf(ty_set_o,type,
set_o: $tType ).
thf(ty_isReceiverOf_p_v,type,
isReceiverOf_p_v: p > message_p_v > $o ).
thf(ty_prefix1615116500t_unit,type,
prefix1615116500t_unit: list_c1059388851t_unit > list_c1059388851t_unit > $o ).
thf(ty_bot_bot_set_o,type,
bot_bot_set_o: set_o ).
thf(ty_start,type,
start: p > s ).
thf(ty_last_c571238084t_unit,type,
last_c571238084t_unit: list_c1059388851t_unit > config256849571t_unit ).
thf(ty_eigen__3,type,
eigen__3: list_message_p_v ).
thf(ty_eigen__4,type,
eigen__4: config256849571t_unit ).
thf(ty_trace,type,
trace: list_message_p_v ).
thf(ty_pSilDecVal_p_s_v,type,
pSilDecVal_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > ( p > s ) > $o > p > config256849571t_unit > $o ).
thf(ty_execution_p_s_v,type,
execution_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > ( p > s ) > list_c1059388851t_unit > list_message_p_v > $o ).
thf(ty_eigen__2,type,
eigen__2: list_c1059388851t_unit ).
thf(ty_ord_less_eq_set_o,type,
ord_less_eq_set_o: set_o > set_o > $o ).
thf(ty_eigen__6,type,
eigen__6: config256849571t_unit ).
thf(ty_eigen__5,type,
eigen__5: config256849571t_unit ).
thf(ty_exec,type,
exec: list_c1059388851t_unit ).
thf(ty_last_message_p_v,type,
last_message_p_v: list_message_p_v > message_p_v ).
thf(ty_msg,type,
msg: message_p_v ).
thf(ty_exec2,type,
exec2: list_c1059388851t_unit ).
thf(ty_trace2,type,
trace2: list_message_p_v ).
thf(ty_sends,type,
sends: p > s > messageValue_v > message_p_v > nat ).
thf(ty_initReachable_p_s_v,type,
initReachable_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > ( p > s ) > config256849571t_unit > $o ).
thf(ty_c,type,
c: config256849571t_unit ).
thf(ty_trans,type,
trans: p > s > messageValue_v > s ).
thf(ty_eigen__7,type,
eigen__7: config256849571t_unit ).
thf(ty_prefix47729710ge_p_v,type,
prefix47729710ge_p_v: list_message_p_v > list_message_p_v > $o ).
thf(ty_steps_p_s_v,type,
steps_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > config256849571t_unit > message_p_v > config256849571t_unit > $o ).
thf(ty_eigen__1,type,
eigen__1: list_message_p_v ).
thf(ty_eigen__8,type,
eigen__8: config256849571t_unit ).
thf(ty_eigen__9,type,
eigen__9: config256849571t_unit ).
thf(ty_eigen__0,type,
eigen__0: list_c1059388851t_unit ).
thf(ty_cMsg,type,
cMsg: config256849571t_unit ).
thf(ty_reachable_p_s_v,type,
reachable_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > config256849571t_unit > config256849571t_unit > $o ).
thf(ty_vUniform_p_s_v,type,
vUniform_p_s_v: ( p > s > messageValue_v > s ) > ( p > s > messageValue_v > message_p_v > nat ) > ( p > s ) > $o > config256849571t_unit > $o ).
thf(ty_p2,type,
p2: p ).
thf(ty_insert_o,type,
insert_o: $o > set_o > set_o ).
thf(ty_collect_o,type,
collect_o: ( $o > $o ) > set_o ).
thf(sP1,plain,
( sP1
<=> ( initReachable_p_s_v @ trans @ sends @ start @ ( last_c571238084t_unit @ exec2 ) ) ),
introduced(definition,[new_symbols(definition,[sP1])]) ).
thf(sP2,plain,
( sP2
<=> ( ( isReceiverOf_p_v @ p2 @ msg )
=> ( sP1
=> ( ord_less_eq_set_o
@ ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ ( last_c571238084t_unit @ exec2 ) ) )
@ ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ cMsg ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])]) ).
thf(sP3,plain,
( sP3
<=> ( ( steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ cMsg )
=> sP2 ) ),
introduced(definition,[new_symbols(definition,[sP3])]) ).
thf(sP4,plain,
( sP4
<=> ( ord_less_eq_set_o
@ ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ ( last_c571238084t_unit @ exec2 ) ) )
@ ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ cMsg ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])]) ).
thf(sP5,plain,
( sP5
<=> ( sP1
=> sP4 ) ),
introduced(definition,[new_symbols(definition,[sP5])]) ).
thf(sP6,plain,
( sP6
<=> ( isReceiverOf_p_v @ p2 @ msg ) ),
introduced(definition,[new_symbols(definition,[sP6])]) ).
thf(sP7,plain,
( sP7
<=> ( steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ cMsg ) ),
introduced(definition,[new_symbols(definition,[sP7])]) ).
thf(conj_0,conjecture,
sP4 ).
thf(h0,negated_conjecture,
~ sP4,
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(h1,assumption,
~ ! [X1: list_message_p_v] :
( ( execution_p_s_v @ trans @ sends @ start @ eigen__0 @ X1 )
=> ( ( prefix1615116500t_unit @ exec2 @ eigen__0 )
=> ( ( prefix47729710ge_p_v @ trace2 @ X1 )
=> ( ( ( last_c571238084t_unit @ eigen__0 )
= cMsg )
=> ( ( last_message_p_v @ X1 )
!= msg ) ) ) ) ),
introduced(assumption,[]) ).
thf(h2,assumption,
~ ( ( execution_p_s_v @ trans @ sends @ start @ eigen__0 @ eigen__1 )
=> ( ( prefix1615116500t_unit @ exec2 @ eigen__0 )
=> ( ( prefix47729710ge_p_v @ trace2 @ eigen__1 )
=> ( ( ( last_c571238084t_unit @ eigen__0 )
= cMsg )
=> ( ( last_message_p_v @ eigen__1 )
!= msg ) ) ) ) ),
introduced(assumption,[]) ).
thf(h3,assumption,
execution_p_s_v @ trans @ sends @ start @ eigen__0 @ eigen__1,
introduced(assumption,[]) ).
thf(h4,assumption,
~ ( ( prefix1615116500t_unit @ exec2 @ eigen__0 )
=> ( ( prefix47729710ge_p_v @ trace2 @ eigen__1 )
=> ( ( ( last_c571238084t_unit @ eigen__0 )
= cMsg )
=> ( ( last_message_p_v @ eigen__1 )
!= msg ) ) ) ),
introduced(assumption,[]) ).
thf(h5,assumption,
prefix1615116500t_unit @ exec2 @ eigen__0,
introduced(assumption,[]) ).
thf(h6,assumption,
~ ( ( prefix47729710ge_p_v @ trace2 @ eigen__1 )
=> ( ( ( last_c571238084t_unit @ eigen__0 )
= cMsg )
=> ( ( last_message_p_v @ eigen__1 )
!= msg ) ) ),
introduced(assumption,[]) ).
thf(h7,assumption,
prefix47729710ge_p_v @ trace2 @ eigen__1,
introduced(assumption,[]) ).
thf(h8,assumption,
~ ( ( ( last_c571238084t_unit @ eigen__0 )
= cMsg )
=> ( ( last_message_p_v @ eigen__1 )
!= msg ) ),
introduced(assumption,[]) ).
thf(h9,assumption,
( ( last_c571238084t_unit @ eigen__0 )
= cMsg ),
introduced(assumption,[]) ).
thf(h10,assumption,
( ( last_message_p_v @ eigen__1 )
= msg ),
introduced(assumption,[]) ).
thf(h11,assumption,
~ ! [X1: list_message_p_v] :
( ( execution_p_s_v @ trans @ sends @ start @ eigen__2 @ X1 )
=> ( ( ( ( prefix1615116500t_unit @ exec @ eigen__2 )
=> ~ ( prefix47729710ge_p_v @ trace @ X1 ) )
=> ~ ( ( exec = eigen__2 )
=> ( trace != X1 ) ) )
=> ( ( last_c571238084t_unit @ eigen__2 )
!= c ) ) ),
introduced(assumption,[]) ).
thf(h12,assumption,
~ ( ( execution_p_s_v @ trans @ sends @ start @ eigen__2 @ eigen__3 )
=> ( ( ( ( prefix1615116500t_unit @ exec @ eigen__2 )
=> ~ ( prefix47729710ge_p_v @ trace @ eigen__3 ) )
=> ~ ( ( exec = eigen__2 )
=> ( trace != eigen__3 ) ) )
=> ( ( last_c571238084t_unit @ eigen__2 )
!= c ) ) ),
introduced(assumption,[]) ).
thf(h13,assumption,
execution_p_s_v @ trans @ sends @ start @ eigen__2 @ eigen__3,
introduced(assumption,[]) ).
thf(h14,assumption,
~ ( ( ( ( prefix1615116500t_unit @ exec @ eigen__2 )
=> ~ ( prefix47729710ge_p_v @ trace @ eigen__3 ) )
=> ~ ( ( exec = eigen__2 )
=> ( trace != eigen__3 ) ) )
=> ( ( last_c571238084t_unit @ eigen__2 )
!= c ) ),
introduced(assumption,[]) ).
thf(h15,assumption,
( ( ( prefix1615116500t_unit @ exec @ eigen__2 )
=> ~ ( prefix47729710ge_p_v @ trace @ eigen__3 ) )
=> ~ ( ( exec = eigen__2 )
=> ( trace != eigen__3 ) ) ),
introduced(assumption,[]) ).
thf(h16,assumption,
( ( last_c571238084t_unit @ eigen__2 )
= c ),
introduced(assumption,[]) ).
thf(h17,assumption,
~ ( ( prefix1615116500t_unit @ exec @ eigen__2 )
=> ~ ( prefix47729710ge_p_v @ trace @ eigen__3 ) ),
introduced(assumption,[]) ).
thf(h18,assumption,
~ ( ( exec = eigen__2 )
=> ( trace != eigen__3 ) ),
introduced(assumption,[]) ).
thf(1,plain,
( ~ sP5
| ~ sP1
| sP4 ),
inference(prop_rule,[status(thm)],[]) ).
thf(2,plain,
( ~ sP2
| ~ sP6
| sP5 ),
inference(prop_rule,[status(thm)],[]) ).
thf(3,plain,
( ~ sP3
| ~ sP7
| sP2 ),
inference(prop_rule,[status(thm)],[]) ).
thf(fact_0_PisReceiverOf,axiom,
sP6 ).
thf(fact_1_InitReachLastExec_H,axiom,
sP1 ).
thf(fact_3_CMsg,axiom,
sP7 ).
thf(fact_6__092_060open_062_092_060lbrakk_062p_A_061_Ap_059_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_059_AisReceiverOf_Ap_Amsg_059_AinitReachable_A_Ilast_Aexec_H_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Aval_091p_Mlast_Aexec_H_093_A_092_060subseteq_062_Aval_091p_McMsg_093_092_060close_062,axiom,
sP3 ).
thf(4,plain,
$false,
inference(prop_unsat,[status(thm),assumptions([h17,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[1,2,3,h0,fact_0_PisReceiverOf,fact_1_InitReachLastExec_H,fact_3_CMsg,fact_6__092_060open_062_092_060lbrakk_062p_A_061_Ap_059_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_059_AisReceiverOf_Ap_Amsg_059_AinitReachable_A_Ilast_Aexec_H_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Aval_091p_Mlast_Aexec_H_093_A_092_060subseteq_062_Aval_091p_McMsg_093_092_060close_062]) ).
thf(h19,assumption,
exec = eigen__2,
introduced(assumption,[]) ).
thf(h20,assumption,
trace = eigen__3,
introduced(assumption,[]) ).
thf(h21,assumption,
~ ( ( prefix1615116500t_unit @ exec @ exec2 )
=> ~ ( prefix47729710ge_p_v @ trace @ trace2 ) ),
introduced(assumption,[]) ).
thf(h22,assumption,
~ ( ( exec = exec2 )
=> ( trace != trace2 ) ),
introduced(assumption,[]) ).
thf(h23,assumption,
prefix1615116500t_unit @ exec @ exec2,
introduced(assumption,[]) ).
thf(h24,assumption,
prefix47729710ge_p_v @ trace @ trace2,
introduced(assumption,[]) ).
thf(h25,assumption,
~ ( ( reachable_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec ) @ eigen__7 )
=> ( ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ eigen__7 ) )
!= ( insert_o @ ~ $false @ ( insert_o @ $false @ bot_bot_set_o ) ) ) ),
introduced(assumption,[]) ).
thf(h26,assumption,
reachable_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec ) @ eigen__7,
introduced(assumption,[]) ).
thf(h27,assumption,
( ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ eigen__7 ) )
= ( insert_o @ ~ $false @ ( insert_o @ $false @ bot_bot_set_o ) ) ),
introduced(assumption,[]) ).
thf(h28,assumption,
~ ( ( initReachable_p_s_v @ trans @ sends @ start @ ( last_c571238084t_unit @ exec ) )
=> ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec ) ) ),
introduced(assumption,[]) ).
thf(h29,assumption,
~ ( vUniform_p_s_v @ trans @ sends @ start @ ~ $false @ ( last_c571238084t_unit @ exec ) ),
introduced(assumption,[]) ).
thf(h30,assumption,
initReachable_p_s_v @ trans @ sends @ start @ ( last_c571238084t_unit @ exec ),
introduced(assumption,[]) ).
thf(h31,assumption,
~ ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec ) ),
introduced(assumption,[]) ).
thf(h32,assumption,
~ ( sP1
=> ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec2 ) ) ),
introduced(assumption,[]) ).
thf(h33,assumption,
~ ( vUniform_p_s_v @ trans @ sends @ start @ ~ $false @ ( last_c571238084t_unit @ exec2 ) ),
introduced(assumption,[]) ).
thf(h34,assumption,
sP1,
introduced(assumption,[]) ).
thf(h35,assumption,
~ ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec2 ) ),
introduced(assumption,[]) ).
thf(h36,assumption,
steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ eigen__8,
introduced(assumption,[]) ).
thf(h37,assumption,
steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ eigen__9,
introduced(assumption,[]) ).
thf(h38,assumption,
~ sP7,
introduced(assumption,[]) ).
thf(h39,assumption,
sP2,
introduced(assumption,[]) ).
thf(5,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h38,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[fact_3_CMsg,h38]) ).
thf(h40,assumption,
~ sP6,
introduced(assumption,[]) ).
thf(h41,assumption,
sP5,
introduced(assumption,[]) ).
thf(6,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h40,h39,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[fact_0_PisReceiverOf,h40]) ).
thf(h42,assumption,
~ sP1,
introduced(assumption,[]) ).
thf(h43,assumption,
sP4,
introduced(assumption,[]) ).
thf(7,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h42,h41,h39,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[h34,h42]) ).
thf(8,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h43,h41,h39,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[h43,h0]) ).
thf(9,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h41,h39,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h42]),tab_imp(discharge,[h43])],[h41,7,8,h42,h43]) ).
thf(10,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h39,h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h40]),tab_imp(discharge,[h41])],[h39,6,9,h40,h41]) ).
thf(11,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h37,h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h38]),tab_imp(discharge,[h39])],[fact_6__092_060open_062_092_060lbrakk_062p_A_061_Ap_059_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_059_AisReceiverOf_Ap_Amsg_059_AinitReachable_A_Ilast_Aexec_H_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Aval_091p_Mlast_Aexec_H_093_A_092_060subseteq_062_Aval_091p_McMsg_093_092_060close_062,5,10,h38,h39]) ).
thf(fact_10__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062cMsg_O_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: config256849571t_unit] :
~ ( steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ X1 ) ).
thf(12,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h36,h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h37]),tab_negall(eigenvar,eigen__9)],[fact_10__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062cMsg_O_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,11,h37]) ).
thf(13,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h34,h35,h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h36]),tab_negall(eigenvar,eigen__8)],[fact_10__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062cMsg_O_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,12,h36]) ).
thf(14,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h32,h33,h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h34,h35])],[h32,13,h34,h35]) ).
thf(fact_14_nonUniformC_H,axiom,
~ ( ~ ( sP1
=> ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec2 ) ) )
=> ( vUniform_p_s_v @ trans @ sends @ start @ ~ $false @ ( last_c571238084t_unit @ exec2 ) ) ) ).
thf(15,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h30,h31,h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h32,h33])],[fact_14_nonUniformC_H,14,h32,h33]) ).
thf(16,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h28,h29,h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h30,h31])],[h28,15,h30,h31]) ).
thf(fact_38_NonUniformLexec,axiom,
~ ( ~ ( ( initReachable_p_s_v @ trans @ sends @ start @ ( last_c571238084t_unit @ exec ) )
=> ( vUniform_p_s_v @ trans @ sends @ start @ $false @ ( last_c571238084t_unit @ exec ) ) )
=> ( vUniform_p_s_v @ trans @ sends @ start @ ~ $false @ ( last_c571238084t_unit @ exec ) ) ) ).
thf(17,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h26,h27,h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h28,h29])],[fact_38_NonUniformLexec,16,h28,h29]) ).
thf(18,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h25,h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h26,h27])],[h25,17,h26,h27]) ).
thf(fact_202__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062c_H_O_A_092_060lbrakk_062reachable_A_Ilast_Aexec_J_Ac_H_059_Aval_091p_Mc_H_093_A_061_A_123True_M_AFalse_125_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: config256849571t_unit] :
( ( reachable_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec ) @ X1 )
=> ( ( collect_o
@ ^ [X2: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X2 @ p2 @ X1 ) )
!= ( insert_o @ ~ $false @ ( insert_o @ $false @ bot_bot_set_o ) ) ) ) ).
thf(19,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h23,h24,h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h25]),tab_negall(eigenvar,eigen__7)],[fact_202__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062c_H_O_A_092_060lbrakk_062reachable_A_Ilast_Aexec_J_Ac_H_059_Aval_091p_Mc_H_093_A_061_A_123True_M_AFalse_125_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,18,h25]) ).
thf(20,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h21,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h23,h24])],[h21,19,h23,h24]) ).
thf(h44,assumption,
exec = exec2,
introduced(assumption,[]) ).
thf(h45,assumption,
trace = trace2,
introduced(assumption,[]) ).
thf(h46,assumption,
~ ( ( reachable_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec ) @ eigen__4 )
=> ( ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ eigen__4 ) )
!= ( insert_o @ ~ $false @ ( insert_o @ $false @ bot_bot_set_o ) ) ) ),
introduced(assumption,[]) ).
thf(h47,assumption,
reachable_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec ) @ eigen__4,
introduced(assumption,[]) ).
thf(h48,assumption,
( ( collect_o
@ ^ [X1: $o] : ( pSilDecVal_p_s_v @ trans @ sends @ start @ X1 @ p2 @ eigen__4 ) )
= ( insert_o @ ~ $false @ ( insert_o @ $false @ bot_bot_set_o ) ) ),
introduced(assumption,[]) ).
thf(h49,assumption,
steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ eigen__5,
introduced(assumption,[]) ).
thf(h50,assumption,
steps_p_s_v @ trans @ sends @ ( last_c571238084t_unit @ exec2 ) @ msg @ eigen__6,
introduced(assumption,[]) ).
thf(21,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h38,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[fact_3_CMsg,h38]) ).
thf(22,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h40,h39,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[fact_0_PisReceiverOf,h40]) ).
thf(23,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h42,h41,h39,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[h34,h42]) ).
thf(24,plain,
$false,
inference(tab_conflict,[status(thm),assumptions([h43,h41,h39,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0])],[h43,h0]) ).
thf(25,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h41,h39,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h42]),tab_imp(discharge,[h43])],[h41,23,24,h42,h43]) ).
thf(26,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h39,h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h40]),tab_imp(discharge,[h41])],[h39,22,25,h40,h41]) ).
thf(27,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h50,h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h38]),tab_imp(discharge,[h39])],[fact_6__092_060open_062_092_060lbrakk_062p_A_061_Ap_059_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_059_AisReceiverOf_Ap_Amsg_059_AinitReachable_A_Ilast_Aexec_H_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Aval_091p_Mlast_Aexec_H_093_A_092_060subseteq_062_Aval_091p_McMsg_093_092_060close_062,21,26,h38,h39]) ).
thf(28,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h49,h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h50]),tab_negall(eigenvar,eigen__6)],[fact_10__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062cMsg_O_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,27,h50]) ).
thf(29,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h34,h35,h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h49]),tab_negall(eigenvar,eigen__5)],[fact_10__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062cMsg_O_Alast_Aexec_H_A_092_060turnstile_062_Amsg_A_092_060mapsto_062_AcMsg_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,28,h49]) ).
thf(30,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h32,h33,h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h34,h35])],[h32,29,h34,h35]) ).
thf(31,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h30,h31,h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h32,h33])],[fact_14_nonUniformC_H,30,h32,h33]) ).
thf(32,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h28,h29,h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h30,h31])],[h28,31,h30,h31]) ).
thf(33,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h47,h48,h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h28,h29])],[fact_38_NonUniformLexec,32,h28,h29]) ).
thf(34,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h46,h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h47,h48])],[h46,33,h47,h48]) ).
thf(35,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h44,h45,h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h46]),tab_negall(eigenvar,eigen__4)],[fact_202__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062c_H_O_A_092_060lbrakk_062reachable_A_Ilast_Aexec_J_Ac_H_059_Aval_091p_Mc_H_093_A_061_A_123True_M_AFalse_125_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,34,h46]) ).
thf(36,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h22,h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h44,h45])],[h22,35,h44,h45]) ).
thf(fact_261_NewExec_I2_J,axiom,
( ( ( prefix1615116500t_unit @ exec @ exec2 )
=> ~ ( prefix47729710ge_p_v @ trace @ trace2 ) )
=> ~ ( ( exec = exec2 )
=> ( trace != trace2 ) ) ) ).
thf(37,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h19,h20,h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h21]),tab_imp(discharge,[h22])],[fact_261_NewExec_I2_J,20,36,h21,h22]) ).
thf(38,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h18,h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h19,h20])],[h18,37,h19,h20]) ).
thf(39,plain,
$false,
inference(tab_imp,[status(thm),assumptions([h15,h16,h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h17]),tab_imp(discharge,[h18])],[h15,4,38,h17,h18]) ).
thf(40,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h13,h14,h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h15,h16])],[h14,39,h15,h16]) ).
thf(41,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h12,h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h13,h14])],[h12,40,h13,h14]) ).
thf(42,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h11,h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h12]),tab_negall(eigenvar,eigen__3)],[h11,41,h12]) ).
thf(fact_270__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062exec_H_Atrace_H_O_A_092_060lbrakk_062execution_Atrans_Asends_Astart_Aexec_H_Atrace_H_059_AprefixList_Aexec_Aexec_H_A_092_060and_062_AprefixList_Atrace_Atrace_H_A_092_060or_062_Aexec_A_061_Aexec_H_A_092_060and_062_Atrace_A_061_Atrace_H_059_Alast_Aexec_H_A_061_Ac_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: list_c1059388851t_unit,X2: list_message_p_v] :
( ( execution_p_s_v @ trans @ sends @ start @ X1 @ X2 )
=> ( ( ( ( prefix1615116500t_unit @ exec @ X1 )
=> ~ ( prefix47729710ge_p_v @ trace @ X2 ) )
=> ~ ( ( exec = X1 )
=> ( trace != X2 ) ) )
=> ( ( last_c571238084t_unit @ X1 )
!= c ) ) ) ).
thf(43,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h9,h10,h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h11]),tab_negall(eigenvar,eigen__2)],[fact_270__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062exec_H_Atrace_H_O_A_092_060lbrakk_062execution_Atrans_Asends_Astart_Aexec_H_Atrace_H_059_AprefixList_Aexec_Aexec_H_A_092_060and_062_AprefixList_Atrace_Atrace_H_A_092_060or_062_Aexec_A_061_Aexec_H_A_092_060and_062_Atrace_A_061_Atrace_H_059_Alast_Aexec_H_A_061_Ac_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,42,h11]) ).
thf(44,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h7,h8,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h9,h10])],[h8,43,h9,h10]) ).
thf(45,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h7,h8])],[h6,44,h7,h8]) ).
thf(46,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h3,h4,h2,h1,h0]),tab_negimp(discharge,[h5,h6])],[h4,45,h5,h6]) ).
thf(47,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h2,h1,h0]),tab_negimp(discharge,[h3,h4])],[h2,46,h3,h4]) ).
thf(48,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,47,h2]) ).
thf(fact_271__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062execMsg_AtraceMsg_O_A_092_060lbrakk_062execution_Atrans_Asends_Astart_AexecMsg_AtraceMsg_059_AprefixList_Aexec_H_AexecMsg_059_AprefixList_Atrace_H_AtraceMsg_059_Alast_AexecMsg_A_061_AcMsg_059_Alast_AtraceMsg_A_061_Amsg_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: list_c1059388851t_unit,X2: list_message_p_v] :
( ( execution_p_s_v @ trans @ sends @ start @ X1 @ X2 )
=> ( ( prefix1615116500t_unit @ exec2 @ X1 )
=> ( ( prefix47729710ge_p_v @ trace2 @ X2 )
=> ( ( ( last_c571238084t_unit @ X1 )
= cMsg )
=> ( ( last_message_p_v @ X2 )
!= msg ) ) ) ) ) ).
thf(49,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[fact_271__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062execMsg_AtraceMsg_O_A_092_060lbrakk_062execution_Atrans_Asends_Astart_AexecMsg_AtraceMsg_059_AprefixList_Aexec_H_AexecMsg_059_AprefixList_Atrace_H_AtraceMsg_059_Alast_AexecMsg_A_061_AcMsg_059_Alast_AtraceMsg_A_061_Amsg_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,48,h1]) ).
thf(0,theorem,
sP4,
inference(contra,[status(thm),contra(discharge,[h0])],[49,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP057^1 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.00/0.12 % Command : lash -P picomus -M modes -p tstp -t %d %s
% 0.16/0.33 % Computer : n007.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu Feb 26 00:59:08 EST 2026
% 0.16/0.33 % CPUTime :
% 0.22/0.45 % SZS status Theorem
% 0.22/0.45 % Mode: cade22sinegrackle2x6978
% 0.22/0.45 % Steps: 706
% 0.22/0.45 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------