%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP422-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n007.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 : 600s
% DateTime : Sat Jul 16 10:30:14 EDT 2022
% Result : Unsatisfiable 32.05s 8.33s
% Output : CNFRefutation 32.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP422-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n007.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 : 600
% 0.12/0.33 % DateTime : Mon Jun 13 21:09:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 27559: Facts:
% 0.12/0.34 27559: Id : 2, {_}:
% 0.12/0.34 inverse
% 0.12/0.34 (multiply
% 0.12/0.34 (inverse
% 0.12/0.34 (multiply ?2
% 0.12/0.34 (inverse
% 0.12/0.34 (multiply (inverse ?3)
% 0.12/0.34 (multiply (inverse ?4)
% 0.12/0.34 (inverse (multiply (inverse ?4) ?4)))))))
% 0.12/0.34 (multiply ?2 ?4))
% 0.12/0.34 =>=
% 0.12/0.34 ?3
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 27559: Goal:
% 0.12/0.34 27559: Id : 1, {_}:
% 0.12/0.34 multiply (multiply (inverse b2) b2) a2 =>= a2
% 0.12/0.34 [] by prove_these_axioms_2
% 32.05/8.33 Statistics :
% 32.05/8.33 Max weight : 86
% 32.05/8.33 Found proof, 7.986629s
% 32.05/8.33 % SZS status Unsatisfiable for theBenchmark.p
% 32.05/8.33 % SZS output start CNFRefutation for theBenchmark.p
% 32.05/8.33 Id : 3, {_}: inverse (multiply (inverse (multiply ?6 (inverse (multiply (inverse ?7) (multiply (inverse ?8) (inverse (multiply (inverse ?8) ?8))))))) (multiply ?6 ?8)) =>= ?7 [8, 7, 6] by single_axiom ?6 ?7 ?8
% 32.05/8.33 Id : 2, {_}: inverse (multiply (inverse (multiply ?2 (inverse (multiply (inverse ?3) (multiply (inverse ?4) (inverse (multiply (inverse ?4) ?4))))))) (multiply ?2 ?4)) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 32.05/8.33 Id : 18, {_}: inverse (multiply (inverse (multiply ?69 ?70)) (multiply ?69 ?71)) =?= multiply (inverse ?71) (inverse (multiply (inverse ?70) (multiply (inverse (inverse (multiply (inverse ?71) ?71))) (inverse (multiply (inverse (inverse (multiply (inverse ?71) ?71))) (inverse (multiply (inverse ?71) ?71))))))) [71, 70, 69] by Super 3 with 2 at 2,1,1,1,2
% 32.05/8.33 Id : 7, {_}: inverse (multiply (inverse (multiply ?28 ?29)) (multiply ?28 ?30)) =?= multiply (inverse ?30) (inverse (multiply (inverse ?29) (multiply (inverse (inverse (multiply (inverse ?30) ?30))) (inverse (multiply (inverse (inverse (multiply (inverse ?30) ?30))) (inverse (multiply (inverse ?30) ?30))))))) [30, 29, 28] by Super 3 with 2 at 2,1,1,1,2
% 32.05/8.33 Id : 33, {_}: inverse (multiply (inverse (multiply ?152 ?153)) (multiply ?152 ?154)) =?= inverse (multiply (inverse (multiply ?155 ?153)) (multiply ?155 ?154)) [155, 154, 153, 152] by Super 18 with 7 at 3
% 32.05/8.33 Id : 75, {_}: inverse (multiply (inverse (multiply ?255 (inverse (multiply (inverse ?256) (multiply (inverse (multiply ?257 ?258)) (inverse (multiply (inverse (multiply ?259 ?258)) (multiply ?259 ?258)))))))) (multiply ?255 (multiply ?257 ?258))) =>= ?256 [259, 258, 257, 256, 255] by Super 2 with 33 at 2,2,1,2,1,1,1,2
% 32.05/8.33 Id : 79, {_}: inverse (multiply (inverse (multiply ?281 (inverse (multiply (inverse (multiply (inverse (multiply ?282 ?283)) (multiply ?282 ?284))) (multiply (inverse ?285) (inverse (multiply (inverse ?285) ?285))))))) (multiply ?281 ?285)) =?= multiply (inverse (multiply ?286 ?283)) (multiply ?286 ?284) [286, 285, 284, 283, 282, 281] by Super 2 with 33 at 1,1,2,1,1,1,2
% 32.05/8.33 Id : 184, {_}: multiply (inverse (multiply ?872 ?873)) (multiply ?872 ?874) =?= multiply (inverse (multiply ?875 ?873)) (multiply ?875 ?874) [875, 874, 873, 872] by Demod 79 with 2 at 2
% 32.05/8.33 Id : 191, {_}: multiply (inverse (multiply ?917 (multiply ?918 ?919))) (multiply ?917 ?920) =?= multiply ?921 (multiply (inverse (multiply ?918 (inverse (multiply (inverse ?921) (multiply (inverse ?919) (inverse (multiply (inverse ?919) ?919))))))) ?920) [921, 920, 919, 918, 917] by Super 184 with 2 at 1,3
% 32.05/8.33 Id : 3296, {_}: inverse (multiply (inverse (multiply ?24042 (inverse (multiply (inverse (multiply ?24043 (multiply ?24044 ?24045))) (multiply ?24043 (inverse (multiply (inverse (multiply ?24046 (inverse (multiply (inverse (inverse ?24047)) (multiply (inverse ?24045) (inverse (multiply (inverse ?24045) ?24045))))))) (multiply ?24046 (inverse (multiply (inverse (inverse ?24047)) (multiply (inverse ?24045) (inverse (multiply (inverse ?24045) ?24045))))))))))))) (multiply ?24042 (multiply ?24044 (inverse (multiply (inverse (inverse ?24047)) (multiply (inverse ?24045) (inverse (multiply (inverse ?24045) ?24045)))))))) =>= ?24047 [24047, 24046, 24045, 24044, 24043, 24042] by Super 75 with 191 at 1,2,1,1,1,2
% 32.05/8.33 Id : 327, {_}: inverse (multiply (inverse (multiply ?1499 (inverse (multiply (inverse (multiply ?1500 ?1501)) (multiply ?1500 (inverse (multiply (inverse ?1502) ?1502))))))) (multiply ?1499 ?1502)) =>= multiply (inverse ?1502) ?1501 [1502, 1501, 1500, 1499] by Super 2 with 33 at 2,1,1,1,2
% 32.05/8.33 Id : 142, {_}: multiply (inverse (multiply ?282 ?283)) (multiply ?282 ?284) =?= multiply (inverse (multiply ?286 ?283)) (multiply ?286 ?284) [286, 284, 283, 282] by Demod 79 with 2 at 2
% 32.05/8.33 Id : 337, {_}: inverse (multiply (inverse (multiply ?1569 (inverse (multiply (inverse (multiply ?1570 ?1571)) (multiply ?1570 (inverse (multiply (inverse (multiply ?1572 ?1573)) (multiply ?1572 ?1573)))))))) (multiply ?1569 (multiply ?1574 ?1573))) =>= multiply (inverse (multiply ?1574 ?1573)) ?1571 [1574, 1573, 1572, 1571, 1570, 1569] by Super 327 with 142 at 1,2,2,1,2,1,1,1,2
% 32.05/8.33 Id : 3666, {_}: multiply (inverse (multiply ?26832 (inverse (multiply (inverse (inverse ?26833)) (multiply (inverse ?26834) (inverse (multiply (inverse ?26834) ?26834))))))) (multiply ?26832 ?26834) =>= ?26833 [26834, 26833, 26832] by Demod 3296 with 337 at 2
% 32.05/8.33 Id : 3752, {_}: multiply (inverse (inverse (multiply (inverse (multiply ?27477 (inverse ?27478))) (multiply ?27477 ?27479)))) (multiply (inverse ?27479) (inverse (multiply (inverse ?27479) ?27479))) =>= ?27478 [27479, 27478, 27477] by Super 3666 with 7 at 1,1,2
% 32.05/8.33 Id : 3515, {_}: multiply (inverse (multiply ?24044 (inverse (multiply (inverse (inverse ?24047)) (multiply (inverse ?24045) (inverse (multiply (inverse ?24045) ?24045))))))) (multiply ?24044 ?24045) =>= ?24047 [24045, 24047, 24044] by Demod 3296 with 337 at 2
% 32.05/8.33 Id : 231, {_}: inverse (multiply (inverse (inverse (multiply (inverse (multiply ?1146 ?1147)) (multiply ?1146 ?1148)))) (multiply (inverse ?1148) (inverse (multiply (inverse ?1148) ?1148)))) =>= ?1147 [1148, 1147, 1146] by Super 2 with 7 at 1,1,1,2
% 32.05/8.33 Id : 237, {_}: inverse (multiply (inverse (inverse (multiply (inverse (multiply ?1182 ?1183)) (multiply ?1182 (multiply ?1184 ?1185))))) (multiply (inverse (multiply ?1184 ?1185)) (inverse (multiply (inverse (multiply ?1186 ?1185)) (multiply ?1186 ?1185))))) =>= ?1183 [1186, 1185, 1184, 1183, 1182] by Super 231 with 142 at 1,2,2,1,2
% 32.05/8.33 Id : 3663, {_}: multiply (inverse (multiply ?26816 (multiply ?26817 ?26818))) (multiply ?26816 (multiply ?26817 ?26818)) =?= multiply (inverse ?26819) ?26819 [26819, 26818, 26817, 26816] by Super 191 with 3515 at 2,3
% 32.05/8.33 Id : 4796, {_}: inverse (multiply (inverse (inverse (multiply (inverse ?34637) ?34637))) (multiply (inverse (multiply ?34638 ?34639)) (inverse (multiply (inverse (multiply ?34640 ?34639)) (multiply ?34640 ?34639))))) =>= multiply ?34638 ?34639 [34640, 34639, 34638, 34637] by Super 237 with 3663 at 1,1,1,1,2
% 32.05/8.33 Id : 5106, {_}: inverse (multiply (inverse (inverse (multiply (inverse ?36515) ?36515))) (multiply (inverse (multiply ?36516 (multiply ?36517 ?36518))) (inverse (multiply (inverse ?36519) ?36519)))) =>= multiply ?36516 (multiply ?36517 ?36518) [36519, 36518, 36517, 36516, 36515] by Super 4796 with 3663 at 1,2,2,1,2
% 32.05/8.33 Id : 5170, {_}: inverse (multiply (inverse (inverse (multiply (inverse ?37070) ?37070))) (multiply (inverse ?37071) (inverse (multiply (inverse ?37072) ?37072)))) =?= multiply (inverse (multiply ?37073 (inverse (multiply (inverse (inverse ?37071)) (multiply (inverse ?37074) (inverse (multiply (inverse ?37074) ?37074))))))) (multiply ?37073 ?37074) [37074, 37073, 37072, 37071, 37070] by Super 5106 with 3515 at 1,1,2,1,2
% 32.05/8.33 Id : 5324, {_}: inverse (multiply (inverse (inverse (multiply (inverse ?37070) ?37070))) (multiply (inverse ?37071) (inverse (multiply (inverse ?37072) ?37072)))) =>= ?37071 [37072, 37071, 37070] by Demod 5170 with 3515 at 3
% 32.05/8.33 Id : 5364, {_}: multiply (inverse (multiply ?37738 ?37739)) (multiply ?37738 ?37739) =?= multiply (inverse ?37740) ?37740 [37740, 37739, 37738] by Super 3515 with 5324 at 2,1,1,2
% 32.05/8.33 Id : 6473, {_}: multiply (inverse (inverse (multiply (inverse ?44321) ?44321))) (multiply (inverse (inverse ?44322)) (inverse (multiply (inverse (inverse ?44322)) (inverse ?44322)))) =>= ?44322 [44322, 44321] by Super 3752 with 5364 at 1,1,1,2
% 32.05/8.33 Id : 6741, {_}: multiply (inverse (inverse (multiply (inverse ?45616) ?45616))) (multiply (inverse (inverse ?45617)) (inverse (multiply (inverse (multiply ?45618 ?45619)) (multiply ?45618 ?45619)))) =>= ?45617 [45619, 45618, 45617, 45616] by Super 6473 with 5364 at 1,2,2,2
% 32.05/8.33 Id : 6801, {_}: multiply (inverse (inverse (multiply (inverse ?46057) ?46057))) (multiply (inverse (inverse ?46058)) (inverse (multiply (inverse ?46059) ?46059))) =>= ?46058 [46059, 46058, 46057] by Super 6741 with 5364 at 1,2,2,2
% 32.05/8.33 Id : 250, {_}: inverse (multiply (inverse (inverse (multiply (inverse (multiply (inverse (multiply ?1260 ?1261)) (multiply ?1260 ?1262))) (multiply (inverse (multiply ?1263 ?1261)) ?1264)))) (multiply (inverse ?1264) (inverse (multiply (inverse ?1264) ?1264)))) =>= multiply ?1263 ?1262 [1264, 1263, 1262, 1261, 1260] by Super 231 with 142 at 1,1,1,1,1,1,2
% 32.05/8.33 Id : 81, {_}: inverse (multiply (inverse (multiply ?295 (inverse (multiply (inverse (multiply ?296 ?297)) (multiply ?296 (inverse (multiply (inverse ?298) ?298))))))) (multiply ?295 ?298)) =>= multiply (inverse ?298) ?297 [298, 297, 296, 295] by Super 2 with 33 at 2,1,1,1,2
% 32.05/8.33 Id : 5398, {_}: inverse (multiply (inverse (multiply ?37965 (inverse (multiply (inverse ?37966) ?37966)))) (multiply ?37965 ?37967)) =?= multiply (inverse ?37967) (inverse (multiply (inverse ?37967) ?37967)) [37967, 37966, 37965] by Super 7 with 5324 at 2,3
% 32.05/8.33 Id : 7515, {_}: multiply (inverse (inverse (multiply (inverse ?50471) ?50471))) (inverse (multiply (inverse (multiply ?50472 (inverse (multiply (inverse ?50473) ?50473)))) (multiply ?50472 (inverse ?50474)))) =>= ?50474 [50474, 50473, 50472, 50471] by Super 6801 with 5398 at 2,2
% 32.05/8.33 Id : 8028, {_}: multiply (inverse (inverse (multiply (inverse ?53734) ?53734))) (multiply (inverse ?53735) ?53735) =?= multiply (inverse ?53736) ?53736 [53736, 53735, 53734] by Super 6801 with 7515 at 2,2
% 32.05/8.33 Id : 8259, {_}: multiply (inverse ?54789) ?54789 =?= multiply (inverse ?54790) ?54790 [54790, 54789] by Super 6801 with 8028 at 2
% 32.05/8.33 Id : 8773, {_}: multiply (inverse (multiply ?58099 ?58100)) (multiply ?58099 ?58101) =?= multiply (inverse (multiply (inverse ?58101) ?58100)) (multiply (inverse ?58102) ?58102) [58102, 58101, 58100, 58099] by Super 142 with 8259 at 2,3
% 32.05/8.33 Id : 12158, {_}: inverse (multiply (inverse (multiply ?78124 (inverse (multiply (inverse (multiply (inverse (multiply ?78125 ?78126)) (multiply ?78125 ?78127))) (multiply (inverse (multiply (inverse ?78127) ?78126)) (inverse (multiply (inverse ?78128) ?78128))))))) (multiply ?78124 ?78128)) =?= multiply (inverse ?78128) (multiply (inverse ?78129) ?78129) [78129, 78128, 78127, 78126, 78125, 78124] by Super 81 with 8773 at 1,1,1,2,1,1,1,2
% 32.05/8.33 Id : 343, {_}: inverse (multiply (inverse (multiply ?1608 (inverse (multiply (inverse (multiply (inverse (multiply ?1609 ?1610)) (multiply ?1609 ?1611))) (multiply (inverse (multiply ?1612 ?1610)) (inverse (multiply (inverse ?1613) ?1613))))))) (multiply ?1608 ?1613)) =>= multiply (inverse ?1613) (multiply ?1612 ?1611) [1613, 1612, 1611, 1610, 1609, 1608] by Super 327 with 142 at 1,1,1,2,1,1,1,2
% 32.05/8.33 Id : 12692, {_}: multiply (inverse ?78128) (multiply (inverse ?78127) ?78127) =?= multiply (inverse ?78128) (multiply (inverse ?78129) ?78129) [78129, 78127, 78128] by Demod 12158 with 343 at 2
% 32.05/8.33 Id : 12959, {_}: inverse (multiply (inverse (inverse (multiply (inverse (multiply (inverse (multiply (inverse ?83336) ?83337)) (multiply (inverse ?83336) (multiply (inverse ?83338) ?83338)))) (multiply (inverse (multiply ?83339 ?83337)) ?83340)))) (multiply (inverse ?83340) (inverse (multiply (inverse ?83340) ?83340)))) =?= multiply ?83339 (multiply (inverse ?83341) ?83341) [83341, 83340, 83339, 83338, 83337, 83336] by Super 250 with 12692 at 2,1,1,1,1,1,1,2
% 32.05/8.33 Id : 13282, {_}: multiply ?83339 (multiply (inverse ?83338) ?83338) =?= multiply ?83339 (multiply (inverse ?83341) ?83341) [83341, 83338, 83339] by Demod 12959 with 250 at 2
% 32.05/8.33 Id : 8911, {_}: multiply (inverse (inverse (multiply (inverse (multiply ?58933 (inverse ?58934))) (multiply ?58933 ?58935)))) (multiply (inverse ?58935) (inverse (multiply (inverse ?58936) ?58936))) =>= ?58934 [58936, 58935, 58934, 58933] by Super 3752 with 8259 at 1,2,2,2
% 32.05/8.33 Id : 18675, {_}: multiply (inverse (inverse (multiply (inverse (multiply ?119910 (inverse ?119911))) (multiply ?119910 (inverse (multiply (inverse ?119912) ?119912)))))) (multiply (inverse ?119913) ?119913) =>= ?119911 [119913, 119912, 119911, 119910] by Super 13282 with 8911 at 3
% 32.05/8.33 Id : 8503, {_}: inverse (multiply (inverse ?56487) ?56487) =?= inverse (multiply (inverse ?56488) ?56488) [56488, 56487] by Super 5324 with 8028 at 1,2
% 32.05/8.33 Id : 8587, {_}: multiply (inverse (inverse (multiply (inverse ?57029) ?57029))) (inverse (multiply (inverse ?57030) ?57030)) =?= multiply (inverse ?57031) ?57031 [57031, 57030, 57029] by Super 7515 with 8259 at 1,2,2
% 32.05/8.33 Id : 10007, {_}: inverse (multiply (inverse ?65045) ?65045) =?= inverse (multiply (inverse (inverse (multiply (inverse ?65046) ?65046))) (inverse (multiply (inverse ?65047) ?65047))) [65047, 65046, 65045] by Super 8503 with 8587 at 1,3
% 32.05/8.33 Id : 9332, {_}: inverse (multiply (inverse ?61162) ?61162) =?= inverse (multiply (inverse ?61163) ?61163) [61163, 61162] by Super 5324 with 8028 at 1,2
% 32.05/8.33 Id : 9348, {_}: inverse (multiply (inverse ?61263) ?61263) =?= inverse (multiply (inverse (multiply (inverse ?61264) ?61264)) (multiply (inverse ?61265) ?61265)) [61265, 61264, 61263] by Super 9332 with 8503 at 1,1,3
% 32.05/8.33 Id : 10152, {_}: inverse (multiply (inverse (multiply ?65993 ?65994)) (multiply ?65993 ?65995)) =?= multiply (inverse ?65995) (inverse (multiply (inverse ?65994) (multiply (inverse ?65996) ?65996))) [65996, 65995, 65994, 65993] by Super 7 with 8587 at 2,1,2,3
% 32.05/8.33 Id : 25822, {_}: inverse (multiply (inverse ?165610) ?165610) =?= multiply (inverse ?165611) (inverse (multiply (inverse ?165611) (multiply (inverse ?165612) ?165612))) [165612, 165611, 165610] by Super 9348 with 10152 at 3
% 32.05/8.33 Id : 25930, {_}: inverse (multiply (inverse ?166299) ?166299) =?= multiply (inverse (multiply (inverse ?166300) ?166300)) (inverse (multiply (inverse ?166301) ?166301)) [166301, 166300, 166299] by Super 25822 with 8259 at 1,2,3
% 32.05/8.33 Id : 27202, {_}: inverse (multiply (inverse ?173993) ?173993) =?= inverse (multiply (inverse (inverse (multiply (inverse ?173994) ?173994))) (multiply (inverse (multiply (inverse ?173995) ?173995)) (inverse (multiply (inverse ?173996) ?173996)))) [173996, 173995, 173994, 173993] by Super 10007 with 25930 at 2,1,3
% 32.05/8.33 Id : 27672, {_}: inverse (multiply (inverse ?173993) ?173993) =?= multiply (inverse ?173995) ?173995 [173995, 173993] by Demod 27202 with 5324 at 3
% 32.05/8.33 Id : 27743, {_}: multiply (inverse (inverse (multiply (inverse (inverse (multiply (inverse ?177053) ?177053))) (multiply (inverse (inverse ?177054)) (inverse (multiply (inverse ?177055) ?177055)))))) (multiply (inverse ?177056) ?177056) =>= ?177054 [177056, 177055, 177054, 177053] by Super 18675 with 27672 at 1,1,1,1,1,2
% 32.05/8.33 Id : 28487, {_}: multiply (inverse (inverse ?180979)) (multiply (inverse ?180980) ?180980) =>= ?180979 [180980, 180979] by Demod 27743 with 5324 at 1,1,2
% 32.05/8.33 Id : 28554, {_}: multiply (inverse (inverse ?181320)) (inverse (multiply (inverse ?181321) ?181321)) =>= ?181320 [181321, 181320] by Super 28487 with 27672 at 2,2
% 32.05/8.33 Id : 28650, {_}: multiply (inverse (inverse (multiply (inverse ?46057) ?46057))) ?46058 =>= ?46058 [46058, 46057] by Demod 6801 with 28554 at 2,2
% 32.05/8.33 Id : 8733, {_}: inverse (multiply (inverse (multiply ?57913 ?57914)) (multiply ?57913 ?57915)) =?= inverse (multiply (inverse (multiply (inverse ?57915) ?57914)) (multiply (inverse ?57916) ?57916)) [57916, 57915, 57914, 57913] by Super 33 with 8259 at 2,1,3
% 32.05/8.33 Id : 28792, {_}: inverse (multiply (inverse (multiply ?182288 (inverse (multiply (inverse ?182289) ?182289)))) (multiply ?182288 (inverse ?182290))) =?= inverse (multiply (inverse ?182290) (multiply (inverse ?182291) ?182291)) [182291, 182290, 182289, 182288] by Super 8733 with 28554 at 1,1,1,3
% 32.05/8.33 Id : 28654, {_}: inverse (multiply (inverse (multiply ?50472 (inverse (multiply (inverse ?50473) ?50473)))) (multiply ?50472 (inverse ?50474))) =>= ?50474 [50474, 50473, 50472] by Demod 7515 with 28650 at 2
% 32.05/8.33 Id : 28952, {_}: ?182290 =<= inverse (multiply (inverse ?182290) (multiply (inverse ?182291) ?182291)) [182291, 182290] by Demod 28792 with 28654 at 2
% 32.05/8.33 Id : 29267, {_}: multiply (inverse (multiply (inverse ?183126) ?183126)) ?183127 =>= ?183127 [183127, 183126] by Super 28650 with 28952 at 1,1,2
% 32.05/8.33 Id : 29210, {_}: inverse (multiply (inverse (multiply ?65993 ?65994)) (multiply ?65993 ?65995)) =>= multiply (inverse ?65995) ?65994 [65995, 65994, 65993] by Demod 10152 with 28952 at 2,3
% 32.05/8.33 Id : 8775, {_}: multiply (inverse (multiply ?58109 ?58110)) (multiply ?58109 ?58111) =?= multiply (inverse (multiply (inverse ?58112) ?58112)) (multiply (inverse ?58110) ?58111) [58112, 58111, 58110, 58109] by Super 142 with 8259 at 1,1,3
% 32.05/8.33 Id : 29543, {_}: multiply (inverse (multiply ?58109 ?58110)) (multiply ?58109 ?58111) =>= multiply (inverse ?58110) ?58111 [58111, 58110, 58109] by Demod 8775 with 29267 at 3
% 32.05/8.33 Id : 29549, {_}: inverse (multiply (inverse ?65994) ?65995) =>= multiply (inverse ?65995) ?65994 [65995, 65994] by Demod 29210 with 29543 at 1,2
% 32.05/8.33 Id : 29592, {_}: multiply (multiply (inverse ?183126) ?183126) ?183127 =>= ?183127 [183127, 183126] by Demod 29267 with 29549 at 1,2
% 32.05/8.33 Id : 29693, {_}: a2 === a2 [] by Demod 1 with 29592 at 2
% 32.05/8.33 Id : 1, {_}: multiply (multiply (inverse b2) b2) a2 =>= a2 [] by prove_these_axioms_2
% 32.05/8.33 % SZS output end CNFRefutation for theBenchmark.p
% 32.05/8.33 27562: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 7.989838 using nrkbo
%------------------------------------------------------------------------------