%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG274^5 : TPTP v9.2.0. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n013.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:12:18 PM UTC 2025
% Result : Theorem 26.19s 26.33s
% Output : Proof 26.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ALG274^5 : TPTP v9.2.0. Bugfixed v5.3.0.
% 0.11/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n013.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 23:27:38 EDT 2025
% 0.12/0.33 % CPUTime :
% 26.19/26.33 % SZS status Theorem
% 26.19/26.33 % Mode: mode371
% 26.19/26.33 % Inferences: 5574
% 26.19/26.33 % SZS output start Proof
% 26.19/26.33 thf(def_cGRP_ASSOC,definition,(cGRP_ASSOC = (^[X1:g>g>g]:(![X2:g]:(![X3:g]:(![X4:g]:(((X1 @ ((X1 @ X2) @ X3)) @ X4) = ((X1 @ X2) @ ((X1 @ X3) @ X4))))))))).
% 26.19/26.33 thf(def_cGRP_DIVISORS,definition,(cGRP_DIVISORS = (^[X1:g>g>g]:(![X2:g]:(![X3:g]:(~(((~((![X4:g]:(~((((X1 @ X2) @ X4) = X3)))))) => (![X4:g]:(~((((X1 @ X4) @ X2) = X3)))))))))))).
% 26.19/26.33 thf(def_cGRP_RIGHT_INVERSE,definition,(cGRP_RIGHT_INVERSE = (^[X1:g>g>g]:(^[X2:g]:(![X3:g]:(~((![X4:g]:(~((((X1 @ X3) @ X4) = X2))))))))))).
% 26.19/26.33 thf(def_cGRP_RIGHT_UNIT,definition,(cGRP_RIGHT_UNIT = (^[X1:g>g>g]:(^[X2:g]:(![X3:g]:(((X1 @ X3) @ X2) = X3)))))).
% 26.19/26.33 thf(def_cGROUP3,definition,(cGROUP3 = (^[X1:g>g>g]:(^[X2:g]:(~(((~(((cGRP_ASSOC @ X1) => (~(((cGRP_RIGHT_UNIT @ X1) @ X2)))))) => (~(((cGRP_RIGHT_INVERSE @ X1) @ X2)))))))))).
% 26.19/26.33 thf(def_cGROUP4,definition,(cGROUP4 = (^[X1:g>g>g]:(~(((cGRP_ASSOC @ X1) => (~((cGRP_DIVISORS @ X1))))))))).
% 26.19/26.33 thf(cEQUIV_03_04,conjecture,(![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP3 @ X1) @ X2)))))) = (cGROUP4 @ X1)))).
% 26.19/26.33 thf(h0,negated_conjecture,(~((![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP3 @ X1) @ X2)))))) = (cGROUP4 @ X1))))),inference(assume_negation,[status(cth)],[cEQUIV_03_04])).
% 26.19/26.33 thf(ax3218, axiom, (~(p60)|p59), file('<stdin>', ax3218)).
% 26.19/26.33 thf(ax3220, axiom, (~(p6)|p53), file('<stdin>', ax3220)).
% 26.19/26.33 thf(ax3212, axiom, (~(p59)|p64), file('<stdin>', ax3212)).
% 26.19/26.33 thf(ax3219, axiom, p60, file('<stdin>', ax3219)).
% 26.19/26.33 thf(ax3271, axiom, (p1|~(p8)), file('<stdin>', ax3271)).
% 26.19/26.33 thf(ax3278, axiom, ~(p1), file('<stdin>', ax3278)).
% 26.19/26.33 thf(ax3213, axiom, (~(p53)|p55), file('<stdin>', ax3213)).
% 26.19/26.33 thf(ax3273, axiom, p6, file('<stdin>', ax3273)).
% 26.19/26.33 thf(ax3211, axiom, (~(p64)|p8|p63), file('<stdin>', ax3211)).
% 26.19/26.33 thf(ax741, axiom, (~(p86)|p1998), file('<stdin>', ax741)).
% 26.19/26.33 thf(ax3209, axiom, (~(p62)|~(p55)|~(p61)), file('<stdin>', ax3209)).
% 26.19/26.33 thf(ax3210, axiom, (~(p63)|p62), file('<stdin>', ax3210)).
% 26.19/26.33 thf(ax742, axiom, (~(p7)|p1992), file('<stdin>', ax742)).
% 26.19/26.33 thf(ax711, axiom, (~(p1998)|p2026), file('<stdin>', ax711)).
% 26.19/26.33 thf(ax3193, axiom, p86, file('<stdin>', ax3193)).
% 26.19/26.33 thf(ax736, axiom, (~(p1992)|p1994), file('<stdin>', ax736)).
% 26.19/26.33 thf(ax3272, axiom, p7, file('<stdin>', ax3272)).
% 26.19/26.33 thf(ax710, axiom, (~(p2026)|p61|p2025), file('<stdin>', ax710)).
% 26.19/26.33 thf(ax3203, axiom, (~(p60)|p74), file('<stdin>', ax3203)).
% 26.19/26.33 thf(ax708, axiom, (~(p2024)|~(p1994)|~(p2023)), file('<stdin>', ax708)).
% 26.19/26.33 thf(ax709, axiom, (~(p2025)|p2024), file('<stdin>', ax709)).
% 26.19/26.33 thf(ax3231, axiom, (~(p5)|p43), file('<stdin>', ax3231)).
% 26.19/26.33 thf(ax3155, axiom, (~(p74)|p121), file('<stdin>', ax3155)).
% 26.19/26.33 thf(ax3208, axiom, (~(p43)|p65), file('<stdin>', ax3208)).
% 26.19/26.33 thf(ax3274, axiom, p5, file('<stdin>', ax3274)).
% 26.19/26.33 thf(ax3154, axiom, (~(p121)|p61|p120), file('<stdin>', ax3154)).
% 26.19/26.33 thf(ax482, axiom, (p2023|~(p54)|~(p2027)), file('<stdin>', ax482)).
% 26.19/26.33 thf(ax3198, axiom, (~(p60)|p79), file('<stdin>', ax3198)).
% 26.19/26.33 thf(ax3152, axiom, (~(p119)|~(p65)|~(p118)), file('<stdin>', ax3152)).
% 26.19/26.33 thf(ax3153, axiom, (~(p120)|p119), file('<stdin>', ax3153)).
% 26.19/26.33 thf(ax3192, axiom, (~(p86)|p85), file('<stdin>', ax3192)).
% 26.19/26.33 thf(nax54, axiom, (p54<=![X1:g]:(~((fcGRP_ASSOC @ f__0=>~(fcGRP_RIGHT_UNIT @ f__0 @ X1)))=>~(fcGRP_RIGHT_INVERSE @ f__0 @ X1))), file('<stdin>', nax54)).
% 26.19/26.33 thf(ax3238, axiom, (~(p4)|p37), file('<stdin>', ax3238)).
% 26.19/26.33 thf(ax2956, axiom, (~(p79)|p293), file('<stdin>', ax2956)).
% 26.19/26.33 thf(ax2856, axiom, (~(p85)|p366), file('<stdin>', ax2856)).
% 26.19/26.33 thf(nax2027, axiom, (p2027<=(fcGRP_ASSOC @ f__0=>~(fcGRP_DIVISORS @ f__0))), file('<stdin>', nax2027)).
% 26.19/26.33 thf(ax3207, axiom, (~(p37)|p66), file('<stdin>', ax3207)).
% 26.19/26.33 thf(ax3275, axiom, p4, file('<stdin>', ax3275)).
% 26.19/26.33 thf(ax2955, axiom, (~(p293)|p118|p292), file('<stdin>', ax2955)).
% 26.19/26.33 thf(ax3253, axiom, (~(p2)|p24), file('<stdin>', ax3253)).
% 26.19/26.33 thf(ax2855, axiom, (~(p366)|~(p87)|p365), file('<stdin>', ax2855)).
% 26.19/26.33 thf(nax87, axiom, (p87<=fcGRP_ASSOC @ f__0), file('<stdin>', nax87)).
% 26.19/26.33 thf(ax2953, axiom, (~(p291)|~(p66)|~(p290)), file('<stdin>', ax2953)).
% 26.19/26.33 thf(ax2954, axiom, (~(p292)|p291), file('<stdin>', ax2954)).
% 26.19/26.33 thf(ax3187, axiom, (~(p24)|p81), file('<stdin>', ax3187)).
% 26.19/26.33 thf(ax3277, axiom, p2, file('<stdin>', ax3277)).
% 26.19/26.33 thf(ax727, axiom, (~(p1998)|p2010), file('<stdin>', ax727)).
% 26.19/26.33 thf(ax2853, axiom, (~(p364)|~(p81)|p187), file('<stdin>', ax2853)).
% 26.19/26.33 thf(ax2854, axiom, (~(p365)|p364), file('<stdin>', ax2854)).
% 26.19/26.33 thf(ax726, axiom, (~(p2010)|p290|p2009), file('<stdin>', ax726)).
% 26.19/26.33 thf(ax715, axiom, (~(p1998)|p2022), file('<stdin>', ax715)).
% 26.19/26.33 thf(ax692, axiom, (~(p86)|p2045), file('<stdin>', ax692)).
% 26.19/26.33 thf(ax724, axiom, (~(p2008)|~(p1994)|~(p2007)), file('<stdin>', ax724)).
% 26.19/26.33 thf(ax725, axiom, (~(p2009)|p2008), file('<stdin>', ax725)).
% 26.19/26.33 thf(ax714, axiom, (~(p2022)|p118|p2021), file('<stdin>', ax714)).
% 26.19/26.33 thf(ax2852, axiom, (~(p187)|p367), file('<stdin>', ax2852)).
% 26.19/26.33 thf(ax3246, axiom, (~(p3)|p30), file('<stdin>', ax3246)).
% 26.19/26.33 thf(ax606, axiom, (~(p2045)|p2113), file('<stdin>', ax606)).
% 26.19/26.33 thf(ax712, axiom, (~(p2020)|~(p1994)|~(p2019)), file('<stdin>', ax712)).
% 26.19/26.33 thf(ax713, axiom, (~(p2021)|p2020), file('<stdin>', ax713)).
% 26.19/26.33 thf(pax367, axiom, (p367=>![X1:g, X2:g]:(f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ f__1 @ (f__0 @ X1 @ X2))), file('<stdin>', pax367)).
% 26.19/26.33 thf(ax3206, axiom, (~(p30)|p67), file('<stdin>', ax3206)).
% 26.19/26.33 thf(ax3276, axiom, p3, file('<stdin>', ax3276)).
% 26.19/26.33 thf(ax605, axiom, (~(p2113)|p2007|p2112), file('<stdin>', ax605)).
% 26.19/26.33 thf(ax528, axiom, (~(p2045)|p2173), file('<stdin>', ax528)).
% 26.19/26.33 thf(nax70, axiom, (p70<=![X1:g]:(~((fcGRP_ASSOC @ f__0=>~(![X2:g]:(f__0 @ X2 @ X1)=(X2))))=>~(fcGRP_RIGHT_INVERSE @ f__0 @ X1))), file('<stdin>', nax70)).
% 26.19/26.33 thf(ax603, axiom, (~(p2111)|~(p67)|~(p2110)), file('<stdin>', ax603)).
% 26.19/26.33 thf(ax604, axiom, (~(p2112)|p2111), file('<stdin>', ax604)).
% 26.19/26.33 thf(ax527, axiom, (~(p2173)|p2019|p2172), file('<stdin>', ax527)).
% 26.19/26.33 thf(ax525, axiom, (~(p2171)|~(p67)|~(p2170)), file('<stdin>', ax525)).
% 26.19/26.33 thf(ax526, axiom, (~(p2172)|p2171), file('<stdin>', ax526)).
% 26.19/26.33 thf(pax134, axiom, (p134=>![X1:g]:(~((fcGRP_ASSOC @ f__0=>~(![X2:g]:(f__0 @ X2 @ X1)=(X2))))=>~(![X2:g]:~(![X3:g]:~((f__0 @ X2 @ X3)=(X1)))))), file('<stdin>', pax134)).
% 26.19/26.33 thf(nax2236, axiom, (p2236<=(fcGRP_ASSOC @ f__0=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', nax2236)).
% 26.19/26.33 thf(ax255, axiom, (p2110|p134|p2236), file('<stdin>', ax255)).
% 26.19/26.33 thf(pax187, axiom, (p187=>![X1:g, X2:g, X3:g]:(f__0 @ (f__0 @ X2 @ X2) @ X3)=(f__0 @ X1 @ (f__0 @ X2 @ X3))), file('<stdin>', pax187)).
% 26.19/26.33 thf(pax2236, axiom, (p2236=>(fcGRP_ASSOC @ f__0=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', pax2236)).
% 26.19/26.33 thf(ax142, axiom, (p2170|~(p70)|~(p2236)), file('<stdin>', ax142)).
% 26.19/26.33 thf(nax2525, axiom, (p2525<=(![X1:g, X2:g, X3:g]:(f__0 @ (f__0 @ X2 @ X2) @ X3)=(f__0 @ X1 @ (f__0 @ X2 @ X3))=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', nax2525)).
% 26.19/26.33 thf(pax2525, axiom, (p2525=>(![X1:g, X2:g, X3:g]:(f__0 @ (f__0 @ X2 @ X2) @ X3)=(f__0 @ X1 @ (f__0 @ X2 @ X3))=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', pax2525)).
% 26.19/26.33 thf(c_0_79, plain, (~p60|p59), inference(fof_simplification,[status(thm)],[ax3218])).
% 26.19/26.33 thf(c_0_80, plain, (~p6|p53), inference(fof_simplification,[status(thm)],[ax3220])).
% 26.19/26.33 thf(c_0_81, plain, (~p59|p64), inference(fof_simplification,[status(thm)],[ax3212])).
% 26.19/26.33 thf(c_0_82, plain, (p59|~p60), inference(split_conjunct,[status(thm)],[c_0_79])).
% 26.19/26.33 thf(c_0_83, plain, p60, inference(split_conjunct,[status(thm)],[ax3219])).
% 26.19/26.33 thf(c_0_84, plain, (p1|~p8), inference(fof_simplification,[status(thm)],[ax3271])).
% 26.19/26.33 thf(c_0_85, plain, ~p1, inference(fof_simplification,[status(thm)],[ax3278])).
% 26.19/26.33 thf(c_0_86, plain, (~p53|p55), inference(fof_simplification,[status(thm)],[ax3213])).
% 26.19/26.33 thf(c_0_87, plain, (p53|~p6), inference(split_conjunct,[status(thm)],[c_0_80])).
% 26.19/26.33 thf(c_0_88, plain, p6, inference(split_conjunct,[status(thm)],[ax3273])).
% 26.19/26.33 thf(c_0_89, plain, (~p64|p8|p63), inference(fof_simplification,[status(thm)],[ax3211])).
% 26.19/26.33 thf(c_0_90, plain, (p64|~p59), inference(split_conjunct,[status(thm)],[c_0_81])).
% 26.19/26.33 thf(c_0_91, plain, p59, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 26.19/26.33 thf(c_0_92, plain, (p1|~p8), inference(split_conjunct,[status(thm)],[c_0_84])).
% 26.19/26.33 thf(c_0_93, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_85])).
% 26.19/26.33 thf(c_0_94, plain, (~p86|p1998), inference(fof_simplification,[status(thm)],[ax741])).
% 26.19/26.33 thf(c_0_95, plain, (~p62|~p55|~p61), inference(fof_simplification,[status(thm)],[ax3209])).
% 26.19/26.33 thf(c_0_96, plain, (p55|~p53), inference(split_conjunct,[status(thm)],[c_0_86])).
% 26.19/26.33 thf(c_0_97, plain, p53, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_87, c_0_88])])).
% 26.19/26.33 thf(c_0_98, plain, (~p63|p62), inference(fof_simplification,[status(thm)],[ax3210])).
% 26.19/26.33 thf(c_0_99, plain, (p8|p63|~p64), inference(split_conjunct,[status(thm)],[c_0_89])).
% 26.19/26.33 thf(c_0_100, plain, p64, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_91])])).
% 26.19/26.33 thf(c_0_101, plain, ~p8, inference(sr,[status(thm)],[c_0_92, c_0_93])).
% 26.19/26.33 thf(c_0_102, plain, (~p7|p1992), inference(fof_simplification,[status(thm)],[ax742])).
% 26.19/26.33 thf(c_0_103, plain, (~p1998|p2026), inference(fof_simplification,[status(thm)],[ax711])).
% 26.19/26.33 thf(c_0_104, plain, (p1998|~p86), inference(split_conjunct,[status(thm)],[c_0_94])).
% 26.19/26.33 thf(c_0_105, plain, p86, inference(split_conjunct,[status(thm)],[ax3193])).
% 26.19/26.33 thf(c_0_106, plain, (~p62|~p55|~p61), inference(split_conjunct,[status(thm)],[c_0_95])).
% 26.19/26.33 thf(c_0_107, plain, p55, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 26.19/26.33 thf(c_0_108, plain, (p62|~p63), inference(split_conjunct,[status(thm)],[c_0_98])).
% 26.19/26.33 thf(c_0_109, plain, p63, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_99, c_0_100])]), c_0_101])).
% 26.19/26.33 thf(c_0_110, plain, (~p1992|p1994), inference(fof_simplification,[status(thm)],[ax736])).
% 26.19/26.33 thf(c_0_111, plain, (p1992|~p7), inference(split_conjunct,[status(thm)],[c_0_102])).
% 26.19/26.33 thf(c_0_112, plain, p7, inference(split_conjunct,[status(thm)],[ax3272])).
% 26.19/26.33 thf(c_0_113, plain, (~p2026|p61|p2025), inference(fof_simplification,[status(thm)],[ax710])).
% 26.19/26.33 thf(c_0_114, plain, (p2026|~p1998), inference(split_conjunct,[status(thm)],[c_0_103])).
% 26.19/26.33 thf(c_0_115, plain, p1998, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_105])])).
% 26.19/26.33 thf(c_0_116, plain, (~p61|~p62), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_107])])).
% 26.19/26.33 thf(c_0_117, plain, p62, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108, c_0_109])])).
% 26.19/26.33 thf(c_0_118, plain, (~p60|p74), inference(fof_simplification,[status(thm)],[ax3203])).
% 26.19/26.33 thf(c_0_119, plain, (~p2024|~p1994|~p2023), inference(fof_simplification,[status(thm)],[ax708])).
% 26.19/26.33 thf(c_0_120, plain, (p1994|~p1992), inference(split_conjunct,[status(thm)],[c_0_110])).
% 26.19/26.33 thf(c_0_121, plain, p1992, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_111, c_0_112])])).
% 26.19/26.33 thf(c_0_122, plain, (~p2025|p2024), inference(fof_simplification,[status(thm)],[ax709])).
% 26.19/26.33 thf(c_0_123, plain, (p61|p2025|~p2026), inference(split_conjunct,[status(thm)],[c_0_113])).
% 26.19/26.33 thf(c_0_124, plain, p2026, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_115])])).
% 26.19/26.33 thf(c_0_125, plain, ~p61, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_117])])).
% 26.19/26.33 thf(c_0_126, plain, (~p5|p43), inference(fof_simplification,[status(thm)],[ax3231])).
% 26.19/26.33 thf(c_0_127, plain, (~p74|p121), inference(fof_simplification,[status(thm)],[ax3155])).
% 26.19/26.33 thf(c_0_128, plain, (p74|~p60), inference(split_conjunct,[status(thm)],[c_0_118])).
% 26.19/26.33 thf(c_0_129, plain, (~p2024|~p1994|~p2023), inference(split_conjunct,[status(thm)],[c_0_119])).
% 26.19/26.33 thf(c_0_130, plain, p1994, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_121])])).
% 26.19/26.33 thf(c_0_131, plain, (p2024|~p2025), inference(split_conjunct,[status(thm)],[c_0_122])).
% 26.19/26.33 thf(c_0_132, plain, p2025, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_123, c_0_124])]), c_0_125])).
% 26.19/26.33 thf(c_0_133, plain, (~p43|p65), inference(fof_simplification,[status(thm)],[ax3208])).
% 26.19/26.33 thf(c_0_134, plain, (p43|~p5), inference(split_conjunct,[status(thm)],[c_0_126])).
% 26.19/26.33 thf(c_0_135, plain, p5, inference(split_conjunct,[status(thm)],[ax3274])).
% 26.19/26.33 thf(c_0_136, plain, (~p121|p61|p120), inference(fof_simplification,[status(thm)],[ax3154])).
% 26.19/26.33 thf(c_0_137, plain, (p121|~p74), inference(split_conjunct,[status(thm)],[c_0_127])).
% 26.19/26.33 thf(c_0_138, plain, p74, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_83])])).
% 26.19/26.33 thf(c_0_139, plain, (p2023|~p54|~p2027), inference(fof_simplification,[status(thm)],[ax482])).
% 26.19/26.33 thf(c_0_140, plain, (~p2023|~p2024), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_129, c_0_130])])).
% 26.19/26.33 thf(c_0_141, plain, p2024, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_132])])).
% 26.19/26.33 thf(c_0_142, plain, (~p60|p79), inference(fof_simplification,[status(thm)],[ax3198])).
% 26.19/26.33 thf(c_0_143, plain, (~p119|~p65|~p118), inference(fof_simplification,[status(thm)],[ax3152])).
% 26.19/26.33 thf(c_0_144, plain, (p65|~p43), inference(split_conjunct,[status(thm)],[c_0_133])).
% 26.19/26.33 thf(c_0_145, plain, p43, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_134, c_0_135])])).
% 26.19/26.33 thf(c_0_146, plain, (~p120|p119), inference(fof_simplification,[status(thm)],[ax3153])).
% 26.19/26.33 thf(c_0_147, plain, (p61|p120|~p121), inference(split_conjunct,[status(thm)],[c_0_136])).
% 26.19/26.33 thf(c_0_148, plain, p121, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_137, c_0_138])])).
% 26.19/26.33 thf(c_0_149, plain, (~p86|p85), inference(fof_simplification,[status(thm)],[ax3192])).
% 26.19/26.33 thf(c_0_150, plain, (p2023|~p54|~p2027), inference(split_conjunct,[status(thm)],[c_0_139])).
% 26.19/26.33 thf(c_0_151, plain, ~p2023, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_140, c_0_141])])).
% 26.19/26.33 thf(c_0_152, plain, (((fcGRP_ASSOC @ f__0|p54)&(fcGRP_RIGHT_UNIT @ f__0 @ esk88_0|p54))&(fcGRP_RIGHT_INVERSE @ f__0 @ esk88_0|p54)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax54])])])])])).
% 26.19/26.33 thf(c_0_153, plain, (~p4|p37), inference(fof_simplification,[status(thm)],[ax3238])).
% 26.19/26.33 thf(c_0_154, plain, (~p79|p293), inference(fof_simplification,[status(thm)],[ax2956])).
% 26.19/26.33 thf(c_0_155, plain, (p79|~p60), inference(split_conjunct,[status(thm)],[c_0_142])).
% 26.19/26.33 thf(c_0_156, plain, (~p119|~p65|~p118), inference(split_conjunct,[status(thm)],[c_0_143])).
% 26.19/26.33 thf(c_0_157, plain, p65, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_144, c_0_145])])).
% 26.19/26.33 thf(c_0_158, plain, (p119|~p120), inference(split_conjunct,[status(thm)],[c_0_146])).
% 26.19/26.33 thf(c_0_159, plain, p120, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_147, c_0_148])]), c_0_125])).
% 26.19/26.33 thf(c_0_160, plain, (~p85|p366), inference(fof_simplification,[status(thm)],[ax2856])).
% 26.19/26.33 thf(c_0_161, plain, (p85|~p86), inference(split_conjunct,[status(thm)],[c_0_149])).
% 26.19/26.33 thf(c_0_162, plain, ((fcGRP_ASSOC @ f__0|p2027)&(fcGRP_DIVISORS @ f__0|p2027)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2027])])])).
% 26.19/26.33 thf(c_0_163, plain, (~p54|~p2027), inference(sr,[status(thm)],[c_0_150, c_0_151])).
% 26.19/26.33 thf(c_0_164, plain, (fcGRP_ASSOC @ f__0|p54), inference(split_conjunct,[status(thm)],[c_0_152])).
% 26.19/26.33 thf(c_0_165, plain, (~p37|p66), inference(fof_simplification,[status(thm)],[ax3207])).
% 26.19/26.33 thf(c_0_166, plain, (p37|~p4), inference(split_conjunct,[status(thm)],[c_0_153])).
% 26.19/26.33 thf(c_0_167, plain, p4, inference(split_conjunct,[status(thm)],[ax3275])).
% 26.19/26.33 thf(c_0_168, plain, (~p293|p118|p292), inference(fof_simplification,[status(thm)],[ax2955])).
% 26.19/26.33 thf(c_0_169, plain, (p293|~p79), inference(split_conjunct,[status(thm)],[c_0_154])).
% 26.19/26.33 thf(c_0_170, plain, p79, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_155, c_0_83])])).
% 26.19/26.33 thf(c_0_171, plain, (~p118|~p119), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_156, c_0_157])])).
% 26.19/26.33 thf(c_0_172, plain, p119, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_158, c_0_159])])).
% 26.19/26.33 thf(c_0_173, plain, (~p2|p24), inference(fof_simplification,[status(thm)],[ax3253])).
% 26.19/26.33 thf(c_0_174, plain, (~p366|~p87|p365), inference(fof_simplification,[status(thm)],[ax2855])).
% 26.19/26.33 thf(c_0_175, plain, (p366|~p85), inference(split_conjunct,[status(thm)],[c_0_160])).
% 26.19/26.33 thf(c_0_176, plain, p85, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_161, c_0_105])])).
% 26.19/26.33 thf(c_0_177, plain, (~fcGRP_ASSOC @ f__0|p87), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax87])])).
% 26.19/26.33 thf(c_0_178, plain, (fcGRP_ASSOC @ f__0|p2027), inference(split_conjunct,[status(thm)],[c_0_162])).
% 26.19/26.33 thf(c_0_179, plain, (fcGRP_ASSOC @ f__0|~p2027), inference(spm,[status(thm)],[c_0_163, c_0_164])).
% 26.19/26.33 thf(c_0_180, plain, (~p291|~p66|~p290), inference(fof_simplification,[status(thm)],[ax2953])).
% 26.19/26.33 thf(c_0_181, plain, (p66|~p37), inference(split_conjunct,[status(thm)],[c_0_165])).
% 26.19/26.33 thf(c_0_182, plain, p37, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_166, c_0_167])])).
% 26.19/26.33 thf(c_0_183, plain, (~p292|p291), inference(fof_simplification,[status(thm)],[ax2954])).
% 26.19/26.33 thf(c_0_184, plain, (p118|p292|~p293), inference(split_conjunct,[status(thm)],[c_0_168])).
% 26.19/26.33 thf(c_0_185, plain, p293, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_169, c_0_170])])).
% 26.19/26.33 thf(c_0_186, plain, ~p118, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_171, c_0_172])])).
% 26.19/26.33 thf(c_0_187, plain, (~p24|p81), inference(fof_simplification,[status(thm)],[ax3187])).
% 26.19/26.33 thf(c_0_188, plain, (p24|~p2), inference(split_conjunct,[status(thm)],[c_0_173])).
% 26.19/26.33 thf(c_0_189, plain, p2, inference(split_conjunct,[status(thm)],[ax3277])).
% 26.19/26.33 thf(c_0_190, plain, (p365|~p366|~p87), inference(split_conjunct,[status(thm)],[c_0_174])).
% 26.19/26.33 thf(c_0_191, plain, p366, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_175, c_0_176])])).
% 26.19/26.33 thf(c_0_192, plain, (p87|~fcGRP_ASSOC @ f__0), inference(split_conjunct,[status(thm)],[c_0_177])).
% 26.19/26.33 thf(c_0_193, plain, fcGRP_ASSOC @ f__0, inference(csr,[status(thm)],[c_0_178, c_0_179])).
% 26.19/26.33 thf(c_0_194, plain, (~p1998|p2010), inference(fof_simplification,[status(thm)],[ax727])).
% 26.19/26.33 thf(c_0_195, plain, (~p291|~p66|~p290), inference(split_conjunct,[status(thm)],[c_0_180])).
% 26.19/26.33 thf(c_0_196, plain, p66, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_181, c_0_182])])).
% 26.19/26.33 thf(c_0_197, plain, (p291|~p292), inference(split_conjunct,[status(thm)],[c_0_183])).
% 26.19/26.33 thf(c_0_198, plain, p292, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_184, c_0_185])]), c_0_186])).
% 26.19/26.33 thf(c_0_199, plain, (~p364|~p81|p187), inference(fof_simplification,[status(thm)],[ax2853])).
% 26.19/26.33 thf(c_0_200, plain, (p81|~p24), inference(split_conjunct,[status(thm)],[c_0_187])).
% 26.19/26.33 thf(c_0_201, plain, p24, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_188, c_0_189])])).
% 26.19/26.33 thf(c_0_202, plain, (~p365|p364), inference(fof_simplification,[status(thm)],[ax2854])).
% 26.19/26.33 thf(c_0_203, plain, (p365|~p87), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_190, c_0_191])])).
% 26.19/26.33 thf(c_0_204, plain, p87, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192, c_0_193])])).
% 26.19/26.33 thf(c_0_205, plain, (~p2010|p290|p2009), inference(fof_simplification,[status(thm)],[ax726])).
% 26.19/26.33 thf(c_0_206, plain, (p2010|~p1998), inference(split_conjunct,[status(thm)],[c_0_194])).
% 26.19/26.33 thf(c_0_207, plain, (~p290|~p291), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_195, c_0_196])])).
% 26.19/26.33 thf(c_0_208, plain, p291, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_197, c_0_198])])).
% 26.19/26.33 thf(c_0_209, plain, (~p1998|p2022), inference(fof_simplification,[status(thm)],[ax715])).
% 26.19/26.33 thf(c_0_210, plain, (p187|~p364|~p81), inference(split_conjunct,[status(thm)],[c_0_199])).
% 26.19/26.33 thf(c_0_211, plain, p81, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_200, c_0_201])])).
% 26.19/26.33 thf(c_0_212, plain, (p364|~p365), inference(split_conjunct,[status(thm)],[c_0_202])).
% 26.19/26.33 thf(c_0_213, plain, p365, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_203, c_0_204])])).
% 26.19/26.33 thf(c_0_214, plain, (~p86|p2045), inference(fof_simplification,[status(thm)],[ax692])).
% 26.19/26.33 thf(c_0_215, plain, (~p2008|~p1994|~p2007), inference(fof_simplification,[status(thm)],[ax724])).
% 26.19/26.33 thf(c_0_216, plain, (~p2009|p2008), inference(fof_simplification,[status(thm)],[ax725])).
% 26.19/26.33 thf(c_0_217, plain, (p290|p2009|~p2010), inference(split_conjunct,[status(thm)],[c_0_205])).
% 26.19/26.33 thf(c_0_218, plain, p2010, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_206, c_0_115])])).
% 26.19/26.33 thf(c_0_219, plain, ~p290, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_207, c_0_208])])).
% 26.19/26.33 thf(c_0_220, plain, (~p2022|p118|p2021), inference(fof_simplification,[status(thm)],[ax714])).
% 26.19/26.33 thf(c_0_221, plain, (p2022|~p1998), inference(split_conjunct,[status(thm)],[c_0_209])).
% 26.19/26.33 thf(c_0_222, plain, (~p187|p367), inference(fof_simplification,[status(thm)],[ax2852])).
% 26.19/26.33 thf(c_0_223, plain, (p187|~p364), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210, c_0_211])])).
% 26.19/26.33 thf(c_0_224, plain, p364, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_212, c_0_213])])).
% 26.19/26.33 thf(c_0_225, plain, (~p3|p30), inference(fof_simplification,[status(thm)],[ax3246])).
% 26.19/26.33 thf(c_0_226, plain, (~p2045|p2113), inference(fof_simplification,[status(thm)],[ax606])).
% 26.19/26.33 thf(c_0_227, plain, (p2045|~p86), inference(split_conjunct,[status(thm)],[c_0_214])).
% 26.19/26.33 thf(c_0_228, plain, (~p2008|~p1994|~p2007), inference(split_conjunct,[status(thm)],[c_0_215])).
% 26.19/26.33 thf(c_0_229, plain, (p2008|~p2009), inference(split_conjunct,[status(thm)],[c_0_216])).
% 26.19/26.33 thf(c_0_230, plain, p2009, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_217, c_0_218])]), c_0_219])).
% 26.19/26.33 thf(c_0_231, plain, (~p2020|~p1994|~p2019), inference(fof_simplification,[status(thm)],[ax712])).
% 26.19/26.33 thf(c_0_232, plain, (~p2021|p2020), inference(fof_simplification,[status(thm)],[ax713])).
% 26.19/26.33 thf(c_0_233, plain, (p118|p2021|~p2022), inference(split_conjunct,[status(thm)],[c_0_220])).
% 26.19/26.33 thf(c_0_234, plain, p2022, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_221, c_0_115])])).
% 26.19/26.33 thf(c_0_235, plain, ![X78:g, X79:g]:(~p367|(f__0 @ (f__0 @ X78 @ X78) @ X79)=(f__0 @ f__1 @ (f__0 @ X78 @ X79))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax367])])])).
% 26.19/26.33 thf(c_0_236, plain, (p367|~p187), inference(split_conjunct,[status(thm)],[c_0_222])).
% 26.19/26.33 thf(c_0_237, plain, p187, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_223, c_0_224])])).
% 26.19/26.33 thf(c_0_238, plain, (~p30|p67), inference(fof_simplification,[status(thm)],[ax3206])).
% 26.19/26.33 thf(c_0_239, plain, (p30|~p3), inference(split_conjunct,[status(thm)],[c_0_225])).
% 26.19/26.33 thf(c_0_240, plain, p3, inference(split_conjunct,[status(thm)],[ax3276])).
% 26.19/26.33 thf(c_0_241, plain, (~p2113|p2007|p2112), inference(fof_simplification,[status(thm)],[ax605])).
% 26.19/26.33 thf(c_0_242, plain, (p2113|~p2045), inference(split_conjunct,[status(thm)],[c_0_226])).
% 26.19/26.33 thf(c_0_243, plain, p2045, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_227, c_0_105])])).
% 26.19/26.33 thf(c_0_244, plain, (~p2007|~p2008), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_228, c_0_130])])).
% 26.19/26.33 thf(c_0_245, plain, p2008, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_229, c_0_230])])).
% 26.19/26.33 thf(c_0_246, plain, (~p2045|p2173), inference(fof_simplification,[status(thm)],[ax528])).
% 26.19/26.33 thf(c_0_247, plain, (~p2020|~p1994|~p2019), inference(split_conjunct,[status(thm)],[c_0_231])).
% 26.19/26.33 thf(c_0_248, plain, (p2020|~p2021), inference(split_conjunct,[status(thm)],[c_0_232])).
% 26.19/26.33 thf(c_0_249, plain, p2021, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_233, c_0_234])]), c_0_186])).
% 26.19/26.33 thf(c_0_250, plain, ![X1:g, X2:g]:((f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ f__1 @ (f__0 @ X1 @ X2))|~p367), inference(split_conjunct,[status(thm)],[c_0_235])).
% 26.19/26.33 thf(c_0_251, plain, p367, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_236, c_0_237])])).
% 26.19/26.33 thf(c_0_252, plain, ![X185:g]:(((fcGRP_ASSOC @ f__0|p70)&((f__0 @ X185 @ esk87_0)=(X185)|p70))&(fcGRP_RIGHT_INVERSE @ f__0 @ esk87_0|p70)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax70])])])])])])).
% 26.19/26.33 thf(c_0_253, plain, (~p2111|~p67|~p2110), inference(fof_simplification,[status(thm)],[ax603])).
% 26.19/26.33 thf(c_0_254, plain, (p67|~p30), inference(split_conjunct,[status(thm)],[c_0_238])).
% 26.19/26.33 thf(c_0_255, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_239, c_0_240])])).
% 26.19/26.33 thf(c_0_256, plain, (~p2112|p2111), inference(fof_simplification,[status(thm)],[ax604])).
% 26.19/26.33 thf(c_0_257, plain, (p2007|p2112|~p2113), inference(split_conjunct,[status(thm)],[c_0_241])).
% 26.19/26.33 thf(c_0_258, plain, p2113, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_242, c_0_243])])).
% 26.19/26.33 thf(c_0_259, plain, ~p2007, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_244, c_0_245])])).
% 26.19/26.33 thf(c_0_260, plain, (~p2173|p2019|p2172), inference(fof_simplification,[status(thm)],[ax527])).
% 26.19/26.33 thf(c_0_261, plain, (p2173|~p2045), inference(split_conjunct,[status(thm)],[c_0_246])).
% 26.19/26.33 thf(c_0_262, plain, (~p2019|~p2020), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_247, c_0_130])])).
% 26.19/26.33 thf(c_0_263, plain, p2020, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_248, c_0_249])])).
% 26.19/26.33 thf(c_0_264, plain, ![X1:g, X2:g]:(f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ f__1 @ (f__0 @ X1 @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_250, c_0_251])])).
% 26.19/26.33 thf(c_0_265, plain, ![X1:g]:((f__0 @ X1 @ esk87_0)=(X1)|p70), inference(split_conjunct,[status(thm)],[c_0_252])).
% 26.19/26.33 thf(c_0_266, plain, (~p2111|~p67|~p2110), inference(split_conjunct,[status(thm)],[c_0_253])).
% 26.19/26.33 thf(c_0_267, plain, p67, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_254, c_0_255])])).
% 26.19/26.33 thf(c_0_268, plain, (p2111|~p2112), inference(split_conjunct,[status(thm)],[c_0_256])).
% 26.19/26.33 thf(c_0_269, plain, p2112, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_257, c_0_258])]), c_0_259])).
% 26.19/26.33 thf(c_0_270, plain, (~p2171|~p67|~p2170), inference(fof_simplification,[status(thm)],[ax525])).
% 26.19/26.33 thf(c_0_271, plain, (~p2172|p2171), inference(fof_simplification,[status(thm)],[ax526])).
% 26.19/26.33 thf(c_0_272, plain, (p2019|p2172|~p2173), inference(split_conjunct,[status(thm)],[c_0_260])).
% 26.19/26.33 thf(c_0_273, plain, p2173, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_261, c_0_243])])).
% 26.19/26.33 thf(c_0_274, plain, ~p2019, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_262, c_0_263])])).
% 26.19/26.33 thf(c_0_275, plain, ![X1:g]:((f__0 @ (f__0 @ X1 @ X1) @ esk87_0)=(f__0 @ f__1 @ X1)|p70), inference(spm,[status(thm)],[c_0_264, c_0_265])).
% 26.19/26.33 thf(c_0_276, plain, ![X160:g, X163:g]:(~p134|(~fcGRP_ASSOC @ f__0|(f__0 @ (esk75_1 @ X160) @ X160)!=(esk75_1 @ X160)|(f__0 @ (esk76_1 @ X160) @ X163)!=(X160))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax134])])])])])).
% 26.19/26.33 thf(c_0_277, plain, (~p2110|~p2111), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_266, c_0_267])])).
% 26.19/26.33 thf(c_0_278, plain, p2111, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_268, c_0_269])])).
% 26.19/26.33 thf(c_0_279, plain, (~p2171|~p67|~p2170), inference(split_conjunct,[status(thm)],[c_0_270])).
% 26.19/26.33 thf(c_0_280, plain, (p2171|~p2172), inference(split_conjunct,[status(thm)],[c_0_271])).
% 26.19/26.33 thf(c_0_281, plain, p2172, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_272, c_0_273])]), c_0_274])).
% 26.19/26.33 thf(c_0_282, plain, ((f__0 @ esk87_0 @ esk87_0)=(f__0 @ f__1 @ esk87_0)|p70), inference(spm,[status(thm)],[c_0_275, c_0_265])).
% 26.19/26.33 thf(c_0_283, plain, ![X2:g, X1:g]:(~p134|~fcGRP_ASSOC @ f__0|(f__0 @ (esk75_1 @ X1) @ X1)!=(esk75_1 @ X1)|(f__0 @ (esk76_1 @ X1) @ X2)!=(X1)), inference(split_conjunct,[status(thm)],[c_0_276])).
% 26.19/26.33 thf(c_0_284, plain, ![X60:g, X61:g, X63:g, X64:g]:((fcGRP_ASSOC @ f__0|p2236)&(((f__0 @ X60 @ (esk26_2 @ X60 @ X61))=(X61)|p2236)&((f__0 @ (esk27_2 @ X63 @ X64) @ X63)=(X64)|p2236))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2236])])])])])])])).
% 26.19/26.33 thf(c_0_285, plain, (p2110|p134|p2236), inference(split_conjunct,[status(thm)],[ax255])).
% 26.19/26.33 thf(c_0_286, plain, ~p2110, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_277, c_0_278])])).
% 26.19/26.33 thf(c_0_287, plain, ![X126:g, X127:g, X128:g]:(~p187|(f__0 @ (f__0 @ X127 @ X127) @ X128)=(f__0 @ X126 @ (f__0 @ X127 @ X128))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax187])])])).
% 26.19/26.33 thf(c_0_288, plain, ![X58:g, X59:g]:(~p2236|(~fcGRP_ASSOC @ f__0|((f__0 @ esk24_0 @ X58)!=(esk25_0)|(f__0 @ X59 @ esk24_0)!=(esk25_0)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax2236])])])])])).
% 26.19/26.33 thf(c_0_289, plain, (p2170|~p70|~p2236), inference(fof_simplification,[status(thm)],[ax142])).
% 26.19/26.33 thf(c_0_290, plain, (~p2170|~p2171), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_279, c_0_267])])).
% 26.19/26.33 thf(c_0_291, plain, p2171, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_280, c_0_281])])).
% 26.19/26.33 thf(c_0_292, plain, ((f__0 @ f__1 @ esk87_0)=(esk87_0)|p70), inference(spm,[status(thm)],[c_0_265, c_0_282])).
% 26.19/26.33 thf(c_0_293, plain, ![X2:g, X1:g]:((f__0 @ (esk75_1 @ X1) @ X1)!=(esk75_1 @ X1)|(f__0 @ (esk76_1 @ X1) @ X2)!=(X1)|~p134), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_283, c_0_193])])).
% 26.19/26.33 thf(c_0_294, plain, ![X1:g, X2:g]:((f__0 @ X1 @ (esk26_2 @ X1 @ X2))=(X2)|p2236), inference(split_conjunct,[status(thm)],[c_0_284])).
% 26.19/26.33 thf(c_0_295, plain, (p134|p2236), inference(sr,[status(thm)],[c_0_285, c_0_286])).
% 26.19/26.33 thf(c_0_296, plain, ![X1:g, X3:g, X2:g]:((f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ X3 @ (f__0 @ X1 @ X2))|~p187), inference(split_conjunct,[status(thm)],[c_0_287])).
% 26.19/26.33 thf(c_0_297, plain, ![X1:g, X2:g]:(~p2236|~fcGRP_ASSOC @ f__0|(f__0 @ esk24_0 @ X1)!=(esk25_0)|(f__0 @ X2 @ esk24_0)!=(esk25_0)), inference(split_conjunct,[status(thm)],[c_0_288])).
% 26.19/26.33 thf(c_0_298, plain, ![X19:g, X20:g, X21:g, X22:g, X23:g, X25:g, X26:g]:(((f__0 @ (f__0 @ X20 @ X20) @ X21)=(f__0 @ X19 @ (f__0 @ X20 @ X21))|p2525)&(((f__0 @ X22 @ (esk9_2 @ X22 @ X23))=(X23)|p2525)&((f__0 @ (esk10_2 @ X25 @ X26) @ X25)=(X26)|p2525))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2525])])])])])])])).
% 26.19/26.33 thf(c_0_299, plain, (p2170|~p70|~p2236), inference(split_conjunct,[status(thm)],[c_0_289])).
% 26.19/26.33 thf(c_0_300, plain, ~p2170, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_290, c_0_291])])).
% 26.19/26.33 thf(c_0_301, plain, ((esk87_0)=(f__1)|p70), inference(spm,[status(thm)],[c_0_265, c_0_292])).
% 26.19/26.33 thf(c_0_302, plain, ![X1:g]:(p2236|(f__0 @ (esk75_1 @ X1) @ X1)!=(esk75_1 @ X1)), inference(csr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_293, c_0_294])]), c_0_295])).
% 26.19/26.33 thf(c_0_303, plain, ![X1:g, X3:g, X2:g]:(f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ X3 @ (f__0 @ X1 @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_296, c_0_237])])).
% 26.19/26.33 thf(c_0_304, plain, ![X1:g, X2:g]:((f__0 @ (esk27_2 @ X1 @ X2) @ X1)=(X2)|p2236), inference(split_conjunct,[status(thm)],[c_0_284])).
% 26.19/26.33 thf(c_0_305, plain, ![X1:g, X2:g]:((f__0 @ X1 @ esk24_0)!=(esk25_0)|(f__0 @ esk24_0 @ X2)!=(esk25_0)|~p2236), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_297, c_0_193])])).
% 26.19/26.33 thf(c_0_306, plain, ![X1:g, X2:g]:((f__0 @ (esk10_2 @ X1 @ X2) @ X1)=(X2)|p2525), inference(split_conjunct,[status(thm)],[c_0_298])).
% 26.19/26.33 thf(c_0_307, plain, (~p70|~p2236), inference(sr,[status(thm)],[c_0_299, c_0_300])).
% 26.19/26.33 thf(c_0_308, plain, ![X1:g]:((f__0 @ X1 @ f__1)=(X1)|p70), inference(spm,[status(thm)],[c_0_265, c_0_301])).
% 26.19/26.33 thf(c_0_309, plain, ![X1:g, X2:g]:(p2236|(f__0 @ (f__0 @ X1 @ X1) @ X2)!=(esk75_1 @ (f__0 @ X1 @ X2))), inference(spm,[status(thm)],[c_0_302, c_0_303])).
% 26.19/26.33 thf(c_0_310, plain, ![X1:g, X2:g, X3:g]:((f__0 @ (f__0 @ X1 @ X1) @ X2)=(X3)|p2236), inference(spm,[status(thm)],[c_0_304, c_0_303])).
% 26.19/26.33 thf(c_0_311, plain, ![X17:g, X18:g]:(~p2525|((f__0 @ (f__0 @ esk5_0 @ esk5_0) @ esk6_0)!=(f__0 @ esk4_0 @ (f__0 @ esk5_0 @ esk6_0))|((f__0 @ esk7_0 @ X17)!=(esk8_0)|(f__0 @ X18 @ esk7_0)!=(esk8_0)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax2525])])])])])).
% 26.19/26.33 thf(c_0_312, plain, ![X1:g]:(p2525|(f__0 @ esk24_0 @ X1)!=(esk25_0)|~p2236), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_305, c_0_306])])).
% 26.19/26.33 thf(c_0_313, plain, ![X1:g, X2:g]:((f__0 @ X1 @ (esk9_2 @ X1 @ X2))=(X2)|p2525), inference(split_conjunct,[status(thm)],[c_0_298])).
% 26.19/26.33 thf(c_0_314, plain, ![X1:g]:((f__0 @ X1 @ f__1)=(X1)|~p2236), inference(spm,[status(thm)],[c_0_307, c_0_308])).
% 26.19/26.33 thf(c_0_315, plain, p2236, inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_309, c_0_310])])).
% 26.19/26.33 thf(c_0_316, plain, ![X1:g, X2:g]:(~p2525|(f__0 @ (f__0 @ esk5_0 @ esk5_0) @ esk6_0)!=(f__0 @ esk4_0 @ (f__0 @ esk5_0 @ esk6_0))|(f__0 @ esk7_0 @ X1)!=(esk8_0)|(f__0 @ X2 @ esk7_0)!=(esk8_0)), inference(split_conjunct,[status(thm)],[c_0_311])).
% 26.19/26.33 thf(c_0_317, plain, (p2525|~p2236), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_312, c_0_313])])).
% 26.19/26.33 thf(c_0_318, plain, ![X1:g]:(f__0 @ X1 @ f__1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_314, c_0_315])])).
% 26.19/26.33 thf(c_0_319, plain, ![X1:g, X2:g]:((f__0 @ X1 @ esk7_0)!=(esk8_0)|(f__0 @ esk7_0 @ X2)!=(esk8_0)|~p2525), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_316, c_0_264]), c_0_303]), c_0_264])])).
% 26.19/26.33 thf(c_0_320, plain, p2525, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_317, c_0_315])])).
% 26.19/26.33 thf(c_0_321, plain, ![X2:g, X1:g]:(f__0 @ X1 @ X1)=(f__0 @ X2 @ X1), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_303, c_0_318]), c_0_318])).
% 26.19/26.33 thf(c_0_322, plain, ![X1:g, X2:g]:((f__0 @ X1 @ esk7_0)!=(esk8_0)|(f__0 @ esk7_0 @ X2)!=(esk8_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_319, c_0_320])])).
% 26.19/26.33 thf(c_0_323, plain, ![X1:g]:(f__1)=(X1), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_318, c_0_321]), c_0_318])).
% 26.19/26.33 thf(c_0_324, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_322, c_0_323]), c_0_323]), c_0_323]), c_0_323])]), ['proof']).
% 26.19/26.33 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 26.19/26.33 thf(0,theorem,(![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP3 @ X1) @ X2)))))) = (cGROUP4 @ X1))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 26.19/26.33 % SZS output end Proof
%------------------------------------------------------------------------------