%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : ALG005-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n032.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 : Thu Jul 14 17:29:29 EDT 2022
% Result : Unsatisfiable 13.32s 3.64s
% Output : CNFRefutation 13.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.09 % Problem : ALG005-1 : TPTP v8.1.0. Released v2.2.0.
% 0.06/0.10 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 600
% 0.09/0.28 % DateTime : Wed Jun 8 11:01:51 EDT 2022
% 0.09/0.29 % CPUTime :
% 0.09/0.29 29463: Facts:
% 0.09/0.29 29463: Id : 2, {_}:
% 0.09/0.29 difference ?2 (difference ?3 ?2) =>= ?2
% 0.09/0.29 [3, 2] by set_difference_1 ?2 ?3
% 0.09/0.29 29463: Id : 3, {_}:
% 0.09/0.29 difference ?5 (difference ?5 ?6) =?= difference ?6 (difference ?6 ?5)
% 0.09/0.29 [6, 5] by set_difference_2 ?5 ?6
% 0.09/0.29 29463: Id : 4, {_}:
% 0.09/0.29 difference (difference ?8 ?9) ?10
% 0.09/0.29 =<=
% 0.09/0.29 difference (difference ?8 ?10) (difference ?9 ?10)
% 0.09/0.29 [10, 9, 8] by set_difference_3 ?8 ?9 ?10
% 0.09/0.29 29463: Id : 5, {_}:
% 0.09/0.29 multiply ?12 ?13 =<= difference ?12 (difference ?12 ?13)
% 0.09/0.29 [13, 12] by intersection ?12 ?13
% 0.09/0.29 29463: Goal:
% 0.09/0.29 29463: Id : 1, {_}:
% 0.09/0.29 multiply (multiply a b) c =>= multiply a (multiply b c)
% 0.09/0.29 [] by prove_associativity_of_multiply
% 13.32/3.64 Statistics :
% 13.32/3.64 Max weight : 31
% 13.32/3.64 Found proof, 3.350422s
% 13.32/3.64 % SZS status Unsatisfiable for theBenchmark.p
% 13.32/3.64 % SZS output start CNFRefutation for theBenchmark.p
% 13.32/3.64 Id : 6, {_}: difference ?15 (difference ?16 ?15) =>= ?15 [16, 15] by set_difference_1 ?15 ?16
% 13.32/3.64 Id : 27, {_}: difference (difference ?68 ?69) ?70 =<= difference (difference ?68 ?70) (difference ?69 ?70) [70, 69, 68] by set_difference_3 ?68 ?69 ?70
% 13.32/3.64 Id : 2, {_}: difference ?2 (difference ?3 ?2) =>= ?2 [3, 2] by set_difference_1 ?2 ?3
% 13.32/3.64 Id : 4, {_}: difference (difference ?8 ?9) ?10 =<= difference (difference ?8 ?10) (difference ?9 ?10) [10, 9, 8] by set_difference_3 ?8 ?9 ?10
% 13.32/3.64 Id : 58, {_}: multiply ?132 ?133 =<= difference ?132 (difference ?132 ?133) [133, 132] by intersection ?132 ?133
% 13.32/3.64 Id : 5, {_}: multiply ?12 ?13 =<= difference ?12 (difference ?12 ?13) [13, 12] by intersection ?12 ?13
% 13.32/3.64 Id : 3, {_}: difference ?5 (difference ?5 ?6) =?= difference ?6 (difference ?6 ?5) [6, 5] by set_difference_2 ?5 ?6
% 13.32/3.64 Id : 51, {_}: multiply ?5 ?6 =<= difference ?6 (difference ?6 ?5) [6, 5] by Demod 3 with 5 at 2
% 13.32/3.64 Id : 52, {_}: multiply ?5 ?6 =?= multiply ?6 ?5 [6, 5] by Demod 51 with 5 at 3
% 13.32/3.64 Id : 60, {_}: multiply (difference ?138 ?139) (difference ?140 ?139) =<= difference (difference ?138 ?139) (difference (difference ?138 ?140) ?139) [140, 139, 138] by Super 58 with 4 at 2,3
% 13.32/3.64 Id : 67, {_}: multiply (difference ?138 ?139) (difference ?140 ?139) =?= difference (difference ?138 (difference ?138 ?140)) ?139 [140, 139, 138] by Demod 60 with 4 at 3
% 13.32/3.64 Id : 987, {_}: multiply (difference ?1693 ?1694) (difference ?1695 ?1694) =>= difference (multiply ?1693 ?1695) ?1694 [1695, 1694, 1693] by Demod 67 with 5 at 1,3
% 13.32/3.64 Id : 55, {_}: difference (difference ?124 (difference ?124 ?125)) ?125 =>= multiply (difference ?124 ?125) ?125 [125, 124] by Super 4 with 5 at 3
% 13.32/3.64 Id : 65, {_}: difference (multiply ?124 ?125) ?125 =>= multiply (difference ?124 ?125) ?125 [125, 124] by Demod 55 with 5 at 1,2
% 13.32/3.64 Id : 66, {_}: difference (multiply ?124 ?125) ?125 =>= multiply ?125 (difference ?124 ?125) [125, 124] by Demod 65 with 52 at 3
% 13.32/3.64 Id : 59, {_}: multiply ?135 (difference ?136 ?135) =>= difference ?135 ?135 [136, 135] by Super 58 with 2 at 2,3
% 13.32/3.64 Id : 175, {_}: difference (multiply ?124 ?125) ?125 =>= difference ?125 ?125 [125, 124] by Demod 66 with 59 at 3
% 13.32/3.64 Id : 1010, {_}: multiply (difference ?1792 ?1792) (difference ?1793 ?1792) =?= difference (multiply (multiply ?1794 ?1792) ?1793) ?1792 [1794, 1793, 1792] by Super 987 with 175 at 1,2
% 13.32/3.64 Id : 68, {_}: multiply (difference ?138 ?139) (difference ?140 ?139) =>= difference (multiply ?138 ?140) ?139 [140, 139, 138] by Demod 67 with 5 at 1,3
% 13.32/3.64 Id : 1070, {_}: difference (multiply ?1792 ?1793) ?1792 =<= difference (multiply (multiply ?1794 ?1792) ?1793) ?1792 [1794, 1793, 1792] by Demod 1010 with 68 at 2
% 13.32/3.64 Id : 183, {_}: difference (multiply ?325 ?326) ?326 =>= difference ?326 ?326 [326, 325] by Demod 66 with 59 at 3
% 13.32/3.64 Id : 184, {_}: difference (multiply ?328 ?329) ?328 =>= difference ?328 ?328 [329, 328] by Super 183 with 52 at 1,2
% 13.32/3.64 Id : 1071, {_}: difference ?1792 ?1792 =<= difference (multiply (multiply ?1794 ?1792) ?1793) ?1792 [1793, 1794, 1792] by Demod 1070 with 184 at 2
% 13.32/3.64 Id : 7755, {_}: multiply (multiply (multiply ?11940 ?11941) ?11942) ?11941 =<= difference (multiply (multiply ?11940 ?11941) ?11942) (difference ?11941 ?11941) [11942, 11941, 11940] by Super 5 with 1071 at 2,3
% 13.32/3.64 Id : 7868, {_}: multiply ?11941 (multiply (multiply ?11940 ?11941) ?11942) =<= difference (multiply (multiply ?11940 ?11941) ?11942) (difference ?11941 ?11941) [11942, 11940, 11941] by Demod 7755 with 52 at 2
% 13.32/3.64 Id : 32, {_}: difference (difference ?89 ?90) (difference ?91 ?89) =>= difference ?89 (difference ?90 (difference ?91 ?89)) [91, 90, 89] by Super 27 with 2 at 1,3
% 13.32/3.64 Id : 341, {_}: difference (difference ?560 ?561) ?560 =<= difference ?560 (difference ?560 (difference ?561 ?560)) [561, 560] by Super 4 with 32 at 3
% 13.32/3.64 Id : 385, {_}: difference (difference ?560 ?561) ?560 =>= multiply ?560 (difference ?561 ?560) [561, 560] by Demod 341 with 5 at 3
% 13.32/3.64 Id : 431, {_}: difference (difference ?746 ?747) ?746 =>= difference ?746 ?746 [747, 746] by Demod 385 with 59 at 3
% 13.32/3.64 Id : 386, {_}: difference (difference ?560 ?561) ?560 =>= difference ?560 ?560 [561, 560] by Demod 385 with 59 at 3
% 13.32/3.64 Id : 438, {_}: difference (difference ?767 ?767) (difference ?767 ?768) =?= difference (difference ?767 ?768) (difference ?767 ?768) [768, 767] by Super 431 with 386 at 1,2
% 13.32/3.64 Id : 4689, {_}: difference (difference ?7748 ?7748) (difference ?7748 ?7749) =>= difference (difference ?7748 ?7748) ?7749 [7749, 7748] by Demod 438 with 4 at 3
% 13.32/3.64 Id : 4724, {_}: difference (difference ?7872 (difference ?7872 (difference ?7872 ?7872))) (difference (difference ?7872 ?7872) ?7873) =>= difference (difference (difference ?7872 ?7872) (difference ?7872 ?7872)) ?7873 [7873, 7872] by Super 4689 with 32 at 1,2
% 13.32/3.64 Id : 4999, {_}: difference (multiply ?7872 (difference ?7872 ?7872)) (difference (difference ?7872 ?7872) ?7873) =>= difference (difference (difference ?7872 ?7872) (difference ?7872 ?7872)) ?7873 [7873, 7872] by Demod 4724 with 5 at 1,2
% 13.32/3.64 Id : 5000, {_}: difference (multiply ?7872 (difference ?7872 ?7872)) (difference (difference ?7872 ?7872) ?7873) =>= difference (difference ?7872 (difference ?7872 (difference ?7872 ?7872))) ?7873 [7873, 7872] by Demod 4999 with 32 at 1,3
% 13.32/3.64 Id : 5001, {_}: difference (difference ?7872 ?7872) (difference (difference ?7872 ?7872) ?7873) =<= difference (difference ?7872 (difference ?7872 (difference ?7872 ?7872))) ?7873 [7873, 7872] by Demod 5000 with 59 at 1,2
% 13.32/3.64 Id : 5002, {_}: difference (difference ?7872 ?7872) (difference (difference ?7872 ?7872) ?7873) =>= difference (multiply ?7872 (difference ?7872 ?7872)) ?7873 [7873, 7872] by Demod 5001 with 5 at 1,3
% 13.32/3.64 Id : 5003, {_}: multiply (difference ?7872 ?7872) ?7873 =<= difference (multiply ?7872 (difference ?7872 ?7872)) ?7873 [7873, 7872] by Demod 5002 with 5 at 2
% 13.32/3.64 Id : 5004, {_}: multiply (difference ?7872 ?7872) ?7873 =<= difference (difference ?7872 ?7872) ?7873 [7873, 7872] by Demod 5003 with 59 at 1,3
% 13.32/3.64 Id : 235, {_}: multiply (multiply ?393 ?394) ?393 =<= difference (multiply ?393 ?394) (difference ?393 ?393) [394, 393] by Super 5 with 184 at 2,3
% 13.32/3.64 Id : 252, {_}: multiply ?393 (multiply ?393 ?394) =<= difference (multiply ?393 ?394) (difference ?393 ?393) [394, 393] by Demod 235 with 52 at 2
% 13.32/3.64 Id : 349, {_}: difference (difference ?590 ?591) (difference ?592 ?590) =>= difference ?590 (difference ?591 (difference ?592 ?590)) [592, 591, 590] by Super 27 with 2 at 1,3
% 13.32/3.64 Id : 368, {_}: difference (multiply ?671 ?672) (difference ?673 ?671) =<= difference ?671 (difference (difference ?671 ?672) (difference ?673 ?671)) [673, 672, 671] by Super 349 with 5 at 1,2
% 13.32/3.64 Id : 408, {_}: difference (multiply ?671 ?672) (difference ?673 ?671) =<= difference ?671 (difference ?671 (difference ?672 (difference ?673 ?671))) [673, 672, 671] by Demod 368 with 32 at 2,3
% 13.32/3.64 Id : 409, {_}: difference (multiply ?671 ?672) (difference ?673 ?671) =>= multiply ?671 (difference ?672 (difference ?673 ?671)) [673, 672, 671] by Demod 408 with 5 at 3
% 13.32/3.64 Id : 3379, {_}: multiply ?393 (multiply ?393 ?394) =<= multiply ?393 (difference ?394 (difference ?393 ?393)) [394, 393] by Demod 252 with 409 at 3
% 13.32/3.64 Id : 178, {_}: multiply (multiply ?310 ?311) ?311 =<= difference (multiply ?310 ?311) (difference ?311 ?311) [311, 310] by Super 5 with 175 at 2,3
% 13.32/3.64 Id : 194, {_}: multiply ?311 (multiply ?310 ?311) =<= difference (multiply ?310 ?311) (difference ?311 ?311) [310, 311] by Demod 178 with 52 at 2
% 13.32/3.64 Id : 9, {_}: difference (difference ?23 ?24) (difference ?24 (difference ?24 ?23)) =>= difference ?23 ?24 [24, 23] by Super 2 with 3 at 2,2
% 13.32/3.64 Id : 133, {_}: difference (difference ?23 ?24) (multiply ?24 ?23) =>= difference ?23 ?24 [24, 23] by Demod 9 with 5 at 2,2
% 13.32/3.64 Id : 138, {_}: difference (multiply ?262 ?263) (difference ?263 ?262) =>= multiply ?262 ?263 [263, 262] by Super 2 with 133 at 2,2
% 13.32/3.64 Id : 3380, {_}: multiply ?262 (difference ?263 (difference ?263 ?262)) =>= multiply ?262 ?263 [263, 262] by Demod 138 with 409 at 2
% 13.32/3.64 Id : 3381, {_}: multiply ?262 (multiply ?263 ?262) =>= multiply ?262 ?263 [263, 262] by Demod 3380 with 5 at 2,2
% 13.32/3.64 Id : 3382, {_}: multiply ?311 ?310 =<= difference (multiply ?310 ?311) (difference ?311 ?311) [310, 311] by Demod 194 with 3381 at 2
% 13.32/3.64 Id : 24, {_}: difference (difference ?57 ?58) (difference (difference ?57 ?58) (difference ?59 ?58)) =?= difference (difference ?59 ?58) (difference (difference ?59 ?57) ?58) [59, 58, 57] by Super 3 with 4 at 2,3
% 13.32/3.64 Id : 39, {_}: difference (difference ?57 ?58) (difference (difference ?57 ?59) ?58) =?= difference (difference ?59 ?58) (difference (difference ?59 ?57) ?58) [59, 58, 57] by Demod 24 with 4 at 2,2
% 13.32/3.64 Id : 40, {_}: difference (difference ?57 ?58) (difference (difference ?57 ?59) ?58) =?= difference (difference ?59 (difference ?59 ?57)) ?58 [59, 58, 57] by Demod 39 with 4 at 3
% 13.32/3.64 Id : 41, {_}: difference (difference ?57 (difference ?57 ?59)) ?58 =?= difference (difference ?59 (difference ?59 ?57)) ?58 [58, 59, 57] by Demod 40 with 4 at 2
% 13.32/3.64 Id : 4276, {_}: difference (multiply ?57 ?59) ?58 =<= difference (difference ?59 (difference ?59 ?57)) ?58 [58, 59, 57] by Demod 41 with 5 at 1,2
% 13.32/3.64 Id : 4277, {_}: difference (multiply ?57 ?59) ?58 =?= difference (multiply ?59 ?57) ?58 [58, 59, 57] by Demod 4276 with 5 at 1,3
% 13.32/3.64 Id : 4290, {_}: multiply ?6858 ?6859 =<= difference (multiply ?6858 ?6859) (difference ?6858 ?6858) [6859, 6858] by Super 3382 with 4277 at 3
% 13.32/3.64 Id : 4496, {_}: multiply ?6858 ?6859 =<= multiply ?6858 (difference ?6859 (difference ?6858 ?6858)) [6859, 6858] by Demod 4290 with 409 at 3
% 13.32/3.64 Id : 4497, {_}: multiply ?6858 ?6859 =<= multiply ?6858 (multiply ?6858 ?6859) [6859, 6858] by Demod 4496 with 3379 at 3
% 13.32/3.64 Id : 4535, {_}: multiply ?393 ?394 =<= multiply ?393 (difference ?394 (difference ?393 ?393)) [394, 393] by Demod 3379 with 4497 at 2
% 13.32/3.64 Id : 470, {_}: difference (difference ?767 ?767) (difference ?767 ?768) =>= difference (difference ?767 ?767) ?768 [768, 767] by Demod 438 with 4 at 3
% 13.32/3.64 Id : 4687, {_}: multiply (difference ?7743 ?7743) ?7744 =<= multiply (difference ?7743 ?7743) (difference ?7744 (difference (difference ?7743 ?7743) ?7743)) [7744, 7743] by Super 4535 with 470 at 2,2,3
% 13.32/3.64 Id : 7, {_}: difference (difference ?18 ?19) ?19 =>= difference ?18 ?19 [19, 18] by Super 6 with 2 at 2,2
% 13.32/3.64 Id : 4740, {_}: multiply (difference ?7743 ?7743) ?7744 =<= multiply (difference ?7743 ?7743) (difference ?7744 (difference ?7743 ?7743)) [7744, 7743] by Demod 4687 with 7 at 2,2,3
% 13.32/3.64 Id : 4741, {_}: multiply (difference ?7743 ?7743) ?7744 =?= difference (difference ?7743 ?7743) (difference ?7743 ?7743) [7744, 7743] by Demod 4740 with 59 at 3
% 13.32/3.64 Id : 4742, {_}: multiply (difference ?7743 ?7743) ?7744 =?= difference ?7743 (difference ?7743 (difference ?7743 ?7743)) [7744, 7743] by Demod 4741 with 32 at 3
% 13.32/3.64 Id : 4743, {_}: multiply (difference ?7743 ?7743) ?7744 =?= multiply ?7743 (difference ?7743 ?7743) [7744, 7743] by Demod 4742 with 5 at 3
% 13.32/3.64 Id : 4744, {_}: multiply (difference ?7743 ?7743) ?7744 =>= difference ?7743 ?7743 [7744, 7743] by Demod 4743 with 59 at 3
% 13.32/3.64 Id : 5157, {_}: difference ?7872 ?7872 =<= difference (difference ?7872 ?7872) ?7873 [7873, 7872] by Demod 5004 with 4744 at 2
% 13.32/3.64 Id : 5202, {_}: difference ?8202 (difference ?8203 ?8203) =>= ?8202 [8203, 8202] by Super 2 with 5157 at 2,2
% 13.32/3.64 Id : 10508, {_}: multiply ?15820 (multiply (multiply ?15821 ?15820) ?15822) =>= multiply (multiply ?15821 ?15820) ?15822 [15822, 15821, 15820] by Demod 7868 with 5202 at 3
% 13.32/3.64 Id : 10509, {_}: multiply ?15824 (multiply (multiply ?15824 ?15825) ?15826) =>= multiply (multiply ?15825 ?15824) ?15826 [15826, 15825, 15824] by Super 10508 with 52 at 1,2,2
% 13.32/3.64 Id : 1011, {_}: multiply (difference ?1796 ?1796) (difference ?1797 ?1796) =?= difference (multiply (multiply ?1796 ?1798) ?1797) ?1796 [1798, 1797, 1796] by Super 987 with 184 at 1,2
% 13.32/3.64 Id : 1072, {_}: difference (multiply ?1796 ?1797) ?1796 =<= difference (multiply (multiply ?1796 ?1798) ?1797) ?1796 [1798, 1797, 1796] by Demod 1011 with 68 at 2
% 13.32/3.64 Id : 1073, {_}: difference ?1796 ?1796 =<= difference (multiply (multiply ?1796 ?1798) ?1797) ?1796 [1797, 1798, 1796] by Demod 1072 with 184 at 2
% 13.32/3.64 Id : 8005, {_}: multiply (multiply (multiply ?12279 ?12280) ?12281) ?12279 =<= difference (multiply (multiply ?12279 ?12280) ?12281) (difference ?12279 ?12279) [12281, 12280, 12279] by Super 5 with 1073 at 2,3
% 13.32/3.64 Id : 8121, {_}: multiply ?12279 (multiply (multiply ?12279 ?12280) ?12281) =<= difference (multiply (multiply ?12279 ?12280) ?12281) (difference ?12279 ?12279) [12281, 12280, 12279] by Demod 8005 with 52 at 2
% 13.32/3.64 Id : 8122, {_}: multiply ?12279 (multiply (multiply ?12279 ?12280) ?12281) =>= multiply (multiply ?12279 ?12280) ?12281 [12281, 12280, 12279] by Demod 8121 with 5202 at 3
% 13.32/3.64 Id : 12952, {_}: multiply (multiply ?15824 ?15825) ?15826 =?= multiply (multiply ?15825 ?15824) ?15826 [15826, 15825, 15824] by Demod 10509 with 8122 at 2
% 13.32/3.64 Id : 119, {_}: multiply ?231 (difference ?231 ?232) =<= difference ?231 (multiply ?231 ?232) [232, 231] by Super 58 with 5 at 2,3
% 13.32/3.64 Id : 120, {_}: multiply ?234 (difference ?234 ?235) =<= difference ?234 (multiply ?235 ?234) [235, 234] by Super 119 with 52 at 2,3
% 13.32/3.64 Id : 423, {_}: multiply (difference ?720 ?721) ?720 =<= difference (difference ?720 ?721) (difference ?720 ?720) [721, 720] by Super 5 with 386 at 2,3
% 13.32/3.64 Id : 459, {_}: multiply ?720 (difference ?720 ?721) =<= difference (difference ?720 ?721) (difference ?720 ?720) [721, 720] by Demod 423 with 52 at 2
% 13.32/3.64 Id : 460, {_}: multiply ?720 (difference ?720 ?721) =<= difference ?720 (difference ?721 (difference ?720 ?720)) [721, 720] by Demod 459 with 32 at 3
% 13.32/3.64 Id : 5586, {_}: multiply ?720 (difference ?720 ?721) =>= difference ?720 ?721 [721, 720] by Demod 460 with 5202 at 2,3
% 13.32/3.64 Id : 5589, {_}: difference ?234 ?235 =<= difference ?234 (multiply ?235 ?234) [235, 234] by Demod 120 with 5586 at 2
% 13.32/3.64 Id : 993, {_}: multiply (difference ?1718 ?1719) (difference ?1719 ?1719) =?= difference (multiply ?1718 (multiply ?1720 ?1719)) ?1719 [1720, 1719, 1718] by Super 987 with 175 at 2,2
% 13.32/3.64 Id : 1057, {_}: difference (multiply ?1718 ?1719) ?1719 =<= difference (multiply ?1718 (multiply ?1720 ?1719)) ?1719 [1720, 1719, 1718] by Demod 993 with 68 at 2
% 13.32/3.64 Id : 1058, {_}: difference ?1719 ?1719 =<= difference (multiply ?1718 (multiply ?1720 ?1719)) ?1719 [1720, 1718, 1719] by Demod 1057 with 175 at 2
% 13.32/3.64 Id : 6372, {_}: multiply (multiply ?9827 (multiply ?9828 ?9829)) ?9829 =<= difference (multiply ?9827 (multiply ?9828 ?9829)) (difference ?9829 ?9829) [9829, 9828, 9827] by Super 5 with 1058 at 2,3
% 13.32/3.64 Id : 6460, {_}: multiply ?9829 (multiply ?9827 (multiply ?9828 ?9829)) =<= difference (multiply ?9827 (multiply ?9828 ?9829)) (difference ?9829 ?9829) [9828, 9827, 9829] by Demod 6372 with 52 at 2
% 13.32/3.64 Id : 8995, {_}: multiply ?13421 (multiply ?13422 (multiply ?13423 ?13421)) =>= multiply ?13422 (multiply ?13423 ?13421) [13423, 13422, 13421] by Demod 6460 with 5202 at 3
% 13.32/3.64 Id : 8996, {_}: multiply ?13425 (multiply ?13426 (multiply ?13425 ?13427)) =>= multiply ?13426 (multiply ?13427 ?13425) [13427, 13426, 13425] by Super 8995 with 52 at 2,2,2
% 13.32/3.64 Id : 994, {_}: multiply (difference ?1722 ?1723) (difference ?1723 ?1723) =?= difference (multiply ?1722 (multiply ?1723 ?1724)) ?1723 [1724, 1723, 1722] by Super 987 with 184 at 2,2
% 13.32/3.64 Id : 1059, {_}: difference (multiply ?1722 ?1723) ?1723 =<= difference (multiply ?1722 (multiply ?1723 ?1724)) ?1723 [1724, 1723, 1722] by Demod 994 with 68 at 2
% 13.32/3.64 Id : 1060, {_}: difference ?1723 ?1723 =<= difference (multiply ?1722 (multiply ?1723 ?1724)) ?1723 [1724, 1722, 1723] by Demod 1059 with 175 at 2
% 13.32/3.64 Id : 6988, {_}: multiply (multiply ?10682 (multiply ?10683 ?10684)) ?10683 =<= difference (multiply ?10682 (multiply ?10683 ?10684)) (difference ?10683 ?10683) [10684, 10683, 10682] by Super 5 with 1060 at 2,3
% 13.32/3.64 Id : 7087, {_}: multiply ?10683 (multiply ?10682 (multiply ?10683 ?10684)) =<= difference (multiply ?10682 (multiply ?10683 ?10684)) (difference ?10683 ?10683) [10684, 10682, 10683] by Demod 6988 with 52 at 2
% 13.32/3.64 Id : 7088, {_}: multiply ?10683 (multiply ?10682 (multiply ?10683 ?10684)) =>= multiply ?10682 (multiply ?10683 ?10684) [10684, 10682, 10683] by Demod 7087 with 5202 at 3
% 13.32/3.64 Id : 11444, {_}: multiply ?13426 (multiply ?13425 ?13427) =?= multiply ?13426 (multiply ?13427 ?13425) [13427, 13425, 13426] by Demod 8996 with 7088 at 2
% 13.32/3.64 Id : 179, {_}: difference (difference ?313 (multiply ?314 ?315)) ?315 =?= difference (difference ?313 ?315) (difference ?315 ?315) [315, 314, 313] by Super 4 with 175 at 2,3
% 13.32/3.64 Id : 191, {_}: difference (difference ?313 (multiply ?314 ?315)) ?315 =>= difference (difference ?313 ?315) ?315 [315, 314, 313] by Demod 179 with 4 at 3
% 13.32/3.64 Id : 192, {_}: difference (difference ?313 (multiply ?314 ?315)) ?315 =>= difference ?313 ?315 [315, 314, 313] by Demod 191 with 7 at 3
% 13.32/3.64 Id : 2167, {_}: multiply (difference ?3258 (multiply ?3259 ?3260)) ?3260 =<= difference (difference ?3258 (multiply ?3259 ?3260)) (difference ?3258 ?3260) [3260, 3259, 3258] by Super 5 with 192 at 2,3
% 13.32/3.64 Id : 34140, {_}: multiply ?55099 (difference ?55100 (multiply ?55101 ?55099)) =<= difference (difference ?55100 (multiply ?55101 ?55099)) (difference ?55100 ?55099) [55101, 55100, 55099] by Demod 2167 with 52 at 2
% 13.32/3.64 Id : 34141, {_}: multiply (difference ?55103 ?55104) (difference ?55104 (multiply ?55105 (difference ?55103 ?55104))) =>= difference (difference ?55104 (multiply ?55105 (difference ?55103 ?55104))) ?55104 [55105, 55104, 55103] by Super 34140 with 2 at 2,3
% 13.32/3.64 Id : 6607, {_}: difference (difference ?10208 ?10209) (difference ?10209 ?10210) =<= difference (difference ?10208 (difference ?10209 ?10210)) (multiply ?10209 ?10210) [10210, 10209, 10208] by Super 4 with 5 at 2,3
% 13.32/3.64 Id : 6617, {_}: difference (difference ?10248 ?10249) (difference ?10249 (difference ?10249 ?10250)) =<= difference (difference ?10248 (difference ?10249 (difference ?10249 ?10250))) (difference ?10249 ?10250) [10250, 10249, 10248] by Super 6607 with 5586 at 2,3
% 13.32/3.64 Id : 6786, {_}: difference (difference ?10248 ?10249) (multiply ?10249 ?10250) =<= difference (difference ?10248 (difference ?10249 (difference ?10249 ?10250))) (difference ?10249 ?10250) [10250, 10249, 10248] by Demod 6617 with 5 at 2,2
% 13.32/3.64 Id : 28, {_}: difference (difference ?72 ?73) (difference ?74 ?73) =<= difference (difference ?72 (difference ?74 ?73)) ?73 [74, 73, 72] by Super 27 with 2 at 2,3
% 13.32/3.64 Id : 48, {_}: difference (difference ?72 ?74) ?73 =<= difference (difference ?72 (difference ?74 ?73)) ?73 [73, 74, 72] by Demod 28 with 4 at 2
% 13.32/3.64 Id : 6787, {_}: difference (difference ?10248 ?10249) (multiply ?10249 ?10250) =<= difference (difference ?10248 ?10249) (difference ?10249 ?10250) [10250, 10249, 10248] by Demod 6786 with 48 at 3
% 13.32/3.64 Id : 9131, {_}: multiply (difference ?13643 ?13644) (difference ?13644 ?13645) =<= difference (difference ?13643 ?13644) (difference (difference ?13643 ?13644) (multiply ?13644 ?13645)) [13645, 13644, 13643] by Super 5 with 6787 at 2,3
% 13.32/3.64 Id : 9321, {_}: multiply (difference ?13643 ?13644) (difference ?13644 ?13645) =>= multiply (difference ?13643 ?13644) (multiply ?13644 ?13645) [13645, 13644, 13643] by Demod 9131 with 5 at 3
% 13.32/3.64 Id : 34488, {_}: multiply (difference ?55103 ?55104) (multiply ?55104 (multiply ?55105 (difference ?55103 ?55104))) =>= difference (difference ?55104 (multiply ?55105 (difference ?55103 ?55104))) ?55104 [55105, 55104, 55103] by Demod 34141 with 9321 at 2
% 13.32/3.64 Id : 34489, {_}: multiply (difference ?55103 ?55104) (multiply ?55104 (multiply ?55105 (difference ?55103 ?55104))) =>= difference ?55104 ?55104 [55105, 55104, 55103] by Demod 34488 with 386 at 3
% 13.32/3.64 Id : 6461, {_}: multiply ?9829 (multiply ?9827 (multiply ?9828 ?9829)) =>= multiply ?9827 (multiply ?9828 ?9829) [9828, 9827, 9829] by Demod 6460 with 5202 at 3
% 13.32/3.64 Id : 34490, {_}: multiply ?55104 (multiply ?55105 (difference ?55103 ?55104)) =>= difference ?55104 ?55104 [55103, 55105, 55104] by Demod 34489 with 6461 at 2
% 13.32/3.64 Id : 34835, {_}: multiply ?56159 (multiply (difference ?56160 ?56159) ?56161) =>= difference ?56159 ?56159 [56161, 56160, 56159] by Super 11444 with 34490 at 3
% 13.32/3.64 Id : 35898, {_}: difference (multiply (difference ?57544 ?57545) ?57546) ?57545 =<= difference (multiply (difference ?57544 ?57545) ?57546) (difference ?57545 ?57545) [57546, 57545, 57544] by Super 5589 with 34835 at 2,3
% 13.32/3.64 Id : 34815, {_}: difference (multiply ?56075 (difference ?56076 ?56077)) ?56077 =<= difference (multiply ?56075 (difference ?56076 ?56077)) (difference ?56077 ?56077) [56077, 56076, 56075] by Super 5589 with 34490 at 2,3
% 13.32/3.64 Id : 989, {_}: multiply (difference ?1701 ?1702) (difference ?1703 ?1702) =<= difference (multiply ?1701 (difference ?1703 ?1702)) ?1702 [1703, 1702, 1701] by Super 987 with 7 at 2,2
% 13.32/3.64 Id : 1054, {_}: difference (multiply ?1701 ?1703) ?1702 =<= difference (multiply ?1701 (difference ?1703 ?1702)) ?1702 [1702, 1703, 1701] by Demod 989 with 68 at 2
% 13.32/3.64 Id : 35046, {_}: difference (multiply ?56075 ?56076) ?56077 =<= difference (multiply ?56075 (difference ?56076 ?56077)) (difference ?56077 ?56077) [56077, 56076, 56075] by Demod 34815 with 1054 at 2
% 13.32/3.64 Id : 35047, {_}: difference (multiply ?56075 ?56076) ?56077 =>= multiply ?56075 (difference ?56076 ?56077) [56077, 56076, 56075] by Demod 35046 with 5202 at 3
% 13.32/3.64 Id : 36099, {_}: multiply (difference ?57544 ?57545) (difference ?57546 ?57545) =<= difference (multiply (difference ?57544 ?57545) ?57546) (difference ?57545 ?57545) [57546, 57545, 57544] by Demod 35898 with 35047 at 2
% 13.32/3.64 Id : 36100, {_}: multiply (difference ?57544 ?57545) (difference ?57546 ?57545) =>= multiply (difference ?57544 ?57545) ?57546 [57546, 57545, 57544] by Demod 36099 with 5202 at 3
% 13.32/3.64 Id : 1006, {_}: multiply (difference ?1775 ?1776) (difference ?1777 ?1776) =<= difference (multiply (difference ?1775 ?1776) ?1777) ?1776 [1777, 1776, 1775] by Super 987 with 7 at 1,2
% 13.32/3.64 Id : 1069, {_}: difference (multiply ?1775 ?1777) ?1776 =<= difference (multiply (difference ?1775 ?1776) ?1777) ?1776 [1776, 1777, 1775] by Demod 1006 with 68 at 2
% 13.32/3.64 Id : 35382, {_}: multiply ?1775 (difference ?1777 ?1776) =<= difference (multiply (difference ?1775 ?1776) ?1777) ?1776 [1776, 1777, 1775] by Demod 1069 with 35047 at 2
% 13.32/3.64 Id : 35383, {_}: multiply ?1775 (difference ?1777 ?1776) =<= multiply (difference ?1775 ?1776) (difference ?1777 ?1776) [1776, 1777, 1775] by Demod 35382 with 35047 at 3
% 13.32/3.64 Id : 36101, {_}: multiply ?57544 (difference ?57546 ?57545) =<= multiply (difference ?57544 ?57545) ?57546 [57545, 57546, 57544] by Demod 36100 with 35383 at 2
% 13.32/3.64 Id : 37247, {_}: difference ?59806 (difference ?59807 ?59808) =<= difference ?59806 (multiply ?59807 (difference ?59806 ?59808)) [59808, 59807, 59806] by Super 5589 with 36101 at 2,3
% 13.32/3.64 Id : 37271, {_}: difference ?59923 (difference ?59924 (difference ?59923 ?59925)) =>= difference ?59923 (multiply ?59924 (multiply ?59923 ?59925)) [59925, 59924, 59923] by Super 37247 with 5 at 2,2,3
% 13.32/3.64 Id : 61, {_}: multiply ?142 (difference ?142 ?143) =<= difference ?142 (multiply ?142 ?143) [143, 142] by Super 58 with 5 at 2,3
% 13.32/3.64 Id : 5588, {_}: difference ?142 ?143 =<= difference ?142 (multiply ?142 ?143) [143, 142] by Demod 61 with 5586 at 2
% 13.32/3.64 Id : 37278, {_}: difference ?59958 (difference ?59959 (multiply ?59958 ?59960)) =>= difference ?59958 (multiply ?59959 (difference ?59958 ?59960)) [59960, 59959, 59958] by Super 37247 with 5588 at 2,2,3
% 13.32/3.64 Id : 36373, {_}: difference ?58219 (difference ?58220 ?58221) =<= difference ?58219 (multiply ?58220 (difference ?58219 ?58221)) [58221, 58220, 58219] by Super 5589 with 36101 at 2,3
% 13.32/3.64 Id : 37495, {_}: difference ?59958 (difference ?59959 (multiply ?59958 ?59960)) =>= difference ?59958 (difference ?59959 ?59960) [59960, 59959, 59958] by Demod 37278 with 36373 at 3
% 13.32/3.64 Id : 41778, {_}: difference ?66507 (difference ?66508 (difference ?66507 ?66509)) =<= difference ?66507 (multiply ?66508 (multiply ?66507 (multiply ?66508 ?66509))) [66509, 66508, 66507] by Super 37271 with 37495 at 2,2
% 13.32/3.64 Id : 41866, {_}: difference ?66507 (multiply ?66508 (multiply ?66507 ?66509)) =<= difference ?66507 (multiply ?66508 (multiply ?66507 (multiply ?66508 ?66509))) [66509, 66508, 66507] by Demod 41778 with 37271 at 2
% 13.32/3.64 Id : 41867, {_}: difference ?66507 (multiply ?66508 (multiply ?66507 ?66509)) =?= difference ?66507 (multiply ?66507 (multiply ?66508 ?66509)) [66509, 66508, 66507] by Demod 41866 with 7088 at 2,3
% 13.32/3.64 Id : 45208, {_}: difference ?72570 (multiply ?72571 (multiply ?72570 ?72572)) =>= difference ?72570 (multiply ?72571 ?72572) [72572, 72571, 72570] by Demod 41867 with 5588 at 3
% 13.32/3.64 Id : 45244, {_}: difference ?72742 (multiply (multiply ?72742 ?72743) ?72744) =>= difference ?72742 (multiply ?72744 ?72743) [72744, 72743, 72742] by Super 45208 with 52 at 2,2
% 13.32/3.64 Id : 47723, {_}: multiply ?76702 (multiply (multiply ?76702 ?76703) ?76704) =<= difference ?76702 (difference ?76702 (multiply ?76704 ?76703)) [76704, 76703, 76702] by Super 5 with 45244 at 2,3
% 13.32/3.64 Id : 47952, {_}: multiply (multiply ?76702 ?76703) ?76704 =<= difference ?76702 (difference ?76702 (multiply ?76704 ?76703)) [76704, 76703, 76702] by Demod 47723 with 8122 at 2
% 13.32/3.64 Id : 47953, {_}: multiply (multiply ?76702 ?76703) ?76704 =>= multiply ?76702 (multiply ?76704 ?76703) [76704, 76703, 76702] by Demod 47952 with 5 at 3
% 13.32/3.64 Id : 48231, {_}: multiply ?15824 (multiply ?15826 ?15825) =<= multiply (multiply ?15825 ?15824) ?15826 [15825, 15826, 15824] by Demod 12952 with 47953 at 2
% 13.32/3.64 Id : 48232, {_}: multiply ?15824 (multiply ?15826 ?15825) =?= multiply ?15825 (multiply ?15826 ?15824) [15825, 15826, 15824] by Demod 48231 with 47953 at 3
% 13.32/3.64 Id : 29, {_}: difference (difference ?76 ?77) (difference ?77 ?78) =<= difference (difference ?76 (difference ?77 ?78)) (difference ?78 (difference ?78 ?77)) [78, 77, 76] by Super 27 with 3 at 2,3
% 13.32/3.64 Id : 268, {_}: difference (difference ?76 ?77) (difference ?77 ?78) =<= difference (difference ?76 (difference ?77 ?78)) (multiply ?78 ?77) [78, 77, 76] by Demod 29 with 5 at 2,3
% 13.32/3.64 Id : 271, {_}: multiply (difference ?433 (difference ?434 ?435)) (multiply ?435 ?434) =<= difference (difference ?433 (difference ?434 ?435)) (difference (difference ?433 ?434) (difference ?434 ?435)) [435, 434, 433] by Super 5 with 268 at 2,3
% 13.32/3.64 Id : 298, {_}: multiply (multiply ?435 ?434) (difference ?433 (difference ?434 ?435)) =<= difference (difference ?433 (difference ?434 ?435)) (difference (difference ?433 ?434) (difference ?434 ?435)) [433, 434, 435] by Demod 271 with 52 at 2
% 13.32/3.64 Id : 299, {_}: multiply (multiply ?435 ?434) (difference ?433 (difference ?434 ?435)) =?= difference (difference ?433 (difference ?433 ?434)) (difference ?434 ?435) [433, 434, 435] by Demod 298 with 4 at 3
% 13.32/3.64 Id : 300, {_}: multiply (multiply ?435 ?434) (difference ?433 (difference ?434 ?435)) =>= difference (multiply ?433 ?434) (difference ?434 ?435) [433, 434, 435] by Demod 299 with 5 at 1,3
% 13.32/3.64 Id : 35388, {_}: multiply (multiply ?435 ?434) (difference ?433 (difference ?434 ?435)) =>= multiply ?433 (difference ?434 (difference ?434 ?435)) [433, 434, 435] by Demod 300 with 35047 at 3
% 13.32/3.64 Id : 35400, {_}: multiply (multiply ?435 ?434) (difference ?433 (difference ?434 ?435)) =>= multiply ?433 (multiply ?434 ?435) [433, 434, 435] by Demod 35388 with 5 at 2,3
% 13.32/3.64 Id : 41704, {_}: multiply (multiply (multiply ?66139 ?66140) ?66141) (difference ?66139 (difference ?66141 ?66140)) =>= multiply ?66139 (multiply ?66141 (multiply ?66139 ?66140)) [66141, 66140, 66139] by Super 35400 with 37495 at 2,2
% 13.32/3.64 Id : 35366, {_}: multiply ?57 (difference ?59 ?58) =<= difference (multiply ?59 ?57) ?58 [58, 59, 57] by Demod 4277 with 35047 at 2
% 13.32/3.64 Id : 35367, {_}: multiply ?57 (difference ?59 ?58) =?= multiply ?59 (difference ?57 ?58) [58, 59, 57] by Demod 35366 with 35047 at 3
% 13.32/3.64 Id : 42002, {_}: multiply ?66139 (difference (multiply (multiply ?66139 ?66140) ?66141) (difference ?66141 ?66140)) =>= multiply ?66139 (multiply ?66141 (multiply ?66139 ?66140)) [66141, 66140, 66139] by Demod 41704 with 35367 at 2
% 13.32/3.64 Id : 42003, {_}: multiply ?66139 (difference (multiply (multiply ?66139 ?66140) ?66141) (difference ?66141 ?66140)) =>= multiply ?66141 (multiply ?66139 ?66140) [66141, 66140, 66139] by Demod 42002 with 7088 at 3
% 13.32/3.64 Id : 42004, {_}: multiply ?66139 (multiply (multiply ?66139 ?66140) (difference ?66141 (difference ?66141 ?66140))) =>= multiply ?66141 (multiply ?66139 ?66140) [66141, 66140, 66139] by Demod 42003 with 35047 at 2,2
% 13.32/3.64 Id : 42005, {_}: multiply (multiply ?66139 ?66140) (difference ?66141 (difference ?66141 ?66140)) =>= multiply ?66141 (multiply ?66139 ?66140) [66141, 66140, 66139] by Demod 42004 with 8122 at 2
% 13.32/3.64 Id : 42006, {_}: multiply (multiply ?66139 ?66140) (multiply ?66141 ?66140) =>= multiply ?66141 (multiply ?66139 ?66140) [66141, 66140, 66139] by Demod 42005 with 5 at 2,2
% 13.32/3.64 Id : 48238, {_}: multiply ?66139 (multiply (multiply ?66141 ?66140) ?66140) =>= multiply ?66141 (multiply ?66139 ?66140) [66140, 66141, 66139] by Demod 42006 with 47953 at 2
% 13.32/3.64 Id : 48239, {_}: multiply ?66139 (multiply ?66141 (multiply ?66140 ?66140)) =>= multiply ?66141 (multiply ?66139 ?66140) [66140, 66141, 66139] by Demod 48238 with 47953 at 2,2
% 13.32/3.64 Id : 57, {_}: multiply ?130 ?130 =>= ?130 [130] by Super 2 with 5 at 2
% 13.32/3.64 Id : 48240, {_}: multiply ?66139 (multiply ?66141 ?66140) =?= multiply ?66141 (multiply ?66139 ?66140) [66140, 66141, 66139] by Demod 48239 with 57 at 2,2,2
% 13.32/3.64 Id : 48669, {_}: multiply a (multiply b c) =?= multiply a (multiply b c) [] by Demod 48668 with 48240 at 2
% 13.32/3.64 Id : 48668, {_}: multiply b (multiply a c) =>= multiply a (multiply b c) [] by Demod 48667 with 48232 at 2
% 13.32/3.64 Id : 48667, {_}: multiply c (multiply a b) =>= multiply a (multiply b c) [] by Demod 1 with 52 at 2
% 13.32/3.64 Id : 1, {_}: multiply (multiply a b) c =>= multiply a (multiply b c) [] by prove_associativity_of_multiply
% 13.32/3.64 % SZS output end CNFRefutation for theBenchmark.p
% 13.32/3.64 29464: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 3.290605 using kbo
%------------------------------------------------------------------------------