%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP052^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n001.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 9 01:46:49 PM UTC 2025
% Result : Theorem 181.36s 178.11s
% Output : Proof 181.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ITP052^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n001.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 8 18:24:23 EDT 2025
% 0.12/0.34 % CPUTime :
% 181.36/178.11 % SZS status Theorem
% 181.36/178.11 % Mode: mode503:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 181.36/178.11 % Inferences: 9705
% 181.36/178.11 % SZS output start Proof
% 181.36/178.11 thf(conj_1,conjecture,(((inf_in586391887at_nat @ (set_Pr2131844118at_nat @ p)) @ (converse_nat_nat @ (set_Pr2131844118at_nat @ p))) = bot_bo2130386637at_nat)).
% 181.36/178.11 thf(h0,negated_conjecture,(~((((inf_in586391887at_nat @ (set_Pr2131844118at_nat @ p)) @ (converse_nat_nat @ (set_Pr2131844118at_nat @ p))) = bot_bo2130386637at_nat))),inference(assume_negation,[status(cth)],[conj_1])).
% 181.36/178.11 thf(ax1251, axiom, (~(p110)|p4226), file('<stdin>', ax1251)).
% 181.36/178.11 thf(ax1252, axiom, (~(p4226)|p4225), file('<stdin>', ax1252)).
% 181.36/178.11 thf(ax7102, axiom, p110, file('<stdin>', ax7102)).
% 181.36/178.11 thf(ax1261, axiom, (~(p217)|p4221), file('<stdin>', ax1261)).
% 181.36/178.11 thf(ax1253, axiom, (~(p4225)|p4224), file('<stdin>', ax1253)).
% 181.36/178.11 thf(ax1259, axiom, (~(p4220)|~(p171)|p4219), file('<stdin>', ax1259)).
% 181.36/178.11 thf(ax1260, axiom, (~(p4221)|p4220), file('<stdin>', ax1260)).
% 181.36/178.11 thf(ax6999, axiom, p217, file('<stdin>', ax6999)).
% 181.36/178.11 thf(ax1254, axiom, (~(p4224)|p4223), file('<stdin>', ax1254)).
% 181.36/178.11 thf(ax7041, axiom, p171, file('<stdin>', ax7041)).
% 181.36/178.11 thf(ax1256, axiom, (~(p4222)|~(p10)|p4217), file('<stdin>', ax1256)).
% 181.36/178.11 thf(ax1255, axiom, (~(p4223)|p4222), file('<stdin>', ax1255)).
% 181.36/178.11 thf(nax176, axiom, (p176<=![X663:set_Pr1986765409at_nat]:((fbot_bo2130386637at_nat)=(X663)=>(X663)=(fbot_bo2130386637at_nat))), file('<stdin>', nax176)).
% 181.36/178.11 thf(ax1258, axiom, (~(p4219)|p4218), file('<stdin>', ax1258)).
% 181.36/178.11 thf(ax7202, axiom, p10, file('<stdin>', ax7202)).
% 181.36/178.11 thf(ax7035, axiom, (~(p176)|p177), file('<stdin>', ax7035)).
% 181.36/178.11 thf(ax1257, axiom, (~(p4218)|~(p4217)|p4216), file('<stdin>', ax1257)).
% 181.36/178.11 thf(ax7034, axiom, (~(p177)|~(p172)|p1), file('<stdin>', ax7034)).
% 181.36/178.11 thf(ax7211, axiom, ~(p1), file('<stdin>', ax7211)).
% 181.36/178.11 thf(pax32, axiom, (p32=>![X847:product_prod_nat_nat > capacity, X848:nat, X849:list_P559422087at_nat, X850:nat]:(fisSimp1359852763pacity @ X847 @ X848 @ X849 @ X850=>(finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ X849) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ X849)))=(fbot_bo2130386637at_nat))), file('<stdin>', pax32)).
% 181.36/178.11 thf(pax4216, axiom, (p4216=>fisSimp1359852763pacity @ (fresidu203630698pacity @ fc @ ff) @ fs @ fp @ ft), file('<stdin>', pax4216)).
% 181.36/178.11 thf(nax172, axiom, (p172<=(fbot_bo2130386637at_nat)=(finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ fp) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ fp)))), file('<stdin>', nax172)).
% 181.36/178.11 thf(ax7180, axiom, p32, file('<stdin>', ax7180)).
% 181.36/178.11 thf(c_0_23, plain, (~p110|p4226), inference(fof_simplification,[status(thm)],[ax1251])).
% 181.36/178.11 thf(c_0_24, plain, (~p4226|p4225), inference(fof_simplification,[status(thm)],[ax1252])).
% 181.36/178.11 thf(c_0_25, plain, (p4226|~p110), inference(split_conjunct,[status(thm)],[c_0_23])).
% 181.36/178.11 thf(c_0_26, plain, p110, inference(split_conjunct,[status(thm)],[ax7102])).
% 181.36/178.11 thf(c_0_27, plain, (~p217|p4221), inference(fof_simplification,[status(thm)],[ax1261])).
% 181.36/178.11 thf(c_0_28, plain, (~p4225|p4224), inference(fof_simplification,[status(thm)],[ax1253])).
% 181.36/178.11 thf(c_0_29, plain, (p4225|~p4226), inference(split_conjunct,[status(thm)],[c_0_24])).
% 181.36/178.11 thf(c_0_30, plain, p4226, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 181.36/178.11 thf(c_0_31, plain, (~p4220|~p171|p4219), inference(fof_simplification,[status(thm)],[ax1259])).
% 181.36/178.11 thf(c_0_32, plain, (~p4221|p4220), inference(fof_simplification,[status(thm)],[ax1260])).
% 181.36/178.11 thf(c_0_33, plain, (p4221|~p217), inference(split_conjunct,[status(thm)],[c_0_27])).
% 181.36/178.11 thf(c_0_34, plain, p217, inference(split_conjunct,[status(thm)],[ax6999])).
% 181.36/178.11 thf(c_0_35, plain, (~p4224|p4223), inference(fof_simplification,[status(thm)],[ax1254])).
% 181.36/178.11 thf(c_0_36, plain, (p4224|~p4225), inference(split_conjunct,[status(thm)],[c_0_28])).
% 181.36/178.11 thf(c_0_37, plain, p4225, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 181.36/178.11 thf(c_0_38, plain, (p4219|~p4220|~p171), inference(split_conjunct,[status(thm)],[c_0_31])).
% 181.36/178.11 thf(c_0_39, plain, p171, inference(split_conjunct,[status(thm)],[ax7041])).
% 181.36/178.11 thf(c_0_40, plain, (p4220|~p4221), inference(split_conjunct,[status(thm)],[c_0_32])).
% 181.36/178.11 thf(c_0_41, plain, p4221, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 181.36/178.11 thf(c_0_42, plain, (~p4222|~p10|p4217), inference(fof_simplification,[status(thm)],[ax1256])).
% 181.36/178.11 thf(c_0_43, plain, (~p4223|p4222), inference(fof_simplification,[status(thm)],[ax1255])).
% 181.36/178.11 thf(c_0_44, plain, (p4223|~p4224), inference(split_conjunct,[status(thm)],[c_0_35])).
% 181.36/178.11 thf(c_0_45, plain, p4224, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 181.36/178.11 thf(c_0_46, plain, (((fbot_bo2130386637at_nat)=(esk1390_0)|p176)&((esk1390_0)!=(fbot_bo2130386637at_nat)|p176)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax176])])])])])).
% 181.36/178.11 thf(c_0_47, plain, (~p4219|p4218), inference(fof_simplification,[status(thm)],[ax1258])).
% 181.36/178.11 thf(c_0_48, plain, (p4219|~p4220), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])])).
% 181.36/178.11 thf(c_0_49, plain, p4220, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41])])).
% 181.36/178.11 thf(c_0_50, plain, (p4217|~p4222|~p10), inference(split_conjunct,[status(thm)],[c_0_42])).
% 181.36/178.11 thf(c_0_51, plain, p10, inference(split_conjunct,[status(thm)],[ax7202])).
% 181.36/178.11 thf(c_0_52, plain, (p4222|~p4223), inference(split_conjunct,[status(thm)],[c_0_43])).
% 181.36/178.11 thf(c_0_53, plain, p4223, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_45])])).
% 181.36/178.11 thf(c_0_54, plain, (~p176|p177), inference(fof_simplification,[status(thm)],[ax7035])).
% 181.36/178.11 thf(c_0_55, plain, ((fbot_bo2130386637at_nat)=(esk1390_0)|p176), inference(split_conjunct,[status(thm)],[c_0_46])).
% 181.36/178.11 thf(c_0_56, plain, (p176|(esk1390_0)!=(fbot_bo2130386637at_nat)), inference(split_conjunct,[status(thm)],[c_0_46])).
% 181.36/178.11 thf(c_0_57, plain, (~p4218|~p4217|p4216), inference(fof_simplification,[status(thm)],[ax1257])).
% 181.36/178.11 thf(c_0_58, plain, (p4218|~p4219), inference(split_conjunct,[status(thm)],[c_0_47])).
% 181.36/178.11 thf(c_0_59, plain, p4219, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 181.36/178.11 thf(c_0_60, plain, (p4217|~p4222), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 181.36/178.11 thf(c_0_61, plain, p4222, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_53])])).
% 181.36/178.11 thf(c_0_62, plain, (~p177|~p172|p1), inference(fof_simplification,[status(thm)],[ax7034])).
% 181.36/178.11 thf(c_0_63, plain, (p177|~p176), inference(split_conjunct,[status(thm)],[c_0_54])).
% 181.36/178.11 thf(c_0_64, plain, p176, inference(csr,[status(thm)],[c_0_55, c_0_56])).
% 181.36/178.11 thf(c_0_65, plain, ~p1, inference(fof_simplification,[status(thm)],[ax7211])).
% 181.36/178.11 thf(c_0_66, plain, ![X4401:product_prod_nat_nat > capacity, X4402:nat, X4403:list_P559422087at_nat, X4404:nat]:(~p32|(~fisSimp1359852763pacity @ X4401 @ X4402 @ X4403 @ X4404|(finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ X4403) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ X4403)))=(fbot_bo2130386637at_nat))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax32])])])).
% 181.36/178.11 thf(c_0_67, plain, (~p4216|fisSimp1359852763pacity @ (fresidu203630698pacity @ fc @ ff) @ fs @ fp @ ft), inference(fof_nnf,[status(thm)],[pax4216])).
% 181.36/178.11 thf(c_0_68, plain, (p4216|~p4218|~p4217), inference(split_conjunct,[status(thm)],[c_0_57])).
% 181.36/178.11 thf(c_0_69, plain, p4218, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59])])).
% 181.36/178.11 thf(c_0_70, plain, p4217, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61])])).
% 181.36/178.11 thf(c_0_71, plain, ((fbot_bo2130386637at_nat)!=(finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ fp) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ fp)))|p172), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax172])])).
% 181.36/178.11 thf(c_0_72, plain, (p1|~p177|~p172), inference(split_conjunct,[status(thm)],[c_0_62])).
% 181.36/178.11 thf(c_0_73, plain, p177, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 181.36/178.11 thf(c_0_74, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_65])).
% 181.36/178.11 thf(c_0_75, plain, ![X78:product_prod_nat_nat > capacity, X95:nat, X98:list_P559422087at_nat, X96:nat]:((finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ X98) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ X98)))=(fbot_bo2130386637at_nat)|~p32|~fisSimp1359852763pacity @ X78 @ X95 @ X98 @ X96), inference(split_conjunct,[status(thm)],[c_0_66])).
% 181.36/178.11 thf(c_0_76, plain, p32, inference(split_conjunct,[status(thm)],[ax7180])).
% 181.36/178.11 thf(c_0_77, plain, (fisSimp1359852763pacity @ (fresidu203630698pacity @ fc @ ff) @ fs @ fp @ ft|~p4216), inference(split_conjunct,[status(thm)],[c_0_67])).
% 181.36/178.11 thf(c_0_78, plain, p4216, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])]), c_0_70])])).
% 181.36/178.11 thf(c_0_79, plain, (p172|(fbot_bo2130386637at_nat)!=(finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ fp) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ fp)))), inference(split_conjunct,[status(thm)],[c_0_71])).
% 181.36/178.11 thf(c_0_80, plain, ~p172, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])]), c_0_74])).
% 181.36/178.11 thf(c_0_81, plain, ![X78:product_prod_nat_nat > capacity, X95:nat, X98:list_P559422087at_nat, X96:nat]:((finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ X98) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ X98)))=(fbot_bo2130386637at_nat)|~fisSimp1359852763pacity @ X78 @ X95 @ X98 @ X96), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_76])])).
% 181.36/178.11 thf(c_0_82, plain, fisSimp1359852763pacity @ (fresidu203630698pacity @ fc @ ff) @ fs @ fp @ ft, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_78])])).
% 181.36/178.11 thf(c_0_83, plain, (finf_in586391887at_nat @ (fset_Pr2131844118at_nat @ fp) @ (fconverse_nat_nat @ (fset_Pr2131844118at_nat @ fp)))!=(fbot_bo2130386637at_nat), inference(sr,[status(thm)],[c_0_79, c_0_80])).
% 181.36/178.11 thf(c_0_84, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_82]), c_0_83]), ['proof']).
% 181.36/178.11 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 181.36/178.11 thf(0,theorem,(((inf_in586391887at_nat @ (set_Pr2131844118at_nat @ p)) @ (converse_nat_nat @ (set_Pr2131844118at_nat @ p))) = bot_bo2130386637at_nat),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 181.36/178.11 % SZS output end Proof
%------------------------------------------------------------------------------