%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP683-11 : TPTP v8.1.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n019.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:35 EDT 2022
% Result : Unsatisfiable 2.65s 1.01s
% Output : CNFRefutation 2.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP683-11 : TPTP v8.1.0. Released v8.1.0.
% 0.03/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jun 14 00:31:09 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.35 16154: Facts:
% 0.13/0.35 16154: Id : 2, {_}: ld ?2 (mult ?2 ?2) =>= ?2 [2] by f01 ?2
% 0.13/0.35 16154: Id : 3, {_}: rd (mult ?4 ?4) ?4 =>= ?4 [4] by f02 ?4
% 0.13/0.35 16154: Id : 4, {_}: mult ?6 (ld ?6 ?7) =>= ld ?6 (mult ?6 ?7) [7, 6] by f03 ?6 ?7
% 0.13/0.35 16154: Id : 5, {_}:
% 0.13/0.35 mult (rd ?9 ?10) ?10 =>= rd (mult ?9 ?10) ?10
% 0.13/0.35 [10, 9] by f04 ?9 ?10
% 0.13/0.35 16154: Id : 6, {_}:
% 0.13/0.35 ld (ld ?12 ?13) (mult (ld ?12 ?13) (mult ?14 ?15))
% 0.13/0.35 =>=
% 0.13/0.35 mult (ld ?12 (mult ?12 ?14)) ?15
% 0.13/0.35 [15, 14, 13, 12] by f05 ?12 ?13 ?14 ?15
% 0.13/0.35 16154: Id : 7, {_}:
% 0.13/0.35 rd (mult (mult ?17 ?18) (rd ?19 ?20)) (rd ?19 ?20)
% 0.13/0.35 =>=
% 0.13/0.35 mult ?17 (rd (mult ?18 ?20) ?20)
% 0.13/0.35 [20, 19, 18, 17] by f06 ?17 ?18 ?19 ?20
% 0.13/0.35 16154: Id : 8, {_}:
% 0.13/0.35 ld ?22 (mult ?22 (ld ?23 ?23)) =<= rd (mult (rd ?22 ?22) ?23) ?23
% 0.13/0.35 [23, 22] by f07 ?22 ?23
% 0.13/0.35 16154: Goal:
% 0.13/0.35 16154: Id : 1, {_}: mult (rd (mult x3 x4) x4) x5 =>= mult x3 x5 [] by goal
% 2.65/1.01 Statistics :
% 2.65/1.01 Max weight : 52
% 2.65/1.01 Found proof, 0.665993s
% 2.65/1.01 % SZS status Unsatisfiable for theBenchmark.p
% 2.65/1.01 % SZS output start CNFRefutation for theBenchmark.p
% 2.65/1.01 Id : 7, {_}: rd (mult (mult ?17 ?18) (rd ?19 ?20)) (rd ?19 ?20) =>= mult ?17 (rd (mult ?18 ?20) ?20) [20, 19, 18, 17] by f06 ?17 ?18 ?19 ?20
% 2.65/1.01 Id : 5, {_}: mult (rd ?9 ?10) ?10 =>= rd (mult ?9 ?10) ?10 [10, 9] by f04 ?9 ?10
% 2.65/1.01 Id : 53, {_}: ld ?156 (mult ?156 (ld ?157 ?157)) =<= rd (mult (rd ?156 ?156) ?157) ?157 [157, 156] by f07 ?156 ?157
% 2.65/1.01 Id : 8, {_}: ld ?22 (mult ?22 (ld ?23 ?23)) =<= rd (mult (rd ?22 ?22) ?23) ?23 [23, 22] by f07 ?22 ?23
% 2.65/1.01 Id : 3, {_}: rd (mult ?4 ?4) ?4 =>= ?4 [4] by f02 ?4
% 2.65/1.01 Id : 35, {_}: rd (mult (mult ?100 ?101) (rd ?102 ?103)) (rd ?102 ?103) =>= mult ?100 (rd (mult ?101 ?103) ?103) [103, 102, 101, 100] by f06 ?100 ?101 ?102 ?103
% 2.65/1.01 Id : 4, {_}: mult ?6 (ld ?6 ?7) =>= ld ?6 (mult ?6 ?7) [7, 6] by f03 ?6 ?7
% 2.65/1.01 Id : 2, {_}: ld ?2 (mult ?2 ?2) =>= ?2 [2] by f01 ?2
% 2.65/1.01 Id : 20, {_}: ld (ld ?54 ?55) (mult (ld ?54 ?55) (mult ?56 ?57)) =>= mult (ld ?54 (mult ?54 ?56)) ?57 [57, 56, 55, 54] by f05 ?54 ?55 ?56 ?57
% 2.65/1.01 Id : 23, {_}: ld (ld ?69 (mult ?69 ?69)) (mult ?69 (mult ?70 ?71)) =>= mult (ld ?69 (mult ?69 ?70)) ?71 [71, 70, 69] by Super 20 with 2 at 1,2,2
% 2.65/1.01 Id : 113, {_}: ld ?276 (mult ?276 (mult ?277 ?278)) =<= mult (ld ?276 (mult ?276 ?277)) ?278 [278, 277, 276] by Demod 23 with 2 at 1,2
% 2.65/1.01 Id : 118, {_}: ld ?296 (mult ?296 (mult ?296 ?297)) =>= mult ?296 ?297 [297, 296] by Super 113 with 2 at 1,3
% 2.65/1.01 Id : 36, {_}: rd (mult (mult ?105 ?106) (rd (mult ?107 ?107) ?107)) ?107 =>= mult ?105 (rd (mult ?106 ?107) ?107) [107, 106, 105] by Super 35 with 3 at 2,2
% 2.65/1.01 Id : 229, {_}: rd (mult (mult ?513 ?514) ?515) ?515 =<= mult ?513 (rd (mult ?514 ?515) ?515) [515, 514, 513] by Demod 36 with 3 at 2,1,2
% 2.65/1.01 Id : 55, {_}: ld ?162 (mult ?162 (ld ?162 ?162)) =<= rd (rd (mult ?162 ?162) ?162) ?162 [162] by Super 53 with 5 at 1,3
% 2.65/1.01 Id : 60, {_}: ld ?162 (ld ?162 (mult ?162 ?162)) =<= rd (rd (mult ?162 ?162) ?162) ?162 [162] by Demod 55 with 4 at 2,2
% 2.65/1.01 Id : 61, {_}: ld ?162 (ld ?162 (mult ?162 ?162)) =>= rd ?162 ?162 [162] by Demod 60 with 3 at 1,3
% 2.65/1.01 Id : 62, {_}: ld ?162 ?162 =<= rd ?162 ?162 [162] by Demod 61 with 2 at 2,2
% 2.65/1.01 Id : 63, {_}: ld ?22 (mult ?22 (ld ?23 ?23)) =<= rd (mult (ld ?22 ?22) ?23) ?23 [23, 22] by Demod 8 with 62 at 1,1,3
% 2.65/1.01 Id : 238, {_}: rd (mult (mult ?550 (ld ?551 ?551)) ?552) ?552 =<= mult ?550 (ld ?551 (mult ?551 (ld ?552 ?552))) [552, 551, 550] by Super 229 with 63 at 2,3
% 2.65/1.01 Id : 933, {_}: rd (mult (mult ?1690 (ld ?1690 ?1690)) ?1691) ?1691 =>= ld ?1690 (mult ?1690 (mult ?1690 (ld ?1691 ?1691))) [1691, 1690] by Super 4 with 238 at 2
% 2.65/1.01 Id : 980, {_}: rd (mult (ld ?1690 (mult ?1690 ?1690)) ?1691) ?1691 =>= ld ?1690 (mult ?1690 (mult ?1690 (ld ?1691 ?1691))) [1691, 1690] by Demod 933 with 4 at 1,1,2
% 2.65/1.01 Id : 981, {_}: rd (mult (ld ?1690 (mult ?1690 ?1690)) ?1691) ?1691 =>= mult ?1690 (ld ?1691 ?1691) [1691, 1690] by Demod 980 with 118 at 3
% 2.65/1.01 Id : 30, {_}: ld ?69 (mult ?69 (mult ?70 ?71)) =<= mult (ld ?69 (mult ?69 ?70)) ?71 [71, 70, 69] by Demod 23 with 2 at 1,2
% 2.65/1.01 Id : 982, {_}: rd (ld ?1690 (mult ?1690 (mult ?1690 ?1691))) ?1691 =>= mult ?1690 (ld ?1691 ?1691) [1691, 1690] by Demod 981 with 30 at 1,2
% 2.65/1.01 Id : 983, {_}: rd (mult ?1690 ?1691) ?1691 =<= mult ?1690 (ld ?1691 ?1691) [1691, 1690] by Demod 982 with 118 at 1,2
% 2.65/1.01 Id : 1031, {_}: ld ?1826 (mult ?1826 (rd (mult ?1826 ?1827) ?1827)) =>= mult ?1826 (ld ?1827 ?1827) [1827, 1826] by Super 118 with 983 at 2,2,2
% 2.65/1.01 Id : 45, {_}: rd (mult (mult ?105 ?106) ?107) ?107 =<= mult ?105 (rd (mult ?106 ?107) ?107) [107, 106, 105] by Demod 36 with 3 at 2,1,2
% 2.65/1.01 Id : 1067, {_}: ld ?1826 (rd (mult (mult ?1826 ?1826) ?1827) ?1827) =>= mult ?1826 (ld ?1827 ?1827) [1827, 1826] by Demod 1031 with 45 at 2,2
% 2.65/1.01 Id : 2910, {_}: ld ?4376 (rd (mult (mult ?4376 ?4376) ?4377) ?4377) =>= rd (mult ?4376 ?4377) ?4377 [4377, 4376] by Demod 1067 with 983 at 3
% 2.65/1.01 Id : 214, {_}: rd (mult (mult ?17 ?18) (rd ?19 ?20)) (rd ?19 ?20) =>= rd (mult (mult ?17 ?18) ?20) ?20 [20, 19, 18, 17] by Demod 7 with 45 at 3
% 2.65/1.01 Id : 235, {_}: rd (mult (mult ?538 ?539) ?539) ?539 =>= mult ?538 ?539 [539, 538] by Super 229 with 3 at 2,3
% 2.65/1.01 Id : 333, {_}: mult ?671 (rd ?672 ?673) =<= rd (mult (mult ?671 (rd ?672 ?673)) ?673) ?673 [673, 672, 671] by Super 214 with 235 at 2
% 2.65/1.01 Id : 2927, {_}: ld (rd ?4434 ?4435) (mult (rd ?4434 ?4435) (rd ?4434 ?4435)) =>= rd (mult (rd ?4434 ?4435) ?4435) ?4435 [4435, 4434] by Super 2910 with 333 at 2,2
% 2.65/1.01 Id : 3005, {_}: rd ?4434 ?4435 =<= rd (mult (rd ?4434 ?4435) ?4435) ?4435 [4435, 4434] by Demod 2927 with 2 at 2
% 2.65/1.01 Id : 3028, {_}: rd ?4474 ?4475 =<= rd (rd (mult ?4474 ?4475) ?4475) ?4475 [4475, 4474] by Demod 3005 with 5 at 1,3
% 2.65/1.01 Id : 3035, {_}: rd ?4498 (ld ?4499 ?4499) =<= rd (rd (rd (mult ?4498 ?4499) ?4499) (ld ?4499 ?4499)) (ld ?4499 ?4499) [4499, 4498] by Super 3028 with 983 at 1,1,3
% 2.65/1.01 Id : 1032, {_}: rd (mult (rd (mult ?1829 ?1830) ?1830) (ld ?1830 ?1830)) (ld ?1830 ?1830) =>= mult ?1829 (ld ?1830 ?1830) [1830, 1829] by Super 235 with 983 at 1,1,2
% 2.65/1.01 Id : 1059, {_}: rd (rd (mult (rd (mult ?1829 ?1830) ?1830) ?1830) ?1830) (ld ?1830 ?1830) =>= mult ?1829 (ld ?1830 ?1830) [1830, 1829] by Demod 1032 with 983 at 1,2
% 2.65/1.01 Id : 1060, {_}: rd (rd (mult (rd (mult ?1829 ?1830) ?1830) ?1830) ?1830) (ld ?1830 ?1830) =>= rd (mult ?1829 ?1830) ?1830 [1830, 1829] by Demod 1059 with 983 at 3
% 2.65/1.01 Id : 1061, {_}: rd (rd (rd (mult (mult ?1829 ?1830) ?1830) ?1830) ?1830) (ld ?1830 ?1830) =>= rd (mult ?1829 ?1830) ?1830 [1830, 1829] by Demod 1060 with 5 at 1,1,2
% 2.65/1.01 Id : 1062, {_}: rd (rd (mult ?1829 ?1830) ?1830) (ld ?1830 ?1830) =>= rd (mult ?1829 ?1830) ?1830 [1830, 1829] by Demod 1061 with 235 at 1,1,2
% 2.65/1.01 Id : 3060, {_}: rd ?4498 (ld ?4499 ?4499) =<= rd (rd (mult ?4498 ?4499) ?4499) (ld ?4499 ?4499) [4499, 4498] by Demod 3035 with 1062 at 1,3
% 2.65/1.01 Id : 3061, {_}: rd ?4498 (ld ?4499 ?4499) =<= rd (mult ?4498 ?4499) ?4499 [4499, 4498] by Demod 3060 with 1062 at 3
% 2.65/1.01 Id : 3076, {_}: mult (rd ?9 ?10) ?10 =>= rd ?9 (ld ?10 ?10) [10, 9] by Demod 5 with 3061 at 3
% 2.65/1.01 Id : 3104, {_}: mult (rd ?4584 (ld ?4585 ?4585)) ?4585 =>= rd (mult ?4584 ?4585) (ld ?4585 ?4585) [4585, 4584] by Super 3076 with 3061 at 1,2
% 2.65/1.01 Id : 2719, {_}: rd (rd (mult ?4158 ?4159) ?4159) (ld ?4159 ?4159) =>= rd (mult ?4158 ?4159) ?4159 [4159, 4158] by Demod 1061 with 235 at 1,1,2
% 2.65/1.01 Id : 2733, {_}: rd (mult ?4207 ?4208) (ld ?4208 ?4208) =<= rd (mult (mult ?4207 ?4208) ?4208) ?4208 [4208, 4207] by Super 2719 with 235 at 1,2
% 2.65/1.01 Id : 2796, {_}: rd (mult ?4207 ?4208) (ld ?4208 ?4208) =>= mult ?4207 ?4208 [4208, 4207] by Demod 2733 with 235 at 3
% 2.65/1.01 Id : 3122, {_}: mult (rd ?4584 (ld ?4585 ?4585)) ?4585 =>= mult ?4584 ?4585 [4585, 4584] by Demod 3104 with 2796 at 3
% 2.65/1.01 Id : 3006, {_}: rd ?4434 ?4435 =<= rd (rd (mult ?4434 ?4435) ?4435) ?4435 [4435, 4434] by Demod 3005 with 5 at 1,3
% 2.65/1.01 Id : 3062, {_}: rd ?4434 ?4435 =<= rd (rd ?4434 (ld ?4435 ?4435)) ?4435 [4435, 4434] by Demod 3006 with 3061 at 1,3
% 2.65/1.01 Id : 50, {_}: mult (ld ?143 (mult ?143 (ld ?144 ?144))) ?144 =>= rd (mult (mult (rd ?143 ?143) ?144) ?144) ?144 [144, 143] by Super 5 with 8 at 1,2
% 2.65/1.01 Id : 450, {_}: ld ?143 (mult ?143 (mult (ld ?144 ?144) ?144)) =<= rd (mult (mult (rd ?143 ?143) ?144) ?144) ?144 [144, 143] by Demod 50 with 30 at 2
% 2.65/1.01 Id : 451, {_}: ld ?143 (mult ?143 (mult (ld ?144 ?144) ?144)) =>= mult (rd ?143 ?143) ?144 [144, 143] by Demod 450 with 235 at 3
% 2.65/1.01 Id : 64, {_}: mult (ld ?169 ?169) ?169 =>= rd (mult ?169 ?169) ?169 [169] by Super 5 with 62 at 1,2
% 2.65/1.01 Id : 71, {_}: mult (ld ?169 ?169) ?169 =>= ?169 [169] by Demod 64 with 3 at 3
% 2.65/1.01 Id : 452, {_}: ld ?143 (mult ?143 ?144) =<= mult (rd ?143 ?143) ?144 [144, 143] by Demod 451 with 71 at 2,2,2
% 2.65/1.01 Id : 453, {_}: ld ?143 (mult ?143 ?144) =<= mult (ld ?143 ?143) ?144 [144, 143] by Demod 452 with 62 at 1,3
% 2.65/1.01 Id : 470, {_}: ld (ld ?911 ?911) (ld ?911 (mult ?911 (mult (ld ?911 ?911) ?912))) =>= mult (ld ?911 ?911) ?912 [912, 911] by Super 118 with 453 at 2,2
% 2.65/1.01 Id : 484, {_}: ld (ld ?911 ?911) (ld ?911 (mult ?911 (ld ?911 (mult ?911 ?912)))) =>= mult (ld ?911 ?911) ?912 [912, 911] by Demod 470 with 453 at 2,2,2,2
% 2.65/1.01 Id : 485, {_}: ld (ld ?911 ?911) (ld ?911 (mult ?911 (ld ?911 (mult ?911 ?912)))) =>= ld ?911 (mult ?911 ?912) [912, 911] by Demod 484 with 453 at 3
% 2.65/1.01 Id : 486, {_}: ld (ld ?911 ?911) (ld ?911 (ld ?911 (mult ?911 (mult ?911 ?912)))) =>= ld ?911 (mult ?911 ?912) [912, 911] by Demod 485 with 4 at 2,2,2
% 2.65/1.01 Id : 1609, {_}: ld (ld ?2684 ?2684) (ld ?2684 (mult ?2684 ?2685)) =>= ld ?2684 (mult ?2684 ?2685) [2685, 2684] by Demod 486 with 118 at 2,2,2
% 2.65/1.01 Id : 467, {_}: ld (ld ?903 ?903) (ld ?903 (mult ?903 (ld ?903 ?903))) =>= ld ?903 ?903 [903] by Super 2 with 453 at 2,2
% 2.65/1.01 Id : 489, {_}: ld (ld ?903 ?903) (ld ?903 (ld ?903 (mult ?903 ?903))) =>= ld ?903 ?903 [903] by Demod 467 with 4 at 2,2,2
% 2.65/1.01 Id : 490, {_}: ld (ld ?903 ?903) (ld ?903 ?903) =>= ld ?903 ?903 [903] by Demod 489 with 2 at 2,2,2
% 2.65/1.01 Id : 1624, {_}: ld (ld ?2737 ?2737) (ld (ld ?2737 ?2737) (mult (ld ?2737 ?2737) ?2738)) =>= ld (ld ?2737 ?2737) (mult (ld ?2737 ?2737) ?2738) [2738, 2737] by Super 1609 with 490 at 1,2
% 2.65/1.01 Id : 21, {_}: ld (ld ?59 ?60) (mult (ld ?59 ?60) (ld ?61 (mult ?61 ?62))) =>= mult (ld ?59 (mult ?59 ?61)) (ld ?61 ?62) [62, 61, 60, 59] by Super 20 with 4 at 2,2,2
% 2.65/1.01 Id : 138, {_}: ld (ld ?59 ?60) (mult (ld ?59 ?60) (ld ?61 (mult ?61 ?62))) =>= ld ?59 (mult ?59 (mult ?61 (ld ?61 ?62))) [62, 61, 60, 59] by Demod 21 with 30 at 3
% 2.65/1.01 Id : 145, {_}: ld (ld ?344 ?345) (mult (ld ?344 ?345) (ld ?346 (mult ?346 ?347))) =>= ld ?344 (mult ?344 (ld ?346 (mult ?346 ?347))) [347, 346, 345, 344] by Demod 138 with 4 at 2,2,3
% 2.65/1.01 Id : 150, {_}: ld (ld ?369 ?370) (mult (ld ?369 ?370) ?371) =?= ld ?369 (mult ?369 (ld ?371 (mult ?371 ?371))) [371, 370, 369] by Super 145 with 2 at 2,2,2
% 2.65/1.01 Id : 185, {_}: ld (ld ?369 ?370) (mult (ld ?369 ?370) ?371) =>= ld ?369 (mult ?369 ?371) [371, 370, 369] by Demod 150 with 2 at 2,2,3
% 2.65/1.01 Id : 630, {_}: ld ?1130 (mult ?1130 (ld ?1130 ?1131)) =>= ld ?1130 ?1131 [1131, 1130] by Super 2 with 185 at 2
% 2.65/1.01 Id : 660, {_}: ld ?1130 (ld ?1130 (mult ?1130 ?1131)) =>= ld ?1130 ?1131 [1131, 1130] by Demod 630 with 4 at 2,2
% 2.65/1.01 Id : 1679, {_}: ld (ld ?2737 ?2737) ?2738 =<= ld (ld ?2737 ?2737) (mult (ld ?2737 ?2737) ?2738) [2738, 2737] by Demod 1624 with 660 at 2
% 2.65/1.01 Id : 1680, {_}: ld (ld ?2737 ?2737) ?2738 =>= ld ?2737 (mult ?2737 ?2738) [2738, 2737] by Demod 1679 with 185 at 3
% 2.65/1.01 Id : 1038, {_}: ld ?1853 (ld ?1853 (rd (mult ?1853 ?1854) ?1854)) =>= ld ?1853 (ld ?1854 ?1854) [1854, 1853] by Super 660 with 983 at 2,2,2
% 2.65/1.01 Id : 3086, {_}: ld ?1853 (ld ?1853 (rd ?1853 (ld ?1854 ?1854))) =>= ld ?1853 (ld ?1854 ?1854) [1854, 1853] by Demod 1038 with 3061 at 2,2,2
% 2.65/1.01 Id : 40, {_}: rd (mult (ld ?127 (mult ?127 ?128)) (rd ?129 ?130)) (rd ?129 ?130) =>= mult ?127 (rd (mult (ld ?127 ?128) ?130) ?130) [130, 129, 128, 127] by Super 35 with 4 at 1,1,2
% 2.65/1.01 Id : 1347, {_}: rd (ld ?127 (mult ?127 (mult ?128 (rd ?129 ?130)))) (rd ?129 ?130) =>= mult ?127 (rd (mult (ld ?127 ?128) ?130) ?130) [130, 129, 128, 127] by Demod 40 with 30 at 1,2
% 2.65/1.01 Id : 1348, {_}: rd (ld ?127 (mult ?127 (mult ?128 (rd ?129 ?130)))) (rd ?129 ?130) =>= rd (mult (mult ?127 (ld ?127 ?128)) ?130) ?130 [130, 129, 128, 127] by Demod 1347 with 45 at 3
% 2.65/1.01 Id : 1349, {_}: rd (ld ?127 (mult ?127 (mult ?128 (rd ?129 ?130)))) (rd ?129 ?130) =>= rd (mult (ld ?127 (mult ?127 ?128)) ?130) ?130 [130, 129, 128, 127] by Demod 1348 with 4 at 1,1,3
% 2.65/1.01 Id : 1355, {_}: rd (ld ?2309 (mult ?2309 (mult ?2310 (rd ?2311 ?2312)))) (rd ?2311 ?2312) =>= rd (ld ?2309 (mult ?2309 (mult ?2310 ?2312))) ?2312 [2312, 2311, 2310, 2309] by Demod 1349 with 30 at 1,3
% 2.65/1.01 Id : 1381, {_}: rd (mult ?2448 (rd ?2449 ?2450)) (rd ?2449 ?2450) =?= rd (ld ?2448 (mult ?2448 (mult ?2448 ?2450))) ?2450 [2450, 2449, 2448] by Super 1355 with 118 at 1,2
% 2.65/1.01 Id : 1445, {_}: rd (mult ?2448 (rd ?2449 ?2450)) (rd ?2449 ?2450) =>= rd (mult ?2448 ?2450) ?2450 [2450, 2449, 2448] by Demod 1381 with 118 at 1,3
% 2.65/1.01 Id : 3938, {_}: rd ?2448 (ld (rd ?2449 ?2450) (rd ?2449 ?2450)) =>= rd (mult ?2448 ?2450) ?2450 [2450, 2449, 2448] by Demod 1445 with 3061 at 2
% 2.65/1.01 Id : 3939, {_}: rd ?2448 (ld (rd ?2449 ?2450) (rd ?2449 ?2450)) =>= rd ?2448 (ld ?2450 ?2450) [2450, 2449, 2448] by Demod 3938 with 3061 at 3
% 2.65/1.01 Id : 3951, {_}: ld ?5526 (ld ?5526 (rd ?5526 (ld ?5527 ?5527))) =?= ld ?5526 (ld (rd ?5528 ?5527) (rd ?5528 ?5527)) [5528, 5527, 5526] by Super 3086 with 3939 at 2,2,2
% 2.65/1.01 Id : 6748, {_}: ld ?8993 (ld ?8994 ?8994) =<= ld ?8993 (ld (rd ?8995 ?8994) (rd ?8995 ?8994)) [8995, 8994, 8993] by Demod 3951 with 3086 at 2
% 2.65/1.02 Id : 6750, {_}: ld ?9000 (ld (ld ?9001 ?9001) (ld ?9001 ?9001)) =<= ld ?9000 (ld (rd (mult ?9002 ?9001) (ld ?9001 ?9001)) (mult ?9002 ?9001)) [9002, 9001, 9000] by Super 6748 with 2796 at 2,2,3
% 2.65/1.02 Id : 7025, {_}: ld ?9000 (ld ?9001 (mult ?9001 (ld ?9001 ?9001))) =<= ld ?9000 (ld (rd (mult ?9002 ?9001) (ld ?9001 ?9001)) (mult ?9002 ?9001)) [9002, 9001, 9000] by Demod 6750 with 1680 at 2,2
% 2.65/1.02 Id : 7026, {_}: ld ?9000 (ld ?9001 (mult ?9001 (ld ?9001 ?9001))) =?= ld ?9000 (ld (mult ?9002 ?9001) (mult ?9002 ?9001)) [9002, 9001, 9000] by Demod 7025 with 2796 at 1,2,3
% 2.65/1.02 Id : 1025, {_}: ld ?1809 (mult ?1809 (mult (ld ?1810 ?1810) ?1811)) =<= mult (ld ?1809 (rd (mult ?1809 ?1810) ?1810)) ?1811 [1811, 1810, 1809] by Super 30 with 983 at 2,1,3
% 2.65/1.02 Id : 1081, {_}: ld ?1809 (mult ?1809 (ld ?1810 (mult ?1810 ?1811))) =<= mult (ld ?1809 (rd (mult ?1809 ?1810) ?1810)) ?1811 [1811, 1810, 1809] by Demod 1025 with 453 at 2,2,2
% 2.65/1.02 Id : 3761, {_}: ld ?5383 (mult ?5383 (ld ?5384 (mult ?5384 ?5385))) =<= mult (ld ?5383 (rd ?5383 (ld ?5384 ?5384))) ?5385 [5385, 5384, 5383] by Demod 1081 with 3061 at 2,1,3
% 2.65/1.02 Id : 3765, {_}: ld (mult ?5399 ?5400) (mult (mult ?5399 ?5400) (ld ?5400 (mult ?5400 ?5401))) =>= mult (ld (mult ?5399 ?5400) (mult ?5399 ?5400)) ?5401 [5401, 5400, 5399] by Super 3761 with 2796 at 2,1,3
% 2.65/1.02 Id : 634, {_}: ld (ld ?1147 ?1148) (mult (ld ?1147 ?1148) ?1149) =>= ld ?1147 (mult ?1147 ?1149) [1149, 1148, 1147] by Demod 150 with 2 at 2,2,3
% 2.65/1.02 Id : 636, {_}: ld (ld ?1154 (mult ?1154 (mult ?1154 ?1155))) (mult (mult ?1154 ?1155) ?1156) =>= ld ?1154 (mult ?1154 ?1156) [1156, 1155, 1154] by Super 634 with 118 at 1,2,2
% 2.65/1.02 Id : 671, {_}: ld (mult ?1154 ?1155) (mult (mult ?1154 ?1155) ?1156) =>= ld ?1154 (mult ?1154 ?1156) [1156, 1155, 1154] by Demod 636 with 118 at 1,2
% 2.65/1.02 Id : 3855, {_}: ld ?5399 (mult ?5399 (ld ?5400 (mult ?5400 ?5401))) =<= mult (ld (mult ?5399 ?5400) (mult ?5399 ?5400)) ?5401 [5401, 5400, 5399] by Demod 3765 with 671 at 2
% 2.65/1.02 Id : 3856, {_}: ld ?5399 (mult ?5399 (ld ?5400 (mult ?5400 ?5401))) =<= ld (mult ?5399 ?5400) (mult (mult ?5399 ?5400) ?5401) [5401, 5400, 5399] by Demod 3855 with 453 at 3
% 2.65/1.02 Id : 3857, {_}: ld ?5399 (mult ?5399 (ld ?5400 (mult ?5400 ?5401))) =>= ld ?5399 (mult ?5399 ?5401) [5401, 5400, 5399] by Demod 3856 with 671 at 3
% 2.65/1.02 Id : 5735, {_}: ld ?7405 (ld ?7405 (mult ?7405 ?7406)) =?= ld ?7405 (ld ?7407 (mult ?7407 ?7406)) [7407, 7406, 7405] by Super 660 with 3857 at 2,2
% 2.65/1.02 Id : 5813, {_}: ld ?7405 ?7406 =<= ld ?7405 (ld ?7407 (mult ?7407 ?7406)) [7407, 7406, 7405] by Demod 5735 with 660 at 2
% 2.65/1.02 Id : 7027, {_}: ld ?9000 (ld ?9001 ?9001) =<= ld ?9000 (ld (mult ?9002 ?9001) (mult ?9002 ?9001)) [9002, 9001, 9000] by Demod 7026 with 5813 at 2
% 2.65/1.02 Id : 9541, {_}: ld (ld (ld (mult ?12183 ?12184) (mult ?12183 ?12184)) (ld ?12184 ?12184)) ?12185 =<= ld (ld (mult ?12183 ?12184) (mult ?12183 ?12184)) (mult (ld (mult ?12183 ?12184) (mult ?12183 ?12184)) ?12185) [12185, 12184, 12183] by Super 1680 with 7027 at 1,2
% 2.65/1.02 Id : 9709, {_}: ld (ld (mult ?12183 ?12184) (mult (mult ?12183 ?12184) (ld ?12184 ?12184))) ?12185 =<= ld (ld (mult ?12183 ?12184) (mult ?12183 ?12184)) (mult (ld (mult ?12183 ?12184) (mult ?12183 ?12184)) ?12185) [12185, 12184, 12183] by Demod 9541 with 1680 at 1,2
% 2.65/1.02 Id : 9710, {_}: ld (ld (mult ?12183 ?12184) (mult (mult ?12183 ?12184) (ld ?12184 ?12184))) ?12185 =>= ld (mult ?12183 ?12184) (mult (mult ?12183 ?12184) ?12185) [12185, 12184, 12183] by Demod 9709 with 185 at 3
% 2.65/1.02 Id : 9711, {_}: ld (ld ?12183 (mult ?12183 (ld ?12184 ?12184))) ?12185 =>= ld (mult ?12183 ?12184) (mult (mult ?12183 ?12184) ?12185) [12185, 12184, 12183] by Demod 9710 with 671 at 1,2
% 2.65/1.02 Id : 9712, {_}: ld (ld ?12183 (mult ?12183 (ld ?12184 ?12184))) ?12185 =>= ld ?12183 (mult ?12183 ?12185) [12185, 12184, 12183] by Demod 9711 with 671 at 3
% 2.65/1.02 Id : 3084, {_}: rd ?1690 (ld ?1691 ?1691) =<= mult ?1690 (ld ?1691 ?1691) [1691, 1690] by Demod 983 with 3061 at 2
% 2.65/1.02 Id : 9713, {_}: ld (ld ?12183 (rd ?12183 (ld ?12184 ?12184))) ?12185 =>= ld ?12183 (mult ?12183 ?12185) [12185, 12184, 12183] by Demod 9712 with 3084 at 2,1,2
% 2.65/1.02 Id : 11189, {_}: mult (rd ?13803 (ld ?13804 (mult ?13804 (ld ?13804 (rd ?13804 (ld ?13805 ?13805)))))) (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) =>= mult ?13803 (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) [13805, 13804, 13803] by Super 3122 with 9713 at 2,1,2
% 2.65/1.02 Id : 5730, {_}: mult ?7381 (ld ?7381 (mult ?7381 ?7382)) =<= ld ?7381 (mult ?7381 (mult ?7381 (ld ?7383 (mult ?7383 ?7382)))) [7383, 7382, 7381] by Super 4 with 3857 at 2,2
% 2.65/1.02 Id : 5827, {_}: ld ?7381 (mult ?7381 (mult ?7381 ?7382)) =<= ld ?7381 (mult ?7381 (mult ?7381 (ld ?7383 (mult ?7383 ?7382)))) [7383, 7382, 7381] by Demod 5730 with 4 at 2
% 2.65/1.02 Id : 5828, {_}: ld ?7381 (mult ?7381 (mult ?7381 ?7382)) =?= mult ?7381 (ld ?7383 (mult ?7383 ?7382)) [7383, 7382, 7381] by Demod 5827 with 118 at 3
% 2.65/1.02 Id : 5829, {_}: mult ?7381 ?7382 =<= mult ?7381 (ld ?7383 (mult ?7383 ?7382)) [7383, 7382, 7381] by Demod 5828 with 118 at 2
% 2.65/1.02 Id : 6034, {_}: mult (rd ?7945 (ld ?7946 (mult ?7946 ?7947))) ?7947 =<= rd ?7945 (ld (ld ?7946 (mult ?7946 ?7947)) (ld ?7946 (mult ?7946 ?7947))) [7947, 7946, 7945] by Super 3076 with 5829 at 2
% 2.65/1.02 Id : 6133, {_}: mult (rd ?7945 (ld ?7946 (mult ?7946 ?7947))) ?7947 =>= rd ?7945 (ld (ld ?7946 (mult ?7946 ?7947)) ?7947) [7947, 7946, 7945] by Demod 6034 with 5813 at 2,3
% 2.65/1.02 Id : 5917, {_}: ld (ld (ld ?7734 (mult ?7734 ?7735)) ?7735) ?7736 =<= ld (ld ?7734 (mult ?7734 ?7735)) (mult (ld ?7734 (mult ?7734 ?7735)) ?7736) [7736, 7735, 7734] by Super 1680 with 5813 at 1,2
% 2.65/1.02 Id : 5974, {_}: ld (ld (ld ?7734 (mult ?7734 ?7735)) ?7735) ?7736 =>= ld ?7734 (mult ?7734 ?7736) [7736, 7735, 7734] by Demod 5917 with 185 at 3
% 2.65/1.02 Id : 7736, {_}: ld (ld (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) ?9803) (mult (ld ?9801 (mult ?9801 ?9803)) ?9804) =?= ld (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) (mult (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) ?9804) [9804, 9803, 9802, 9801] by Super 185 with 5974 at 1,2,2
% 2.65/1.02 Id : 7884, {_}: ld (ld ?9801 (mult ?9801 ?9803)) (mult (ld ?9801 (mult ?9801 ?9803)) ?9804) =?= ld (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) (mult (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) ?9804) [9802, 9804, 9803, 9801] by Demod 7736 with 5974 at 1,2
% 2.65/1.02 Id : 7885, {_}: ld (ld ?9801 (mult ?9801 ?9803)) (ld ?9801 (mult ?9801 (mult ?9803 ?9804))) =?= ld (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) (mult (ld (ld ?9801 (mult ?9801 ?9802)) ?9802) ?9804) [9802, 9804, 9803, 9801] by Demod 7884 with 30 at 2,2
% 2.65/1.02 Id : 7886, {_}: ld (ld ?9801 (mult ?9801 ?9803)) (ld ?9801 (mult ?9801 (mult ?9803 ?9804))) =?= ld (ld ?9801 (mult ?9801 ?9802)) (mult (ld ?9801 (mult ?9801 ?9802)) ?9804) [9802, 9804, 9803, 9801] by Demod 7885 with 185 at 3
% 2.65/1.02 Id : 7887, {_}: ld (ld ?9801 (mult ?9801 ?9803)) (mult ?9803 ?9804) =?= ld (ld ?9801 (mult ?9801 ?9802)) (mult (ld ?9801 (mult ?9801 ?9802)) ?9804) [9802, 9804, 9803, 9801] by Demod 7886 with 5813 at 2
% 2.65/1.02 Id : 9934, {_}: ld (ld ?12491 (mult ?12491 ?12492)) (mult ?12492 ?12493) =>= ld ?12491 (mult ?12491 ?12493) [12493, 12492, 12491] by Demod 7887 with 185 at 3
% 2.65/1.02 Id : 9935, {_}: ld (ld ?12495 (mult ?12495 ?12496)) (ld ?12496 (mult ?12496 ?12497)) =>= ld ?12495 (mult ?12495 (ld ?12496 ?12497)) [12497, 12496, 12495] by Super 9934 with 4 at 2,2
% 2.65/1.02 Id : 10010, {_}: ld (ld ?12495 (mult ?12495 ?12496)) ?12497 =>= ld ?12495 (mult ?12495 (ld ?12496 ?12497)) [12497, 12496, 12495] by Demod 9935 with 5813 at 2
% 2.65/1.02 Id : 10090, {_}: mult (rd ?7945 (ld ?7946 (mult ?7946 ?7947))) ?7947 =>= rd ?7945 (ld ?7946 (mult ?7946 (ld ?7947 ?7947))) [7947, 7946, 7945] by Demod 6133 with 10010 at 2,3
% 2.65/1.02 Id : 10091, {_}: mult (rd ?7945 (ld ?7946 (mult ?7946 ?7947))) ?7947 =>= rd ?7945 (ld ?7946 (rd ?7946 (ld ?7947 ?7947))) [7947, 7946, 7945] by Demod 10090 with 3084 at 2,2,3
% 2.65/1.02 Id : 5922, {_}: rd ?7754 (ld (ld ?7755 (mult ?7755 ?7756)) (ld ?7755 (mult ?7755 ?7756))) =>= mult ?7754 (ld (ld ?7755 (mult ?7755 ?7756)) ?7756) [7756, 7755, 7754] by Super 3084 with 5813 at 2,3
% 2.65/1.02 Id : 5970, {_}: rd ?7754 (ld (ld ?7755 (mult ?7755 ?7756)) ?7756) =<= mult ?7754 (ld (ld ?7755 (mult ?7755 ?7756)) ?7756) [7756, 7755, 7754] by Demod 5922 with 5813 at 2,2
% 2.65/1.02 Id : 10087, {_}: rd ?7754 (ld ?7755 (mult ?7755 (ld ?7756 ?7756))) =<= mult ?7754 (ld (ld ?7755 (mult ?7755 ?7756)) ?7756) [7756, 7755, 7754] by Demod 5970 with 10010 at 2,2
% 2.65/1.02 Id : 10088, {_}: rd ?7754 (ld ?7755 (mult ?7755 (ld ?7756 ?7756))) =<= mult ?7754 (ld ?7755 (mult ?7755 (ld ?7756 ?7756))) [7756, 7755, 7754] by Demod 10087 with 10010 at 2,3
% 2.65/1.02 Id : 10095, {_}: rd ?7754 (ld ?7755 (rd ?7755 (ld ?7756 ?7756))) =<= mult ?7754 (ld ?7755 (mult ?7755 (ld ?7756 ?7756))) [7756, 7755, 7754] by Demod 10088 with 3084 at 2,2,2
% 2.65/1.02 Id : 10096, {_}: rd ?7754 (ld ?7755 (rd ?7755 (ld ?7756 ?7756))) =>= mult ?7754 (ld ?7756 ?7756) [7756, 7755, 7754] by Demod 10095 with 5829 at 3
% 2.65/1.02 Id : 10097, {_}: rd ?7754 (ld ?7755 (rd ?7755 (ld ?7756 ?7756))) =>= rd ?7754 (ld ?7756 ?7756) [7756, 7755, 7754] by Demod 10096 with 3084 at 3
% 2.65/1.02 Id : 10098, {_}: mult (rd ?7945 (ld ?7946 (mult ?7946 ?7947))) ?7947 =>= rd ?7945 (ld ?7947 ?7947) [7947, 7946, 7945] by Demod 10091 with 10097 at 3
% 2.65/1.02 Id : 11326, {_}: rd ?13803 (ld (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) (ld ?13804 (rd ?13804 (ld ?13805 ?13805)))) =>= mult ?13803 (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) [13805, 13804, 13803] by Demod 11189 with 10098 at 2
% 2.65/1.02 Id : 1017, {_}: rd (mult (rd (mult ?550 ?551) ?551) ?552) ?552 =<= mult ?550 (ld ?551 (mult ?551 (ld ?552 ?552))) [552, 551, 550] by Demod 238 with 983 at 1,1,2
% 2.65/1.02 Id : 1018, {_}: rd (mult (rd (mult ?550 ?551) ?551) ?552) ?552 =<= mult ?550 (ld ?551 (rd (mult ?551 ?552) ?552)) [552, 551, 550] by Demod 1017 with 983 at 2,2,3
% 2.65/1.02 Id : 3081, {_}: rd (rd (mult ?550 ?551) ?551) (ld ?552 ?552) =<= mult ?550 (ld ?551 (rd (mult ?551 ?552) ?552)) [552, 551, 550] by Demod 1018 with 3061 at 2
% 2.65/1.02 Id : 3082, {_}: rd (rd (mult ?550 ?551) ?551) (ld ?552 ?552) =<= mult ?550 (ld ?551 (rd ?551 (ld ?552 ?552))) [552, 551, 550] by Demod 3081 with 3061 at 2,2,3
% 2.65/1.02 Id : 3083, {_}: rd (rd ?550 (ld ?551 ?551)) (ld ?552 ?552) =<= mult ?550 (ld ?551 (rd ?551 (ld ?552 ?552))) [552, 551, 550] by Demod 3082 with 3061 at 1,2
% 2.65/1.02 Id : 11327, {_}: rd ?13803 (ld (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) (ld ?13804 (rd ?13804 (ld ?13805 ?13805)))) =>= rd (rd ?13803 (ld ?13804 ?13804)) (ld ?13805 ?13805) [13805, 13804, 13803] by Demod 11326 with 3083 at 3
% 2.65/1.02 Id : 11328, {_}: rd ?13803 (ld ?13804 (mult ?13804 (ld ?13804 (rd ?13804 (ld ?13805 ?13805))))) =>= rd (rd ?13803 (ld ?13804 ?13804)) (ld ?13805 ?13805) [13805, 13804, 13803] by Demod 11327 with 9713 at 2,2
% 2.65/1.02 Id : 11329, {_}: rd ?13803 (ld ?13804 (ld ?13804 (mult ?13804 (rd ?13804 (ld ?13805 ?13805))))) =>= rd (rd ?13803 (ld ?13804 ?13804)) (ld ?13805 ?13805) [13805, 13804, 13803] by Demod 11328 with 4 at 2,2,2
% 2.65/1.02 Id : 11330, {_}: rd ?13803 (ld ?13804 (rd ?13804 (ld ?13805 ?13805))) =<= rd (rd ?13803 (ld ?13804 ?13804)) (ld ?13805 ?13805) [13805, 13804, 13803] by Demod 11329 with 5813 at 2,2
% 2.65/1.02 Id : 11331, {_}: rd ?13803 (ld ?13805 ?13805) =<= rd (rd ?13803 (ld ?13804 ?13804)) (ld ?13805 ?13805) [13804, 13805, 13803] by Demod 11330 with 10097 at 2
% 2.65/1.02 Id : 13075, {_}: rd (rd ?15277 (ld ?15278 ?15278)) ?15279 =?= rd (rd ?15277 (ld ?15279 ?15279)) ?15279 [15279, 15278, 15277] by Super 3062 with 11331 at 1,3
% 2.65/1.02 Id : 13145, {_}: rd (rd ?15277 (ld ?15278 ?15278)) ?15279 =>= rd ?15277 ?15279 [15279, 15278, 15277] by Demod 13075 with 3062 at 3
% 2.65/1.02 Id : 13324, {_}: mult (rd ?15592 (ld ?15593 ?15593)) ?15593 =?= mult (rd ?15592 (ld ?15594 ?15594)) ?15593 [15594, 15593, 15592] by Super 3122 with 13145 at 1,2
% 2.65/1.02 Id : 13391, {_}: mult ?15592 ?15593 =<= mult (rd ?15592 (ld ?15594 ?15594)) ?15593 [15594, 15593, 15592] by Demod 13324 with 3122 at 2
% 2.65/1.02 Id : 14247, {_}: mult x3 x5 =?= mult x3 x5 [] by Demod 14246 with 13391 at 2
% 2.65/1.02 Id : 14246, {_}: mult (rd x3 (ld x4 x4)) x5 =>= mult x3 x5 [] by Demod 1 with 3061 at 1,2
% 2.65/1.02 Id : 1, {_}: mult (rd (mult x3 x4) x4) x5 =>= mult x3 x5 [] by goal
% 2.65/1.02 % SZS output end CNFRefutation for theBenchmark.p
% 2.65/1.02 16155: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.662761 using kbo
%------------------------------------------------------------------------------