%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG276^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 : n011.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.05s 26.27s
% Output : Proof 26.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG276^5 : TPTP v9.2.0. Bugfixed v5.3.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n011.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 23:30:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 26.05/26.27 % SZS status Theorem
% 26.05/26.27 % Mode: mode371
% 26.05/26.27 % Inferences: 5574
% 26.05/26.27 % SZS output start Proof
% 26.05/26.27 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.05/26.27 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.05/26.27 thf(def_cGRP_INVERSE,definition,(cGRP_INVERSE = (^[X1:g>g>g]:(^[X2:g]:(![X3:g]:(~((![X4:g]:((((X1 @ X3) @ X4) = X2) => (~((((X1 @ X4) @ X3) = X2)))))))))))).
% 26.05/26.27 thf(def_cGRP_UNIT,definition,(cGRP_UNIT = (^[X1:g>g>g]:(^[X2:g]:(![X3:g]:(~(((((X1 @ X2) @ X3) = X3) => (~((((X1 @ X3) @ X2) = X3))))))))))).
% 26.05/26.27 thf(def_cGROUP1,definition,(cGROUP1 = (^[X1:g>g>g]:(^[X2:g]:(~(((~(((cGRP_ASSOC @ X1) => (~(((cGRP_UNIT @ X1) @ X2)))))) => (~(((cGRP_INVERSE @ X1) @ X2)))))))))).
% 26.05/26.27 thf(def_cGROUP4,definition,(cGROUP4 = (^[X1:g>g>g]:(~(((cGRP_ASSOC @ X1) => (~((cGRP_DIVISORS @ X1))))))))).
% 26.05/26.27 thf(cEQUIV_01_04,conjecture,(![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP1 @ X1) @ X2)))))) = (cGROUP4 @ X1)))).
% 26.05/26.27 thf(h0,negated_conjecture,(~((![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP1 @ X1) @ X2)))))) = (cGROUP4 @ X1))))),inference(assume_negation,[status(cth)],[cEQUIV_01_04])).
% 26.05/26.27 thf(ax3220, axiom, (~(p64)|p63), file('<stdin>', ax3220)).
% 26.05/26.27 thf(ax3222, axiom, (~(p6)|p57), file('<stdin>', ax3222)).
% 26.05/26.27 thf(ax3214, axiom, (~(p63)|p68), file('<stdin>', ax3214)).
% 26.05/26.27 thf(ax3221, axiom, p64, file('<stdin>', ax3221)).
% 26.05/26.27 thf(ax3277, axiom, (p1|~(p8)), file('<stdin>', ax3277)).
% 26.05/26.27 thf(ax3284, axiom, ~(p1), file('<stdin>', ax3284)).
% 26.05/26.27 thf(ax3215, axiom, (~(p57)|p59), file('<stdin>', ax3215)).
% 26.05/26.27 thf(ax3279, axiom, p6, file('<stdin>', ax3279)).
% 26.05/26.27 thf(ax3213, axiom, (~(p68)|p8|p67), file('<stdin>', ax3213)).
% 26.05/26.27 thf(ax3193, axiom, (~(p91)|p90), file('<stdin>', ax3193)).
% 26.05/26.27 thf(ax3211, axiom, (~(p66)|~(p59)|~(p65)), file('<stdin>', ax3211)).
% 26.05/26.27 thf(ax3212, axiom, (~(p67)|p66), file('<stdin>', ax3212)).
% 26.05/26.27 thf(ax3259, axiom, (~(p2)|p24), file('<stdin>', ax3259)).
% 26.05/26.27 thf(ax3148, axiom, (~(p90)|p134), file('<stdin>', ax3148)).
% 26.05/26.27 thf(ax3194, axiom, p91, file('<stdin>', ax3194)).
% 26.05/26.27 thf(ax3188, axiom, (~(p24)|p86), file('<stdin>', ax3188)).
% 26.05/26.27 thf(ax3283, axiom, p2, file('<stdin>', ax3283)).
% 26.05/26.27 thf(ax3147, axiom, (~(p134)|p65|p133), file('<stdin>', ax3147)).
% 26.05/26.27 thf(ax742, axiom, (~(p91)|p2003), file('<stdin>', ax742)).
% 26.05/26.27 thf(ax3145, axiom, (~(p132)|~(p86)|~(p131)), file('<stdin>', ax3145)).
% 26.05/26.27 thf(ax3146, axiom, (~(p133)|p132), file('<stdin>', ax3146)).
% 26.05/26.27 thf(ax743, axiom, (~(p7)|p1997), file('<stdin>', ax743)).
% 26.05/26.27 thf(ax712, axiom, (~(p2003)|p2031), file('<stdin>', ax712)).
% 26.05/26.27 thf(ax724, axiom, (~(p2003)|p2019), file('<stdin>', ax724)).
% 26.05/26.27 thf(ax737, axiom, (~(p1997)|p1999), file('<stdin>', ax737)).
% 26.05/26.27 thf(ax3278, axiom, p7, file('<stdin>', ax3278)).
% 26.05/26.27 thf(ax711, axiom, (~(p2031)|p65|p2030), file('<stdin>', ax711)).
% 26.05/26.27 thf(ax723, axiom, (~(p2019)|p131|p2018), file('<stdin>', ax723)).
% 26.05/26.27 thf(ax709, axiom, (~(p2029)|~(p1999)|~(p2028)), file('<stdin>', ax709)).
% 26.05/26.27 thf(ax710, axiom, (~(p2030)|p2029), file('<stdin>', ax710)).
% 26.05/26.27 thf(ax692, axiom, (~(p91)|p2051), file('<stdin>', ax692)).
% 26.05/26.27 thf(ax721, axiom, (~(p2017)|~(p1999)|~(p2016)), file('<stdin>', ax721)).
% 26.05/26.27 thf(ax722, axiom, (~(p2018)|p2017), file('<stdin>', ax722)).
% 26.05/26.27 thf(ax3252, axiom, (~(p3)|p30), file('<stdin>', ax3252)).
% 26.05/26.27 thf(ax576, axiom, (~(p2051)|p2142), file('<stdin>', ax576)).
% 26.05/26.27 thf(ax482, axiom, (p2028|~(p58)|~(p2032)), file('<stdin>', ax482)).
% 26.05/26.27 thf(ax3208, axiom, (~(p30)|p71), file('<stdin>', ax3208)).
% 26.05/26.27 thf(ax3282, axiom, p3, file('<stdin>', ax3282)).
% 26.05/26.27 thf(ax575, axiom, (~(p2142)|p2016|p2141), file('<stdin>', ax575)).
% 26.05/26.27 thf(nax58, axiom, (p58<=![X1:g]:(~((fcGRP_ASSOC @ f__0=>~(fcGRP_UNIT @ f__0 @ X1)))=>~(fcGRP_INVERSE @ f__0 @ X1))), file('<stdin>', nax58)).
% 26.05/26.27 thf(ax573, axiom, (~(p2140)|~(p71)|~(p2139)), file('<stdin>', ax573)).
% 26.05/26.27 thf(ax574, axiom, (~(p2141)|p2140), file('<stdin>', ax574)).
% 26.05/26.27 thf(ax3204, axiom, (~(p64)|p79), file('<stdin>', ax3204)).
% 26.05/26.27 thf(nax2032, axiom, (p2032<=(fcGRP_ASSOC @ f__0=>~(fcGRP_DIVISORS @ f__0))), file('<stdin>', nax2032)).
% 26.05/26.27 thf(ax3237, axiom, (~(p5)|p43), file('<stdin>', ax3237)).
% 26.05/26.27 thf(ax3156, axiom, (~(p79)|p126), file('<stdin>', ax3156)).
% 26.05/26.27 thf(pax2242, axiom, (p2242=>(fcGRP_ASSOC @ f__0=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', pax2242)).
% 26.05/26.27 thf(ax3210, axiom, (~(p43)|p69), file('<stdin>', ax3210)).
% 26.05/26.27 thf(ax3280, axiom, p5, file('<stdin>', ax3280)).
% 26.05/26.27 thf(ax3155, axiom, (~(p126)|p65|p125), file('<stdin>', ax3155)).
% 26.05/26.27 thf(nax85, axiom, (p85<=![X1:g]:(~((![X2:g, X3:g, X4:g]:(f__0 @ (f__0 @ X3 @ X3) @ X4)=(f__0 @ X2 @ (f__0 @ X3 @ X4))=>~(fcGRP_UNIT @ f__0 @ X1)))=>~(fcGRP_INVERSE @ f__0 @ X1))), file('<stdin>', nax85)).
% 26.05/26.27 thf(ax220, axiom, (p2139|p85|p2242), file('<stdin>', ax220)).
% 26.05/26.27 thf(ax3199, axiom, (~(p64)|p84), file('<stdin>', ax3199)).
% 26.05/26.27 thf(ax3153, axiom, (~(p124)|~(p69)|~(p123)), file('<stdin>', ax3153)).
% 26.05/26.27 thf(ax3154, axiom, (~(p125)|p124), file('<stdin>', ax3154)).
% 26.05/26.27 thf(nax139, axiom, (p139<=![X1:g]:(~((fcGRP_ASSOC @ f__0=>~(![X2:g]:~(((f__0 @ X1 @ X2)=(X2)=>~((f__0 @ X2 @ X1)=(X2)))))))=>~(![X2:g]:~(![X3:g]:((f__0 @ X2 @ X3)=(X1)=>~((f__0 @ X3 @ X2)=(X1))))))), file('<stdin>', nax139)).
% 26.05/26.27 thf(ax3244, axiom, (~(p4)|p37), file('<stdin>', ax3244)).
% 26.05/26.27 thf(ax2957, axiom, (~(p84)|p298), file('<stdin>', ax2957)).
% 26.05/26.27 thf(ax664, axiom, (~(p2051)|p2074), file('<stdin>', ax664)).
% 26.05/26.27 thf(ax3209, axiom, (~(p37)|p70), file('<stdin>', ax3209)).
% 26.05/26.27 thf(ax3281, axiom, p4, file('<stdin>', ax3281)).
% 26.05/26.27 thf(ax2956, axiom, (~(p298)|p123|p297), file('<stdin>', ax2956)).
% 26.05/26.27 thf(ax660, axiom, (~(p90)|p2078), file('<stdin>', ax660)).
% 26.05/26.27 thf(ax663, axiom, (~(p2074)|~(p1999)|p2073), file('<stdin>', ax663)).
% 26.05/26.27 thf(ax2954, axiom, (~(p296)|~(p70)|~(p295)), file('<stdin>', ax2954)).
% 26.05/26.27 thf(ax2955, axiom, (~(p297)|p296), file('<stdin>', ax2955)).
% 26.05/26.27 thf(ax659, axiom, (~(p2078)|~(p1999)|p2077), file('<stdin>', ax659)).
% 26.05/26.27 thf(ax661, axiom, (~(p2072)|~(p71)|p2071), file('<stdin>', ax661)).
% 26.05/26.27 thf(ax662, axiom, (~(p2073)|p2072), file('<stdin>', ax662)).
% 26.05/26.27 thf(ax657, axiom, (~(p2076)|~(p86)|p2075), file('<stdin>', ax657)).
% 26.05/26.27 thf(ax658, axiom, (~(p2077)|p2076), file('<stdin>', ax658)).
% 26.05/26.27 thf(ax2914, axiom, (p131|~(p85)|p16), file('<stdin>', ax2914)).
% 26.05/26.27 thf(ax2550, axiom, (p295|~(p139)|p16), file('<stdin>', ax2550)).
% 26.05/26.27 thf(ax351, axiom, (~(p2071)|~(p16)|~(p2242)), file('<stdin>', ax351)).
% 26.05/26.27 thf(ax337, axiom, (~(p2075)|~(p16)|~(p2265)), file('<stdin>', ax337)).
% 26.05/26.27 thf(ax2549, axiom, (p295|p139|~(p16)), file('<stdin>', ax2549)).
% 26.05/26.27 thf(nax2242, axiom, (p2242<=(fcGRP_ASSOC @ f__0=>~(![X1:g, X2:g]:~((~(![X3:g]:~((f__0 @ X1 @ X3)=(X2)))=>![X3:g]:~((f__0 @ X3 @ X1)=(X2))))))), file('<stdin>', nax2242)).
% 26.05/26.27 thf(nax2265, axiom, (p2265<=(![X1:g, X2:g, X3:g]:(f__0 @ (f__0 @ X2 @ X2) @ X3)=(f__0 @ X1 @ (f__0 @ X2 @ X3))=>~(fcGRP_DIVISORS @ f__0))), file('<stdin>', nax2265)).
% 26.05/26.27 thf(ax2908, axiom, (~(p139)|p332), file('<stdin>', ax2908)).
% 26.05/26.27 thf(pax332, axiom, (p332=>(~((fcGRP_ASSOC @ f__0=>~(![X1:g]:~(((f__0 @ f__1 @ X1)=(X1)=>~((f__0 @ X1 @ f__1)=(X1)))))))=>~(![X1:g]:~(![X2:g]:((f__0 @ X1 @ X2)=(f__1)=>~((f__0 @ X2 @ X1)=(f__1))))))), file('<stdin>', pax332)).
% 26.05/26.27 thf(c_0_80, plain, (~p64|p63), inference(fof_simplification,[status(thm)],[ax3220])).
% 26.05/26.27 thf(c_0_81, plain, (~p6|p57), inference(fof_simplification,[status(thm)],[ax3222])).
% 26.05/26.27 thf(c_0_82, plain, (~p63|p68), inference(fof_simplification,[status(thm)],[ax3214])).
% 26.05/26.27 thf(c_0_83, plain, (p63|~p64), inference(split_conjunct,[status(thm)],[c_0_80])).
% 26.05/26.27 thf(c_0_84, plain, p64, inference(split_conjunct,[status(thm)],[ax3221])).
% 26.05/26.27 thf(c_0_85, plain, (p1|~p8), inference(fof_simplification,[status(thm)],[ax3277])).
% 26.05/26.27 thf(c_0_86, plain, ~p1, inference(fof_simplification,[status(thm)],[ax3284])).
% 26.05/26.27 thf(c_0_87, plain, (~p57|p59), inference(fof_simplification,[status(thm)],[ax3215])).
% 26.05/26.27 thf(c_0_88, plain, (p57|~p6), inference(split_conjunct,[status(thm)],[c_0_81])).
% 26.05/26.27 thf(c_0_89, plain, p6, inference(split_conjunct,[status(thm)],[ax3279])).
% 26.05/26.27 thf(c_0_90, plain, (~p68|p8|p67), inference(fof_simplification,[status(thm)],[ax3213])).
% 26.05/26.27 thf(c_0_91, plain, (p68|~p63), inference(split_conjunct,[status(thm)],[c_0_82])).
% 26.05/26.27 thf(c_0_92, plain, p63, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84])])).
% 26.05/26.27 thf(c_0_93, plain, (p1|~p8), inference(split_conjunct,[status(thm)],[c_0_85])).
% 26.05/26.27 thf(c_0_94, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_86])).
% 26.05/26.27 thf(c_0_95, plain, (~p91|p90), inference(fof_simplification,[status(thm)],[ax3193])).
% 26.05/26.27 thf(c_0_96, plain, (~p66|~p59|~p65), inference(fof_simplification,[status(thm)],[ax3211])).
% 26.05/26.27 thf(c_0_97, plain, (p59|~p57), inference(split_conjunct,[status(thm)],[c_0_87])).
% 26.05/26.27 thf(c_0_98, plain, p57, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 26.05/26.27 thf(c_0_99, plain, (~p67|p66), inference(fof_simplification,[status(thm)],[ax3212])).
% 26.05/26.27 thf(c_0_100, plain, (p8|p67|~p68), inference(split_conjunct,[status(thm)],[c_0_90])).
% 26.05/26.27 thf(c_0_101, plain, p68, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_92])])).
% 26.05/26.27 thf(c_0_102, plain, ~p8, inference(sr,[status(thm)],[c_0_93, c_0_94])).
% 26.05/26.27 thf(c_0_103, plain, (~p2|p24), inference(fof_simplification,[status(thm)],[ax3259])).
% 26.05/26.27 thf(c_0_104, plain, (~p90|p134), inference(fof_simplification,[status(thm)],[ax3148])).
% 26.05/26.27 thf(c_0_105, plain, (p90|~p91), inference(split_conjunct,[status(thm)],[c_0_95])).
% 26.05/26.27 thf(c_0_106, plain, p91, inference(split_conjunct,[status(thm)],[ax3194])).
% 26.05/26.27 thf(c_0_107, plain, (~p66|~p59|~p65), inference(split_conjunct,[status(thm)],[c_0_96])).
% 26.05/26.27 thf(c_0_108, plain, p59, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_98])])).
% 26.05/26.27 thf(c_0_109, plain, (p66|~p67), inference(split_conjunct,[status(thm)],[c_0_99])).
% 26.05/26.27 thf(c_0_110, plain, p67, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_100, c_0_101])]), c_0_102])).
% 26.05/26.27 thf(c_0_111, plain, (~p24|p86), inference(fof_simplification,[status(thm)],[ax3188])).
% 26.05/26.27 thf(c_0_112, plain, (p24|~p2), inference(split_conjunct,[status(thm)],[c_0_103])).
% 26.05/26.27 thf(c_0_113, plain, p2, inference(split_conjunct,[status(thm)],[ax3283])).
% 26.05/26.27 thf(c_0_114, plain, (~p134|p65|p133), inference(fof_simplification,[status(thm)],[ax3147])).
% 26.05/26.27 thf(c_0_115, plain, (p134|~p90), inference(split_conjunct,[status(thm)],[c_0_104])).
% 26.05/26.27 thf(c_0_116, plain, p90, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_105, c_0_106])])).
% 26.05/26.27 thf(c_0_117, plain, (~p65|~p66), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_107, c_0_108])])).
% 26.05/26.27 thf(c_0_118, plain, p66, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_109, c_0_110])])).
% 26.05/26.27 thf(c_0_119, plain, (~p91|p2003), inference(fof_simplification,[status(thm)],[ax742])).
% 26.05/26.27 thf(c_0_120, plain, (~p132|~p86|~p131), inference(fof_simplification,[status(thm)],[ax3145])).
% 26.05/26.27 thf(c_0_121, plain, (p86|~p24), inference(split_conjunct,[status(thm)],[c_0_111])).
% 26.05/26.27 thf(c_0_122, plain, p24, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])])).
% 26.05/26.27 thf(c_0_123, plain, (~p133|p132), inference(fof_simplification,[status(thm)],[ax3146])).
% 26.05/26.27 thf(c_0_124, plain, (p65|p133|~p134), inference(split_conjunct,[status(thm)],[c_0_114])).
% 26.05/26.27 thf(c_0_125, plain, p134, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_115, c_0_116])])).
% 26.05/26.27 thf(c_0_126, plain, ~p65, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_118])])).
% 26.05/26.27 thf(c_0_127, plain, (~p7|p1997), inference(fof_simplification,[status(thm)],[ax743])).
% 26.05/26.27 thf(c_0_128, plain, (~p2003|p2031), inference(fof_simplification,[status(thm)],[ax712])).
% 26.05/26.27 thf(c_0_129, plain, (p2003|~p91), inference(split_conjunct,[status(thm)],[c_0_119])).
% 26.05/26.27 thf(c_0_130, plain, (~p2003|p2019), inference(fof_simplification,[status(thm)],[ax724])).
% 26.05/26.27 thf(c_0_131, plain, (~p132|~p86|~p131), inference(split_conjunct,[status(thm)],[c_0_120])).
% 26.05/26.27 thf(c_0_132, plain, p86, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_121, c_0_122])])).
% 26.05/26.27 thf(c_0_133, plain, (p132|~p133), inference(split_conjunct,[status(thm)],[c_0_123])).
% 26.05/26.27 thf(c_0_134, plain, p133, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124, c_0_125])]), c_0_126])).
% 26.05/26.27 thf(c_0_135, plain, (~p1997|p1999), inference(fof_simplification,[status(thm)],[ax737])).
% 26.05/26.27 thf(c_0_136, plain, (p1997|~p7), inference(split_conjunct,[status(thm)],[c_0_127])).
% 26.05/26.27 thf(c_0_137, plain, p7, inference(split_conjunct,[status(thm)],[ax3278])).
% 26.05/26.27 thf(c_0_138, plain, (~p2031|p65|p2030), inference(fof_simplification,[status(thm)],[ax711])).
% 26.05/26.27 thf(c_0_139, plain, (p2031|~p2003), inference(split_conjunct,[status(thm)],[c_0_128])).
% 26.05/26.27 thf(c_0_140, plain, p2003, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_129, c_0_106])])).
% 26.05/26.27 thf(c_0_141, plain, (~p2019|p131|p2018), inference(fof_simplification,[status(thm)],[ax723])).
% 26.05/26.27 thf(c_0_142, plain, (p2019|~p2003), inference(split_conjunct,[status(thm)],[c_0_130])).
% 26.05/26.27 thf(c_0_143, plain, (~p131|~p132), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_132])])).
% 26.05/26.27 thf(c_0_144, plain, p132, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_133, c_0_134])])).
% 26.05/26.27 thf(c_0_145, plain, (~p2029|~p1999|~p2028), inference(fof_simplification,[status(thm)],[ax709])).
% 26.05/26.27 thf(c_0_146, plain, (p1999|~p1997), inference(split_conjunct,[status(thm)],[c_0_135])).
% 26.05/26.27 thf(c_0_147, plain, p1997, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_136, c_0_137])])).
% 26.05/26.27 thf(c_0_148, plain, (~p2030|p2029), inference(fof_simplification,[status(thm)],[ax710])).
% 26.05/26.27 thf(c_0_149, plain, (p65|p2030|~p2031), inference(split_conjunct,[status(thm)],[c_0_138])).
% 26.05/26.27 thf(c_0_150, plain, p2031, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_139, c_0_140])])).
% 26.05/26.27 thf(c_0_151, plain, (~p91|p2051), inference(fof_simplification,[status(thm)],[ax692])).
% 26.05/26.27 thf(c_0_152, plain, (~p2017|~p1999|~p2016), inference(fof_simplification,[status(thm)],[ax721])).
% 26.05/26.27 thf(c_0_153, plain, (~p2018|p2017), inference(fof_simplification,[status(thm)],[ax722])).
% 26.05/26.27 thf(c_0_154, plain, (p131|p2018|~p2019), inference(split_conjunct,[status(thm)],[c_0_141])).
% 26.05/26.27 thf(c_0_155, plain, p2019, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_142, c_0_140])])).
% 26.05/26.27 thf(c_0_156, plain, ~p131, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_143, c_0_144])])).
% 26.05/26.27 thf(c_0_157, plain, (~p2029|~p1999|~p2028), inference(split_conjunct,[status(thm)],[c_0_145])).
% 26.05/26.27 thf(c_0_158, plain, p1999, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_146, c_0_147])])).
% 26.05/26.27 thf(c_0_159, plain, (p2029|~p2030), inference(split_conjunct,[status(thm)],[c_0_148])).
% 26.05/26.27 thf(c_0_160, plain, p2030, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149, c_0_150])]), c_0_126])).
% 26.05/26.27 thf(c_0_161, plain, (~p3|p30), inference(fof_simplification,[status(thm)],[ax3252])).
% 26.05/26.27 thf(c_0_162, plain, (~p2051|p2142), inference(fof_simplification,[status(thm)],[ax576])).
% 26.05/26.27 thf(c_0_163, plain, (p2051|~p91), inference(split_conjunct,[status(thm)],[c_0_151])).
% 26.05/26.27 thf(c_0_164, plain, (~p2017|~p1999|~p2016), inference(split_conjunct,[status(thm)],[c_0_152])).
% 26.05/26.27 thf(c_0_165, plain, (p2017|~p2018), inference(split_conjunct,[status(thm)],[c_0_153])).
% 26.05/26.27 thf(c_0_166, plain, p2018, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_154, c_0_155])]), c_0_156])).
% 26.05/26.27 thf(c_0_167, plain, (p2028|~p58|~p2032), inference(fof_simplification,[status(thm)],[ax482])).
% 26.05/26.27 thf(c_0_168, plain, (~p2028|~p2029), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_158])])).
% 26.05/26.27 thf(c_0_169, plain, p2029, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_159, c_0_160])])).
% 26.05/26.27 thf(c_0_170, plain, (~p30|p71), inference(fof_simplification,[status(thm)],[ax3208])).
% 26.05/26.27 thf(c_0_171, plain, (p30|~p3), inference(split_conjunct,[status(thm)],[c_0_161])).
% 26.05/26.27 thf(c_0_172, plain, p3, inference(split_conjunct,[status(thm)],[ax3282])).
% 26.05/26.27 thf(c_0_173, plain, (~p2142|p2016|p2141), inference(fof_simplification,[status(thm)],[ax575])).
% 26.05/26.27 thf(c_0_174, plain, (p2142|~p2051), inference(split_conjunct,[status(thm)],[c_0_162])).
% 26.05/26.27 thf(c_0_175, plain, p2051, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_163, c_0_106])])).
% 26.05/26.27 thf(c_0_176, plain, (~p2016|~p2017), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_164, c_0_158])])).
% 26.05/26.27 thf(c_0_177, plain, p2017, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_165, c_0_166])])).
% 26.05/26.27 thf(c_0_178, plain, (p2028|~p58|~p2032), inference(split_conjunct,[status(thm)],[c_0_167])).
% 26.05/26.27 thf(c_0_179, plain, ~p2028, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_168, c_0_169])])).
% 26.05/26.27 thf(c_0_180, plain, (((fcGRP_ASSOC @ f__0|p58)&(fcGRP_UNIT @ f__0 @ esk92_0|p58))&(fcGRP_INVERSE @ f__0 @ esk92_0|p58)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax58])])])])])).
% 26.05/26.27 thf(c_0_181, plain, (~p2140|~p71|~p2139), inference(fof_simplification,[status(thm)],[ax573])).
% 26.05/26.27 thf(c_0_182, plain, (p71|~p30), inference(split_conjunct,[status(thm)],[c_0_170])).
% 26.05/26.27 thf(c_0_183, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_171, c_0_172])])).
% 26.05/26.27 thf(c_0_184, plain, (~p2141|p2140), inference(fof_simplification,[status(thm)],[ax574])).
% 26.05/26.27 thf(c_0_185, plain, (p2016|p2141|~p2142), inference(split_conjunct,[status(thm)],[c_0_173])).
% 26.05/26.27 thf(c_0_186, plain, p2142, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_174, c_0_175])])).
% 26.05/26.27 thf(c_0_187, plain, ~p2016, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_176, c_0_177])])).
% 26.05/26.27 thf(c_0_188, plain, (~p64|p79), inference(fof_simplification,[status(thm)],[ax3204])).
% 26.05/26.27 thf(c_0_189, plain, ((fcGRP_ASSOC @ f__0|p2032)&(fcGRP_DIVISORS @ f__0|p2032)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2032])])])).
% 26.05/26.27 thf(c_0_190, plain, (~p58|~p2032), inference(sr,[status(thm)],[c_0_178, c_0_179])).
% 26.05/26.27 thf(c_0_191, plain, (fcGRP_ASSOC @ f__0|p58), inference(split_conjunct,[status(thm)],[c_0_180])).
% 26.05/26.27 thf(c_0_192, plain, (~p2140|~p71|~p2139), inference(split_conjunct,[status(thm)],[c_0_181])).
% 26.05/26.27 thf(c_0_193, plain, p71, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_182, c_0_183])])).
% 26.05/26.27 thf(c_0_194, plain, (p2140|~p2141), inference(split_conjunct,[status(thm)],[c_0_184])).
% 26.05/26.27 thf(c_0_195, plain, p2141, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_185, c_0_186])]), c_0_187])).
% 26.05/26.27 thf(c_0_196, plain, (~p5|p43), inference(fof_simplification,[status(thm)],[ax3237])).
% 26.05/26.27 thf(c_0_197, plain, (~p79|p126), inference(fof_simplification,[status(thm)],[ax3156])).
% 26.05/26.27 thf(c_0_198, plain, (p79|~p64), inference(split_conjunct,[status(thm)],[c_0_188])).
% 26.05/26.27 thf(c_0_199, plain, ![X58:g, X59:g]:(~p2242|(~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)],[pax2242])])])])])).
% 26.05/26.27 thf(c_0_200, plain, (fcGRP_ASSOC @ f__0|p2032), inference(split_conjunct,[status(thm)],[c_0_189])).
% 26.05/26.27 thf(c_0_201, plain, (fcGRP_ASSOC @ f__0|~p2032), inference(spm,[status(thm)],[c_0_190, c_0_191])).
% 26.05/26.27 thf(c_0_202, plain, (~p2139|~p2140), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192, c_0_193])])).
% 26.05/26.27 thf(c_0_203, plain, p2140, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_194, c_0_195])])).
% 26.05/26.27 thf(c_0_204, plain, (~p43|p69), inference(fof_simplification,[status(thm)],[ax3210])).
% 26.05/26.27 thf(c_0_205, plain, (p43|~p5), inference(split_conjunct,[status(thm)],[c_0_196])).
% 26.05/26.27 thf(c_0_206, plain, p5, inference(split_conjunct,[status(thm)],[ax3280])).
% 26.05/26.27 thf(c_0_207, plain, (~p126|p65|p125), inference(fof_simplification,[status(thm)],[ax3155])).
% 26.05/26.27 thf(c_0_208, plain, (p126|~p79), inference(split_conjunct,[status(thm)],[c_0_197])).
% 26.05/26.27 thf(c_0_209, plain, p79, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_198, c_0_84])])).
% 26.05/26.27 thf(c_0_210, plain, ![X1:g, X2:g]:(~p2242|~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_199])).
% 26.05/26.27 thf(c_0_211, plain, fcGRP_ASSOC @ f__0, inference(csr,[status(thm)],[c_0_200, c_0_201])).
% 26.05/26.27 thf(c_0_212, plain, ![X176:g, X177:g, X178:g]:((((f__0 @ (f__0 @ X177 @ X177) @ X178)=(f__0 @ X176 @ (f__0 @ X177 @ X178))|p85)&(fcGRP_UNIT @ f__0 @ esk85_0|p85))&(fcGRP_INVERSE @ f__0 @ esk85_0|p85)), 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)],[nax85])])])])])])).
% 26.05/26.27 thf(c_0_213, plain, (p2139|p85|p2242), inference(split_conjunct,[status(thm)],[ax220])).
% 26.05/26.27 thf(c_0_214, plain, ~p2139, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_202, c_0_203])])).
% 26.05/26.27 thf(c_0_215, plain, (~p64|p84), inference(fof_simplification,[status(thm)],[ax3199])).
% 26.05/26.27 thf(c_0_216, plain, (~p124|~p69|~p123), inference(fof_simplification,[status(thm)],[ax3153])).
% 26.05/26.27 thf(c_0_217, plain, (p69|~p43), inference(split_conjunct,[status(thm)],[c_0_204])).
% 26.05/26.27 thf(c_0_218, plain, p43, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_205, c_0_206])])).
% 26.05/26.27 thf(c_0_219, plain, (~p125|p124), inference(fof_simplification,[status(thm)],[ax3154])).
% 26.05/26.27 thf(c_0_220, plain, (p65|p125|~p126), inference(split_conjunct,[status(thm)],[c_0_207])).
% 26.05/26.27 thf(c_0_221, plain, p126, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_208, c_0_209])])).
% 26.05/26.27 thf(c_0_222, plain, ![X1:g, X2:g]:((f__0 @ X1 @ esk24_0)!=(esk25_0)|(f__0 @ esk24_0 @ X2)!=(esk25_0)|~p2242), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210, c_0_211])])).
% 26.05/26.27 thf(c_0_223, plain, ![X1:g, X3:g, X2:g]:((f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ X3 @ (f__0 @ X1 @ X2))|p85), inference(split_conjunct,[status(thm)],[c_0_212])).
% 26.05/26.27 thf(c_0_224, plain, (p85|p2242), inference(sr,[status(thm)],[c_0_213, c_0_214])).
% 26.05/26.27 thf(c_0_225, plain, ![X168:g, X169:g]:(((fcGRP_ASSOC @ f__0|p139)&(((f__0 @ esk80_0 @ X168)=(X168)|p139)&((f__0 @ X168 @ esk80_0)=(X168)|p139)))&(((f__0 @ X169 @ (esk81_1 @ X169))=(esk80_0)|p139)&((f__0 @ (esk81_1 @ X169) @ X169)=(esk80_0)|p139))), 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)],[nax139])])])])])])).
% 26.05/26.27 thf(c_0_226, plain, (~p4|p37), inference(fof_simplification,[status(thm)],[ax3244])).
% 26.05/26.27 thf(c_0_227, plain, (~p84|p298), inference(fof_simplification,[status(thm)],[ax2957])).
% 26.05/26.27 thf(c_0_228, plain, (p84|~p64), inference(split_conjunct,[status(thm)],[c_0_215])).
% 26.05/26.27 thf(c_0_229, plain, (~p124|~p69|~p123), inference(split_conjunct,[status(thm)],[c_0_216])).
% 26.05/26.27 thf(c_0_230, plain, p69, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_217, c_0_218])])).
% 26.05/26.27 thf(c_0_231, plain, (p124|~p125), inference(split_conjunct,[status(thm)],[c_0_219])).
% 26.05/26.27 thf(c_0_232, plain, p125, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_220, c_0_221])]), c_0_126])).
% 26.05/26.27 thf(c_0_233, plain, (~p2051|p2074), inference(fof_simplification,[status(thm)],[ax664])).
% 26.05/26.27 thf(c_0_234, plain, ![X1:g, X2:g, X3:g]:(p85|(f__0 @ X1 @ (f__0 @ X2 @ esk24_0))!=(esk25_0)|(f__0 @ esk24_0 @ X3)!=(esk25_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_222, c_0_223]), c_0_224])).
% 26.05/26.27 thf(c_0_235, plain, ![X1:g]:((f__0 @ (esk81_1 @ X1) @ X1)=(esk80_0)|p139), inference(split_conjunct,[status(thm)],[c_0_225])).
% 26.05/26.27 thf(c_0_236, plain, (~p37|p70), inference(fof_simplification,[status(thm)],[ax3209])).
% 26.05/26.27 thf(c_0_237, plain, (p37|~p4), inference(split_conjunct,[status(thm)],[c_0_226])).
% 26.05/26.27 thf(c_0_238, plain, p4, inference(split_conjunct,[status(thm)],[ax3281])).
% 26.05/26.27 thf(c_0_239, plain, (~p298|p123|p297), inference(fof_simplification,[status(thm)],[ax2956])).
% 26.05/26.27 thf(c_0_240, plain, (p298|~p84), inference(split_conjunct,[status(thm)],[c_0_227])).
% 26.05/26.27 thf(c_0_241, plain, p84, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_228, c_0_84])])).
% 26.05/26.27 thf(c_0_242, plain, (~p123|~p124), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_229, c_0_230])])).
% 26.05/26.27 thf(c_0_243, plain, p124, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_231, c_0_232])])).
% 26.05/26.27 thf(c_0_244, plain, (~p90|p2078), inference(fof_simplification,[status(thm)],[ax660])).
% 26.05/26.27 thf(c_0_245, plain, (~p2074|~p1999|p2073), inference(fof_simplification,[status(thm)],[ax663])).
% 26.05/26.27 thf(c_0_246, plain, (p2074|~p2051), inference(split_conjunct,[status(thm)],[c_0_233])).
% 26.05/26.27 thf(c_0_247, plain, ![X1:g, X2:g]:(p139|p85|(f__0 @ X1 @ esk80_0)!=(esk25_0)|(f__0 @ esk24_0 @ X2)!=(esk25_0)), inference(spm,[status(thm)],[c_0_234, c_0_235])).
% 26.05/26.27 thf(c_0_248, plain, ![X1:g]:((f__0 @ X1 @ esk80_0)=(X1)|p139), inference(split_conjunct,[status(thm)],[c_0_225])).
% 26.05/26.27 thf(c_0_249, plain, (~p296|~p70|~p295), inference(fof_simplification,[status(thm)],[ax2954])).
% 26.05/26.27 thf(c_0_250, plain, (p70|~p37), inference(split_conjunct,[status(thm)],[c_0_236])).
% 26.05/26.27 thf(c_0_251, plain, p37, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_237, c_0_238])])).
% 26.05/26.27 thf(c_0_252, plain, (~p297|p296), inference(fof_simplification,[status(thm)],[ax2955])).
% 26.05/26.27 thf(c_0_253, plain, (p123|p297|~p298), inference(split_conjunct,[status(thm)],[c_0_239])).
% 26.05/26.27 thf(c_0_254, plain, p298, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_240, c_0_241])])).
% 26.05/26.27 thf(c_0_255, plain, ~p123, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_242, c_0_243])])).
% 26.05/26.27 thf(c_0_256, plain, (~p2078|~p1999|p2077), inference(fof_simplification,[status(thm)],[ax659])).
% 26.05/26.27 thf(c_0_257, plain, (p2078|~p90), inference(split_conjunct,[status(thm)],[c_0_244])).
% 26.05/26.27 thf(c_0_258, plain, (~p2072|~p71|p2071), inference(fof_simplification,[status(thm)],[ax661])).
% 26.05/26.27 thf(c_0_259, plain, (~p2073|p2072), inference(fof_simplification,[status(thm)],[ax662])).
% 26.05/26.27 thf(c_0_260, plain, (p2073|~p2074|~p1999), inference(split_conjunct,[status(thm)],[c_0_245])).
% 26.05/26.27 thf(c_0_261, plain, p2074, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_246, c_0_175])])).
% 26.05/26.27 thf(c_0_262, plain, ![X1:g]:(p85|p139|(f__0 @ esk24_0 @ X1)!=(esk25_0)), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_247, c_0_248])])).
% 26.05/26.27 thf(c_0_263, plain, (~p296|~p70|~p295), inference(split_conjunct,[status(thm)],[c_0_249])).
% 26.05/26.27 thf(c_0_264, plain, p70, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_250, c_0_251])])).
% 26.05/26.27 thf(c_0_265, plain, (p296|~p297), inference(split_conjunct,[status(thm)],[c_0_252])).
% 26.05/26.27 thf(c_0_266, plain, p297, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_253, c_0_254])]), c_0_255])).
% 26.05/26.27 thf(c_0_267, plain, (~p2076|~p86|p2075), inference(fof_simplification,[status(thm)],[ax657])).
% 26.05/26.27 thf(c_0_268, plain, (~p2077|p2076), inference(fof_simplification,[status(thm)],[ax658])).
% 26.05/26.27 thf(c_0_269, plain, (p2077|~p2078|~p1999), inference(split_conjunct,[status(thm)],[c_0_256])).
% 26.05/26.27 thf(c_0_270, plain, p2078, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_257, c_0_116])])).
% 26.05/26.27 thf(c_0_271, plain, (p2071|~p2072|~p71), inference(split_conjunct,[status(thm)],[c_0_258])).
% 26.05/26.27 thf(c_0_272, plain, (p2072|~p2073), inference(split_conjunct,[status(thm)],[c_0_259])).
% 26.05/26.27 thf(c_0_273, plain, p2073, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_260, c_0_158]), c_0_261])])).
% 26.05/26.27 thf(c_0_274, plain, (p131|~p85|p16), inference(fof_simplification,[status(thm)],[ax2914])).
% 26.05/26.27 thf(c_0_275, plain, ![X1:g, X2:g]:(p139|p85|(f__0 @ (f__0 @ X1 @ X1) @ X2)!=(esk25_0)), inference(spm,[status(thm)],[c_0_262, c_0_223])).
% 26.05/26.27 thf(c_0_276, plain, (p295|~p139|p16), inference(fof_simplification,[status(thm)],[ax2550])).
% 26.05/26.27 thf(c_0_277, plain, (~p295|~p296), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_263, c_0_264])])).
% 26.05/26.27 thf(c_0_278, plain, p296, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_265, c_0_266])])).
% 26.05/26.27 thf(c_0_279, plain, (p2075|~p2076|~p86), inference(split_conjunct,[status(thm)],[c_0_267])).
% 26.05/26.27 thf(c_0_280, plain, (p2076|~p2077), inference(split_conjunct,[status(thm)],[c_0_268])).
% 26.05/26.27 thf(c_0_281, plain, p2077, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_269, c_0_158]), c_0_270])])).
% 26.05/26.27 thf(c_0_282, plain, (~p2071|~p16|~p2242), inference(fof_simplification,[status(thm)],[ax351])).
% 26.05/26.27 thf(c_0_283, plain, (p2071|~p2072), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_271, c_0_193])])).
% 26.05/26.27 thf(c_0_284, plain, p2072, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_272, c_0_273])])).
% 26.05/26.27 thf(c_0_285, plain, (p131|p16|~p85), inference(split_conjunct,[status(thm)],[c_0_274])).
% 26.05/26.27 thf(c_0_286, plain, ![X1:g]:(p85|p139|(f__0 @ esk80_0 @ X1)!=(esk25_0)), inference(spm,[status(thm)],[c_0_275, c_0_248])).
% 26.05/26.27 thf(c_0_287, plain, ![X1:g]:((f__0 @ esk80_0 @ X1)=(X1)|p139), inference(split_conjunct,[status(thm)],[c_0_225])).
% 26.05/26.27 thf(c_0_288, plain, (p295|p16|~p139), inference(split_conjunct,[status(thm)],[c_0_276])).
% 26.05/26.27 thf(c_0_289, plain, ~p295, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_277, c_0_278])])).
% 26.05/26.27 thf(c_0_290, plain, (~p2075|~p16|~p2265), inference(fof_simplification,[status(thm)],[ax337])).
% 26.05/26.27 thf(c_0_291, plain, (p2075|~p2076), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_279, c_0_132])])).
% 26.05/26.27 thf(c_0_292, plain, p2076, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_280, c_0_281])])).
% 26.05/26.27 thf(c_0_293, plain, (p295|p139|~p16), inference(fof_simplification,[status(thm)],[ax2549])).
% 26.05/26.27 thf(c_0_294, plain, (~p2071|~p16|~p2242), inference(split_conjunct,[status(thm)],[c_0_282])).
% 26.05/26.27 thf(c_0_295, plain, p2071, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_283, c_0_284])])).
% 26.05/26.27 thf(c_0_296, plain, (p16|~p85), inference(sr,[status(thm)],[c_0_285, c_0_156])).
% 26.05/26.27 thf(c_0_297, plain, (p139|p85), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_286, c_0_287])])).
% 26.05/26.27 thf(c_0_298, plain, (p16|~p139), inference(sr,[status(thm)],[c_0_288, c_0_289])).
% 26.05/26.27 thf(c_0_299, plain, (~p2075|~p16|~p2265), inference(split_conjunct,[status(thm)],[c_0_290])).
% 26.05/26.27 thf(c_0_300, plain, p2075, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_291, c_0_292])])).
% 26.05/26.27 thf(c_0_301, plain, (p295|p139|~p16), inference(split_conjunct,[status(thm)],[c_0_293])).
% 26.05/26.27 thf(c_0_302, plain, ![X60:g, X61:g, X63:g, X64:g]:((fcGRP_ASSOC @ f__0|p2242)&(((f__0 @ X60 @ (esk26_2 @ X60 @ X61))=(X61)|p2242)&((f__0 @ (esk27_2 @ X63 @ X64) @ X63)=(X64)|p2242))), 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)],[nax2242])])])])])])])).
% 26.05/26.27 thf(c_0_303, plain, (~p16|~p2242), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_294, c_0_295])])).
% 26.05/26.27 thf(c_0_304, plain, p16, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_296, c_0_297]), c_0_298])).
% 26.05/26.27 thf(c_0_305, plain, ![X43:g, X44:g, X45:g]:(((f__0 @ (f__0 @ X44 @ X44) @ X45)=(f__0 @ X43 @ (f__0 @ X44 @ X45))|p2265)&(fcGRP_DIVISORS @ f__0|p2265)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2265])])])])])).
% 26.05/26.27 thf(c_0_306, plain, (~p16|~p2265), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_299, c_0_300])])).
% 26.05/26.27 thf(c_0_307, plain, (~p139|p332), inference(fof_simplification,[status(thm)],[ax2908])).
% 26.05/26.27 thf(c_0_308, plain, (p139|~p16), inference(sr,[status(thm)],[c_0_301, c_0_289])).
% 26.05/26.27 thf(c_0_309, plain, ![X1:g, X2:g]:((f__0 @ (esk27_2 @ X1 @ X2) @ X1)=(X2)|p2242), inference(split_conjunct,[status(thm)],[c_0_302])).
% 26.05/26.27 thf(c_0_310, plain, ~p2242, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_303, c_0_304])])).
% 26.05/26.27 thf(c_0_311, plain, ![X1:g, X3:g, X2:g]:((f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ X3 @ (f__0 @ X1 @ X2))|p2265), inference(split_conjunct,[status(thm)],[c_0_305])).
% 26.05/26.27 thf(c_0_312, plain, ~p2265, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_306, c_0_304])])).
% 26.05/26.27 thf(c_0_313, plain, ![X102:g]:(~p332|(~fcGRP_ASSOC @ f__0|((f__0 @ f__1 @ esk45_0)!=(esk45_0)|(f__0 @ esk45_0 @ f__1)!=(esk45_0))|((f__0 @ esk46_0 @ X102)!=(f__1)|(f__0 @ X102 @ esk46_0)!=(f__1)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax332])])])])])).
% 26.05/26.27 thf(c_0_314, plain, (p332|~p139), inference(split_conjunct,[status(thm)],[c_0_307])).
% 26.05/26.27 thf(c_0_315, plain, p139, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_308, c_0_304])])).
% 26.05/26.27 thf(c_0_316, plain, ![X1:g, X2:g]:((f__0 @ X1 @ (esk26_2 @ X1 @ X2))=(X2)|p2242), inference(split_conjunct,[status(thm)],[c_0_302])).
% 26.05/26.27 thf(c_0_317, plain, ![X1:g, X2:g]:(f__0 @ (esk27_2 @ X1 @ X2) @ X1)=(X2), inference(sr,[status(thm)],[c_0_309, c_0_310])).
% 26.05/26.27 thf(c_0_318, plain, ![X1:g, X3:g, X2:g]:(f__0 @ (f__0 @ X1 @ X1) @ X2)=(f__0 @ X3 @ (f__0 @ X1 @ X2)), inference(sr,[status(thm)],[c_0_311, c_0_312])).
% 26.05/26.27 thf(c_0_319, plain, ![X1:g]:(~p332|~fcGRP_ASSOC @ f__0|(f__0 @ f__1 @ esk45_0)!=(esk45_0)|(f__0 @ esk45_0 @ f__1)!=(esk45_0)|(f__0 @ esk46_0 @ X1)!=(f__1)|(f__0 @ X1 @ esk46_0)!=(f__1)), inference(split_conjunct,[status(thm)],[c_0_313])).
% 26.05/26.27 thf(c_0_320, plain, p332, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_314, c_0_315])])).
% 26.05/26.27 thf(c_0_321, plain, ![X1:g, X2:g]:(f__0 @ X1 @ (esk26_2 @ X1 @ X2))=(X2), inference(sr,[status(thm)],[c_0_316, c_0_310])).
% 26.05/26.27 thf(c_0_322, plain, ![X1:g, X2:g, X3:g]:(f__0 @ (f__0 @ X1 @ X1) @ X2)=(X3), inference(spm,[status(thm)],[c_0_317, c_0_318])).
% 26.05/26.27 thf(c_0_323, plain, ![X1:g]:((f__0 @ f__1 @ esk45_0)!=(esk45_0)|(f__0 @ esk45_0 @ f__1)!=(esk45_0)|(f__0 @ X1 @ esk46_0)!=(f__1)|(f__0 @ esk46_0 @ X1)!=(f__1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_319, c_0_211]), c_0_320])])).
% 26.05/26.27 thf(c_0_324, plain, ![X1:g, X2:g]:(X1)=(X2), inference(spm,[status(thm)],[c_0_321, c_0_322])).
% 26.05/26.27 thf(c_0_325, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_323, c_0_324]), c_0_324]), c_0_324]), c_0_324]), ['proof']).
% 26.05/26.27 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 26.05/26.27 thf(0,theorem,(![X1:g>g>g]:((~((![X2:g]:(~(((cGROUP1 @ X1) @ X2)))))) = (cGROUP4 @ X1))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 26.05/26.27 % SZS output end Proof
%------------------------------------------------------------------------------