%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SWV750-1 : TPTP v9.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.MBlzzjl5mS true
% 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 : Thu Oct 2 05:01:55 PM UTC 2025
% Result : Unsatisfiable 172.11s 25.21s
% Output : Refutation 172.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV750-1 : TPTP v9.2.0. Released v4.1.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.MBlzzjl5mS true
% 0.13/0.34 % Computer : n007.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 : 300
% 0.13/0.34 % DateTime : Wed Oct 1 12:25:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.34 % Running in FO mode
% 0.50/0.62 % Total configuration time : 435
% 0.50/0.62 % Estimated wc time : 1092
% 0.50/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 172.11/25.21 % Solved by fo/fo6_bce.sh.
% 172.11/25.21 % BCE start: 691
% 172.11/25.21 % BCE eliminated: 13
% 172.11/25.21 % PE start: 678
% 172.11/25.21 logic: eq
% 172.11/25.21 % PE eliminated: 1
% 172.11/25.21 % done 5526 iterations in 24.488s
% 172.11/25.21 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 172.11/25.21 % SZS output start Refutation
% 172.11/25.21 thf(v_X_type, type, v_X: $i).
% 172.11/25.21 thf(c_lessequals_type, type, c_lessequals: $i > $i > $i > $o).
% 172.11/25.21 thf(v_Ka_type, type, v_Ka: $i).
% 172.11/25.21 thf(v_evso_type, type, v_evso: $i).
% 172.11/25.21 thf(c_Message_Oagent_OServer_type, type, c_Message_Oagent_OServer: $i).
% 172.11/25.21 thf(c_Message_Omsg_OAgent_type, type, c_Message_Omsg_OAgent: $i > $i).
% 172.11/25.21 thf(hBOOL_type, type, hBOOL: $i > $o).
% 172.11/25.21 thf(c_List_Oset_type, type, c_List_Oset: $i > $i > $i).
% 172.11/25.21 thf(v_Ba_type, type, v_Ba: $i).
% 172.11/25.21 thf(v_B_type, type, v_B: $i).
% 172.11/25.21 thf(c_in_type, type, c_in: $i > $i > $i > $i).
% 172.11/25.21 thf(tc_fun_type, type, tc_fun: $i > $i > $i).
% 172.11/25.21 thf(v_A_type, type, v_A: $i).
% 172.11/25.21 thf(c_Lattices_Oupper__semilattice__class_Osup_type, type, c_Lattices_Oupper__semilattice__class_Osup:
% 172.11/25.21 $i > $i > $i > $i).
% 172.11/25.21 thf(c_Message_Omsg_OKey_type, type, c_Message_Omsg_OKey: $i).
% 172.11/25.21 thf(tc_Event_Oevent_type, type, tc_Event_Oevent: $i).
% 172.11/25.21 thf(hAPP_type, type, hAPP: $i > $i > $i).
% 172.11/25.21 thf(v_NA_type, type, v_NA: $i).
% 172.11/25.21 thf(v_Aa_type, type, v_Aa: $i).
% 172.11/25.21 thf(c_Message_Omsg_OMPair_type, type, c_Message_Omsg_OMPair: $i > $i > $i).
% 172.11/25.21 thf(v_K_type, type, v_K: $i).
% 172.11/25.21 thf(c_Event_Oevent_OSays_type, type, c_Event_Oevent_OSays: $i > $i > $i > $i).
% 172.11/25.21 thf(v_NAa_type, type, v_NAa: $i).
% 172.11/25.21 thf(tc_List_Olist_type, type, tc_List_Olist: $i > $i).
% 172.11/25.21 thf(c_Public_OshrK_type, type, c_Public_OshrK: $i).
% 172.11/25.21 thf(c_Message_Omsg_ONonce_type, type, c_Message_Omsg_ONonce: $i > $i).
% 172.11/25.21 thf(tc_bool_type, type, tc_bool: $i).
% 172.11/25.21 thf(c_Orderings_Obot__class_Obot_type, type, c_Orderings_Obot__class_Obot:
% 172.11/25.21 $i > $i).
% 172.11/25.21 thf(c_NS__Shared__Mirabelle_Ons__shared_type, type, c_NS__Shared__Mirabelle_Ons__shared:
% 172.11/25.21 $i).
% 172.11/25.21 thf(c_Message_Omsg_OCrypt_type, type, c_Message_Omsg_OCrypt: $i > $i > $i).
% 172.11/25.21 thf(cls_conjecture_7, conjecture,
% 172.11/25.21 (~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_A ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 v_NA @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_B ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_K ) @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_B ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_K ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_A ) ) ) ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ v_evso @ tc_Event_Oevent ) @ tc_Event_Oevent ) ))).
% 172.11/25.21 thf(zf_stmt_0, negated_conjecture,
% 172.11/25.21 (hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_A ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 v_NA @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_B ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_K ) @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_B ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_K ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_A ) ) ) ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ v_evso @ tc_Event_Oevent ) @ tc_Event_Oevent )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_7])).
% 172.11/25.21 thf(zip_derived_cl657, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_A) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ v_NA @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_K) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_K) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_A)))))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_0])).
% 172.11/25.21 thf(cls_conjecture_9, conjecture, (( v_K ) != ( v_Ka ))).
% 172.11/25.21 thf(zf_stmt_1, negated_conjecture, (( v_K ) = ( v_Ka )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_9])).
% 172.11/25.21 thf(zip_derived_cl659, plain, (((v_K) = (v_Ka))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_1])).
% 172.11/25.21 thf(zip_derived_cl659, plain, (((v_K) = (v_Ka))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_1])).
% 172.11/25.21 thf(zip_derived_cl2673, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_A) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ v_NA @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_A)))))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent))),
% 172.11/25.21 inference('demod', [status(thm)],
% 172.11/25.21 [zip_derived_cl657, zip_derived_cl659, zip_derived_cl659])).
% 172.11/25.21 thf(cls_mem__def_0, axiom,
% 172.11/25.21 (( hBOOL @ ( hAPP @ V_S @ V_x ) ) |
% 172.11/25.21 ( ~( hBOOL @ ( c_in @ V_x @ V_S @ T_a ) ) ))).
% 172.11/25.21 thf(zip_derived_cl630, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (hAPP @ X0 @ X1)) | ~ (hBOOL @ (c_in @ X1 @ X0 @ X2)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_0])).
% 172.11/25.21 thf(zip_derived_cl3884, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (hAPP @ (c_List_Oset @ v_evso @ tc_Event_Oevent) @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_A) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ v_NA @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_A))))))))))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl2673, zip_derived_cl630])).
% 172.11/25.21 thf(cls_mem__def_1, axiom,
% 172.11/25.21 (( hBOOL @ ( c_in @ V_x @ V_S @ T_a ) ) |
% 172.11/25.21 ( ~( hBOOL @ ( hAPP @ V_S @ V_x ) ) ))).
% 172.11/25.21 thf(zip_derived_cl629, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (c_in @ X0 @ X1 @ X2)) | ~ (hBOOL @ (hAPP @ X1 @ X0)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_1])).
% 172.11/25.21 thf(zip_derived_cl4149, plain,
% 172.11/25.21 (![X0 : $i]:
% 172.11/25.21 (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_A) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ v_NA @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_A)))))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ X0))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl3884, zip_derived_cl629])).
% 172.11/25.21 thf(cls_subset__iff_0, axiom,
% 172.11/25.21 (( hBOOL @ ( c_in @ V_t @ V_B @ T_a ) ) |
% 172.11/25.21 ( ~( hBOOL @ ( c_in @ V_t @ V_A @ T_a ) ) ) |
% 172.11/25.21 ( ~( c_lessequals @ V_A @ V_B @ ( tc_fun @ T_a @ tc_bool ) ) ))).
% 172.11/25.21 thf(zip_derived_cl236, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 172.11/25.21 ( (hBOOL @ (c_in @ X0 @ X1 @ X2))
% 172.11/25.21 | ~ (hBOOL @ (c_in @ X0 @ X3 @ X2))
% 172.11/25.21 | ~ (c_lessequals @ X3 @ X1 @ (tc_fun @ X2 @ tc_bool)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_subset__iff_0])).
% 172.11/25.21 thf(zip_derived_cl8119, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i]:
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_A @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_A) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ v_NA @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_B) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_A)))))))) @
% 172.11/25.21 X1 @ X0))
% 172.11/25.21 | ~ (c_lessequals @ (c_List_Oset @ v_evso @ tc_Event_Oevent) @ X1 @
% 172.11/25.21 (tc_fun @ X0 @ tc_bool)))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl4149, zip_derived_cl236])).
% 172.11/25.21 thf(cls_conjecture_4, conjecture,
% 172.11/25.21 (~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Aa ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_ONonce @ v_NAa ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Aa ) ) ) ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ v_evso @ tc_Event_Oevent ) @ tc_Event_Oevent ) ))).
% 172.11/25.21 thf(zf_stmt_2, negated_conjecture,
% 172.11/25.21 (hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Aa ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_ONonce @ v_NAa ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Aa ) ) ) ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ v_evso @ tc_Event_Oevent ) @ tc_Event_Oevent )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_4])).
% 172.11/25.21 thf(zip_derived_cl654, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Aa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_ONonce @ v_NAa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_Aa)))))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_2])).
% 172.11/25.21 thf(cls_conjecture_6, conjecture,
% 172.11/25.21 (( v_X ) !=
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Aa ) ) ))).
% 172.11/25.21 thf(zf_stmt_3, negated_conjecture,
% 172.11/25.21 (( v_X ) =
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ v_Ba ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ v_Ka ) @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ v_Aa ) ) )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_6])).
% 172.11/25.21 thf(zip_derived_cl656, plain,
% 172.11/25.21 (((v_X)
% 172.11/25.21 = (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 (c_Message_Omsg_OAgent @ v_Aa))))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_3])).
% 172.11/25.21 thf(zip_derived_cl2684, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Aa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_ONonce @ v_NAa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 v_X))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent))),
% 172.11/25.21 inference('demod', [status(thm)], [zip_derived_cl654, zip_derived_cl656])).
% 172.11/25.21 thf(zip_derived_cl630, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (hAPP @ X0 @ X1)) | ~ (hBOOL @ (c_in @ X1 @ X0 @ X2)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_0])).
% 172.11/25.21 thf(zip_derived_cl3885, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (hAPP @ (c_List_Oset @ v_evso @ tc_Event_Oevent) @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Aa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_ONonce @ v_NAa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 v_X)))))))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl2684, zip_derived_cl630])).
% 172.11/25.21 thf(zip_derived_cl629, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (c_in @ X0 @ X1 @ X2)) | ~ (hBOOL @ (hAPP @ X1 @ X0)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_1])).
% 172.11/25.21 thf(zip_derived_cl4040, plain,
% 172.11/25.21 (![X0 : $i]:
% 172.11/25.21 (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ v_Aa @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ v_Aa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_ONonce @ v_NAa) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ v_Ba) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (hAPP @ c_Message_Omsg_OKey @ v_Ka) @
% 172.11/25.21 v_X))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ X0))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl3885, zip_derived_cl629])).
% 172.11/25.21 thf(cls_conjecture_2, conjecture,
% 172.11/25.21 (~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 v_evso @ c_NS__Shared__Mirabelle_Ons__shared @
% 172.11/25.21 ( tc_List_Olist @ tc_Event_Oevent ) ) ))).
% 172.11/25.21 thf(zf_stmt_4, negated_conjecture,
% 172.11/25.21 (hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 v_evso @ c_NS__Shared__Mirabelle_Ons__shared @
% 172.11/25.21 ( tc_List_Olist @ tc_Event_Oevent ) )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_2])).
% 172.11/25.21 thf(zip_derived_cl652, plain,
% 172.11/25.21 ( (hBOOL @
% 172.11/25.21 (c_in @ v_evso @ c_NS__Shared__Mirabelle_Ons__shared @
% 172.11/25.21 (tc_List_Olist @ tc_Event_Oevent)))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_4])).
% 172.11/25.21 thf(zip_derived_cl630, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (hAPP @ X0 @ X1)) | ~ (hBOOL @ (c_in @ X1 @ X0 @ X2)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_0])).
% 172.11/25.21 thf(zip_derived_cl3896, plain,
% 172.11/25.21 ( (hBOOL @ (hAPP @ c_NS__Shared__Mirabelle_Ons__shared @ v_evso))),
% 172.11/25.21 inference('s_sup-', [status(thm)], [zip_derived_cl652, zip_derived_cl630])).
% 172.11/25.21 thf(zip_derived_cl629, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 ( (hBOOL @ (c_in @ X0 @ X1 @ X2)) | ~ (hBOOL @ (hAPP @ X1 @ X0)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_mem__def_1])).
% 172.11/25.21 thf(zip_derived_cl3917, plain,
% 172.11/25.21 (![X0 : $i]:
% 172.11/25.21 (hBOOL @ (c_in @ v_evso @ c_NS__Shared__Mirabelle_Ons__shared @ X0))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl3896, zip_derived_cl629])).
% 172.11/25.21 thf(cls_unique__session__keys_1, axiom,
% 172.11/25.21 (( ( V_NA ) = ( V_NA_H ) ) |
% 172.11/25.21 ( ~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 V_evs @ c_NS__Shared__Mirabelle_Ons__shared @
% 172.11/25.21 ( tc_List_Olist @ tc_Event_Oevent ) ) ) ) |
% 172.11/25.21 ( ~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ V_A_H @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ V_A_H ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 V_NA_H @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ V_B_H ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ V_K ) @ V_X_H ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ V_evs @ tc_Event_Oevent ) @ tc_Event_Oevent ) ) ) |
% 172.11/25.21 ( ~( hBOOL @
% 172.11/25.21 ( c_in @
% 172.11/25.21 ( c_Event_Oevent_OSays @
% 172.11/25.21 c_Message_Oagent_OServer @ V_A @
% 172.11/25.21 ( c_Message_Omsg_OCrypt @
% 172.11/25.21 ( hAPP @ c_Public_OshrK @ V_A ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 V_NA @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( c_Message_Omsg_OAgent @ V_B ) @
% 172.11/25.21 ( c_Message_Omsg_OMPair @
% 172.11/25.21 ( hAPP @ c_Message_Omsg_OKey @ V_K ) @ V_X ) ) ) ) ) @
% 172.11/25.21 ( c_List_Oset @ V_evs @ tc_Event_Oevent ) @ tc_Event_Oevent ) ) ))).
% 172.11/25.21 thf(zip_derived_cl612, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 172.11/25.21 X7 : $i, X8 : $i, X9 : $i]:
% 172.11/25.21 (((X1) = (X0))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @ X2 @ c_NS__Shared__Mirabelle_Ons__shared @
% 172.11/25.21 (tc_List_Olist @ tc_Event_Oevent)))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ X3 @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ X3) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ X0 @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ X4) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ X5) @ X6))))) @
% 172.11/25.21 (c_List_Oset @ X2 @ tc_Event_Oevent) @ tc_Event_Oevent))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ X7 @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ X7) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ X1 @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ X8) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ X5) @ X9))))) @
% 172.11/25.21 (c_List_Oset @ X2 @ tc_Event_Oevent) @ tc_Event_Oevent)))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_unique__session__keys_1])).
% 172.11/25.21 thf(zip_derived_cl16908, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 172.11/25.21 X7 : $i, X8 : $i]:
% 172.11/25.21 (((X0) = (X1))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ X5 @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ X5) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ X1 @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ X4) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ X3) @ X2))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ X8 @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ X8) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ X0 @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ X7) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ X3) @ X6))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent)))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl3917, zip_derived_cl612])).
% 172.11/25.21 thf(zip_derived_cl86791, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 172.11/25.21 (((X0) = (c_Message_Omsg_ONonce @ v_NAa))
% 172.11/25.21 | ~ (hBOOL @
% 172.11/25.21 (c_in @
% 172.11/25.21 (c_Event_Oevent_OSays @ c_Message_Oagent_OServer @ X3 @
% 172.11/25.21 (c_Message_Omsg_OCrypt @ (hAPP @ c_Public_OshrK @ X3) @
% 172.11/25.21 (c_Message_Omsg_OMPair @ X0 @
% 172.11/25.21 (c_Message_Omsg_OMPair @ (c_Message_Omsg_OAgent @ X2) @
% 172.11/25.21 (c_Message_Omsg_OMPair @
% 172.11/25.21 (hAPP @ c_Message_Omsg_OKey @ v_Ka) @ X1))))) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @ tc_Event_Oevent)))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl4040, zip_derived_cl16908])).
% 172.11/25.21 thf(zip_derived_cl86938, plain,
% 172.11/25.21 ((~ (c_lessequals @ (c_List_Oset @ v_evso @ tc_Event_Oevent) @
% 172.11/25.21 (c_List_Oset @ v_evso @ tc_Event_Oevent) @
% 172.11/25.21 (tc_fun @ tc_Event_Oevent @ tc_bool))
% 172.11/25.21 | ((v_NA) = (c_Message_Omsg_ONonce @ v_NAa)))),
% 172.11/25.21 inference('s_sup-', [status(thm)],
% 172.11/25.21 [zip_derived_cl8119, zip_derived_cl86791])).
% 172.11/25.21 thf(cls_Un__empty__left_0, axiom,
% 172.11/25.21 (( c_Lattices_Oupper__semilattice__class_Osup @
% 172.11/25.21 ( c_Orderings_Obot__class_Obot @ ( tc_fun @ T_a @ tc_bool ) ) @ V_B @
% 172.11/25.21 ( tc_fun @ T_a @ tc_bool ) ) =
% 172.11/25.21 ( V_B ))).
% 172.11/25.21 thf(zip_derived_cl34, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i]:
% 172.11/25.21 ((c_Lattices_Oupper__semilattice__class_Osup @
% 172.11/25.21 (c_Orderings_Obot__class_Obot @ (tc_fun @ X1 @ tc_bool)) @ X0 @
% 172.11/25.21 (tc_fun @ X1 @ tc_bool)) = (X0))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_Un__empty__left_0])).
% 172.11/25.21 thf(cls_Un__upper2_0, axiom,
% 172.11/25.21 (c_lessequals @
% 172.11/25.21 V_B @
% 172.11/25.21 ( c_Lattices_Oupper__semilattice__class_Osup @
% 172.11/25.21 V_A @ V_B @ ( tc_fun @ T_a @ tc_bool ) ) @
% 172.11/25.21 ( tc_fun @ T_a @ tc_bool ))).
% 172.11/25.21 thf(zip_derived_cl72, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i, X2 : $i]:
% 172.11/25.21 (c_lessequals @ X0 @
% 172.11/25.21 (c_Lattices_Oupper__semilattice__class_Osup @ X1 @ X0 @
% 172.11/25.21 (tc_fun @ X2 @ tc_bool)) @
% 172.11/25.21 (tc_fun @ X2 @ tc_bool))),
% 172.11/25.21 inference('cnf', [status(esa)], [cls_Un__upper2_0])).
% 172.11/25.21 thf(zip_derived_cl3315, plain,
% 172.11/25.21 (![X0 : $i, X1 : $i]: (c_lessequals @ X0 @ X0 @ (tc_fun @ X1 @ tc_bool))),
% 172.11/25.21 inference('s_sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl72])).
% 172.11/25.21 thf(zip_derived_cl86946, plain, (((v_NA) = (c_Message_Omsg_ONonce @ v_NAa))),
% 172.11/25.21 inference('demod', [status(thm)],
% 172.11/25.21 [zip_derived_cl86938, zip_derived_cl3315])).
% 172.11/25.21 thf(cls_conjecture_10, conjecture,
% 172.11/25.21 (~( ( ( v_NA ) != ( c_Message_Omsg_ONonce @ v_NAa ) ) |
% 172.11/25.21 ( ( v_K ) != ( v_Ka ) ) ))).
% 172.11/25.21 thf(zf_stmt_5, negated_conjecture,
% 172.11/25.21 (( ( v_NA ) != ( c_Message_Omsg_ONonce @ v_NAa ) ) |
% 172.11/25.21 ( ( v_K ) != ( v_Ka ) )),
% 172.11/25.21 inference('cnf.neg', [status(esa)], [cls_conjecture_10])).
% 172.11/25.21 thf(zip_derived_cl660, plain,
% 172.11/25.21 ((((v_NA) != (c_Message_Omsg_ONonce @ v_NAa)) | ((v_K) != (v_Ka)))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_5])).
% 172.11/25.21 thf(zip_derived_cl659, plain, (((v_K) = (v_Ka))),
% 172.11/25.21 inference('cnf', [status(esa)], [zf_stmt_1])).
% 172.11/25.21 thf(zip_derived_cl2554, plain,
% 172.11/25.21 ((((v_NA) != (c_Message_Omsg_ONonce @ v_NAa)) | ((v_Ka) != (v_Ka)))),
% 172.11/25.21 inference('demod', [status(thm)], [zip_derived_cl660, zip_derived_cl659])).
% 172.11/25.21 thf(zip_derived_cl2555, plain, (((v_NA) != (c_Message_Omsg_ONonce @ v_NAa))),
% 172.11/25.21 inference('simplify', [status(thm)], [zip_derived_cl2554])).
% 172.11/25.21 thf(zip_derived_cl86947, plain, ($false),
% 172.11/25.21 inference('simplify_reflect-', [status(thm)],
% 172.11/25.21 [zip_derived_cl86946, zip_derived_cl2555])).
% 172.11/25.21
% 172.11/25.21 % SZS output end Refutation
% 172.11/25.21
% 172.11/25.21
% 172.11/25.21 % Terminating...
% 172.96/25.34 % Runner terminated.
% 172.96/25.36 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------