%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP205^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 : n016.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:47:17 PM UTC 2025
% Result : Theorem 55.88s 55.39s
% Output : Proof 55.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP205^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 18:44:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 55.88/55.39 % SZS status Theorem
% 55.88/55.39 % Mode: mode498:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 55.88/55.39 % Inferences: 1347
% 55.88/55.39 % SZS output start Proof
% 55.88/55.39 thf(conj_0,conjecture,((ord_le282106107riable @ ((sup_sup_set_variable @ ua) @ (static_BVG @ (the_game @ (produc293487213n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ ((compose @ alpha) @ beta))))))) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ alpha))) @ beta)))).
% 55.88/55.39 thf(h0,negated_conjecture,(~(((ord_le282106107riable @ ((sup_sup_set_variable @ ua) @ (static_BVG @ (the_game @ (produc293487213n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ ((compose @ alpha) @ beta))))))) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ alpha))) @ beta))))),inference(assume_negation,[status(cth)],[conj_0])).
% 55.88/55.39 thf(ax4267, axiom, (~(p45)|p668), file('<stdin>', ax4267)).
% 55.88/55.39 thf(ax3923, axiom, (~(p668)|p995), file('<stdin>', ax3923)).
% 55.88/55.39 thf(ax4910, axiom, p45, file('<stdin>', ax4910)).
% 55.88/55.39 thf(ax3925, axiom, (~(p994)|~(p2)|~(p993)), file('<stdin>', ax3925)).
% 55.88/55.39 thf(ax3924, axiom, (~(p995)|p994), file('<stdin>', ax3924)).
% 55.88/55.39 thf(ax4272, axiom, (~(p43)|p663), file('<stdin>', ax4272)).
% 55.88/55.39 thf(ax4649, axiom, (~(p34)|p298), file('<stdin>', ax4649)).
% 55.88/55.39 thf(ax4652, axiom, (~(p45)|p295), file('<stdin>', ax4652)).
% 55.88/55.39 thf(ax4953, axiom, p2, file('<stdin>', ax4953)).
% 55.88/55.39 thf(ax3926, axiom, (~(p663)|p992), file('<stdin>', ax3926)).
% 55.88/55.39 thf(ax4912, axiom, p43, file('<stdin>', ax4912)).
% 55.88/55.39 thf(ax628, axiom, (~(p298)|p1483), file('<stdin>', ax628)).
% 55.88/55.39 thf(ax4921, axiom, p34, file('<stdin>', ax4921)).
% 55.88/55.39 thf(ax608, axiom, (~(p295)|p2878), file('<stdin>', ax608)).
% 55.88/55.39 thf(ax3820, axiom, (~(p39)|p1096), file('<stdin>', ax3820)).
% 55.88/55.39 thf(ax4384, axiom, (~(p31)|p551), file('<stdin>', ax4384)).
% 55.88/55.39 thf(ax3772, axiom, (~(p42)|p1142), file('<stdin>', ax3772)).
% 55.88/55.39 thf(pax26, axiom, (p26=>![X557:set_variable, X553:set_variable, X560:set_variable]:(fsup_sup_set_variable @ (fsup_sup_set_variable @ X557 @ X553) @ X560)=(fsup_sup_set_variable @ X557 @ (fsup_sup_set_variable @ X553 @ X560))), file('<stdin>', pax26)).
% 55.88/55.39 thf(nax993, axiom, (p993<=![X246:set_variable]:(ford_le282106107riable @ X246 @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))=>![X247:set_variable]:(ford_le282106107riable @ X247 @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))=>~((fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))=(fsup_sup_set_variable @ X246 @ X247))))), file('<stdin>', nax993)).
% 55.88/55.39 thf(pax27, axiom, (p27=>![X557:set_variable, X553:set_variable, X560:set_variable, X561:set_variable]:((X557)=(fsup_sup_set_variable @ X553 @ X560)=>(fsup_sup_set_variable @ X561 @ X557)=(fsup_sup_set_variable @ X553 @ (fsup_sup_set_variable @ X561 @ X560)))), file('<stdin>', pax27)).
% 55.88/55.39 thf(pax16, axiom, (p16=>![X564:set_variable, X553:set_variable]:(fsup_sup_set_variable @ X564 @ (fsup_sup_set_variable @ X564 @ X553))=(fsup_sup_set_variable @ X564 @ X553)), file('<stdin>', pax16)).
% 55.88/55.39 thf(ax3927, axiom, (~(p992)|~(p2)|p991), file('<stdin>', ax3927)).
% 55.88/55.39 thf(ax610, axiom, (~(p2877)|~(p1483)|~(p2876)), file('<stdin>', ax610)).
% 55.88/55.39 thf(ax609, axiom, (~(p2878)|p2877), file('<stdin>', ax609)).
% 55.88/55.39 thf(ax3821, axiom, (~(p1096)|p1095), file('<stdin>', ax3821)).
% 55.88/55.39 thf(ax4916, axiom, p39, file('<stdin>', ax4916)).
% 55.88/55.39 thf(ax3222, axiom, (~(p480)|p1480), file('<stdin>', ax3222)).
% 55.88/55.39 thf(ax831, axiom, (~(p551)|p2721), file('<stdin>', ax831)).
% 55.88/55.39 thf(ax4924, axiom, p31, file('<stdin>', ax4924)).
% 55.88/55.39 thf(ax3729, axiom, (~(p1142)|p1183), file('<stdin>', ax3729)).
% 55.88/55.39 thf(ax4913, axiom, p42, file('<stdin>', ax4913)).
% 55.88/55.39 thf(nax1182, axiom, (p1182<=(fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))))), file('<stdin>', nax1182)).
% 55.88/55.39 thf(ax4929, axiom, p26, file('<stdin>', ax4929)).
% 55.88/55.39 thf(ax4928, axiom, p27, file('<stdin>', ax4928)).
% 55.88/55.39 thf(ax4939, axiom, p16, file('<stdin>', ax4939)).
% 55.88/55.39 thf(pax991, axiom, (p991=>(fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta))))))), file('<stdin>', pax991)).
% 55.88/55.39 thf(ax3822, axiom, (~(p1095)|~(p1)|p1094), file('<stdin>', ax3822)).
% 55.88/55.39 thf(ax3221, axiom, (~(p1480)|p1481), file('<stdin>', ax3221)).
% 55.88/55.39 thf(ax4457, axiom, p480, file('<stdin>', ax4457)).
% 55.88/55.39 thf(ax832, axiom, (~(p2721)|p2720), file('<stdin>', ax832)).
% 55.88/55.39 thf(ax3730, axiom, (~(p1183)|~(p1182)|p1114), file('<stdin>', ax3730)).
% 55.88/55.39 thf(nax2876, axiom, (p2876<=![X46:set_variable]:(ford_le282106107riable @ X46 @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))=>![X47:set_variable]:(ford_le282106107riable @ X47 @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=>~((fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ X46 @ X47))))), file('<stdin>', nax2876)).
% 55.88/55.39 thf(ax3220, axiom, (~(p1481)|~(p1094)|p1479), file('<stdin>', ax3220)).
% 55.88/55.39 thf(ax4954, axiom, p1, file('<stdin>', ax4954)).
% 55.88/55.39 thf(ax833, axiom, (~(p2720)|~(p1114)|p1607), file('<stdin>', ax833)).
% 55.88/55.39 thf(pax1479, axiom, (p1479=>(fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))), file('<stdin>', pax1479)).
% 55.88/55.39 thf(nax84, axiom, (p84<=ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))), file('<stdin>', nax84)).
% 55.88/55.39 thf(ax4871, axiom, ~(p84), file('<stdin>', ax4871)).
% 55.88/55.39 thf(pax1607, axiom, (p1607=>ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))), file('<stdin>', pax1607)).
% 55.88/55.39 thf(c_0_49, plain, (~p45|p668), inference(fof_simplification,[status(thm)],[ax4267])).
% 55.88/55.39 thf(c_0_50, plain, (~p668|p995), inference(fof_simplification,[status(thm)],[ax3923])).
% 55.88/55.39 thf(c_0_51, plain, (p668|~p45), inference(split_conjunct,[status(thm)],[c_0_49])).
% 55.88/55.39 thf(c_0_52, plain, p45, inference(split_conjunct,[status(thm)],[ax4910])).
% 55.88/55.39 thf(c_0_53, plain, (~p994|~p2|~p993), inference(fof_simplification,[status(thm)],[ax3925])).
% 55.88/55.39 thf(c_0_54, plain, (~p995|p994), inference(fof_simplification,[status(thm)],[ax3924])).
% 55.88/55.39 thf(c_0_55, plain, (p995|~p668), inference(split_conjunct,[status(thm)],[c_0_50])).
% 55.88/55.39 thf(c_0_56, plain, p668, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 55.88/55.39 thf(c_0_57, plain, (~p43|p663), inference(fof_simplification,[status(thm)],[ax4272])).
% 55.88/55.39 thf(c_0_58, plain, (~p34|p298), inference(fof_simplification,[status(thm)],[ax4649])).
% 55.88/55.39 thf(c_0_59, plain, (~p45|p295), inference(fof_simplification,[status(thm)],[ax4652])).
% 55.88/55.39 thf(c_0_60, plain, (~p994|~p2|~p993), inference(split_conjunct,[status(thm)],[c_0_53])).
% 55.88/55.39 thf(c_0_61, plain, p2, inference(split_conjunct,[status(thm)],[ax4953])).
% 55.88/55.39 thf(c_0_62, plain, (p994|~p995), inference(split_conjunct,[status(thm)],[c_0_54])).
% 55.88/55.39 thf(c_0_63, plain, p995, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 55.88/55.39 thf(c_0_64, plain, (~p663|p992), inference(fof_simplification,[status(thm)],[ax3926])).
% 55.88/55.39 thf(c_0_65, plain, (p663|~p43), inference(split_conjunct,[status(thm)],[c_0_57])).
% 55.88/55.39 thf(c_0_66, plain, p43, inference(split_conjunct,[status(thm)],[ax4912])).
% 55.88/55.39 thf(c_0_67, plain, (~p298|p1483), inference(fof_simplification,[status(thm)],[ax628])).
% 55.88/55.39 thf(c_0_68, plain, (p298|~p34), inference(split_conjunct,[status(thm)],[c_0_58])).
% 55.88/55.39 thf(c_0_69, plain, p34, inference(split_conjunct,[status(thm)],[ax4921])).
% 55.88/55.39 thf(c_0_70, plain, (~p295|p2878), inference(fof_simplification,[status(thm)],[ax608])).
% 55.88/55.39 thf(c_0_71, plain, (p295|~p45), inference(split_conjunct,[status(thm)],[c_0_59])).
% 55.88/55.39 thf(c_0_72, plain, (~p39|p1096), inference(fof_simplification,[status(thm)],[ax3820])).
% 55.88/55.39 thf(c_0_73, plain, (~p31|p551), inference(fof_simplification,[status(thm)],[ax4384])).
% 55.88/55.39 thf(c_0_74, plain, (~p42|p1142), inference(fof_simplification,[status(thm)],[ax3772])).
% 55.88/55.39 thf(c_0_75, plain, ![X4993:set_variable, X4994:set_variable, X4995:set_variable]:(~p26|(fsup_sup_set_variable @ (fsup_sup_set_variable @ X4993 @ X4994) @ X4995)=(fsup_sup_set_variable @ X4993 @ (fsup_sup_set_variable @ X4994 @ X4995))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax26])])])).
% 55.88/55.39 thf(c_0_76, plain, ((ford_le282106107riable @ esk1119_0 @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))|p993)&((ford_le282106107riable @ esk1120_0 @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))|p993)&((fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))=(fsup_sup_set_variable @ esk1119_0 @ esk1120_0)|p993))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax993])])])])])).
% 55.88/55.39 thf(c_0_77, plain, (~p993|~p994), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61])])).
% 55.88/55.39 thf(c_0_78, plain, p994, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_62, c_0_63])])).
% 55.88/55.39 thf(c_0_79, plain, ![X4985:set_variable, X4986:set_variable, X4987:set_variable, X4988:set_variable]:(~p27|((X4985)!=(fsup_sup_set_variable @ X4986 @ X4987)|(fsup_sup_set_variable @ X4988 @ X4985)=(fsup_sup_set_variable @ X4986 @ (fsup_sup_set_variable @ X4988 @ X4987)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax27])])])).
% 55.88/55.39 thf(c_0_80, plain, ![X5033:set_variable, X5034:set_variable]:(~p16|(fsup_sup_set_variable @ X5033 @ (fsup_sup_set_variable @ X5033 @ X5034))=(fsup_sup_set_variable @ X5033 @ X5034)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax16])])])).
% 55.88/55.39 thf(c_0_81, plain, (~p992|~p2|p991), inference(fof_simplification,[status(thm)],[ax3927])).
% 55.88/55.39 thf(c_0_82, plain, (p992|~p663), inference(split_conjunct,[status(thm)],[c_0_64])).
% 55.88/55.39 thf(c_0_83, plain, p663, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 55.88/55.39 thf(c_0_84, plain, (~p2877|~p1483|~p2876), inference(fof_simplification,[status(thm)],[ax610])).
% 55.88/55.39 thf(c_0_85, plain, (p1483|~p298), inference(split_conjunct,[status(thm)],[c_0_67])).
% 55.88/55.39 thf(c_0_86, plain, p298, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])])).
% 55.88/55.39 thf(c_0_87, plain, (~p2878|p2877), inference(fof_simplification,[status(thm)],[ax609])).
% 55.88/55.39 thf(c_0_88, plain, (p2878|~p295), inference(split_conjunct,[status(thm)],[c_0_70])).
% 55.88/55.39 thf(c_0_89, plain, p295, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_52])])).
% 55.88/55.39 thf(c_0_90, plain, (~p1096|p1095), inference(fof_simplification,[status(thm)],[ax3821])).
% 55.88/55.39 thf(c_0_91, plain, (p1096|~p39), inference(split_conjunct,[status(thm)],[c_0_72])).
% 55.88/55.39 thf(c_0_92, plain, p39, inference(split_conjunct,[status(thm)],[ax4916])).
% 55.88/55.39 thf(c_0_93, plain, (~p480|p1480), inference(fof_simplification,[status(thm)],[ax3222])).
% 55.88/55.39 thf(c_0_94, plain, (~p551|p2721), inference(fof_simplification,[status(thm)],[ax831])).
% 55.88/55.39 thf(c_0_95, plain, (p551|~p31), inference(split_conjunct,[status(thm)],[c_0_73])).
% 55.88/55.39 thf(c_0_96, plain, p31, inference(split_conjunct,[status(thm)],[ax4924])).
% 55.88/55.39 thf(c_0_97, plain, (~p1142|p1183), inference(fof_simplification,[status(thm)],[ax3729])).
% 55.88/55.39 thf(c_0_98, plain, (p1142|~p42), inference(split_conjunct,[status(thm)],[c_0_74])).
% 55.88/55.39 thf(c_0_99, plain, p42, inference(split_conjunct,[status(thm)],[ax4913])).
% 55.88/55.39 thf(c_0_100, plain, ((fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))!=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))))|p1182), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1182])])).
% 55.88/55.39 thf(c_0_101, plain, ![X3:set_variable, X4:set_variable, X6:set_variable]:((fsup_sup_set_variable @ (fsup_sup_set_variable @ X3 @ X4) @ X6)=(fsup_sup_set_variable @ X3 @ (fsup_sup_set_variable @ X4 @ X6))|~p26), inference(split_conjunct,[status(thm)],[c_0_75])).
% 55.88/55.39 thf(c_0_102, plain, p26, inference(split_conjunct,[status(thm)],[ax4929])).
% 55.88/55.39 thf(c_0_103, plain, ((fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))=(fsup_sup_set_variable @ esk1119_0 @ esk1120_0)|p993), inference(split_conjunct,[status(thm)],[c_0_76])).
% 55.88/55.39 thf(c_0_104, plain, ~p993, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_78])])).
% 55.88/55.39 thf(c_0_105, plain, ![X3:set_variable, X4:set_variable, X7:set_variable, X6:set_variable]:((fsup_sup_set_variable @ X7 @ X3)=(fsup_sup_set_variable @ X4 @ (fsup_sup_set_variable @ X7 @ X6))|~p27|(X3)!=(fsup_sup_set_variable @ X4 @ X6)), inference(split_conjunct,[status(thm)],[c_0_79])).
% 55.88/55.39 thf(c_0_106, plain, p27, inference(split_conjunct,[status(thm)],[ax4928])).
% 55.88/55.39 thf(c_0_107, plain, ![X3:set_variable, X4:set_variable]:((fsup_sup_set_variable @ X3 @ (fsup_sup_set_variable @ X3 @ X4))=(fsup_sup_set_variable @ X3 @ X4)|~p16), inference(split_conjunct,[status(thm)],[c_0_80])).
% 55.88/55.39 thf(c_0_108, plain, p16, inference(split_conjunct,[status(thm)],[ax4939])).
% 55.88/55.39 thf(c_0_109, plain, (~p991|(fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta))))))), inference(fof_nnf,[status(thm)],[pax991])).
% 55.88/55.39 thf(c_0_110, plain, (p991|~p992|~p2), inference(split_conjunct,[status(thm)],[c_0_81])).
% 55.88/55.39 thf(c_0_111, plain, p992, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 55.88/55.39 thf(c_0_112, plain, (~p2877|~p1483|~p2876), inference(split_conjunct,[status(thm)],[c_0_84])).
% 55.88/55.39 thf(c_0_113, plain, p1483, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_86])])).
% 55.88/55.39 thf(c_0_114, plain, (p2877|~p2878), inference(split_conjunct,[status(thm)],[c_0_87])).
% 55.88/55.39 thf(c_0_115, plain, p2878, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 55.88/55.39 thf(c_0_116, plain, (~p1095|~p1|p1094), inference(fof_simplification,[status(thm)],[ax3822])).
% 55.88/55.39 thf(c_0_117, plain, (p1095|~p1096), inference(split_conjunct,[status(thm)],[c_0_90])).
% 55.88/55.39 thf(c_0_118, plain, p1096, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_92])])).
% 55.88/55.39 thf(c_0_119, plain, (~p1480|p1481), inference(fof_simplification,[status(thm)],[ax3221])).
% 55.88/55.39 thf(c_0_120, plain, (p1480|~p480), inference(split_conjunct,[status(thm)],[c_0_93])).
% 55.88/55.39 thf(c_0_121, plain, p480, inference(split_conjunct,[status(thm)],[ax4457])).
% 55.88/55.39 thf(c_0_122, plain, (~p2721|p2720), inference(fof_simplification,[status(thm)],[ax832])).
% 55.88/55.39 thf(c_0_123, plain, (p2721|~p551), inference(split_conjunct,[status(thm)],[c_0_94])).
% 55.88/55.39 thf(c_0_124, plain, p551, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_96])])).
% 55.88/55.39 thf(c_0_125, plain, (~p1183|~p1182|p1114), inference(fof_simplification,[status(thm)],[ax3730])).
% 55.88/55.39 thf(c_0_126, plain, (p1183|~p1142), inference(split_conjunct,[status(thm)],[c_0_97])).
% 55.88/55.39 thf(c_0_127, plain, p1142, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 55.88/55.39 thf(c_0_128, plain, (p1182|(fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))!=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))))), inference(split_conjunct,[status(thm)],[c_0_100])).
% 55.88/55.39 thf(c_0_129, plain, ![X3:set_variable, X4:set_variable, X6:set_variable]:(fsup_sup_set_variable @ (fsup_sup_set_variable @ X3 @ X4) @ X6)=(fsup_sup_set_variable @ X3 @ (fsup_sup_set_variable @ X4 @ X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_102])])).
% 55.88/55.39 thf(c_0_130, plain, (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))=(fsup_sup_set_variable @ esk1119_0 @ esk1120_0), inference(sr,[status(thm)],[c_0_103, c_0_104])).
% 55.88/55.39 thf(c_0_131, plain, ![X3:set_variable, X4:set_variable, X6:set_variable]:(fsup_sup_set_variable @ X3 @ (fsup_sup_set_variable @ X4 @ X6))=(fsup_sup_set_variable @ X4 @ (fsup_sup_set_variable @ X3 @ X6)), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_105, c_0_106])])])).
% 55.88/55.39 thf(c_0_132, plain, ![X3:set_variable, X4:set_variable]:(fsup_sup_set_variable @ X3 @ (fsup_sup_set_variable @ X3 @ X4))=(fsup_sup_set_variable @ X3 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_107, c_0_108])])).
% 55.88/55.39 thf(c_0_133, plain, ((fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta))))))|~p991), inference(split_conjunct,[status(thm)],[c_0_109])).
% 55.88/55.39 thf(c_0_134, plain, p991, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_61]), c_0_111])])).
% 55.88/55.39 thf(c_0_135, plain, ((ford_le282106107riable @ esk236_0 @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))))|p2876)&((ford_le282106107riable @ esk237_0 @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))|p2876)&((fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ esk236_0 @ esk237_0)|p2876))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2876])])])])])).
% 55.88/55.39 thf(c_0_136, plain, (~p2876|~p2877), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])])).
% 55.88/55.39 thf(c_0_137, plain, p2877, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_115])])).
% 55.88/55.39 thf(c_0_138, plain, (~p1481|~p1094|p1479), inference(fof_simplification,[status(thm)],[ax3220])).
% 55.88/55.39 thf(c_0_139, plain, (p1094|~p1095|~p1), inference(split_conjunct,[status(thm)],[c_0_116])).
% 55.88/55.39 thf(c_0_140, plain, p1, inference(split_conjunct,[status(thm)],[ax4954])).
% 55.88/55.39 thf(c_0_141, plain, p1095, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_118])])).
% 55.88/55.39 thf(c_0_142, plain, (p1481|~p1480), inference(split_conjunct,[status(thm)],[c_0_119])).
% 55.88/55.39 thf(c_0_143, plain, p1480, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_121])])).
% 55.88/55.39 thf(c_0_144, plain, (~p2720|~p1114|p1607), inference(fof_simplification,[status(thm)],[ax833])).
% 55.88/55.39 thf(c_0_145, plain, (p2720|~p2721), inference(split_conjunct,[status(thm)],[c_0_122])).
% 55.88/55.39 thf(c_0_146, plain, p2721, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_123, c_0_124])])).
% 55.88/55.39 thf(c_0_147, plain, (p1114|~p1183|~p1182), inference(split_conjunct,[status(thm)],[c_0_125])).
% 55.88/55.39 thf(c_0_148, plain, p1183, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_126, c_0_127])])).
% 55.88/55.39 thf(c_0_149, plain, (p1182|(fsup_sup_set_variable @ fua @ (fsup_sup_set_variable @ esk1119_0 @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))) @ esk1120_0))))!=(fsup_sup_set_variable @ fua @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_129]), c_0_130]), c_0_129]), c_0_129]), c_0_131]), c_0_131]), c_0_131]), c_0_131]), c_0_132]), c_0_129])).
% 55.88/55.39 thf(c_0_150, plain, (fsup_sup_set_variable @ esk1119_0 @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))) @ esk1120_0)))=(fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_133, c_0_130]), c_0_129]), c_0_131]), c_0_131]), c_0_134])])).
% 55.88/55.39 thf(c_0_151, plain, (~p1479|(fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))), inference(fof_nnf,[status(thm)],[pax1479])).
% 55.88/55.39 thf(c_0_152, plain, ((fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ esk236_0 @ esk237_0)|p2876), inference(split_conjunct,[status(thm)],[c_0_135])).
% 55.88/55.39 thf(c_0_153, plain, ~p2876, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_136, c_0_137])])).
% 55.88/55.39 thf(c_0_154, plain, (p1479|~p1481|~p1094), inference(split_conjunct,[status(thm)],[c_0_138])).
% 55.88/55.39 thf(c_0_155, plain, p1094, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_139, c_0_140]), c_0_141])])).
% 55.88/55.39 thf(c_0_156, plain, p1481, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_142, c_0_143])])).
% 55.88/55.39 thf(c_0_157, plain, (p1607|~p2720|~p1114), inference(split_conjunct,[status(thm)],[c_0_144])).
% 55.88/55.39 thf(c_0_158, plain, p2720, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_145, c_0_146])])).
% 55.88/55.39 thf(c_0_159, plain, (p1114|~p1182), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_147, c_0_148])])).
% 55.88/55.39 thf(c_0_160, plain, p1182, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149, c_0_150])])).
% 55.88/55.39 thf(c_0_161, plain, (~ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))|p84), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax84])])).
% 55.88/55.39 thf(c_0_162, plain, ~p84, inference(fof_simplification,[status(thm)],[ax4871])).
% 55.88/55.39 thf(c_0_163, plain, (~p1607|ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))), inference(fof_nnf,[status(thm)],[pax1607])).
% 55.88/55.39 thf(c_0_164, plain, ((fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))|~p1479), inference(split_conjunct,[status(thm)],[c_0_151])).
% 55.88/55.39 thf(c_0_165, plain, (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))=(fsup_sup_set_variable @ esk236_0 @ esk237_0), inference(sr,[status(thm)],[c_0_152, c_0_153])).
% 55.88/55.39 thf(c_0_166, plain, p1479, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_154, c_0_155]), c_0_156])])).
% 55.88/55.39 thf(c_0_167, plain, (p1607|~p1114), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_158])])).
% 55.88/55.39 thf(c_0_168, plain, p1114, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_159, c_0_160])])).
% 55.88/55.39 thf(c_0_169, plain, (p84|~ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))), inference(split_conjunct,[status(thm)],[c_0_161])).
% 55.88/55.39 thf(c_0_170, plain, ~p84, inference(split_conjunct,[status(thm)],[c_0_162])).
% 55.88/55.39 thf(c_0_171, plain, (ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ (fcompose @ falpha @ fbeta)))))) @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ (fsup_sup_set_variable @ fua @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha))))) @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta))))) @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))|~p1607), inference(split_conjunct,[status(thm)],[c_0_163])).
% 55.88/55.39 thf(c_0_172, plain, (fsup_sup_set_variable @ fua @ (fsup_sup_set_variable @ esk236_0 @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)))) @ (fsup_sup_set_variable @ (fstatic_BVG @ (fthe_game @ (fproduc293487213n_game @ (fuSubst516392814stappp @ fsigma @ (fproduc893821739n_game @ (fuSubst516392814stappp @ fsigma @ fua @ falpha)) @ fbeta)))) @ esk237_0))))=(fsup_sup_set_variable @ esk236_0 @ esk237_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_164, c_0_129]), c_0_165]), c_0_129]), c_0_129]), c_0_131]), c_0_131]), c_0_165]), c_0_166])])).
% 55.88/55.39 thf(c_0_173, plain, p1607, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_168])])).
% 55.88/55.39 thf(c_0_174, plain, ~ford_le282106107riable @ (fsup_sup_set_variable @ fua @ (fsup_sup_set_variable @ esk1119_0 @ esk1120_0)) @ (fsup_sup_set_variable @ esk236_0 @ esk237_0), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_169, c_0_130]), c_0_165]), c_0_170])).
% 55.88/55.39 thf(c_0_175, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_171, c_0_130]), c_0_129]), c_0_165]), c_0_129]), c_0_129]), c_0_131]), c_0_131]), c_0_172]), c_0_173])]), c_0_174]), ['proof']).
% 55.88/55.39 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 55.88/55.39 thf(0,theorem,((ord_le282106107riable @ ((sup_sup_set_variable @ ua) @ (static_BVG @ (the_game @ (produc293487213n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ ((compose @ alpha) @ beta))))))) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ (produc893821739n_game @ (((uSubst516392814stappp @ sigma) @ ua) @ alpha))) @ beta))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 55.88/55.39 % SZS output end Proof
%------------------------------------------------------------------------------