%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : PHI043^2 : 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 : n019.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 02:13:41 PM UTC 2025
% Result : Theorem 19.16s 19.42s
% Output : Proof 19.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PHI043^2 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n019.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 8 23:17:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 19.16/19.42 % SZS status Theorem
% 19.16/19.42 % Mode: mode485
% 19.16/19.42 % Inferences: 4818
% 19.16/19.42 % SZS output start Proof
% 19.16/19.42 thf(def_meq_ind,definition,(meq_ind = (^[X1:mu]:(^[X2:mu]:(^[X3:$i]:(X1 = X2)))))).
% 19.16/19.42 thf(def_mtrue,definition,(mtrue = (^[X1:$i]:(~($false))))).
% 19.16/19.42 thf(def_mfalse,definition,(mfalse = (^[X1:$i]:$false))).
% 19.16/19.42 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 19.16/19.42 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 19.16/19.42 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(~(((X1 @ X3) => (~((X2 @ X3))))))))))).
% 19.16/19.42 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((X1 @ X3) => (X2 @ X3))))))).
% 19.16/19.42 thf(def_mimplied,definition,(mimplied = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((X2 @ X3) => (X1 @ X3))))))).
% 19.16/19.42 thf(def_mequiv,definition,(mequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((X1 @ X3) = (X2 @ X3))))))).
% 19.16/19.42 thf(def_mxor,definition,(mxor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(((X1 @ X3) => (X2 @ X3)) => (~(((~((X1 @ X3))) => (~((X2 @ X3)))))))))))).
% 19.16/19.42 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:((X1 @ X3) @ X2)))))).
% 19.16/19.42 thf(def_mforall_indset,definition,(mforall_indset = (^[X1:(mu>$i>$o)>$i>$o]:(^[X2:$i]:(![X3:mu>$i>$o]:((X1 @ X3) @ X2)))))).
% 19.16/19.42 thf(def_mforall_prop,definition,(mforall_prop = (^[X1:($i>$o)>$i>$o]:(^[X2:$i]:(![X3:$i>$o]:((X1 @ X3) @ X2)))))).
% 19.16/19.42 thf(def_mexists_ind,definition,(mexists_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(~((![X3:mu]:(~(((X1 @ X3) @ X2)))))))))).
% 19.16/19.42 thf(def_mexists_indset,definition,(mexists_indset = (^[X1:(mu>$i>$o)>$i>$o]:(^[X2:$i]:(~((![X3:mu>$i>$o]:(~(((X1 @ X3) @ X2)))))))))).
% 19.16/19.42 thf(def_mexists_prop,definition,(mexists_prop = (^[X1:($i>$o)>$i>$o]:(^[X2:$i]:(~((![X3:$i>$o]:(~(((X1 @ X3) @ X2)))))))))).
% 19.16/19.42 thf(def_mbox_generic,definition,(mbox_generic = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(![X4:$i]:(((X1 @ X3) @ X4) => (X2 @ X4)))))))).
% 19.16/19.42 thf(def_mdia_generic,definition,(mdia_generic = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(~((![X4:$i]:(((X1 @ X3) @ X4) => (~((X2 @ X4)))))))))))).
% 19.16/19.42 thf(def_mbox,definition,(mbox = (mbox_generic @ rel))).
% 19.16/19.42 thf(def_mdia,definition,(mdia = (mdia_generic @ rel))).
% 19.16/19.42 thf(def_mvalid,definition,(mvalid = (!!))).
% 19.16/19.42 thf(def_minvalid,definition,(minvalid = (^[X1:$i>$o]:(![X2:$i]:(~((X1 @ X2))))))).
% 19.16/19.42 thf(def_mforall_eiw_ind,definition,(mforall_eiw_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:(((eiw_ind @ X2) @ X3) => ((X1 @ X3) @ X2))))))).
% 19.16/19.42 thf(def_mexists_eiw_ind,definition,(mexists_eiw_ind = (^[X1:mu>$i>$o]:(mnot @ (mforall_eiw_ind @ (^[X2:mu]:(mnot @ (X1 @ X2)))))))).
% 19.16/19.42 thf(possible_instantiation_of_the_positive_variable_domain,conjecture,(![X1:$i]:(![X2:mu>$i>$o]:(((p @ X2) @ X1) => (~((![X3:$i]:(((rel @ X1) @ X3) => (~((~((![X4:mu]:(((eiw_ind @ X3) @ X4) => (~(((X2 @ X4) @ X3))))))))))))))))).
% 19.16/19.42 thf(h0,negated_conjecture,(~((![X1:$i]:(![X2:mu>$i>$o]:(((p @ X2) @ X1) => (~((![X3:$i]:(((rel @ X1) @ X3) => (![X4:mu]:(((eiw_ind @ X3) @ X4) => (~(((X2 @ X4) @ X3)))))))))))))),inference(assume_negation,[status(cth)],[possible_instantiation_of_the_positive_variable_domain])).
% 19.16/19.42 thf(ax2902, axiom, (p1|~(p5)), file('<stdin>', ax2902)).
% 19.16/19.42 thf(ax2906, axiom, ~(p1), file('<stdin>', ax2906)).
% 19.16/19.42 thf(ax2664, axiom, (~(p173)|p180), file('<stdin>', ax2664)).
% 19.16/19.42 thf(ax2901, axiom, (p5|~(p6)), file('<stdin>', ax2901)).
% 19.16/19.42 thf(ax2663, axiom, (~(p180)|p179), file('<stdin>', ax2663)).
% 19.16/19.42 thf(ax2672, axiom, p173, file('<stdin>', ax2672)).
% 19.16/19.42 thf(ax2864, axiom, (~(p3)|~(p43)), file('<stdin>', ax2864)).
% 19.16/19.42 thf(ax2678, axiom, (~(p4)|p161), file('<stdin>', ax2678)).
% 19.16/19.42 thf(ax2662, axiom, (~(p179)|p43|p178), file('<stdin>', ax2662)).
% 19.16/19.42 thf(ax2904, axiom, p3, file('<stdin>', ax2904)).
% 19.16/19.42 thf(ax2675, axiom, (~(p161)|p164), file('<stdin>', ax2675)).
% 19.16/19.42 thf(ax2903, axiom, p4, file('<stdin>', ax2903)).
% 19.16/19.42 thf(ax2660, axiom, (~(p177)|~(p175)|~(p7)), file('<stdin>', ax2660)).
% 19.16/19.42 thf(ax2900, axiom, (p6|p7), file('<stdin>', ax2900)).
% 19.16/19.42 thf(ax2661, axiom, (~(p178)|p177), file('<stdin>', ax2661)).
% 19.16/19.42 thf(ax1371, axiom, (~(p8)|p906), file('<stdin>', ax1371)).
% 19.16/19.42 thf(ax2899, axiom, (p6|p8), file('<stdin>', ax2899)).
% 19.16/19.42 thf(nax1236, axiom, (p1236<=(f__30)=(f__30)), file('<stdin>', nax1236)).
% 19.16/19.42 thf(ax2658, axiom, (~(p164)|p181), file('<stdin>', ax2658)).
% 19.16/19.42 thf(ax1372, axiom, (~(p906)|~(p767)|p905), file('<stdin>', ax1372)).
% 19.16/19.42 thf(ax392, axiom, (p1021|p1222|~(p1236)), file('<stdin>', ax392)).
% 19.16/19.42 thf(ax2659, axiom, (~(p181)|~(p176)|p175), file('<stdin>', ax2659)).
% 19.16/19.42 thf(pax1223, axiom, (p1223=>(feiw_ind @ f__21 @ f__30=>~(f__1 @ f__30 @ f__21))), file('<stdin>', pax1223)).
% 19.16/19.42 thf(pax1020, axiom, (p1020=>feiw_ind @ f__21 @ f__30), file('<stdin>', pax1020)).
% 19.16/19.42 thf(pax1222, axiom, (p1222=>f__1 @ f__30 @ f__21), file('<stdin>', pax1222)).
% 19.16/19.42 thf(ax406, axiom, (~(p905)|p1223), file('<stdin>', ax406)).
% 19.16/19.42 thf(ax770, axiom, (p910|~(p1021)), file('<stdin>', ax770)).
% 19.16/19.42 thf(ax1367, axiom, (p768|~(p910)), file('<stdin>', ax1367)).
% 19.16/19.42 thf(ax2007, axiom, (p176|~(p623)), file('<stdin>', ax2007)).
% 19.16/19.42 thf(ax1595, axiom, (p623|~(p768)), file('<stdin>', ax1595)).
% 19.16/19.42 thf(ax771, axiom, (p910|p1020), file('<stdin>', ax771)).
% 19.16/19.42 thf(ax1596, axiom, (p623|p767), file('<stdin>', ax1596)).
% 19.16/19.42 thf(c_0_32, plain, (p1|~p5), inference(fof_simplification,[status(thm)],[ax2902])).
% 19.16/19.42 thf(c_0_33, plain, ~p1, inference(fof_simplification,[status(thm)],[ax2906])).
% 19.16/19.42 thf(c_0_34, plain, (~p173|p180), inference(fof_simplification,[status(thm)],[ax2664])).
% 19.16/19.42 thf(c_0_35, plain, (p5|~p6), inference(fof_simplification,[status(thm)],[ax2901])).
% 19.16/19.42 thf(c_0_36, plain, (p1|~p5), inference(split_conjunct,[status(thm)],[c_0_32])).
% 19.16/19.42 thf(c_0_37, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_33])).
% 19.16/19.42 thf(c_0_38, plain, (~p180|p179), inference(fof_simplification,[status(thm)],[ax2663])).
% 19.16/19.42 thf(c_0_39, plain, (p180|~p173), inference(split_conjunct,[status(thm)],[c_0_34])).
% 19.16/19.42 thf(c_0_40, plain, p173, inference(split_conjunct,[status(thm)],[ax2672])).
% 19.16/19.42 thf(c_0_41, plain, (~p3|~p43), inference(fof_simplification,[status(thm)],[ax2864])).
% 19.16/19.42 thf(c_0_42, plain, (~p4|p161), inference(fof_simplification,[status(thm)],[ax2678])).
% 19.16/19.42 thf(c_0_43, plain, (p5|~p6), inference(split_conjunct,[status(thm)],[c_0_35])).
% 19.16/19.42 thf(c_0_44, plain, ~p5, inference(sr,[status(thm)],[c_0_36, c_0_37])).
% 19.16/19.42 thf(c_0_45, plain, (~p179|p43|p178), inference(fof_simplification,[status(thm)],[ax2662])).
% 19.16/19.42 thf(c_0_46, plain, (p179|~p180), inference(split_conjunct,[status(thm)],[c_0_38])).
% 19.16/19.42 thf(c_0_47, plain, p180, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 19.16/19.42 thf(c_0_48, plain, (~p3|~p43), inference(split_conjunct,[status(thm)],[c_0_41])).
% 19.16/19.42 thf(c_0_49, plain, p3, inference(split_conjunct,[status(thm)],[ax2904])).
% 19.16/19.42 thf(c_0_50, plain, (~p161|p164), inference(fof_simplification,[status(thm)],[ax2675])).
% 19.16/19.42 thf(c_0_51, plain, (p161|~p4), inference(split_conjunct,[status(thm)],[c_0_42])).
% 19.16/19.42 thf(c_0_52, plain, p4, inference(split_conjunct,[status(thm)],[ax2903])).
% 19.16/19.42 thf(c_0_53, plain, (~p177|~p175|~p7), inference(fof_simplification,[status(thm)],[ax2660])).
% 19.16/19.42 thf(c_0_54, plain, (p6|p7), inference(split_conjunct,[status(thm)],[ax2900])).
% 19.16/19.42 thf(c_0_55, plain, ~p6, inference(sr,[status(thm)],[c_0_43, c_0_44])).
% 19.16/19.42 thf(c_0_56, plain, (~p178|p177), inference(fof_simplification,[status(thm)],[ax2661])).
% 19.16/19.42 thf(c_0_57, plain, (p43|p178|~p179), inference(split_conjunct,[status(thm)],[c_0_45])).
% 19.16/19.42 thf(c_0_58, plain, p179, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 19.16/19.42 thf(c_0_59, plain, ~p43, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 19.16/19.42 thf(c_0_60, plain, (~p8|p906), inference(fof_simplification,[status(thm)],[ax1371])).
% 19.16/19.42 thf(c_0_61, plain, (p6|p8), inference(split_conjunct,[status(thm)],[ax2899])).
% 19.16/19.42 thf(c_0_62, plain, ((f__30)!=(f__30)|p1236), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1236])])).
% 19.16/19.42 thf(c_0_63, plain, (~p164|p181), inference(fof_simplification,[status(thm)],[ax2658])).
% 19.16/19.42 thf(c_0_64, plain, (p164|~p161), inference(split_conjunct,[status(thm)],[c_0_50])).
% 19.16/19.42 thf(c_0_65, plain, p161, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 19.16/19.42 thf(c_0_66, plain, (~p177|~p175|~p7), inference(split_conjunct,[status(thm)],[c_0_53])).
% 19.16/19.42 thf(c_0_67, plain, p7, inference(sr,[status(thm)],[c_0_54, c_0_55])).
% 19.16/19.42 thf(c_0_68, plain, (p177|~p178), inference(split_conjunct,[status(thm)],[c_0_56])).
% 19.16/19.42 thf(c_0_69, plain, p178, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_58])]), c_0_59])).
% 19.16/19.42 thf(c_0_70, plain, (~p906|~p767|p905), inference(fof_simplification,[status(thm)],[ax1372])).
% 19.16/19.42 thf(c_0_71, plain, (p906|~p8), inference(split_conjunct,[status(thm)],[c_0_60])).
% 19.16/19.42 thf(c_0_72, plain, p8, inference(sr,[status(thm)],[c_0_61, c_0_55])).
% 19.16/19.42 thf(c_0_73, plain, (p1021|p1222|~p1236), inference(fof_simplification,[status(thm)],[ax392])).
% 19.16/19.42 thf(c_0_74, plain, (p1236|(f__30)!=(f__30)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 19.16/19.42 thf(c_0_75, plain, (~p181|~p176|p175), inference(fof_simplification,[status(thm)],[ax2659])).
% 19.16/19.42 thf(c_0_76, plain, (p181|~p164), inference(split_conjunct,[status(thm)],[c_0_63])).
% 19.16/19.42 thf(c_0_77, plain, p164, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 19.16/19.42 thf(c_0_78, plain, (~p175|~p177), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 19.16/19.42 thf(c_0_79, plain, p177, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])])).
% 19.16/19.42 thf(c_0_80, plain, (~p1223|(~feiw_ind @ f__21 @ f__30|~f__1 @ f__30 @ f__21)), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1223])])).
% 19.16/19.42 thf(c_0_81, plain, (~p1020|feiw_ind @ f__21 @ f__30), inference(fof_nnf,[status(thm)],[pax1020])).
% 19.16/19.42 thf(c_0_82, plain, (~p1222|f__1 @ f__30 @ f__21), inference(fof_nnf,[status(thm)],[pax1222])).
% 19.16/19.42 thf(c_0_83, plain, (p905|~p906|~p767), inference(split_conjunct,[status(thm)],[c_0_70])).
% 19.16/19.42 thf(c_0_84, plain, p906, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_72])])).
% 19.16/19.42 thf(c_0_85, plain, (p1021|p1222|~p1236), inference(split_conjunct,[status(thm)],[c_0_73])).
% 19.16/19.42 thf(c_0_86, plain, p1236, inference(cn,[status(thm)],[c_0_74])).
% 19.16/19.42 thf(c_0_87, plain, (~p905|p1223), inference(fof_simplification,[status(thm)],[ax406])).
% 19.16/19.42 thf(c_0_88, plain, (p910|~p1021), inference(fof_simplification,[status(thm)],[ax770])).
% 19.16/19.42 thf(c_0_89, plain, (p768|~p910), inference(fof_simplification,[status(thm)],[ax1367])).
% 19.16/19.42 thf(c_0_90, plain, (p176|~p623), inference(fof_simplification,[status(thm)],[ax2007])).
% 19.16/19.42 thf(c_0_91, plain, (p623|~p768), inference(fof_simplification,[status(thm)],[ax1595])).
% 19.16/19.42 thf(c_0_92, plain, (p175|~p181|~p176), inference(split_conjunct,[status(thm)],[c_0_75])).
% 19.16/19.42 thf(c_0_93, plain, p181, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_77])])).
% 19.16/19.42 thf(c_0_94, plain, ~p175, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_79])])).
% 19.16/19.42 thf(c_0_95, plain, (~p1223|~feiw_ind @ f__21 @ f__30|~f__1 @ f__30 @ f__21), inference(split_conjunct,[status(thm)],[c_0_80])).
% 19.16/19.42 thf(c_0_96, plain, (feiw_ind @ f__21 @ f__30|~p1020), inference(split_conjunct,[status(thm)],[c_0_81])).
% 19.16/19.42 thf(c_0_97, plain, (f__1 @ f__30 @ f__21|~p1222), inference(split_conjunct,[status(thm)],[c_0_82])).
% 19.16/19.42 thf(c_0_98, plain, (p905|~p767), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84])])).
% 19.16/19.42 thf(c_0_99, plain, (p1222|p1021), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_86])])).
% 19.16/19.42 thf(c_0_100, plain, (p1223|~p905), inference(split_conjunct,[status(thm)],[c_0_87])).
% 19.16/19.42 thf(c_0_101, plain, (p910|~p1021), inference(split_conjunct,[status(thm)],[c_0_88])).
% 19.16/19.42 thf(c_0_102, plain, (p768|~p910), inference(split_conjunct,[status(thm)],[c_0_89])).
% 19.16/19.42 thf(c_0_103, plain, (p910|p1020), inference(split_conjunct,[status(thm)],[ax771])).
% 19.16/19.42 thf(c_0_104, plain, (p623|p767), inference(split_conjunct,[status(thm)],[ax1596])).
% 19.16/19.42 thf(c_0_105, plain, (p176|~p623), inference(split_conjunct,[status(thm)],[c_0_90])).
% 19.16/19.42 thf(c_0_106, plain, (p623|~p768), inference(split_conjunct,[status(thm)],[c_0_91])).
% 19.16/19.42 thf(c_0_107, plain, ~p176, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_93])]), c_0_94])).
% 19.16/19.42 thf(c_0_108, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_95, c_0_96, c_0_97, c_0_98, c_0_99, c_0_100, c_0_101, c_0_102, c_0_103, c_0_104, c_0_105, c_0_106, c_0_107]), ['proof']).
% 19.16/19.42 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 19.16/19.42 thf(0,theorem,(![X1:$i]:(![X2:mu>$i>$o]:(((p @ X2) @ X1) => (~((![X3:$i]:(((rel @ X1) @ X3) => (~((~((![X4:mu]:(((eiw_ind @ X3) @ X4) => (~(((X2 @ X4) @ X3)))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 19.16/19.42 % SZS output end Proof
%------------------------------------------------------------------------------