%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP441-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 : 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 : 600s
% DateTime : Sat Jul 16 10:30:18 EDT 2022
% Result : Unsatisfiable 9.93s 2.83s
% Output : CNFRefutation 9.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP441-1 : TPTP v8.1.0. Released v2.6.0.
% 0.12/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %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 : 600
% 0.12/0.33 % DateTime : Tue Jun 14 06:27:58 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 22818: Facts:
% 0.12/0.34 22818: 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 (inverse ?3) ?4)
% 0.12/0.34 (inverse (multiply ?5 (multiply ?2 ?4))))))
% 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 22818: Goal:
% 0.12/0.34 22818: Id : 1, {_}:
% 0.12/0.34 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.12/0.34 [] by prove_these_axioms_3
% 9.93/2.83 Statistics :
% 9.93/2.83 Max weight : 78
% 9.93/2.83 Found proof, 2.496517s
% 9.93/2.83 % SZS status Unsatisfiable for theBenchmark.p
% 9.93/2.83 % SZS output start CNFRefutation for theBenchmark.p
% 9.93/2.83 Id : 2, {_}: inverse (multiply ?2 (multiply ?3 (multiply (multiply (inverse ?3) ?4) (inverse (multiply ?5 (multiply ?2 ?4)))))) =>= ?5 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
% 9.93/2.83 Id : 3, {_}: inverse (multiply ?7 (multiply ?8 (multiply (multiply (inverse ?8) ?9) (inverse (multiply ?10 (multiply ?7 ?9)))))) =>= ?10 [10, 9, 8, 7] by single_axiom ?7 ?8 ?9 ?10
% 9.93/2.83 Id : 4, {_}: inverse (multiply ?12 (multiply ?13 (multiply (multiply (inverse ?13) (multiply (multiply (inverse ?12) ?14) (inverse (multiply ?15 (multiply ?16 ?14))))) ?15))) =>= ?16 [16, 15, 14, 13, 12] by Super 3 with 2 at 2,2,2,1,2
% 9.93/2.83 Id : 5, {_}: inverse (multiply ?18 (multiply (multiply ?19 (multiply ?20 (multiply (multiply (inverse ?20) ?21) (inverse (multiply ?22 (multiply ?19 ?21)))))) (multiply (multiply ?22 ?23) (inverse (multiply ?24 (multiply ?18 ?23)))))) =>= ?24 [24, 23, 22, 21, 20, 19, 18] by Super 3 with 2 at 1,1,2,2,1,2
% 9.93/2.83 Id : 19, {_}: inverse (multiply ?125 (multiply ?126 (multiply (multiply (inverse ?126) (multiply (multiply (inverse ?125) (multiply (multiply ?127 ?128) (inverse (multiply ?129 (multiply ?130 ?128))))) ?129)) ?130))) =?= multiply ?131 (multiply ?132 (multiply (multiply (inverse ?132) ?133) (inverse (multiply ?127 (multiply ?131 ?133))))) [133, 132, 131, 130, 129, 128, 127, 126, 125] by Super 4 with 5 at 2,2,1,2,2,1,2
% 9.93/2.83 Id : 1084, {_}: inverse (inverse (multiply ?15591 (multiply ?15592 (multiply (multiply (inverse ?15592) (multiply (multiply (inverse ?15591) (multiply (multiply ?15593 ?15594) (inverse (multiply ?15595 (multiply ?15596 ?15594))))) ?15595)) ?15596)))) =>= ?15593 [15596, 15595, 15594, 15593, 15592, 15591] by Super 2 with 19 at 1,2
% 9.93/2.83 Id : 7, {_}: inverse (multiply ?28 (multiply ?29 (multiply (multiply (inverse ?29) (multiply (multiply (inverse ?28) (multiply (multiply (inverse ?30) ?31) (inverse (multiply ?32 (multiply ?33 ?31))))) ?32)) ?33))) =>= ?30 [33, 32, 31, 30, 29, 28] by Super 2 with 4 at 2,2,2,1,2
% 9.93/2.83 Id : 1072, {_}: multiply ?15449 (multiply ?15450 (multiply (multiply (inverse ?15450) ?15451) (inverse (multiply (inverse ?15452) (multiply ?15449 ?15451))))) =>= ?15452 [15452, 15451, 15450, 15449] by Super 7 with 19 at 2
% 9.93/2.83 Id : 2161, {_}: inverse (multiply ?29689 (multiply ?29690 (multiply (multiply (inverse ?29690) (multiply ?29691 (multiply (multiply (inverse ?29691) ?29692) (inverse (multiply (inverse ?29693) (multiply ?29689 ?29692)))))) (inverse (multiply ?29694 ?29693))))) =>= ?29694 [29694, 29693, 29692, 29691, 29690, 29689] by Super 2 with 1072 at 2,1,2,2,2,1,2
% 9.93/2.83 Id : 2267, {_}: inverse (multiply (inverse ?31047) (multiply ?31047 (multiply ?31048 (inverse (multiply ?31049 ?31048))))) =>= ?31049 [31049, 31048, 31047] by Super 2161 with 1072 at 1,2,2,1,2
% 9.93/2.83 Id : 2282, {_}: multiply ?31133 (multiply ?31134 (multiply (multiply (inverse ?31134) (multiply ?31135 (inverse (multiply ?31136 ?31135)))) ?31136)) =>= ?31133 [31136, 31135, 31134, 31133] by Super 1072 with 2267 at 2,2,2,2
% 9.93/2.83 Id : 2669, {_}: multiply ?36554 (multiply ?36555 (multiply (multiply (inverse ?36555) (multiply ?36556 (multiply (multiply (inverse ?36556) (multiply ?36557 (inverse (multiply ?36558 ?36557)))) ?36558))) (inverse (multiply (inverse ?36559) ?36554)))) =>= ?36559 [36559, 36558, 36557, 36556, 36555, 36554] by Super 1072 with 2282 at 2,1,2,2,2,2
% 9.93/2.83 Id : 3228, {_}: multiply ?41323 (multiply ?41324 (multiply (inverse ?41324) (inverse (multiply (inverse ?41325) ?41323)))) =>= ?41325 [41325, 41324, 41323] by Demod 2669 with 2282 at 1,2,2,2
% 9.93/2.84 Id : 2728, {_}: inverse (multiply ?37185 (multiply ?37186 (multiply (multiply (inverse ?37186) (multiply ?37187 (multiply (multiply (inverse ?37187) (multiply ?37188 (inverse (multiply ?37189 ?37188)))) ?37189))) (inverse (multiply ?37190 ?37185))))) =>= ?37190 [37190, 37189, 37188, 37187, 37186, 37185] by Super 2 with 2282 at 2,1,2,2,2,1,2
% 9.93/2.84 Id : 2909, {_}: inverse (multiply ?37185 (multiply ?37186 (multiply (inverse ?37186) (inverse (multiply ?37190 ?37185))))) =>= ?37190 [37190, 37186, 37185] by Demod 2728 with 2282 at 1,2,2,1,2
% 9.93/2.84 Id : 5150, {_}: multiply (multiply ?62401 (multiply (inverse ?62401) (inverse (multiply ?62402 (inverse ?62403))))) (multiply ?62404 (multiply (inverse ?62404) ?62402)) =>= ?62403 [62404, 62403, 62402, 62401] by Super 3228 with 2909 at 2,2,2,2
% 9.93/2.84 Id : 2943, {_}: multiply ?36554 (multiply ?36555 (multiply (inverse ?36555) (inverse (multiply (inverse ?36559) ?36554)))) =>= ?36559 [36559, 36555, 36554] by Demod 2669 with 2282 at 1,2,2,2
% 9.93/2.84 Id : 5189, {_}: multiply (multiply ?62788 (multiply (inverse ?62788) (inverse (multiply (multiply (inverse (inverse ?62789)) (inverse (multiply (inverse ?62790) ?62789))) (inverse ?62791))))) ?62790 =>= ?62791 [62791, 62790, 62789, 62788] by Super 5150 with 2943 at 2,2
% 9.93/2.84 Id : 3272, {_}: multiply (multiply ?41747 (multiply ?41748 (inverse (multiply ?41749 ?41748)))) (multiply ?41750 (multiply (inverse ?41750) ?41749)) =>= ?41747 [41750, 41749, 41748, 41747] by Super 3228 with 2267 at 2,2,2,2
% 9.93/2.84 Id : 7023, {_}: multiply ?83453 (multiply ?83454 (multiply (multiply (inverse ?83454) (multiply (multiply ?83455 (multiply (inverse ?83455) (inverse (multiply ?83456 ?83457)))) ?83456)) ?83457)) =>= ?83453 [83457, 83456, 83455, 83454, 83453] by Super 2282 with 2909 at 2,2,1,2,2,2
% 9.93/2.84 Id : 7027, {_}: multiply ?83486 (multiply ?83487 (multiply (multiply (inverse ?83487) (multiply (multiply ?83488 (multiply (inverse ?83488) (inverse ?83489))) ?83489)) (multiply ?83490 (multiply (multiply (inverse ?83490) (multiply ?83491 (inverse (multiply ?83492 ?83491)))) ?83492)))) =>= ?83486 [83492, 83491, 83490, 83489, 83488, 83487, 83486] by Super 7023 with 2282 at 1,2,2,1,2,1,2,2,2
% 9.93/2.84 Id : 7230, {_}: multiply ?83486 (multiply ?83487 (multiply (inverse ?83487) (multiply (multiply ?83488 (multiply (inverse ?83488) (inverse ?83489))) ?83489))) =>= ?83486 [83489, 83488, 83487, 83486] by Demod 7027 with 2282 at 2,2,2
% 9.93/2.84 Id : 7423, {_}: multiply ?86660 (multiply ?86661 (inverse (multiply (multiply (multiply ?86662 (multiply (inverse ?86662) (inverse ?86663))) ?86663) ?86661))) =>= ?86660 [86663, 86662, 86661, 86660] by Super 3272 with 7230 at 2
% 9.93/2.84 Id : 8418, {_}: inverse (multiply (inverse ?94180) ?94180) =?= multiply (multiply ?94181 (multiply (inverse ?94181) (inverse ?94182))) ?94182 [94182, 94181, 94180] by Super 2909 with 7423 at 2,1,2
% 9.93/2.84 Id : 7669, {_}: inverse (multiply (inverse ?87967) ?87967) =?= multiply (multiply ?87968 (multiply (inverse ?87968) (inverse ?87969))) ?87969 [87969, 87968, 87967] by Super 2909 with 7423 at 2,1,2
% 9.93/2.84 Id : 8483, {_}: inverse (multiply (inverse ?94807) ?94807) =?= inverse (multiply (inverse ?94808) ?94808) [94808, 94807] by Super 8418 with 7669 at 3
% 9.93/2.84 Id : 9277, {_}: multiply (multiply ?101362 (multiply (inverse ?101362) (inverse (multiply (multiply (inverse (inverse ?101363)) (inverse (multiply (inverse ?101364) ?101363))) (inverse (multiply (inverse ?101365) ?101365)))))) ?101364 =?= multiply (inverse ?101366) ?101366 [101366, 101365, 101364, 101363, 101362] by Super 5189 with 8483 at 2,1,2,2,1,2
% 9.93/2.84 Id : 9384, {_}: multiply (inverse ?101365) ?101365 =?= multiply (inverse ?101366) ?101366 [101366, 101365] by Demod 9277 with 5189 at 2
% 9.93/2.84 Id : 12490, {_}: inverse (multiply ?128202 (multiply (inverse (multiply ?128203 ?128202)) (multiply (inverse ?128204) ?128204))) =>= ?128203 [128204, 128203, 128202] by Super 2909 with 9384 at 2,2,1,2
% 9.93/2.84 Id : 12594, {_}: inverse (multiply ?129026 (multiply (inverse ?129027) ?129027)) =>= inverse ?129026 [129027, 129026] by Super 12490 with 9384 at 2,1,2
% 9.93/2.84 Id : 12777, {_}: multiply (multiply ?130410 (multiply (inverse ?130410) (inverse (multiply (multiply (inverse (inverse ?130411)) (inverse (multiply (inverse ?130412) ?130411))) (inverse ?130413))))) ?130412 =?= multiply ?130413 (multiply (inverse ?130414) ?130414) [130414, 130413, 130412, 130411, 130410] by Super 5189 with 12594 at 2,1,2,2,1,2
% 9.93/2.84 Id : 12868, {_}: ?130413 =<= multiply ?130413 (multiply (inverse ?130414) ?130414) [130414, 130413] by Demod 12777 with 5189 at 2
% 9.93/2.84 Id : 12944, {_}: inverse (inverse (inverse (multiply ?131424 (inverse (multiply ?131425 ?131424))))) =>= ?131425 [131425, 131424] by Super 2267 with 12868 at 1,2
% 9.93/2.84 Id : 9468, {_}: inverse (multiply ?102413 (multiply (inverse (multiply ?102414 ?102413)) (multiply (inverse ?102415) ?102415))) =>= ?102414 [102415, 102414, 102413] by Super 2909 with 9384 at 2,2,1,2
% 9.93/2.84 Id : 12883, {_}: inverse (multiply ?102413 (inverse (multiply ?102414 ?102413))) =>= ?102414 [102414, 102413] by Demod 9468 with 12868 at 2,1,2
% 9.93/2.84 Id : 13282, {_}: inverse (inverse ?131425) =>= ?131425 [131425] by Demod 12944 with 12883 at 1,1,2
% 9.93/2.84 Id : 13314, {_}: multiply ?15591 (multiply ?15592 (multiply (multiply (inverse ?15592) (multiply (multiply (inverse ?15591) (multiply (multiply ?15593 ?15594) (inverse (multiply ?15595 (multiply ?15596 ?15594))))) ?15595)) ?15596)) =>= ?15593 [15596, 15595, 15594, 15593, 15592, 15591] by Demod 1084 with 13282 at 2
% 9.93/2.84 Id : 13320, {_}: inverse ?127 =<= multiply ?131 (multiply ?132 (multiply (multiply (inverse ?132) ?133) (inverse (multiply ?127 (multiply ?131 ?133))))) [133, 132, 131, 127] by Demod 19 with 13314 at 1,2
% 9.93/2.84 Id : 13437, {_}: inverse (inverse ?133916) =>= ?133916 [133916] by Demod 12944 with 12883 at 1,1,2
% 9.93/2.84 Id : 13941, {_}: inverse ?136341 =<= multiply ?136342 (inverse (multiply ?136341 ?136342)) [136342, 136341] by Super 13437 with 12883 at 1,2
% 9.93/2.84 Id : 13453, {_}: inverse ?134019 =<= multiply ?134020 (inverse (multiply ?134019 ?134020)) [134020, 134019] by Super 13437 with 12883 at 1,2
% 9.93/2.84 Id : 13961, {_}: inverse ?136426 =<= multiply (inverse (multiply ?136427 ?136426)) (inverse (inverse ?136427)) [136427, 136426] by Super 13941 with 13453 at 1,2,3
% 9.93/2.84 Id : 14071, {_}: inverse ?136426 =<= multiply (inverse (multiply ?136427 ?136426)) ?136427 [136427, 136426] by Demod 13961 with 13282 at 2,3
% 9.93/2.84 Id : 15412, {_}: inverse (inverse (multiply (multiply ?145230 ?145231) ?145232)) =<= multiply ?145230 (multiply ?145233 (multiply (multiply (inverse ?145233) ?145231) (inverse (inverse ?145232)))) [145233, 145232, 145231, 145230] by Super 13320 with 14071 at 1,2,2,2,3
% 9.93/2.84 Id : 15684, {_}: multiply (multiply ?145230 ?145231) ?145232 =<= multiply ?145230 (multiply ?145233 (multiply (multiply (inverse ?145233) ?145231) (inverse (inverse ?145232)))) [145233, 145232, 145231, 145230] by Demod 15412 with 13282 at 2
% 9.93/2.84 Id : 23927, {_}: multiply (multiply ?175117 ?175118) ?175119 =<= multiply ?175117 (multiply ?175120 (multiply (multiply (inverse ?175120) ?175118) ?175119)) [175120, 175119, 175118, 175117] by Demod 15684 with 13282 at 2,2,2,3
% 9.93/2.84 Id : 22, {_}: inverse (multiply ?159 (multiply (multiply ?160 (multiply ?161 (multiply (multiply (inverse ?161) ?162) (inverse (multiply ?163 (multiply ?160 ?162)))))) (multiply (multiply ?163 ?164) (inverse (multiply ?165 (multiply ?159 ?164)))))) =>= ?165 [165, 164, 163, 162, 161, 160, 159] by Super 3 with 2 at 1,1,2,2,1,2
% 9.93/2.84 Id : 24, {_}: inverse (multiply ?176 (multiply (multiply ?177 (multiply ?178 (multiply (multiply (inverse ?178) ?179) (inverse (multiply ?180 (multiply ?177 ?179)))))) (multiply (multiply ?180 (multiply (multiply (inverse ?176) (multiply (multiply (inverse ?181) ?182) (inverse (multiply ?183 (multiply ?184 ?182))))) ?183)) ?184))) =>= ?181 [184, 183, 182, 181, 180, 179, 178, 177, 176] by Super 22 with 4 at 2,2,2,1,2
% 9.93/2.84 Id : 2366, {_}: inverse (multiply (inverse ?31974) (multiply ?31974 (multiply ?31975 (inverse (multiply ?31976 ?31975))))) =>= ?31976 [31976, 31975, 31974] by Super 2161 with 1072 at 1,2,2,1,2
% 9.93/2.84 Id : 2389, {_}: inverse (multiply (inverse ?32188) (multiply ?32188 (multiply (multiply ?32189 (multiply ?32190 (inverse (multiply ?32191 ?32190)))) ?32191))) =>= inverse ?32189 [32191, 32190, 32189, 32188] by Super 2366 with 2267 at 2,2,2,1,2
% 9.93/2.84 Id : 3534, {_}: inverse (multiply ?44366 (multiply (multiply ?44367 (multiply ?44368 (multiply (multiply (inverse ?44368) ?44369) (inverse (multiply ?44370 (multiply ?44367 ?44369)))))) (multiply (multiply ?44370 (multiply (multiply (inverse ?44366) (multiply (multiply (inverse ?44371) ?44372) (inverse (multiply ?44373 (multiply ?44374 ?44372))))) ?44373)) ?44374))) =?= multiply (inverse ?44375) (multiply ?44375 (multiply (multiply ?44371 (multiply ?44376 (inverse (multiply ?44377 ?44376)))) ?44377)) [44377, 44376, 44375, 44374, 44373, 44372, 44371, 44370, 44369, 44368, 44367, 44366] by Super 24 with 2389 at 1,1,2,1,2,1,2,2,1,2
% 9.93/2.84 Id : 3634, {_}: ?44371 =<= multiply (inverse ?44375) (multiply ?44375 (multiply (multiply ?44371 (multiply ?44376 (inverse (multiply ?44377 ?44376)))) ?44377)) [44377, 44376, 44375, 44371] by Demod 3534 with 24 at 2
% 9.93/2.84 Id : 13795, {_}: ?44371 =<= multiply (inverse ?44375) (multiply ?44375 (multiply (multiply ?44371 (inverse ?44377)) ?44377)) [44377, 44375, 44371] by Demod 3634 with 13453 at 2,1,2,2,3
% 9.93/2.84 Id : 3391, {_}: multiply (multiply ?42970 (multiply ?42971 (inverse (multiply ?42972 ?42971)))) (multiply ?42973 (multiply (inverse ?42973) ?42972)) =>= ?42970 [42973, 42972, 42971, 42970] by Super 3228 with 2267 at 2,2,2,2
% 9.93/2.84 Id : 3424, {_}: multiply (multiply ?43304 (multiply ?43305 (inverse (multiply (multiply (inverse (inverse ?43306)) (inverse (multiply (inverse ?43307) ?43306))) ?43305)))) ?43307 =>= ?43304 [43307, 43306, 43305, 43304] by Super 3391 with 2943 at 2,2
% 9.93/2.84 Id : 13312, {_}: multiply (multiply ?43304 (multiply ?43305 (inverse (multiply (multiply ?43306 (inverse (multiply (inverse ?43307) ?43306))) ?43305)))) ?43307 =>= ?43304 [43307, 43306, 43305, 43304] by Demod 3424 with 13282 at 1,1,1,2,2,1,2
% 9.93/2.84 Id : 13803, {_}: multiply (multiply ?43304 (inverse (multiply ?43306 (inverse (multiply (inverse ?43307) ?43306))))) ?43307 =>= ?43304 [43307, 43306, 43304] by Demod 13312 with 13453 at 2,1,2
% 9.93/2.84 Id : 13804, {_}: multiply (multiply ?43304 (inverse (inverse (inverse ?43307)))) ?43307 =>= ?43304 [43307, 43304] by Demod 13803 with 13453 at 1,2,1,2
% 9.93/2.84 Id : 13805, {_}: multiply (multiply ?43304 (inverse ?43307)) ?43307 =>= ?43304 [43307, 43304] by Demod 13804 with 13282 at 2,1,2
% 9.93/2.84 Id : 13813, {_}: ?44371 =<= multiply (inverse ?44375) (multiply ?44375 ?44371) [44375, 44371] by Demod 13795 with 13805 at 2,2,3
% 9.93/2.84 Id : 14206, {_}: inverse (multiply ?137225 ?137226) =<= multiply (inverse ?137226) (inverse ?137225) [137226, 137225] by Super 13813 with 13453 at 2,3
% 9.93/2.84 Id : 15251, {_}: inverse (multiply (inverse ?144544) ?144545) =>= multiply (inverse ?144545) ?144544 [144545, 144544] by Super 14206 with 13282 at 2,3
% 9.93/2.84 Id : 15283, {_}: inverse (inverse ?144768) =<= multiply (inverse (multiply (inverse ?144769) ?144769)) ?144768 [144769, 144768] by Super 15251 with 12868 at 1,2
% 9.93/2.84 Id : 15343, {_}: ?144768 =<= multiply (inverse (multiply (inverse ?144769) ?144769)) ?144768 [144769, 144768] by Demod 15283 with 13282 at 2
% 9.93/2.84 Id : 14216, {_}: inverse (multiply (inverse ?137311) ?137312) =>= multiply (inverse ?137312) ?137311 [137312, 137311] by Super 14206 with 13282 at 2,3
% 9.93/2.84 Id : 15344, {_}: ?144768 =<= multiply (multiply (inverse ?144769) ?144769) ?144768 [144769, 144768] by Demod 15343 with 14216 at 1,3
% 9.93/2.84 Id : 23989, {_}: multiply (multiply ?175580 ?175581) ?175582 =>= multiply ?175580 (multiply ?175581 ?175582) [175582, 175581, 175580] by Super 23927 with 15344 at 2,2,3
% 9.93/2.84 Id : 24851, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 1 with 23989 at 2
% 9.93/2.84 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 9.93/2.84 % SZS output end CNFRefutation for theBenchmark.p
% 9.93/2.84 22819: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 2.500179 using kbo
%------------------------------------------------------------------------------