%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP443-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n008.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:19 EDT 2022
% Result : Unsatisfiable 27.94s 7.29s
% Output : CNFRefutation 27.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRP443-1 : TPTP v8.1.0. Released v2.6.0.
% 0.08/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n008.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 06:46:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 2197: Facts:
% 0.12/0.34 2197: Id : 2, {_}:
% 0.12/0.34 inverse
% 0.12/0.34 (multiply ?2
% 0.12/0.34 (multiply ?3
% 0.12/0.34 (multiply (multiply ?4 (inverse ?4))
% 0.12/0.34 (inverse (multiply ?5 (multiply ?2 ?3))))))
% 0.12/0.34 =>=
% 0.12/0.34 ?5
% 0.12/0.34 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
% 0.12/0.34 2197: Goal:
% 0.12/0.34 2197: Id : 1, {_}:
% 0.12/0.34 multiply (multiply (inverse b2) b2) a2 =>= a2
% 0.12/0.34 [] by prove_these_axioms_2
% 27.94/7.29 Statistics :
% 27.94/7.29 Max weight : 52
% 27.94/7.29 Found proof, 6.957079s
% 27.94/7.29 % SZS status Unsatisfiable for theBenchmark.p
% 27.94/7.29 % SZS output start CNFRefutation for theBenchmark.p
% 27.94/7.29 Id : 3, {_}: inverse (multiply ?7 (multiply ?8 (multiply (multiply ?9 (inverse ?9)) (inverse (multiply ?10 (multiply ?7 ?8)))))) =>= ?10 [10, 9, 8, 7] by single_axiom ?7 ?8 ?9 ?10
% 27.94/7.29 Id : 2, {_}: inverse (multiply ?2 (multiply ?3 (multiply (multiply ?4 (inverse ?4)) (inverse (multiply ?5 (multiply ?2 ?3)))))) =>= ?5 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
% 27.94/7.29 Id : 4, {_}: inverse (multiply ?12 (multiply (multiply (multiply ?13 (inverse ?13)) (inverse (multiply ?14 (multiply ?15 ?12)))) (multiply (multiply ?16 (inverse ?16)) ?14))) =>= ?15 [16, 15, 14, 13, 12] by Super 3 with 2 at 2,2,2,1,2
% 27.94/7.29 Id : 7, {_}: inverse (multiply (multiply (multiply ?28 (inverse ?28)) (inverse (multiply ?29 (multiply ?30 ?31)))) (multiply (multiply (multiply ?32 (inverse ?32)) ?29) (multiply (multiply ?33 (inverse ?33)) ?30))) =>= ?31 [33, 32, 31, 30, 29, 28] by Super 2 with 4 at 2,2,2,1,2
% 27.94/7.29 Id : 9, {_}: inverse (multiply ?44 (multiply (multiply (multiply ?45 (inverse ?45)) (inverse (multiply ?46 (multiply ?47 ?44)))) (multiply (multiply ?48 (inverse ?48)) ?46))) =>= ?47 [48, 47, 46, 45, 44] by Super 3 with 2 at 2,2,2,1,2
% 27.94/7.30 Id : 13, {_}: inverse (multiply (multiply (multiply ?76 (inverse ?76)) ?77) (multiply (multiply (multiply ?78 (inverse ?78)) ?79) (multiply (multiply ?80 (inverse ?80)) ?81))) =?= multiply (multiply ?82 (inverse ?82)) (inverse (multiply ?77 (multiply ?79 ?81))) [82, 81, 80, 79, 78, 77, 76] by Super 9 with 4 at 2,1,2,1,2
% 27.94/7.30 Id : 68, {_}: multiply (multiply ?630 (inverse ?630)) (inverse (multiply (inverse (multiply ?631 (multiply ?632 ?633))) (multiply ?631 ?632))) =>= ?633 [633, 632, 631, 630] by Super 7 with 13 at 2
% 27.94/7.30 Id : 5, {_}: inverse (multiply ?18 (multiply ?19 (multiply (multiply (multiply ?20 (multiply ?21 (multiply (multiply ?22 (inverse ?22)) (inverse (multiply ?23 (multiply ?20 ?21)))))) ?23) (inverse (multiply ?24 (multiply ?18 ?19)))))) =>= ?24 [24, 23, 22, 21, 20, 19, 18] by Super 3 with 2 at 2,1,2,2,1,2
% 27.94/7.30 Id : 128, {_}: multiply (multiply ?1235 (inverse ?1235)) (inverse (multiply (inverse (multiply ?1236 (multiply ?1237 ?1238))) (multiply ?1236 ?1237))) =>= ?1238 [1238, 1237, 1236, 1235] by Super 7 with 13 at 2
% 27.94/7.30 Id : 134, {_}: multiply (multiply ?1280 (inverse ?1280)) (inverse (multiply ?1281 (multiply ?1282 (multiply (multiply ?1283 (inverse ?1283)) (inverse (multiply ?1284 (multiply ?1281 ?1282))))))) =?= multiply (multiply ?1285 (inverse ?1285)) ?1284 [1285, 1284, 1283, 1282, 1281, 1280] by Super 128 with 4 at 1,1,2,2
% 27.94/7.30 Id : 152, {_}: multiply (multiply ?1280 (inverse ?1280)) ?1284 =?= multiply (multiply ?1285 (inverse ?1285)) ?1284 [1285, 1284, 1280] by Demod 134 with 2 at 2,2
% 27.94/7.30 Id : 218, {_}: inverse (multiply ?1829 (multiply ?1830 (multiply (multiply (multiply ?1831 (multiply ?1832 (multiply (multiply ?1833 (inverse ?1833)) (inverse (multiply ?1834 (multiply ?1831 ?1832)))))) ?1834) (inverse (multiply (multiply ?1835 (inverse ?1835)) (multiply ?1829 ?1830)))))) =?= multiply ?1836 (inverse ?1836) [1836, 1835, 1834, 1833, 1832, 1831, 1830, 1829] by Super 5 with 152 at 1,2,2,2,1,2
% 27.94/7.30 Id : 271, {_}: multiply ?1835 (inverse ?1835) =?= multiply ?1836 (inverse ?1836) [1836, 1835] by Demod 218 with 5 at 2
% 27.94/7.30 Id : 293, {_}: multiply (multiply ?2201 (inverse ?2201)) (inverse (multiply (inverse (multiply ?2202 (multiply (inverse ?2202) ?2203))) (multiply ?2204 (inverse ?2204)))) =>= ?2203 [2204, 2203, 2202, 2201] by Super 68 with 271 at 2,1,2,2
% 27.94/7.30 Id : 2509, {_}: inverse (multiply (inverse ?14705) (multiply ?14706 (multiply (multiply ?14707 (inverse ?14707)) (inverse (multiply ?14708 (multiply (inverse ?14708) ?14706)))))) =>= ?14705 [14708, 14707, 14706, 14705] by Super 4 with 293 at 1,2,1,2
% 27.94/7.30 Id : 491, {_}: multiply (multiply ?3328 (inverse ?3328)) (inverse (multiply (inverse (multiply ?3329 (multiply ?3330 (inverse ?3330)))) (multiply ?3329 ?3331))) =>= inverse ?3331 [3331, 3330, 3329, 3328] by Super 68 with 271 at 2,1,1,1,2,2
% 27.94/7.30 Id : 494, {_}: multiply (multiply ?3346 (inverse ?3346)) (inverse (multiply (inverse (multiply ?3347 (multiply ?3348 (inverse ?3348)))) (multiply ?3349 (inverse ?3349)))) =>= inverse (inverse ?3347) [3349, 3348, 3347, 3346] by Super 491 with 271 at 2,1,2,2
% 27.94/7.30 Id : 2583, {_}: inverse (multiply (inverse ?15197) (multiply (inverse (inverse (inverse (multiply ?15198 (multiply ?15199 (inverse ?15199)))))) (inverse (inverse ?15198)))) =>= ?15197 [15199, 15198, 15197] by Super 2509 with 494 at 2,2,1,2
% 27.94/7.30 Id : 2582, {_}: inverse (multiply (inverse ?15193) (multiply (inverse (inverse (inverse (multiply ?15194 (multiply (inverse ?15194) ?15195))))) ?15195)) =>= ?15193 [15195, 15194, 15193] by Super 2509 with 293 at 2,2,1,2
% 27.94/7.30 Id : 3279, {_}: inverse (multiply (inverse (inverse (inverse (multiply ?18725 (multiply (inverse ?18725) ?18726))))) (multiply ?18726 (multiply (multiply ?18727 (inverse ?18727)) ?18728))) =>= inverse ?18728 [18728, 18727, 18726, 18725] by Super 2 with 2582 at 2,2,2,1,2
% 27.94/7.30 Id : 12310, {_}: inverse (inverse (multiply ?70654 (multiply (inverse (inverse (inverse (multiply ?70655 (multiply (inverse ?70655) ?70656))))) ?70656))) =>= ?70654 [70656, 70655, 70654] by Super 2 with 3279 at 2
% 27.94/7.30 Id : 3288, {_}: multiply (multiply ?18790 (inverse ?18790)) (multiply (inverse (inverse (inverse (multiply ?18791 (multiply (inverse ?18791) ?18792))))) (multiply ?18792 ?18793)) =>= ?18793 [18793, 18792, 18791, 18790] by Super 68 with 2582 at 2,2
% 27.94/7.30 Id : 654, {_}: inverse (multiply ?4298 (multiply (inverse ?4298) ?4299)) =?= inverse (multiply ?4300 (multiply (inverse ?4300) ?4299)) [4300, 4299, 4298] by Super 2 with 293 at 2,2,1,2
% 27.94/7.30 Id : 2596, {_}: inverse (multiply (inverse (multiply ?15297 (multiply (inverse ?15297) ?15298))) (multiply ?15299 (multiply (multiply ?15300 (inverse ?15300)) (inverse (multiply ?15301 (multiply (inverse ?15301) ?15299)))))) =?= multiply ?15302 (multiply (inverse ?15302) ?15298) [15302, 15301, 15300, 15299, 15298, 15297] by Super 2509 with 654 at 1,1,2
% 27.94/7.30 Id : 652, {_}: inverse (multiply (inverse ?4286) (multiply ?4287 (multiply (multiply ?4288 (inverse ?4288)) (inverse (multiply ?4289 (multiply (inverse ?4289) ?4287)))))) =>= ?4286 [4289, 4288, 4287, 4286] by Super 4 with 293 at 1,2,1,2
% 27.94/7.30 Id : 2625, {_}: multiply ?15297 (multiply (inverse ?15297) ?15298) =?= multiply ?15302 (multiply (inverse ?15302) ?15298) [15302, 15298, 15297] by Demod 2596 with 652 at 2
% 27.94/7.30 Id : 295, {_}: multiply (multiply ?2211 (inverse ?2211)) (inverse (multiply (inverse (multiply ?2212 (multiply ?2213 (inverse ?2213)))) (multiply ?2212 ?2214))) =>= inverse ?2214 [2214, 2213, 2212, 2211] by Super 68 with 271 at 2,1,1,1,2,2
% 27.94/7.30 Id : 1158, {_}: multiply (multiply ?7388 (inverse ?7388)) (inverse (multiply (inverse (multiply ?7389 (multiply ?7390 (inverse ?7390)))) (multiply ?7391 (inverse ?7391)))) =>= inverse (inverse ?7389) [7391, 7390, 7389, 7388] by Super 491 with 271 at 2,1,2,2
% 27.94/7.30 Id : 1195, {_}: multiply (multiply ?7657 (inverse ?7657)) (inverse (multiply (inverse (multiply (multiply ?7658 (inverse ?7658)) (multiply ?7659 (inverse ?7659)))) (multiply ?7660 (inverse ?7660)))) =?= inverse (inverse (multiply ?7661 (inverse ?7661))) [7661, 7660, 7659, 7658, 7657] by Super 1158 with 152 at 1,1,1,2,2
% 27.94/7.30 Id : 1244, {_}: inverse (inverse (multiply ?7658 (inverse ?7658))) =?= inverse (inverse (multiply ?7661 (inverse ?7661))) [7661, 7658] by Demod 1195 with 494 at 2
% 27.94/7.30 Id : 1302, {_}: multiply ?8156 (inverse ?8156) =?= multiply (inverse (multiply ?8157 (inverse ?8157))) (inverse (inverse (multiply ?8158 (inverse ?8158)))) [8158, 8157, 8156] by Super 271 with 1244 at 2,3
% 27.94/7.30 Id : 1396, {_}: multiply (multiply ?8644 (inverse ?8644)) (inverse (multiply (inverse (multiply (inverse (multiply ?8645 (inverse ?8645))) (multiply ?8646 (inverse ?8646)))) (multiply ?8647 (inverse ?8647)))) =?= inverse (inverse (inverse (multiply ?8648 (inverse ?8648)))) [8648, 8647, 8646, 8645, 8644] by Super 295 with 1302 at 2,1,2,2
% 27.94/7.30 Id : 1587, {_}: inverse (inverse (inverse (multiply ?8645 (inverse ?8645)))) =?= inverse (inverse (inverse (multiply ?8648 (inverse ?8648)))) [8648, 8645] by Demod 1396 with 494 at 2
% 27.94/7.30 Id : 1642, {_}: multiply ?9991 (inverse ?9991) =?= multiply (inverse (inverse (multiply ?9992 (inverse ?9992)))) (inverse (inverse (inverse (multiply ?9993 (inverse ?9993))))) [9993, 9992, 9991] by Super 271 with 1587 at 2,3
% 27.94/7.30 Id : 3293, {_}: multiply (multiply ?18819 (inverse ?18819)) (multiply (inverse (inverse (inverse (multiply ?18820 (multiply (inverse ?18820) ?18821))))) (multiply ?18822 (inverse ?18822))) =>= inverse ?18821 [18822, 18821, 18820, 18819] by Super 295 with 2582 at 2,2
% 27.94/7.30 Id : 15070, {_}: inverse (inverse (inverse (multiply ?85980 (inverse ?85980)))) =?= multiply ?85981 (inverse ?85981) [85981, 85980] by Super 12310 with 3293 at 1,1,2
% 27.94/7.30 Id : 15497, {_}: multiply ?88240 (inverse ?88240) =?= multiply (inverse (inverse (multiply ?88241 (inverse ?88241)))) (multiply ?88242 (inverse ?88242)) [88242, 88241, 88240] by Super 1642 with 15070 at 2,3
% 27.94/7.30 Id : 20187, {_}: multiply ?111541 (multiply (inverse ?111541) (inverse (inverse (inverse (inverse (multiply ?111542 (inverse ?111542))))))) =?= multiply ?111543 (inverse ?111543) [111543, 111542, 111541] by Super 2625 with 15497 at 3
% 27.94/7.30 Id : 28859, {_}: multiply (multiply ?156243 (inverse ?156243)) (multiply (inverse (inverse (inverse (multiply ?156244 (multiply (inverse ?156244) ?156245))))) (multiply ?156246 (inverse ?156246))) =?= multiply (inverse ?156245) (inverse (inverse (inverse (inverse (multiply ?156247 (inverse ?156247)))))) [156247, 156246, 156245, 156244, 156243] by Super 3288 with 20187 at 2,2,2
% 27.94/7.30 Id : 29370, {_}: inverse ?158723 =<= multiply (inverse ?158723) (inverse (inverse (inverse (inverse (multiply ?158724 (inverse ?158724)))))) [158724, 158723] by Demod 28859 with 3293 at 2
% 27.94/7.30 Id : 29760, {_}: inverse ?159910 =<= multiply (inverse ?159910) (inverse (multiply ?159911 (inverse ?159911))) [159911, 159910] by Super 29370 with 15070 at 1,2,3
% 27.94/7.30 Id : 29876, {_}: inverse (multiply ?160415 (multiply ?160416 (multiply (multiply ?160417 (inverse ?160417)) (inverse (multiply ?160418 (multiply ?160415 ?160416)))))) =?= multiply ?160418 (inverse (multiply ?160419 (inverse ?160419))) [160419, 160418, 160417, 160416, 160415] by Super 29760 with 2 at 1,3
% 27.94/7.30 Id : 30004, {_}: ?160418 =<= multiply ?160418 (inverse (multiply ?160419 (inverse ?160419))) [160419, 160418] by Demod 29876 with 2 at 2
% 27.94/7.30 Id : 30223, {_}: inverse (inverse (multiply ?161420 (multiply (inverse (inverse (inverse (multiply ?161421 (inverse ?161421))))) (inverse (multiply ?161422 (inverse ?161422)))))) =>= ?161420 [161422, 161421, 161420] by Super 12310 with 30004 at 2,1,1,1,1,2,1,1,2
% 27.94/7.30 Id : 31131, {_}: inverse (inverse (multiply ?164477 (inverse (inverse (inverse (multiply ?164478 (inverse ?164478))))))) =>= ?164477 [164478, 164477] by Demod 30223 with 30004 at 2,1,1,2
% 27.94/7.30 Id : 31242, {_}: inverse (inverse (multiply ?164948 (multiply ?164949 (inverse ?164949)))) =>= ?164948 [164949, 164948] by Super 31131 with 15070 at 2,1,1,2
% 27.94/7.30 Id : 31352, {_}: inverse (multiply (inverse ?15197) (multiply (inverse ?15198) (inverse (inverse ?15198)))) =>= ?15197 [15198, 15197] by Demod 2583 with 31242 at 1,1,2,1,2
% 27.94/7.30 Id : 31521, {_}: inverse (multiply (inverse ?165944) (multiply (inverse (inverse (multiply ?165945 (multiply ?165946 (inverse ?165946))))) (inverse ?165945))) =>= ?165944 [165946, 165945, 165944] by Super 31352 with 31242 at 1,2,2,1,2
% 27.94/7.30 Id : 31648, {_}: inverse (multiply (inverse ?165944) (multiply ?165945 (inverse ?165945))) =>= ?165944 [165945, 165944] by Demod 31521 with 31242 at 1,2,1,2
% 27.94/7.30 Id : 31725, {_}: multiply (multiply ?2201 (inverse ?2201)) (multiply ?2202 (multiply (inverse ?2202) ?2203)) =>= ?2203 [2203, 2202, 2201] by Demod 293 with 31648 at 2,2
% 27.94/7.30 Id : 15633, {_}: multiply ?88922 (multiply (inverse ?88922) (inverse (inverse ?88923))) =?= multiply ?88923 (inverse (inverse (inverse (multiply ?88924 (inverse ?88924))))) [88924, 88923, 88922] by Super 2625 with 15070 at 2,3
% 27.94/7.30 Id : 31212, {_}: inverse (inverse (multiply ?164847 (inverse (inverse (inverse (inverse (inverse (inverse (multiply ?164848 (inverse ?164848)))))))))) =>= ?164847 [164848, 164847] by Super 31131 with 15070 at 1,1,1,2,1,1,2
% 27.94/7.30 Id : 31726, {_}: multiply (multiply ?3346 (inverse ?3346)) (multiply ?3347 (multiply ?3348 (inverse ?3348))) =>= inverse (inverse ?3347) [3348, 3347, 3346] by Demod 494 with 31648 at 2,2
% 27.94/7.30 Id : 34650, {_}: ?176910 =<= multiply ?176910 (inverse (multiply (inverse (multiply ?176911 (multiply ?176912 (inverse ?176912)))) ?176911)) [176912, 176911, 176910] by Super 30004 with 31242 at 2,1,2,3
% 27.94/7.30 Id : 34788, {_}: ?177608 =<= multiply ?177608 (multiply (multiply ?177609 (inverse ?177609)) (multiply ?177610 (inverse ?177610))) [177610, 177609, 177608] by Super 34650 with 31648 at 2,3
% 27.94/7.30 Id : 35016, {_}: multiply ?178128 (inverse ?178128) =?= inverse (inverse (multiply ?178129 (inverse ?178129))) [178129, 178128] by Super 31726 with 34788 at 2
% 27.94/7.30 Id : 35764, {_}: inverse (inverse (multiply ?180985 (inverse (inverse (inverse (inverse (multiply ?180986 (inverse ?180986)))))))) =>= ?180985 [180986, 180985] by Super 31212 with 35016 at 1,1,1,1,2,1,1,2
% 27.94/7.30 Id : 29506, {_}: inverse (multiply ?159293 (multiply ?159294 (multiply (multiply ?159295 (inverse ?159295)) (inverse (multiply ?159296 (multiply ?159293 ?159294)))))) =?= multiply ?159296 (inverse (inverse (inverse (inverse (multiply ?159297 (inverse ?159297)))))) [159297, 159296, 159295, 159294, 159293] by Super 29370 with 2 at 1,3
% 27.94/7.30 Id : 29648, {_}: ?159296 =<= multiply ?159296 (inverse (inverse (inverse (inverse (multiply ?159297 (inverse ?159297)))))) [159297, 159296] by Demod 29506 with 2 at 2
% 27.94/7.30 Id : 35994, {_}: inverse (inverse ?180985) =>= ?180985 [180985] by Demod 35764 with 29648 at 1,1,2
% 27.94/7.30 Id : 36240, {_}: multiply ?88922 (multiply (inverse ?88922) ?88923) =?= multiply ?88923 (inverse (inverse (inverse (multiply ?88924 (inverse ?88924))))) [88924, 88923, 88922] by Demod 15633 with 35994 at 2,2,2
% 27.94/7.30 Id : 36241, {_}: multiply ?88922 (multiply (inverse ?88922) ?88923) =?= multiply ?88923 (inverse (multiply ?88924 (inverse ?88924))) [88924, 88923, 88922] by Demod 36240 with 35994 at 2,3
% 27.94/7.30 Id : 36274, {_}: multiply ?88922 (multiply (inverse ?88922) ?88923) =>= ?88923 [88923, 88922] by Demod 36241 with 30004 at 3
% 27.94/7.30 Id : 36283, {_}: multiply (multiply ?2201 (inverse ?2201)) ?2203 =>= ?2203 [2203, 2201] by Demod 31725 with 36274 at 2,2
% 27.94/7.30 Id : 36367, {_}: multiply (multiply (inverse ?181961) ?181961) ?181962 =>= ?181962 [181962, 181961] by Super 36283 with 35994 at 2,1,2
% 27.94/7.30 Id : 36479, {_}: a2 === a2 [] by Demod 1 with 36367 at 2
% 27.94/7.30 Id : 1, {_}: multiply (multiply (inverse b2) b2) a2 =>= a2 [] by prove_these_axioms_2
% 27.94/7.30 % SZS output end CNFRefutation for theBenchmark.p
% 27.94/7.30 2200: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 6.960906 using nrkbo
%------------------------------------------------------------------------------