%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : BOO031-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 : n020.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 23:44:16 EDT 2022
% Result : Unsatisfiable 4.60s 1.52s
% Output : CNFRefutation 4.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : BOO031-1 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.34 % Computer : n020.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 : Wed Jun 1 22:53:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 5501: Facts:
% 0.13/0.34 5501: Id : 2, {_}:
% 0.13/0.34 add (multiply ?2 ?3) (add (multiply ?3 ?4) (multiply ?4 ?2))
% 0.13/0.34 =>=
% 0.13/0.34 multiply (add ?2 ?3) (multiply (add ?3 ?4) (add ?4 ?2))
% 0.13/0.34 [4, 3, 2] by distributivity ?2 ?3 ?4
% 0.13/0.34 5501: Id : 3, {_}:
% 0.13/0.34 add ?6 (multiply ?7 (multiply ?6 ?8)) =>= ?6
% 0.13/0.34 [8, 7, 6] by l1 ?6 ?7 ?8
% 0.13/0.34 5501: Id : 4, {_}:
% 0.13/0.34 add (add (multiply ?10 ?11) (multiply ?11 ?12)) ?11 =>= ?11
% 0.13/0.34 [12, 11, 10] by l3 ?10 ?11 ?12
% 0.13/0.34 5501: Id : 5, {_}:
% 0.13/0.34 multiply (add ?14 (inverse ?14)) ?15 =>= ?15
% 0.13/0.34 [15, 14] by property3 ?14 ?15
% 0.13/0.34 5501: Id : 6, {_}:
% 0.13/0.34 multiply ?17 (add ?18 (add ?17 ?19)) =>= ?17
% 0.13/0.34 [19, 18, 17] by l2 ?17 ?18 ?19
% 0.13/0.34 5501: Id : 7, {_}:
% 0.13/0.34 multiply (multiply (add ?21 ?22) (add ?22 ?23)) ?22 =>= ?22
% 0.13/0.34 [23, 22, 21] by l4 ?21 ?22 ?23
% 0.13/0.34 5501: Id : 8, {_}:
% 0.13/0.34 add (multiply ?25 (inverse ?25)) ?26 =>= ?26
% 0.13/0.34 [26, 25] by property3_dual ?25 ?26
% 0.13/0.34 5501: Id : 9, {_}: add ?28 (inverse ?28) =>= n1 [28] by additive_inverse ?28
% 0.13/0.34 5501: Id : 10, {_}:
% 0.13/0.34 multiply ?30 (inverse ?30) =>= n0
% 0.13/0.34 [30] by multiplicative_inverse ?30
% 0.13/0.34 5501: Id : 11, {_}:
% 0.13/0.34 add (add ?32 ?33) ?34 =?= add ?32 (add ?33 ?34)
% 0.13/0.34 [34, 33, 32] by associativity_of_add ?32 ?33 ?34
% 0.13/0.34 5501: Id : 12, {_}:
% 0.13/0.34 multiply (multiply ?36 ?37) ?38 =?= multiply ?36 (multiply ?37 ?38)
% 0.13/0.34 [38, 37, 36] by associativity_of_multiply ?36 ?37 ?38
% 0.13/0.34 5501: Goal:
% 0.13/0.34 5501: Id : 1, {_}:
% 0.13/0.34 multiply a (add b c) =<= add (multiply b a) (multiply c a)
% 0.13/0.34 [] by prove_multiply_add_property
% 4.60/1.52 Statistics :
% 4.60/1.52 Max weight : 29
% 4.60/1.52 Found proof, 1.176212s
% 4.60/1.52 % SZS status Unsatisfiable for theBenchmark.p
% 4.60/1.52 % SZS output start CNFRefutation for theBenchmark.p
% 4.60/1.52 Id : 10, {_}: multiply ?30 (inverse ?30) =>= n0 [30] by multiplicative_inverse ?30
% 4.60/1.52 Id : 7, {_}: multiply (multiply (add ?21 ?22) (add ?22 ?23)) ?22 =>= ?22 [23, 22, 21] by l4 ?21 ?22 ?23
% 4.60/1.52 Id : 12, {_}: multiply (multiply ?36 ?37) ?38 =>= multiply ?36 (multiply ?37 ?38) [38, 37, 36] by associativity_of_multiply ?36 ?37 ?38
% 4.60/1.52 Id : 52, {_}: multiply (multiply (add ?189 ?190) (add ?190 ?191)) ?190 =>= ?190 [191, 190, 189] by l4 ?189 ?190 ?191
% 4.60/1.52 Id : 9, {_}: add ?28 (inverse ?28) =>= n1 [28] by additive_inverse ?28
% 4.60/1.52 Id : 5, {_}: multiply (add ?14 (inverse ?14)) ?15 =>= ?15 [15, 14] by property3 ?14 ?15
% 4.60/1.52 Id : 2, {_}: add (multiply ?2 ?3) (add (multiply ?3 ?4) (multiply ?4 ?2)) =>= multiply (add ?2 ?3) (multiply (add ?3 ?4) (add ?4 ?2)) [4, 3, 2] by distributivity ?2 ?3 ?4
% 4.60/1.52 Id : 18, {_}: add (add (multiply ?58 ?59) (multiply ?59 ?60)) ?59 =>= ?59 [60, 59, 58] by l3 ?58 ?59 ?60
% 4.60/1.52 Id : 11, {_}: add (add ?32 ?33) ?34 =>= add ?32 (add ?33 ?34) [34, 33, 32] by associativity_of_add ?32 ?33 ?34
% 4.60/1.52 Id : 4, {_}: add (add (multiply ?10 ?11) (multiply ?11 ?12)) ?11 =>= ?11 [12, 11, 10] by l3 ?10 ?11 ?12
% 4.60/1.52 Id : 37, {_}: multiply ?128 (add ?129 (add ?128 ?130)) =>= ?128 [130, 129, 128] by l2 ?128 ?129 ?130
% 4.60/1.52 Id : 6, {_}: multiply ?17 (add ?18 (add ?17 ?19)) =>= ?17 [19, 18, 17] by l2 ?17 ?18 ?19
% 4.60/1.52 Id : 3, {_}: add ?6 (multiply ?7 (multiply ?6 ?8)) =>= ?6 [8, 7, 6] by l1 ?6 ?7 ?8
% 4.60/1.52 Id : 35, {_}: add ?121 (multiply ?122 ?121) =>= ?121 [122, 121] by Super 3 with 6 at 2,2,2
% 4.60/1.52 Id : 42, {_}: multiply ?149 (add ?149 ?150) =>= ?149 [150, 149] by Super 37 with 4 at 2,2
% 4.60/1.52 Id : 1172, {_}: add (add ?1704 ?1705) ?1704 =>= add ?1704 ?1705 [1705, 1704] by Super 35 with 42 at 2,2
% 4.60/1.52 Id : 1197, {_}: add ?1704 (add ?1705 ?1704) =>= add ?1704 ?1705 [1705, 1704] by Demod 1172 with 11 at 2
% 4.60/1.52 Id : 19, {_}: add (multiply ?62 ?63) ?63 =>= ?63 [63, 62] by Super 18 with 3 at 1,2
% 4.60/1.52 Id : 39, {_}: multiply ?137 (add ?138 ?137) =>= ?137 [138, 137] by Super 37 with 3 at 2,2,2
% 4.60/1.52 Id : 758, {_}: add ?1224 (add ?1225 ?1224) =>= add ?1225 ?1224 [1225, 1224] by Super 19 with 39 at 1,2
% 4.60/1.52 Id : 2108, {_}: add ?1705 ?1704 =?= add ?1704 ?1705 [1704, 1705] by Demod 1197 with 758 at 2
% 4.60/1.52 Id : 32, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) (add (multiply ?109 ?107) ?107) =<= multiply (add (add ?106 (add ?107 ?108)) ?109) (multiply (add ?109 ?107) (add ?107 (add ?106 (add ?107 ?108)))) [109, 108, 107, 106] by Super 2 with 6 at 2,2,2
% 4.60/1.52 Id : 4790, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) (add ?107 (multiply ?109 ?107)) =<= multiply (add (add ?106 (add ?107 ?108)) ?109) (multiply (add ?109 ?107) (add ?107 (add ?106 (add ?107 ?108)))) [109, 108, 107, 106] by Demod 32 with 2108 at 2,2
% 4.60/1.52 Id : 4791, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) (add ?107 (multiply ?109 ?107)) =<= multiply (add ?106 (add (add ?107 ?108) ?109)) (multiply (add ?109 ?107) (add ?107 (add ?106 (add ?107 ?108)))) [109, 108, 107, 106] by Demod 4790 with 11 at 1,3
% 4.60/1.52 Id : 325, {_}: add (multiply ?689 ?690) ?690 =>= ?690 [690, 689] by Super 18 with 3 at 1,2
% 4.60/1.52 Id : 326, {_}: add ?692 (add ?693 (add ?692 ?694)) =>= add ?693 (add ?692 ?694) [694, 693, 692] by Super 325 with 6 at 1,2
% 4.60/1.52 Id : 4792, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) (add ?107 (multiply ?109 ?107)) =<= multiply (add ?106 (add (add ?107 ?108) ?109)) (multiply (add ?109 ?107) (add ?106 (add ?107 ?108))) [109, 108, 107, 106] by Demod 4791 with 326 at 2,2,3
% 4.60/1.52 Id : 4793, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) ?107 =<= multiply (add ?106 (add (add ?107 ?108) ?109)) (multiply (add ?109 ?107) (add ?106 (add ?107 ?108))) [109, 108, 107, 106] by Demod 4792 with 35 at 2,2
% 4.60/1.52 Id : 4794, {_}: add (multiply (add ?106 (add ?107 ?108)) ?109) ?107 =<= multiply (add ?106 (add ?107 (add ?108 ?109))) (multiply (add ?109 ?107) (add ?106 (add ?107 ?108))) [109, 108, 107, 106] by Demod 4793 with 11 at 2,1,3
% 4.60/1.52 Id : 4819, {_}: add ?6174 (multiply (add ?6175 (add ?6174 ?6176)) ?6177) =<= multiply (add ?6175 (add ?6174 (add ?6176 ?6177))) (multiply (add ?6177 ?6174) (add ?6175 (add ?6174 ?6176))) [6177, 6176, 6175, 6174] by Demod 4794 with 2108 at 2
% 4.60/1.52 Id : 79, {_}: multiply n1 ?15 =>= ?15 [15] by Demod 5 with 9 at 1,2
% 4.60/1.52 Id : 329, {_}: add ?702 ?702 =>= ?702 [702] by Super 325 with 79 at 1,2
% 4.60/1.52 Id : 4851, {_}: add ?6338 (multiply (add (add ?6338 ?6339) (add ?6338 ?6339)) ?6340) =<= multiply (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340))) (multiply (add ?6340 ?6338) (add ?6338 ?6339)) [6340, 6339, 6338] by Super 4819 with 329 at 2,2,3
% 4.60/1.52 Id : 5162, {_}: add ?6338 (multiply (add ?6338 (add ?6339 (add ?6338 ?6339))) ?6340) =<= multiply (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340))) (multiply (add ?6340 ?6338) (add ?6338 ?6339)) [6340, 6339, 6338] by Demod 4851 with 11 at 1,2,2
% 4.60/1.52 Id : 1245, {_}: multiply (add ?1827 ?1828) ?1828 =>= ?1828 [1828, 1827] by Super 52 with 6 at 1,2
% 4.60/1.52 Id : 1252, {_}: multiply ?1849 (multiply ?1850 ?1849) =>= multiply ?1850 ?1849 [1850, 1849] by Super 1245 with 35 at 1,2
% 4.60/1.52 Id : 760, {_}: multiply ?1230 (add ?1231 ?1230) =>= ?1230 [1231, 1230] by Super 37 with 3 at 2,2,2
% 4.60/1.52 Id : 22, {_}: add ?71 (multiply ?71 ?72) =>= ?71 [72, 71] by Super 3 with 5 at 2,2
% 4.60/1.52 Id : 766, {_}: multiply (multiply ?1249 ?1250) ?1249 =>= multiply ?1249 ?1250 [1250, 1249] by Super 760 with 22 at 2,2
% 4.60/1.52 Id : 793, {_}: multiply ?1249 (multiply ?1250 ?1249) =>= multiply ?1249 ?1250 [1250, 1249] by Demod 766 with 12 at 2
% 4.60/1.52 Id : 2239, {_}: multiply ?1849 ?1850 =?= multiply ?1850 ?1849 [1850, 1849] by Demod 1252 with 793 at 2
% 4.60/1.52 Id : 5163, {_}: add ?6338 (multiply (add ?6338 (add ?6339 (add ?6338 ?6339))) ?6340) =<= multiply (multiply (add ?6340 ?6338) (add ?6338 ?6339)) (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340))) [6340, 6339, 6338] by Demod 5162 with 2239 at 3
% 4.60/1.52 Id : 5164, {_}: add ?6338 (multiply (add ?6339 (add ?6338 ?6339)) ?6340) =<= multiply (multiply (add ?6340 ?6338) (add ?6338 ?6339)) (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340))) [6340, 6339, 6338] by Demod 5163 with 326 at 1,2,2
% 4.60/1.52 Id : 5165, {_}: add ?6338 (multiply (add ?6339 (add ?6338 ?6339)) ?6340) =<= multiply (add ?6340 ?6338) (multiply (add ?6338 ?6339) (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340)))) [6340, 6339, 6338] by Demod 5164 with 12 at 3
% 4.60/1.52 Id : 5166, {_}: add ?6338 (multiply (add ?6338 ?6339) ?6340) =<= multiply (add ?6340 ?6338) (multiply (add ?6338 ?6339) (add (add ?6338 ?6339) (add ?6338 (add ?6339 ?6340)))) [6340, 6339, 6338] by Demod 5165 with 758 at 1,2,2
% 4.60/1.52 Id : 12053, {_}: add ?16330 (multiply (add ?16330 ?16331) ?16332) =>= multiply (add ?16332 ?16330) (add ?16330 ?16331) [16332, 16331, 16330] by Demod 5166 with 42 at 2,3
% 4.60/1.52 Id : 14215, {_}: add ?19129 (multiply (add ?19130 ?19129) ?19131) =>= multiply (add ?19131 ?19129) (add ?19129 ?19130) [19131, 19130, 19129] by Super 12053 with 2108 at 1,2,2
% 4.60/1.52 Id : 15663, {_}: add ?20969 (multiply ?20970 (add ?20971 ?20969)) =>= multiply (add ?20970 ?20969) (add ?20969 ?20971) [20971, 20970, 20969] by Super 14215 with 2239 at 2,2
% 4.60/1.52 Id : 15669, {_}: add (multiply ?20995 ?20996) (multiply ?20997 ?20996) =<= multiply (add ?20997 (multiply ?20995 ?20996)) (add (multiply ?20995 ?20996) ?20996) [20997, 20996, 20995] by Super 15663 with 35 at 2,2,2
% 4.60/1.52 Id : 12066, {_}: add ?16380 (multiply (add ?16381 ?16380) ?16382) =<= multiply (add ?16382 ?16380) (add ?16380 (add ?16381 ?16380)) [16382, 16381, 16380] by Super 12053 with 758 at 1,2,2
% 4.60/1.52 Id : 12224, {_}: add ?16380 (multiply (add ?16381 ?16380) ?16382) =>= multiply (add ?16382 ?16380) (add ?16381 ?16380) [16382, 16381, 16380] by Demod 12066 with 758 at 2,3
% 4.60/1.52 Id : 12070, {_}: add ?16398 (multiply (add ?16399 ?16398) ?16400) =>= multiply (add ?16400 ?16398) (add ?16398 ?16399) [16400, 16399, 16398] by Super 12053 with 2108 at 1,2,2
% 4.60/1.52 Id : 14941, {_}: multiply (add ?16382 ?16380) (add ?16380 ?16381) =?= multiply (add ?16382 ?16380) (add ?16381 ?16380) [16381, 16380, 16382] by Demod 12224 with 12070 at 2
% 4.60/1.52 Id : 15851, {_}: add (multiply ?20995 ?20996) (multiply ?20997 ?20996) =<= multiply (add ?20997 (multiply ?20995 ?20996)) (add ?20996 (multiply ?20995 ?20996)) [20997, 20996, 20995] by Demod 15669 with 14941 at 3
% 4.60/1.52 Id : 15852, {_}: add (multiply ?20995 ?20996) (multiply ?20997 ?20996) =>= multiply (add ?20997 (multiply ?20995 ?20996)) ?20996 [20997, 20996, 20995] by Demod 15851 with 35 at 2,3
% 4.60/1.52 Id : 15853, {_}: add (multiply ?20995 ?20996) (multiply ?20997 ?20996) =>= multiply ?20996 (add ?20997 (multiply ?20995 ?20996)) [20997, 20996, 20995] by Demod 15852 with 2239 at 3
% 4.60/1.52 Id : 14220, {_}: add (multiply ?19151 ?19152) (multiply ?19151 ?19153) =<= multiply (add ?19153 (multiply ?19151 ?19152)) (add (multiply ?19151 ?19152) ?19151) [19153, 19152, 19151] by Super 14215 with 22 at 1,2,2
% 4.60/1.52 Id : 14386, {_}: add (multiply ?19151 ?19152) (multiply ?19151 ?19153) =<= multiply (add ?19153 (multiply ?19151 ?19152)) (add ?19151 (multiply ?19151 ?19152)) [19153, 19152, 19151] by Demod 14220 with 2108 at 2,3
% 4.60/1.52 Id : 14387, {_}: add (multiply ?19151 ?19152) (multiply ?19151 ?19153) =>= multiply (add ?19153 (multiply ?19151 ?19152)) ?19151 [19153, 19152, 19151] by Demod 14386 with 22 at 2,3
% 4.60/1.52 Id : 16090, {_}: add (multiply ?21437 ?21438) (multiply ?21437 ?21439) =>= multiply ?21437 (add ?21439 (multiply ?21437 ?21438)) [21439, 21438, 21437] by Demod 14387 with 2239 at 3
% 4.60/1.52 Id : 16141, {_}: add (multiply ?21653 ?21654) (multiply ?21654 ?21655) =>= multiply ?21654 (add ?21655 (multiply ?21654 ?21653)) [21655, 21654, 21653] by Super 16090 with 2239 at 1,2
% 4.60/1.52 Id : 14221, {_}: add (multiply ?19155 ?19156) (multiply ?19156 ?19157) =<= multiply (add ?19157 (multiply ?19155 ?19156)) (add (multiply ?19155 ?19156) ?19156) [19157, 19156, 19155] by Super 14215 with 35 at 1,2,2
% 4.60/1.52 Id : 14389, {_}: add (multiply ?19155 ?19156) (multiply ?19156 ?19157) =<= multiply (add ?19157 (multiply ?19155 ?19156)) (add ?19156 (multiply ?19155 ?19156)) [19157, 19156, 19155] by Demod 14221 with 2108 at 2,3
% 4.60/1.52 Id : 14390, {_}: add (multiply ?19155 ?19156) (multiply ?19156 ?19157) =>= multiply (add ?19157 (multiply ?19155 ?19156)) ?19156 [19157, 19156, 19155] by Demod 14389 with 35 at 2,3
% 4.60/1.52 Id : 14391, {_}: add (multiply ?19155 ?19156) (multiply ?19156 ?19157) =>= multiply ?19156 (add ?19157 (multiply ?19155 ?19156)) [19157, 19156, 19155] by Demod 14390 with 2239 at 3
% 4.60/1.52 Id : 18391, {_}: multiply ?21654 (add ?21655 (multiply ?21653 ?21654)) =?= multiply ?21654 (add ?21655 (multiply ?21654 ?21653)) [21653, 21655, 21654] by Demod 16141 with 14391 at 2
% 4.60/1.52 Id : 14263, {_}: add ?19335 (multiply ?19336 (add ?19337 ?19335)) =>= multiply (add ?19336 ?19335) (add ?19335 ?19337) [19337, 19336, 19335] by Super 14215 with 2239 at 2,2
% 4.60/1.52 Id : 17048, {_}: add (multiply ?22728 ?22729) (multiply ?22730 ?22728) =>= multiply ?22728 (add ?22729 (multiply ?22730 ?22728)) [22730, 22729, 22728] by Super 2108 with 14391 at 3
% 4.60/1.52 Id : 15668, {_}: add (multiply ?20991 ?20992) (multiply ?20993 ?20991) =<= multiply (add ?20993 (multiply ?20991 ?20992)) (add (multiply ?20991 ?20992) ?20991) [20993, 20992, 20991] by Super 15663 with 22 at 2,2,2
% 4.60/1.52 Id : 15848, {_}: add (multiply ?20991 ?20992) (multiply ?20993 ?20991) =<= multiply (add ?20993 (multiply ?20991 ?20992)) (add ?20991 (multiply ?20991 ?20992)) [20993, 20992, 20991] by Demod 15668 with 14941 at 3
% 4.60/1.52 Id : 15849, {_}: add (multiply ?20991 ?20992) (multiply ?20993 ?20991) =>= multiply (add ?20993 (multiply ?20991 ?20992)) ?20991 [20993, 20992, 20991] by Demod 15848 with 22 at 2,3
% 4.60/1.52 Id : 15850, {_}: add (multiply ?20991 ?20992) (multiply ?20993 ?20991) =>= multiply ?20991 (add ?20993 (multiply ?20991 ?20992)) [20993, 20992, 20991] by Demod 15849 with 2239 at 3
% 4.60/1.52 Id : 18976, {_}: multiply ?22728 (add ?22730 (multiply ?22728 ?22729)) =?= multiply ?22728 (add ?22729 (multiply ?22730 ?22728)) [22729, 22730, 22728] by Demod 17048 with 15850 at 2
% 4.60/1.52 Id : 19065, {_}: add (multiply ?25546 ?25547) (multiply ?25546 (add ?25547 (multiply ?25548 ?25546))) =>= multiply (add ?25546 (multiply ?25546 ?25547)) (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Super 14263 with 18976 at 2,2
% 4.60/1.52 Id : 14388, {_}: add (multiply ?19151 ?19152) (multiply ?19151 ?19153) =>= multiply ?19151 (add ?19153 (multiply ?19151 ?19152)) [19153, 19152, 19151] by Demod 14387 with 2239 at 3
% 4.60/1.52 Id : 19214, {_}: multiply ?25546 (add (add ?25547 (multiply ?25548 ?25546)) (multiply ?25546 ?25547)) =<= multiply (add ?25546 (multiply ?25546 ?25547)) (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Demod 19065 with 14388 at 2
% 4.60/1.52 Id : 19215, {_}: multiply ?25546 (add (add ?25547 (multiply ?25548 ?25546)) (multiply ?25546 ?25547)) =>= multiply ?25546 (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Demod 19214 with 22 at 1,3
% 4.60/1.52 Id : 19216, {_}: multiply ?25546 (add ?25547 (multiply (add ?25547 (multiply ?25548 ?25546)) ?25546)) =>= multiply ?25546 (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Demod 19215 with 18976 at 2
% 4.60/1.52 Id : 19217, {_}: multiply ?25546 (add ?25547 (multiply ?25546 (add ?25547 (multiply ?25548 ?25546)))) =>= multiply ?25546 (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Demod 19216 with 18391 at 2
% 4.60/1.52 Id : 12104, {_}: add ?16549 (multiply ?16550 (add ?16549 ?16551)) =>= multiply (add ?16550 ?16549) (add ?16549 ?16551) [16551, 16550, 16549] by Super 12053 with 2239 at 2,2
% 4.60/1.52 Id : 19218, {_}: multiply ?25546 (multiply (add ?25546 ?25547) (add ?25547 (multiply ?25548 ?25546))) =>= multiply ?25546 (add (multiply ?25546 ?25547) ?25548) [25548, 25547, 25546] by Demod 19217 with 12104 at 2,2
% 4.60/1.52 Id : 1169, {_}: multiply ?1693 ?1694 =<= multiply ?1693 (multiply (add ?1693 ?1695) ?1694) [1695, 1694, 1693] by Super 12 with 42 at 1,2
% 4.60/1.52 Id : 20218, {_}: multiply ?27026 (add ?27027 (multiply ?27028 ?27026)) =<= multiply ?27026 (add (multiply ?27026 ?27027) ?27028) [27028, 27027, 27026] by Demod 19218 with 1169 at 2
% 4.60/1.52 Id : 17014, {_}: add (multiply ?2 ?3) (multiply ?4 (add ?2 (multiply ?3 ?4))) =>= multiply (add ?2 ?3) (multiply (add ?3 ?4) (add ?4 ?2)) [4, 3, 2] by Demod 2 with 14391 at 2,2
% 4.60/1.52 Id : 20286, {_}: multiply ?27326 (add ?27327 (multiply (multiply ?27328 (add ?27326 (multiply ?27327 ?27328))) ?27326)) =>= multiply ?27326 (multiply (add ?27326 ?27327) (multiply (add ?27327 ?27328) (add ?27328 ?27326))) [27328, 27327, 27326] by Super 20218 with 17014 at 2,3
% 4.60/1.52 Id : 20603, {_}: multiply ?27326 (add ?27327 (multiply ?27326 (multiply ?27328 (add ?27326 (multiply ?27327 ?27328))))) =>= multiply ?27326 (multiply (add ?27326 ?27327) (multiply (add ?27327 ?27328) (add ?27328 ?27326))) [27328, 27327, 27326] by Demod 20286 with 18391 at 2
% 4.60/1.52 Id : 20604, {_}: multiply ?27326 (add ?27327 (multiply ?27326 (multiply ?27328 (add ?27326 (multiply ?27327 ?27328))))) =>= multiply ?27326 (multiply (add ?27327 ?27328) (add ?27328 ?27326)) [27328, 27327, 27326] by Demod 20603 with 1169 at 3
% 4.60/1.52 Id : 670, {_}: add ?1060 ?1061 =<= add ?1060 (add (multiply ?1060 ?1062) ?1061) [1062, 1061, 1060] by Super 11 with 22 at 1,2
% 4.60/1.52 Id : 4610, {_}: multiply (multiply ?5783 ?5784) (add ?5783 ?5785) =>= multiply ?5783 ?5784 [5785, 5784, 5783] by Super 6 with 670 at 2,2
% 4.60/1.52 Id : 4718, {_}: multiply ?5783 (multiply ?5784 (add ?5783 ?5785)) =>= multiply ?5783 ?5784 [5785, 5784, 5783] by Demod 4610 with 12 at 2
% 4.60/1.52 Id : 20605, {_}: multiply ?27326 (add ?27327 (multiply ?27326 ?27328)) =<= multiply ?27326 (multiply (add ?27327 ?27328) (add ?27328 ?27326)) [27328, 27327, 27326] by Demod 20604 with 4718 at 2,2,2
% 4.60/1.52 Id : 15, {_}: add (multiply (multiply (multiply ?48 ?49) ?50) ?48) (multiply ?48 ?49) =<= multiply (add (multiply (multiply ?48 ?49) ?50) ?48) (multiply (add ?48 ?49) (add ?49 (multiply (multiply ?48 ?49) ?50))) [50, 49, 48] by Super 2 with 3 at 2,2
% 4.60/1.52 Id : 163, {_}: add (multiply (multiply ?48 ?49) (multiply ?50 ?48)) (multiply ?48 ?49) =<= multiply (add (multiply (multiply ?48 ?49) ?50) ?48) (multiply (add ?48 ?49) (add ?49 (multiply (multiply ?48 ?49) ?50))) [50, 49, 48] by Demod 15 with 12 at 1,2
% 4.60/1.52 Id : 164, {_}: add (multiply (multiply ?48 ?49) (multiply ?50 ?48)) (multiply ?48 ?49) =<= multiply (add (multiply ?48 (multiply ?49 ?50)) ?48) (multiply (add ?48 ?49) (add ?49 (multiply (multiply ?48 ?49) ?50))) [50, 49, 48] by Demod 163 with 12 at 1,1,3
% 4.60/1.52 Id : 165, {_}: add (multiply (multiply ?48 ?49) (multiply ?50 ?48)) (multiply ?48 ?49) =<= multiply (add (multiply ?48 (multiply ?49 ?50)) ?48) (multiply (add ?48 ?49) (add ?49 (multiply ?48 (multiply ?49 ?50)))) [50, 49, 48] by Demod 164 with 12 at 2,2,2,3
% 4.60/1.52 Id : 166, {_}: add (multiply ?48 (multiply ?49 (multiply ?50 ?48))) (multiply ?48 ?49) =<= multiply (add (multiply ?48 (multiply ?49 ?50)) ?48) (multiply (add ?48 ?49) (add ?49 (multiply ?48 (multiply ?49 ?50)))) [50, 49, 48] by Demod 165 with 12 at 1,2
% 4.60/1.52 Id : 167, {_}: add (multiply ?48 (multiply ?49 (multiply ?50 ?48))) (multiply ?48 ?49) =<= multiply (add (multiply ?48 (multiply ?49 ?50)) ?48) (multiply (add ?48 ?49) ?49) [50, 49, 48] by Demod 166 with 3 at 2,2,3
% 4.60/1.52 Id : 130, {_}: multiply (add ?21 ?22) (multiply (add ?22 ?23) ?22) =>= ?22 [23, 22, 21] by Demod 7 with 12 at 2
% 4.60/1.52 Id : 89, {_}: n0 =<= inverse n1 [] by Super 79 with 10 at 2
% 4.60/1.52 Id : 243, {_}: add n1 n0 =>= n1 [] by Super 9 with 89 at 2,2
% 4.60/1.52 Id : 264, {_}: multiply n1 (add ?616 n1) =>= n1 [616] by Super 6 with 243 at 2,2,2
% 4.60/1.52 Id : 276, {_}: add ?616 n1 =>= n1 [616] by Demod 264 with 79 at 2
% 4.60/1.52 Id : 287, {_}: multiply ?632 (add ?633 n1) =>= ?632 [633, 632] by Super 6 with 276 at 2,2,2
% 4.60/1.52 Id : 305, {_}: multiply ?632 n1 =>= ?632 [632] by Demod 287 with 276 at 2,2
% 4.60/1.52 Id : 387, {_}: multiply (add ?766 n1) (add n1 ?767) =>= n1 [767, 766] by Super 130 with 305 at 2,2
% 4.60/1.52 Id : 421, {_}: multiply n1 (add n1 ?767) =>= n1 [767] by Demod 387 with 276 at 1,2
% 4.60/1.52 Id : 422, {_}: add n1 ?767 =>= n1 [767] by Demod 421 with 79 at 2
% 4.60/1.52 Id : 476, {_}: add (multiply n1 (multiply ?861 (multiply ?862 n1))) (multiply n1 ?861) =>= multiply (add (multiply n1 (multiply ?861 ?862)) n1) (multiply n1 ?861) [862, 861] by Super 167 with 422 at 1,2,3
% 4.60/1.52 Id : 487, {_}: add (multiply ?861 (multiply ?862 n1)) (multiply n1 ?861) =<= multiply (add (multiply n1 (multiply ?861 ?862)) n1) (multiply n1 ?861) [862, 861] by Demod 476 with 79 at 1,2
% 4.60/1.52 Id : 488, {_}: add (multiply ?861 (multiply ?862 n1)) ?861 =<= multiply (add (multiply n1 (multiply ?861 ?862)) n1) (multiply n1 ?861) [862, 861] by Demod 487 with 79 at 2,2
% 4.60/1.52 Id : 489, {_}: add (multiply ?861 (multiply ?862 n1)) ?861 =>= multiply n1 (multiply n1 ?861) [862, 861] by Demod 488 with 276 at 1,3
% 4.60/1.52 Id : 490, {_}: add (multiply ?861 (multiply ?862 n1)) ?861 =>= multiply n1 ?861 [862, 861] by Demod 489 with 79 at 2,3
% 4.60/1.52 Id : 491, {_}: add (multiply ?861 ?862) ?861 =>= multiply n1 ?861 [862, 861] by Demod 490 with 305 at 2,1,2
% 4.60/1.52 Id : 492, {_}: add (multiply ?861 ?862) ?861 =>= ?861 [862, 861] by Demod 491 with 79 at 3
% 4.60/1.52 Id : 1319, {_}: multiply (multiply ?1894 ?1895) (add ?1896 ?1894) =>= multiply ?1894 ?1895 [1896, 1895, 1894] by Super 6 with 492 at 2,2,2
% 4.60/1.52 Id : 1355, {_}: multiply ?1894 (multiply ?1895 (add ?1896 ?1894)) =>= multiply ?1894 ?1895 [1896, 1895, 1894] by Demod 1319 with 12 at 2
% 4.60/1.52 Id : 20606, {_}: multiply ?27326 (add ?27327 (multiply ?27326 ?27328)) =>= multiply ?27326 (add ?27327 ?27328) [27328, 27327, 27326] by Demod 20605 with 1355 at 3
% 4.60/1.52 Id : 20668, {_}: multiply ?21654 (add ?21655 (multiply ?21653 ?21654)) =>= multiply ?21654 (add ?21655 ?21653) [21653, 21655, 21654] by Demod 18391 with 20606 at 3
% 4.60/1.52 Id : 20673, {_}: add (multiply ?20995 ?20996) (multiply ?20997 ?20996) =>= multiply ?20996 (add ?20997 ?20995) [20997, 20996, 20995] by Demod 15853 with 20668 at 3
% 4.60/1.52 Id : 20988, {_}: multiply a (add c b) =?= multiply a (add c b) [] by Demod 20987 with 2108 at 2,3
% 4.60/1.52 Id : 20987, {_}: multiply a (add c b) =?= multiply a (add b c) [] by Demod 20986 with 20673 at 3
% 4.60/1.52 Id : 20986, {_}: multiply a (add c b) =<= add (multiply c a) (multiply b a) [] by Demod 20985 with 2108 at 3
% 4.60/1.52 Id : 20985, {_}: multiply a (add c b) =<= add (multiply b a) (multiply c a) [] by Demod 1 with 2108 at 2,2
% 4.60/1.52 Id : 1, {_}: multiply a (add b c) =<= add (multiply b a) (multiply c a) [] by prove_multiply_add_property
% 4.60/1.52 % SZS output end CNFRefutation for theBenchmark.p
% 4.60/1.52 5502: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 1.183071 using kbo
%------------------------------------------------------------------------------