%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP668-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n026.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:31:30 EDT 2022
% Result : Unsatisfiable 175.67s 44.25s
% Output : CNFRefutation 175.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP668-1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.14 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.14/0.35 % Computer : n026.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Mon Jun 13 18:25:51 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.14/0.36 5657: Facts:
% 0.14/0.36 5657: Id : 2, {_}: mult ?2 (ld ?2 ?3) =>= ?3 [3, 2] by c01 ?2 ?3
% 0.14/0.36 5657: Id : 3, {_}: ld ?5 (mult ?5 ?6) =>= ?6 [6, 5] by c02 ?5 ?6
% 0.14/0.36 5657: Id : 4, {_}: mult (rd ?8 ?9) ?9 =>= ?8 [9, 8] by c03 ?8 ?9
% 0.14/0.36 5657: Id : 5, {_}: rd (mult ?11 ?12) ?12 =>= ?11 [12, 11] by c04 ?11 ?12
% 0.14/0.36 5657: Id : 6, {_}: mult ?14 unit =>= ?14 [14] by c05 ?14
% 0.14/0.36 5657: Id : 7, {_}: mult unit ?16 =>= ?16 [16] by c06 ?16
% 0.14/0.36 5657: Id : 8, {_}:
% 0.14/0.36 mult ?18 (mult ?19 (mult ?19 ?20))
% 0.14/0.36 =?=
% 0.14/0.36 mult (mult (mult ?18 ?19) ?19) ?20
% 0.14/0.36 [20, 19, 18] by c07 ?18 ?19 ?20
% 0.14/0.36 5657: Id : 9, {_}:
% 0.14/0.36 mult (mult ?22 ?23) ?22 =?= mult ?22 (mult ?23 ?22)
% 0.14/0.36 [23, 22] by c08 ?22 ?23
% 0.14/0.36 5657: Goal:
% 0.14/0.36 5657: Id : 1, {_}:
% 0.14/0.36 mult (mult a b) (mult (mult c b) c)
% 0.14/0.36 =<=
% 0.14/0.36 mult (mult a (mult (mult b c) b)) c
% 0.14/0.36 [] by goals
% 175.67/44.25 Statistics :
% 175.67/44.25 Max weight : 20
% 175.67/44.25 Found proof, 43.891486s
% 175.67/44.25 % SZS status Unsatisfiable for theBenchmark.p
% 175.67/44.25 % SZS output start CNFRefutation for theBenchmark.p
% 175.67/44.25 Id : 20, {_}: rd (mult ?52 ?53) ?53 =>= ?52 [53, 52] by c04 ?52 ?53
% 175.67/44.25 Id : 7, {_}: mult unit ?16 =>= ?16 [16] by c06 ?16
% 175.67/44.25 Id : 4, {_}: mult (rd ?8 ?9) ?9 =>= ?8 [9, 8] by c03 ?8 ?9
% 175.67/44.25 Id : 42, {_}: mult ?104 (mult ?105 (mult ?105 ?106)) =<= mult (mult (mult ?104 ?105) ?105) ?106 [106, 105, 104] by c07 ?104 ?105 ?106
% 175.67/44.25 Id : 3, {_}: ld ?5 (mult ?5 ?6) =>= ?6 [6, 5] by c02 ?5 ?6
% 175.67/44.25 Id : 2, {_}: mult ?2 (ld ?2 ?3) =>= ?3 [3, 2] by c01 ?2 ?3
% 175.67/44.25 Id : 6, {_}: mult ?14 unit =>= ?14 [14] by c05 ?14
% 175.67/44.25 Id : 8, {_}: mult ?18 (mult ?19 (mult ?19 ?20)) =<= mult (mult (mult ?18 ?19) ?19) ?20 [20, 19, 18] by c07 ?18 ?19 ?20
% 175.67/44.25 Id : 5, {_}: rd (mult ?11 ?12) ?12 =>= ?11 [12, 11] by c04 ?11 ?12
% 175.67/44.25 Id : 9, {_}: mult (mult ?22 ?23) ?22 =>= mult ?22 (mult ?23 ?22) [23, 22] by c08 ?22 ?23
% 175.67/44.25 Id : 41, {_}: rd (mult ?100 (mult ?101 (mult ?101 ?102))) ?102 =>= mult (mult ?100 ?101) ?101 [102, 101, 100] by Super 5 with 8 at 1,2
% 175.67/44.25 Id : 38, {_}: mult ?89 (mult ?90 (mult ?90 unit)) =>= mult (mult ?89 ?90) ?90 [90, 89] by Super 6 with 8 at 2
% 175.67/44.25 Id : 53, {_}: mult ?89 (mult ?90 ?90) =<= mult (mult ?89 ?90) ?90 [90, 89] by Demod 38 with 6 at 2,2,2
% 175.67/44.25 Id : 1094, {_}: rd (mult ?1574 (mult ?1575 (mult ?1575 ?1576))) ?1576 =>= mult ?1574 (mult ?1575 ?1575) [1576, 1575, 1574] by Demod 41 with 53 at 3
% 175.67/44.25 Id : 53511, {_}: rd (mult ?42709 (mult ?42710 ?42711)) (ld ?42710 ?42711) =>= mult ?42709 (mult ?42710 ?42710) [42711, 42710, 42709] by Super 1094 with 2 at 2,2,1,2
% 175.67/44.25 Id : 2399, {_}: mult (rd ?2829 ?2830) (mult ?2830 (mult ?2830 ?2831)) =>= mult (mult ?2829 ?2830) ?2831 [2831, 2830, 2829] by Super 42 with 4 at 1,1,3
% 175.67/44.25 Id : 3905, {_}: mult (rd ?4307 ?4308) (mult ?4308 ?4309) =<= mult (mult ?4307 ?4308) (ld ?4308 ?4309) [4309, 4308, 4307] by Super 2399 with 2 at 2,2,2
% 175.67/44.25 Id : 348, {_}: rd (mult ?520 (mult ?521 ?520)) ?520 =>= mult ?520 ?521 [521, 520] by Super 5 with 9 at 1,2
% 175.67/44.25 Id : 350, {_}: rd (mult ?526 ?527) ?526 =<= mult ?526 (rd ?527 ?526) [527, 526] by Super 348 with 4 at 2,1,2
% 175.67/44.25 Id : 1037, {_}: ld ?1488 (rd (mult ?1488 ?1489) ?1488) =>= rd ?1489 ?1488 [1489, 1488] by Super 3 with 350 at 2,2
% 175.67/44.25 Id : 1040, {_}: ld ?1497 (rd ?1497 ?1497) =>= rd unit ?1497 [1497] by Super 1037 with 6 at 1,2,2
% 175.67/44.25 Id : 30, {_}: rd ?75 ?75 =>= unit [75] by Super 5 with 7 at 1,2
% 175.67/44.25 Id : 1068, {_}: ld ?1497 unit =>= rd unit ?1497 [1497] by Demod 1040 with 30 at 2,2
% 175.67/44.25 Id : 3913, {_}: mult (rd ?4338 ?4339) (mult ?4339 unit) =<= mult (mult ?4338 ?4339) (rd unit ?4339) [4339, 4338] by Super 3905 with 1068 at 2,3
% 175.67/44.25 Id : 3961, {_}: mult (rd ?4338 ?4339) ?4339 =<= mult (mult ?4338 ?4339) (rd unit ?4339) [4339, 4338] by Demod 3913 with 6 at 2,2
% 175.67/44.25 Id : 3962, {_}: ?4338 =<= mult (mult ?4338 ?4339) (rd unit ?4339) [4339, 4338] by Demod 3961 with 4 at 2
% 175.67/44.25 Id : 4995, {_}: ld (mult ?5487 ?5488) ?5487 =>= rd unit ?5488 [5488, 5487] by Super 3 with 3962 at 2,2
% 175.67/44.25 Id : 5071, {_}: ld ?5635 ?5636 =<= rd unit (ld ?5636 ?5635) [5636, 5635] by Super 4995 with 2 at 1,2
% 175.67/44.25 Id : 1038, {_}: ld ?1491 (rd ?1492 ?1491) =>= rd (ld ?1491 ?1492) ?1491 [1492, 1491] by Super 1037 with 2 at 1,2,2
% 175.67/44.25 Id : 5078, {_}: ld (rd ?5655 ?5656) ?5656 =<= rd unit (rd (ld ?5656 ?5655) ?5656) [5656, 5655] by Super 5071 with 1038 at 2,3
% 175.67/44.25 Id : 4996, {_}: ld ?5490 ?5491 =<= rd unit (ld ?5491 ?5490) [5491, 5490] by Super 4995 with 2 at 1,2
% 175.67/44.25 Id : 2400, {_}: mult (rd ?2833 ?2834) (mult ?2834 ?2835) =<= mult (mult ?2833 ?2834) (ld ?2834 ?2835) [2835, 2834, 2833] by Super 2399 with 2 at 2,2,2
% 175.67/44.25 Id : 4319, {_}: ?4963 =<= mult (mult ?4963 ?4964) (rd unit ?4964) [4964, 4963] by Demod 3961 with 4 at 2
% 175.67/44.25 Id : 4331, {_}: rd ?4995 ?4996 =<= mult ?4995 (rd unit ?4996) [4996, 4995] by Super 4319 with 4 at 1,3
% 175.67/44.25 Id : 4706, {_}: mult (rd ?5379 (rd unit ?5380)) (mult (rd unit ?5380) ?5381) =>= mult (rd ?5379 ?5380) (ld (rd unit ?5380) ?5381) [5381, 5380, 5379] by Super 2400 with 4331 at 1,3
% 175.67/44.25 Id : 4306, {_}: rd ?4923 (rd unit ?4924) =>= mult ?4923 ?4924 [4924, 4923] by Super 5 with 3962 at 1,2
% 175.67/44.25 Id : 4742, {_}: mult (mult ?5379 ?5380) (mult (rd unit ?5380) ?5381) =>= mult (rd ?5379 ?5380) (ld (rd unit ?5380) ?5381) [5381, 5380, 5379] by Demod 4706 with 4306 at 1,2
% 175.67/44.25 Id : 5051, {_}: rd ?5573 (ld ?5574 ?5575) =<= mult ?5573 (ld ?5575 ?5574) [5575, 5574, 5573] by Super 4306 with 4996 at 2,2
% 175.67/44.25 Id : 23970, {_}: mult (mult ?20365 ?20366) (mult (rd unit ?20366) ?20367) =>= rd (rd ?20365 ?20366) (ld ?20367 (rd unit ?20366)) [20367, 20366, 20365] by Demod 4742 with 5051 at 3
% 175.67/44.25 Id : 24011, {_}: mult ?20527 (mult (rd unit ?20527) ?20528) =<= rd (rd unit ?20527) (ld ?20528 (rd unit ?20527)) [20528, 20527] by Super 23970 with 7 at 1,2
% 175.67/44.25 Id : 21, {_}: rd ?55 (ld ?56 ?55) =>= ?56 [56, 55] by Super 20 with 2 at 1,2
% 175.67/44.25 Id : 24708, {_}: mult ?20527 (mult (rd unit ?20527) ?20528) =>= ?20528 [20528, 20527] by Demod 24011 with 21 at 3
% 175.67/44.25 Id : 25234, {_}: ld ?21362 ?21363 =<= mult (rd unit ?21362) ?21363 [21363, 21362] by Super 3 with 24708 at 2,2
% 175.67/44.25 Id : 25237, {_}: ld (ld ?21371 unit) ?21372 =>= mult ?21371 ?21372 [21372, 21371] by Super 25234 with 21 at 1,3
% 175.67/44.25 Id : 25723, {_}: ld (rd unit ?21371) ?21372 =>= mult ?21371 ?21372 [21372, 21371] by Demod 25237 with 1068 at 1,2
% 175.67/44.25 Id : 26187, {_}: ld ?21735 (rd unit ?21736) =>= rd unit (mult ?21736 ?21735) [21736, 21735] by Super 4996 with 25723 at 2,3
% 175.67/44.25 Id : 24785, {_}: ld ?20822 ?20823 =<= mult (rd unit ?20822) ?20823 [20823, 20822] by Super 3 with 24708 at 2,2
% 175.67/44.25 Id : 25211, {_}: rd (rd unit ?21298) ?21299 =<= ld ?21298 (rd unit ?21299) [21299, 21298] by Super 4331 with 24785 at 3
% 175.67/44.25 Id : 26512, {_}: rd (rd unit ?22014) ?22015 =>= rd unit (mult ?22015 ?22014) [22015, 22014] by Demod 26187 with 25211 at 2
% 175.67/44.25 Id : 26515, {_}: rd ?22023 ?22024 =<= rd unit (mult ?22024 (ld ?22023 unit)) [22024, 22023] by Super 26512 with 21 at 1,2
% 175.67/44.25 Id : 26737, {_}: rd ?22023 ?22024 =<= rd unit (rd ?22024 (ld unit ?22023)) [22024, 22023] by Demod 26515 with 5051 at 2,3
% 175.67/44.25 Id : 31, {_}: ld unit ?77 =>= ?77 [77] by Super 3 with 7 at 2,2
% 175.67/44.25 Id : 26738, {_}: rd ?22023 ?22024 =<= rd unit (rd ?22024 ?22023) [22024, 22023] by Demod 26737 with 31 at 2,2,3
% 175.67/44.25 Id : 26820, {_}: ld (rd ?5655 ?5656) ?5656 =>= rd ?5656 (ld ?5656 ?5655) [5656, 5655] by Demod 5078 with 26738 at 3
% 175.67/44.25 Id : 53527, {_}: rd (mult ?42771 (mult (rd ?42772 ?42773) ?42773)) (rd ?42773 (ld ?42773 ?42772)) =>= mult ?42771 (mult (rd ?42772 ?42773) (rd ?42772 ?42773)) [42773, 42772, 42771] by Super 53511 with 26820 at 2,2
% 175.67/44.25 Id : 26835, {_}: ld (rd ?22100 ?22101) ?22102 =<= mult (rd ?22101 ?22100) ?22102 [22102, 22101, 22100] by Super 25723 with 26738 at 1,2
% 175.67/44.25 Id : 53722, {_}: rd (mult ?42771 (ld (rd ?42773 ?42772) ?42773)) (rd ?42773 (ld ?42773 ?42772)) =>= mult ?42771 (mult (rd ?42772 ?42773) (rd ?42772 ?42773)) [42772, 42773, 42771] by Demod 53527 with 26835 at 2,1,2
% 175.67/44.25 Id : 53723, {_}: rd (mult ?42771 (ld (rd ?42773 ?42772) ?42773)) (rd ?42773 (ld ?42773 ?42772)) =>= mult ?42771 (ld (rd ?42773 ?42772) (rd ?42772 ?42773)) [42772, 42773, 42771] by Demod 53722 with 26835 at 2,3
% 175.67/44.25 Id : 53724, {_}: rd (rd ?42771 (ld ?42773 (rd ?42773 ?42772))) (rd ?42773 (ld ?42773 ?42772)) =>= mult ?42771 (ld (rd ?42773 ?42772) (rd ?42772 ?42773)) [42772, 42773, 42771] by Demod 53723 with 5051 at 1,2
% 175.67/44.25 Id : 53725, {_}: rd (rd ?42771 (ld ?42773 (rd ?42773 ?42772))) (rd ?42773 (ld ?42773 ?42772)) =>= rd ?42771 (ld (rd ?42772 ?42773) (rd ?42773 ?42772)) [42772, 42773, 42771] by Demod 53724 with 5051 at 3
% 175.67/44.25 Id : 4679, {_}: ld ?5304 (rd ?5304 ?5305) =>= rd unit ?5305 [5305, 5304] by Super 3 with 4331 at 2,2
% 175.67/44.25 Id : 53726, {_}: rd (rd ?42771 (rd unit ?42772)) (rd ?42773 (ld ?42773 ?42772)) =>= rd ?42771 (ld (rd ?42772 ?42773) (rd ?42773 ?42772)) [42773, 42772, 42771] by Demod 53725 with 4679 at 2,1,2
% 175.67/44.25 Id : 26843, {_}: rd ?22127 (rd ?22128 ?22129) =<= mult ?22127 (rd ?22129 ?22128) [22129, 22128, 22127] by Super 4306 with 26738 at 2,2
% 175.67/44.25 Id : 28912, {_}: ld (rd ?24372 ?24373) (rd ?24374 ?24375) =>= rd (rd ?24373 ?24372) (rd ?24375 ?24374) [24375, 24374, 24373, 24372] by Super 26835 with 26843 at 3
% 175.67/44.25 Id : 53727, {_}: rd (rd ?42771 (rd unit ?42772)) (rd ?42773 (ld ?42773 ?42772)) =>= rd ?42771 (rd (rd ?42773 ?42772) (rd ?42772 ?42773)) [42773, 42772, 42771] by Demod 53726 with 28912 at 2,3
% 175.67/44.25 Id : 53728, {_}: rd (mult ?42771 ?42772) (rd ?42773 (ld ?42773 ?42772)) =>= rd ?42771 (rd (rd ?42773 ?42772) (rd ?42772 ?42773)) [42773, 42772, 42771] by Demod 53727 with 4306 at 1,2
% 175.67/44.25 Id : 505, {_}: rd (mult ?726 (mult ?727 ?727)) ?727 =>= mult ?726 ?727 [727, 726] by Super 5 with 53 at 1,2
% 175.67/44.25 Id : 510, {_}: rd ?740 ?741 =<= mult (rd ?740 (mult ?741 ?741)) ?741 [741, 740] by Super 505 with 4 at 1,2
% 175.67/44.25 Id : 1738, {_}: rd (rd ?2333 ?2334) ?2334 =>= rd ?2333 (mult ?2334 ?2334) [2334, 2333] by Super 5 with 510 at 1,2
% 175.67/44.25 Id : 26846, {_}: rd (rd ?22136 ?22137) (rd ?22137 ?22136) =<= rd unit (mult (rd ?22137 ?22136) (rd ?22137 ?22136)) [22137, 22136] by Super 1738 with 26738 at 1,2
% 175.67/44.25 Id : 46, {_}: mult unit (mult ?119 (mult ?119 ?120)) =>= mult (mult ?119 ?119) ?120 [120, 119] by Super 42 with 7 at 1,1,3
% 175.67/44.25 Id : 57, {_}: mult ?119 (mult ?119 ?120) =<= mult (mult ?119 ?119) ?120 [120, 119] by Demod 46 with 7 at 2
% 175.67/44.25 Id : 894, {_}: rd (mult ?1282 (mult ?1282 ?1283)) ?1283 =>= mult ?1282 ?1282 [1283, 1282] by Super 5 with 57 at 1,2
% 175.67/44.25 Id : 896, {_}: rd (mult (rd ?1288 ?1289) ?1288) ?1289 =<= mult (rd ?1288 ?1289) (rd ?1288 ?1289) [1289, 1288] by Super 894 with 4 at 2,1,2
% 175.67/44.25 Id : 2883, {_}: rd (mult ?3359 ?3360) (ld ?3359 ?3360) =>= mult ?3359 ?3359 [3360, 3359] by Super 894 with 2 at 2,1,2
% 175.67/44.25 Id : 2897, {_}: rd ?3395 (ld (rd ?3395 ?3396) ?3396) =<= mult (rd ?3395 ?3396) (rd ?3395 ?3396) [3396, 3395] by Super 2883 with 4 at 1,2
% 175.67/44.25 Id : 9794, {_}: rd ?3395 (ld (rd ?3395 ?3396) ?3396) =<= rd (mult (rd ?3395 ?3396) ?3395) ?3396 [3396, 3395] by Demod 2897 with 896 at 3
% 175.67/44.25 Id : 9795, {_}: rd ?1288 (ld (rd ?1288 ?1289) ?1289) =<= mult (rd ?1288 ?1289) (rd ?1288 ?1289) [1289, 1288] by Demod 896 with 9794 at 2
% 175.67/44.25 Id : 26824, {_}: rd ?1288 (rd ?1289 (ld ?1289 ?1288)) =<= mult (rd ?1288 ?1289) (rd ?1288 ?1289) [1289, 1288] by Demod 9795 with 26820 at 2,2
% 175.67/44.25 Id : 26917, {_}: rd (rd ?22136 ?22137) (rd ?22137 ?22136) =<= rd unit (rd ?22137 (rd ?22136 (ld ?22136 ?22137))) [22137, 22136] by Demod 26846 with 26824 at 2,3
% 175.67/44.25 Id : 26918, {_}: rd (rd ?22136 ?22137) (rd ?22137 ?22136) =<= rd (rd ?22136 (ld ?22136 ?22137)) ?22137 [22137, 22136] by Demod 26917 with 26738 at 3
% 175.67/44.25 Id : 4682, {_}: mult (rd ?5312 ?5313) ?5312 =<= mult ?5312 (mult (rd unit ?5313) ?5312) [5313, 5312] by Super 9 with 4331 at 1,2
% 175.67/44.25 Id : 25102, {_}: mult (rd ?5312 ?5313) ?5312 =>= mult ?5312 (ld ?5313 ?5312) [5313, 5312] by Demod 4682 with 24785 at 2,3
% 175.67/44.25 Id : 25124, {_}: mult (rd ?5312 ?5313) ?5312 =>= rd ?5312 (ld ?5312 ?5313) [5313, 5312] by Demod 25102 with 5051 at 3
% 175.67/44.25 Id : 25128, {_}: rd ?3395 (ld (rd ?3395 ?3396) ?3396) =<= rd (rd ?3395 (ld ?3395 ?3396)) ?3396 [3396, 3395] by Demod 9794 with 25124 at 1,3
% 175.67/44.25 Id : 26826, {_}: rd ?3395 (rd ?3396 (ld ?3396 ?3395)) =<= rd (rd ?3395 (ld ?3395 ?3396)) ?3396 [3396, 3395] by Demod 25128 with 26820 at 2,2
% 175.67/44.25 Id : 26919, {_}: rd (rd ?22136 ?22137) (rd ?22137 ?22136) =>= rd ?22136 (rd ?22137 (ld ?22137 ?22136)) [22137, 22136] by Demod 26918 with 26826 at 3
% 175.67/44.25 Id : 230036, {_}: rd (mult ?156106 ?156107) (rd ?156108 (ld ?156108 ?156107)) =>= rd ?156106 (rd ?156108 (rd ?156107 (ld ?156107 ?156108))) [156108, 156107, 156106] by Demod 53728 with 26919 at 2,3
% 175.67/44.25 Id : 230050, {_}: rd (mult ?156161 ?156162) (rd (rd unit ?156163) (mult ?156163 ?156162)) =<= rd ?156161 (rd (rd unit ?156163) (rd ?156162 (ld ?156162 (rd unit ?156163)))) [156163, 156162, 156161] by Super 230036 with 25723 at 2,2,2
% 175.67/44.25 Id : 26340, {_}: rd (rd unit ?21735) ?21736 =>= rd unit (mult ?21736 ?21735) [21736, 21735] by Demod 26187 with 25211 at 2
% 175.67/44.25 Id : 230512, {_}: rd (mult ?156161 ?156162) (rd unit (mult (mult ?156163 ?156162) ?156163)) =<= rd ?156161 (rd (rd unit ?156163) (rd ?156162 (ld ?156162 (rd unit ?156163)))) [156163, 156162, 156161] by Demod 230050 with 26340 at 2,2
% 175.67/44.25 Id : 230513, {_}: rd (mult ?156161 ?156162) (rd unit (mult (mult ?156163 ?156162) ?156163)) =<= rd ?156161 (rd unit (mult (rd ?156162 (ld ?156162 (rd unit ?156163))) ?156163)) [156163, 156162, 156161] by Demod 230512 with 26340 at 2,3
% 175.67/44.25 Id : 230514, {_}: mult (mult ?156161 ?156162) (mult (mult ?156163 ?156162) ?156163) =<= rd ?156161 (rd unit (mult (rd ?156162 (ld ?156162 (rd unit ?156163))) ?156163)) [156163, 156162, 156161] by Demod 230513 with 4306 at 2
% 175.67/44.25 Id : 230515, {_}: mult (mult ?156161 ?156162) (mult (mult ?156163 ?156162) ?156163) =<= mult ?156161 (mult (rd ?156162 (ld ?156162 (rd unit ?156163))) ?156163) [156163, 156162, 156161] by Demod 230514 with 4306 at 3
% 175.67/44.25 Id : 230516, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= mult ?156161 (mult (rd ?156162 (ld ?156162 (rd unit ?156163))) ?156163) [156163, 156162, 156161] by Demod 230515 with 9 at 2,2
% 175.67/44.25 Id : 230517, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= mult ?156161 (ld (rd (ld ?156162 (rd unit ?156163)) ?156162) ?156163) [156163, 156162, 156161] by Demod 230516 with 26835 at 2,3
% 175.67/44.28 Id : 230518, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= rd ?156161 (ld ?156163 (rd (ld ?156162 (rd unit ?156163)) ?156162)) [156163, 156162, 156161] by Demod 230517 with 5051 at 3
% 175.67/44.28 Id : 26463, {_}: rd unit (mult ?21299 ?21298) =<= ld ?21298 (rd unit ?21299) [21298, 21299] by Demod 25211 with 26340 at 2
% 175.67/44.28 Id : 230519, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= rd ?156161 (ld ?156163 (rd (rd unit (mult ?156163 ?156162)) ?156162)) [156163, 156162, 156161] by Demod 230518 with 26463 at 1,2,2,3
% 175.67/44.28 Id : 230520, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= rd ?156161 (ld ?156163 (rd unit (mult ?156162 (mult ?156163 ?156162)))) [156163, 156162, 156161] by Demod 230519 with 26340 at 2,2,3
% 175.67/44.28 Id : 230521, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =<= rd ?156161 (rd unit (mult (mult ?156162 (mult ?156163 ?156162)) ?156163)) [156163, 156162, 156161] by Demod 230520 with 26463 at 2,3
% 175.67/44.28 Id : 230522, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =>= mult ?156161 (mult (mult ?156162 (mult ?156163 ?156162)) ?156163) [156163, 156162, 156161] by Demod 230521 with 4306 at 3
% 175.67/44.28 Id : 4472, {_}: rd (mult (rd ?5094 (rd unit ?5095)) ?5094) (rd unit ?5095) =>= mult (rd ?5094 (rd unit ?5095)) (mult ?5094 ?5095) [5095, 5094] by Super 896 with 4306 at 2,3
% 175.67/44.28 Id : 4568, {_}: mult (mult (rd ?5094 (rd unit ?5095)) ?5094) ?5095 =>= mult (rd ?5094 (rd unit ?5095)) (mult ?5094 ?5095) [5095, 5094] by Demod 4472 with 4306 at 2
% 175.67/44.28 Id : 4569, {_}: mult (mult (rd ?5094 (rd unit ?5095)) ?5094) ?5095 =>= mult (mult ?5094 ?5095) (mult ?5094 ?5095) [5095, 5094] by Demod 4568 with 4306 at 1,3
% 175.67/44.28 Id : 4570, {_}: mult (mult (mult ?5094 ?5095) ?5094) ?5095 =>= mult (mult ?5094 ?5095) (mult ?5094 ?5095) [5095, 5094] by Demod 4569 with 4306 at 1,1,2
% 175.67/44.28 Id : 4571, {_}: mult (mult ?5094 (mult ?5095 ?5094)) ?5095 =>= mult (mult ?5094 ?5095) (mult ?5094 ?5095) [5095, 5094] by Demod 4570 with 9 at 1,2
% 175.67/44.28 Id : 895, {_}: rd (mult ?1285 ?1286) (ld ?1285 ?1286) =>= mult ?1285 ?1285 [1286, 1285] by Super 894 with 2 at 2,1,2
% 175.67/44.28 Id : 4316, {_}: rd ?4955 (ld (mult ?4955 ?4956) (rd unit ?4956)) =>= mult (mult ?4955 ?4956) (mult ?4955 ?4956) [4956, 4955] by Super 895 with 3962 at 1,2
% 175.67/44.28 Id : 25803, {_}: rd ?4955 (rd (rd unit (mult ?4955 ?4956)) ?4956) =>= mult (mult ?4955 ?4956) (mult ?4955 ?4956) [4956, 4955] by Demod 4316 with 25211 at 2,2
% 175.67/44.28 Id : 26462, {_}: rd ?4955 (rd unit (mult ?4956 (mult ?4955 ?4956))) =>= mult (mult ?4955 ?4956) (mult ?4955 ?4956) [4956, 4955] by Demod 25803 with 26340 at 2,2
% 175.67/44.28 Id : 26466, {_}: mult ?4955 (mult ?4956 (mult ?4955 ?4956)) =<= mult (mult ?4955 ?4956) (mult ?4955 ?4956) [4956, 4955] by Demod 26462 with 4306 at 2
% 175.67/44.28 Id : 26467, {_}: mult (mult ?5094 (mult ?5095 ?5094)) ?5095 =>= mult ?5094 (mult ?5095 (mult ?5094 ?5095)) [5095, 5094] by Demod 4571 with 26466 at 3
% 175.67/44.28 Id : 230523, {_}: mult (mult ?156161 ?156162) (mult ?156163 (mult ?156162 ?156163)) =>= mult ?156161 (mult ?156162 (mult ?156163 (mult ?156162 ?156163))) [156163, 156162, 156161] by Demod 230522 with 26467 at 2,3
% 175.67/44.28 Id : 4307, {_}: ld (mult ?4926 ?4927) ?4926 =>= rd unit ?4927 [4927, 4926] by Super 3 with 3962 at 2,2
% 175.67/44.28 Id : 53518, {_}: rd (mult ?42734 (mult (mult ?42735 ?42736) ?42735)) (rd unit ?42736) =>= mult ?42734 (mult (mult ?42735 ?42736) (mult ?42735 ?42736)) [42736, 42735, 42734] by Super 53511 with 4307 at 2,2
% 175.67/44.28 Id : 53684, {_}: mult (mult ?42734 (mult (mult ?42735 ?42736) ?42735)) ?42736 =>= mult ?42734 (mult (mult ?42735 ?42736) (mult ?42735 ?42736)) [42736, 42735, 42734] by Demod 53518 with 4306 at 2
% 175.67/44.28 Id : 53685, {_}: mult (mult ?42734 (mult (mult ?42735 ?42736) ?42735)) ?42736 =>= mult ?42734 (mult ?42735 (mult ?42736 (mult ?42735 ?42736))) [42736, 42735, 42734] by Demod 53684 with 26466 at 2,3
% 175.67/44.28 Id : 53686, {_}: mult (mult ?42734 (mult ?42735 (mult ?42736 ?42735))) ?42736 =>= mult ?42734 (mult ?42735 (mult ?42736 (mult ?42735 ?42736))) [42736, 42735, 42734] by Demod 53685 with 9 at 2,1,2
% 175.67/44.28 Id : 491953, {_}: mult a (mult b (mult c (mult b c))) =?= mult a (mult b (mult c (mult b c))) [] by Demod 491952 with 53686 at 3
% 175.67/44.28 Id : 491952, {_}: mult a (mult b (mult c (mult b c))) =<= mult (mult a (mult b (mult c b))) c [] by Demod 491951 with 230523 at 2
% 175.67/44.28 Id : 491951, {_}: mult (mult a b) (mult c (mult b c)) =<= mult (mult a (mult b (mult c b))) c [] by Demod 491950 with 9 at 2,1,3
% 175.67/44.28 Id : 491950, {_}: mult (mult a b) (mult c (mult b c)) =<= mult (mult a (mult (mult b c) b)) c [] by Demod 1 with 9 at 2,2
% 175.67/44.28 Id : 1, {_}: mult (mult a b) (mult (mult c b) c) =<= mult (mult a (mult (mult b c) b)) c [] by goals
% 175.67/44.28 % SZS output end CNFRefutation for theBenchmark.p
% 175.67/44.28 5658: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 43.927284 using kbo
%------------------------------------------------------------------------------