%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP543-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 10:30:43 EDT 2022
% Result : Unsatisfiable 7.40s 2.21s
% Output : CNFRefutation 7.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP543-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.33 % Computer : n015.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Mon Jun 13 17:09:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 14915: Facts:
% 0.13/0.34 14915: Id : 2, {_}:
% 0.13/0.34 divide (divide identity (divide (divide (divide ?2 ?3) ?4) ?2)) ?4
% 0.13/0.34 =>=
% 0.13/0.34 ?3
% 0.13/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.13/0.34 14915: Id : 3, {_}:
% 0.13/0.34 multiply ?6 ?7 =<= divide ?6 (divide identity ?7)
% 0.13/0.34 [7, 6] by multiply ?6 ?7
% 0.13/0.34 14915: Id : 4, {_}: inverse ?9 =<= divide identity ?9 [9] by inverse ?9
% 0.13/0.34 14915: Id : 5, {_}: identity =<= divide ?11 ?11 [11] by identity ?11
% 0.13/0.34 14915: Goal:
% 0.13/0.34 14915: Id : 1, {_}:
% 0.13/0.34 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.13/0.34 [] by prove_these_axioms_3
% 7.40/2.21 Statistics :
% 7.40/2.21 Max weight : 18
% 7.40/2.21 Found proof, 1.872306s
% 7.40/2.21 % SZS status Unsatisfiable for theBenchmark.p
% 7.40/2.21 % SZS output start CNFRefutation for theBenchmark.p
% 7.40/2.21 Id : 5, {_}: identity =<= divide ?11 ?11 [11] by identity ?11
% 7.40/2.21 Id : 2, {_}: divide (divide identity (divide (divide (divide ?2 ?3) ?4) ?2)) ?4 =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 7.40/2.21 Id : 6, {_}: divide (divide identity (divide (divide (divide ?13 ?14) ?15) ?13)) ?15 =>= ?14 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 7.40/2.21 Id : 4, {_}: inverse ?9 =<= divide identity ?9 [9] by inverse ?9
% 7.40/2.21 Id : 3, {_}: multiply ?6 ?7 =<= divide ?6 (divide identity ?7) [7, 6] by multiply ?6 ?7
% 7.40/2.21 Id : 21, {_}: multiply ?6 ?7 =<= divide ?6 (inverse ?7) [7, 6] by Demod 3 with 4 at 2,3
% 7.40/2.21 Id : 8, {_}: divide (divide identity (divide ?22 identity)) ?23 =<= divide (divide (divide ?24 ?22) ?23) ?24 [24, 23, 22] by Super 6 with 2 at 1,2,1,2
% 7.40/2.21 Id : 99, {_}: divide (inverse (divide ?213 identity)) ?214 =<= divide (divide (divide ?215 ?213) ?214) ?215 [215, 214, 213] by Demod 8 with 4 at 1,2
% 7.40/2.21 Id : 103, {_}: divide (inverse (divide ?229 identity)) ?230 =>= divide (divide identity ?230) ?229 [230, 229] by Super 99 with 5 at 1,1,3
% 7.40/2.21 Id : 115, {_}: divide (inverse (divide ?229 identity)) ?230 =>= divide (inverse ?230) ?229 [230, 229] by Demod 103 with 4 at 1,3
% 7.40/2.21 Id : 31, {_}: inverse identity =>= identity [] by Super 4 with 5 at 3
% 7.40/2.21 Id : 38, {_}: multiply ?83 identity =<= divide ?83 identity [83] by Super 21 with 31 at 2,3
% 7.40/2.21 Id : 22, {_}: divide (inverse (divide (divide (divide ?2 ?3) ?4) ?2)) ?4 =>= ?3 [4, 3, 2] by Demod 2 with 4 at 1,2
% 7.40/2.21 Id : 92, {_}: divide (inverse (divide ?22 identity)) ?23 =<= divide (divide (divide ?24 ?22) ?23) ?24 [24, 23, 22] by Demod 8 with 4 at 1,2
% 7.40/2.21 Id : 93, {_}: divide (inverse (divide (inverse (divide ?3 identity)) ?4)) ?4 =>= ?3 [4, 3] by Demod 22 with 92 at 1,1,2
% 7.40/2.21 Id : 120, {_}: divide (inverse (divide (inverse (multiply ?3 identity)) ?4)) ?4 =>= ?3 [4, 3] by Demod 93 with 38 at 1,1,1,1,2
% 7.40/2.21 Id : 102, {_}: divide (inverse (divide ?226 identity)) ?227 =<= divide (divide (inverse ?226) ?227) identity [227, 226] by Super 99 with 4 at 1,1,3
% 7.40/2.21 Id : 237, {_}: divide (inverse (multiply ?226 identity)) ?227 =<= divide (divide (inverse ?226) ?227) identity [227, 226] by Demod 102 with 38 at 1,1,2
% 7.40/2.21 Id : 238, {_}: divide (inverse (multiply ?226 identity)) ?227 =>= multiply (divide (inverse ?226) ?227) identity [227, 226] by Demod 237 with 38 at 3
% 7.40/2.21 Id : 241, {_}: divide (inverse (multiply (divide (inverse ?3) ?4) identity)) ?4 =>= ?3 [4, 3] by Demod 120 with 238 at 1,1,2
% 7.40/2.21 Id : 242, {_}: multiply (divide (inverse (divide (inverse ?3) ?4)) ?4) identity =>= ?3 [4, 3] by Demod 241 with 238 at 2
% 7.40/2.21 Id : 247, {_}: multiply (inverse (multiply ?391 identity)) identity =<= multiply (divide (inverse ?391) identity) identity [391] by Super 38 with 238 at 3
% 7.40/2.21 Id : 260, {_}: multiply (inverse (multiply ?391 identity)) identity =<= multiply (multiply (inverse ?391) identity) identity [391] by Demod 247 with 38 at 1,3
% 7.40/2.21 Id : 250, {_}: divide (inverse (multiply ?401 identity)) ?402 =>= multiply (divide (inverse ?401) ?402) identity [402, 401] by Demod 237 with 38 at 3
% 7.40/2.21 Id : 23, {_}: multiply identity ?57 =>= inverse (inverse ?57) [57] by Super 21 with 4 at 3
% 7.40/2.21 Id : 253, {_}: divide (inverse (inverse (inverse identity))) ?410 =>= multiply (divide (inverse identity) ?410) identity [410] by Super 250 with 23 at 1,1,2
% 7.40/2.21 Id : 268, {_}: divide (inverse (inverse identity)) ?410 =<= multiply (divide (inverse identity) ?410) identity [410] by Demod 253 with 31 at 1,1,1,2
% 7.40/2.21 Id : 269, {_}: divide (inverse (inverse identity)) ?410 =>= multiply (divide identity ?410) identity [410] by Demod 268 with 31 at 1,1,3
% 7.40/2.21 Id : 270, {_}: divide (inverse identity) ?410 =<= multiply (divide identity ?410) identity [410] by Demod 269 with 31 at 1,1,2
% 7.40/2.21 Id : 271, {_}: divide (inverse identity) ?410 =>= multiply (inverse ?410) identity [410] by Demod 270 with 4 at 1,3
% 7.40/2.21 Id : 272, {_}: divide identity ?410 =<= multiply (inverse ?410) identity [410] by Demod 271 with 31 at 1,2
% 7.40/2.21 Id : 273, {_}: inverse ?410 =<= multiply (inverse ?410) identity [410] by Demod 272 with 4 at 2
% 7.40/2.21 Id : 302, {_}: inverse (multiply ?391 identity) =<= multiply (multiply (inverse ?391) identity) identity [391] by Demod 260 with 273 at 2
% 7.40/2.21 Id : 303, {_}: inverse (multiply ?391 identity) =<= multiply (inverse ?391) identity [391] by Demod 302 with 273 at 1,3
% 7.40/2.21 Id : 304, {_}: inverse (multiply ?391 identity) =>= inverse ?391 [391] by Demod 303 with 273 at 3
% 7.40/2.21 Id : 305, {_}: divide (inverse ?226) ?227 =<= multiply (divide (inverse ?226) ?227) identity [227, 226] by Demod 238 with 304 at 1,2
% 7.40/2.21 Id : 307, {_}: divide (inverse (divide (inverse ?3) ?4)) ?4 =>= ?3 [4, 3] by Demod 242 with 305 at 2
% 7.40/2.21 Id : 315, {_}: divide (inverse (divide (inverse ?461) ?462)) ?462 =>= multiply ?461 identity [462, 461] by Super 307 with 304 at 1,1,1,2
% 7.40/2.21 Id : 324, {_}: ?461 =<= multiply ?461 identity [461] by Demod 315 with 307 at 2
% 7.40/2.21 Id : 341, {_}: ?83 =<= divide ?83 identity [83] by Demod 38 with 324 at 2
% 7.40/2.21 Id : 407, {_}: divide (inverse ?229) ?230 =?= divide (inverse ?230) ?229 [230, 229] by Demod 115 with 341 at 1,1,2
% 7.40/2.21 Id : 420, {_}: multiply (inverse ?601) ?602 =<= divide (inverse (inverse ?602)) ?601 [602, 601] by Super 21 with 407 at 3
% 7.40/2.21 Id : 412, {_}: divide (inverse ?4) (divide (inverse ?3) ?4) =>= ?3 [3, 4] by Demod 307 with 407 at 2
% 7.40/2.21 Id : 119, {_}: divide (inverse (multiply ?22 identity)) ?23 =<= divide (divide (divide ?24 ?22) ?23) ?24 [24, 23, 22] by Demod 92 with 38 at 1,1,2
% 7.40/2.21 Id : 30, {_}: multiply (inverse ?74) ?74 =>= identity [74] by Super 21 with 5 at 3
% 7.40/2.21 Id : 171, {_}: divide (inverse (divide (inverse identity) ?301)) ?301 =>= inverse identity [301] by Super 120 with 30 at 1,1,1,1,2
% 7.40/2.21 Id : 180, {_}: divide (inverse (divide identity ?301)) ?301 =>= inverse identity [301] by Demod 171 with 31 at 1,1,1,2
% 7.40/2.21 Id : 181, {_}: divide (inverse (divide identity ?301)) ?301 =>= identity [301] by Demod 180 with 31 at 3
% 7.40/2.21 Id : 182, {_}: divide (inverse (inverse ?301)) ?301 =>= identity [301] by Demod 181 with 4 at 1,1,2
% 7.40/2.21 Id : 191, {_}: divide (inverse (multiply ?311 identity)) ?312 =<= divide (divide identity ?312) (inverse (inverse ?311)) [312, 311] by Super 119 with 182 at 1,1,3
% 7.40/2.21 Id : 200, {_}: divide (inverse (multiply ?311 identity)) ?312 =>= multiply (divide identity ?312) (inverse ?311) [312, 311] by Demod 191 with 21 at 3
% 7.40/2.21 Id : 201, {_}: divide (inverse (multiply ?311 identity)) ?312 =>= multiply (inverse ?312) (inverse ?311) [312, 311] by Demod 200 with 4 at 1,3
% 7.40/2.21 Id : 550, {_}: divide (inverse ?775) ?776 =<= multiply (inverse ?776) (inverse ?775) [776, 775] by Demod 201 with 324 at 1,1,2
% 7.40/2.21 Id : 552, {_}: divide (inverse ?780) identity =>= multiply identity (inverse ?780) [780] by Super 550 with 31 at 1,3
% 7.40/2.21 Id : 565, {_}: inverse ?780 =<= multiply identity (inverse ?780) [780] by Demod 552 with 341 at 2
% 7.40/2.21 Id : 566, {_}: inverse ?780 =<= inverse (inverse (inverse ?780)) [780] by Demod 565 with 23 at 3
% 7.40/2.21 Id : 578, {_}: divide (inverse ?803) (divide (inverse ?804) ?803) =>= inverse (inverse ?804) [804, 803] by Super 412 with 566 at 1,2,2
% 7.40/2.21 Id : 610, {_}: ?804 =<= inverse (inverse ?804) [804] by Demod 578 with 412 at 2
% 7.40/2.21 Id : 661, {_}: multiply (inverse ?601) ?602 =>= divide ?602 ?601 [602, 601] by Demod 420 with 610 at 1,3
% 7.40/2.21 Id : 677, {_}: multiply ?966 ?967 =<= divide ?967 (inverse ?966) [967, 966] by Super 661 with 610 at 1,2
% 7.40/2.21 Id : 682, {_}: multiply ?966 ?967 =?= multiply ?967 ?966 [967, 966] by Demod 677 with 21 at 3
% 7.40/2.21 Id : 11, {_}: divide (divide identity (divide (multiply (divide ?32 ?33) ?34) ?32)) (divide identity ?34) =>= ?33 [34, 33, 32] by Super 2 with 3 at 1,2,1,2
% 7.40/2.21 Id : 18, {_}: multiply (divide identity (divide (multiply (divide ?32 ?33) ?34) ?32)) ?34 =>= ?33 [34, 33, 32] by Demod 11 with 3 at 2
% 7.40/2.21 Id : 622, {_}: multiply (inverse (divide (multiply (divide ?32 ?33) ?34) ?32)) ?34 =>= ?33 [34, 33, 32] by Demod 18 with 4 at 1,2
% 7.40/2.21 Id : 623, {_}: inverse (divide (multiply (divide ?847 ?848) identity) ?847) =>= ?848 [848, 847] by Super 324 with 622 at 3
% 7.40/2.21 Id : 836, {_}: inverse (divide (divide ?1217 ?1218) ?1217) =>= ?1218 [1218, 1217] by Demod 623 with 324 at 1,1,2
% 7.40/2.21 Id : 670, {_}: divide ?942 (divide (inverse ?943) (inverse ?942)) =>= ?943 [943, 942] by Super 412 with 610 at 1,2
% 7.40/2.21 Id : 689, {_}: divide ?942 (multiply (inverse ?943) ?942) =>= ?943 [943, 942] by Demod 670 with 21 at 2,2
% 7.40/2.21 Id : 690, {_}: divide ?942 (divide ?942 ?943) =>= ?943 [943, 942] by Demod 689 with 661 at 2,2
% 7.40/2.21 Id : 843, {_}: inverse (divide ?1242 ?1243) =>= divide ?1243 ?1242 [1243, 1242] by Super 836 with 690 at 1,1,2
% 7.40/2.21 Id : 872, {_}: multiply (divide ?1275 ?1276) ?1277 =<= divide ?1277 (divide ?1276 ?1275) [1277, 1276, 1275] by Super 661 with 843 at 1,2
% 7.40/2.21 Id : 671, {_}: multiply ?945 (inverse ?946) =>= divide ?945 ?946 [946, 945] by Super 21 with 610 at 2,3
% 7.40/2.21 Id : 871, {_}: multiply ?1271 (divide ?1272 ?1273) =<= divide ?1271 (divide ?1273 ?1272) [1273, 1272, 1271] by Super 671 with 843 at 2,2
% 7.40/2.21 Id : 1280, {_}: multiply (divide ?2015 ?2016) ?2017 =?= multiply ?2017 (divide ?2015 ?2016) [2017, 2016, 2015] by Demod 872 with 871 at 3
% 7.40/2.21 Id : 1286, {_}: multiply (divide ?2037 (inverse ?2038)) ?2039 =>= multiply ?2039 (multiply ?2037 ?2038) [2039, 2038, 2037] by Super 1280 with 21 at 2,3
% 7.40/2.21 Id : 1334, {_}: multiply (multiply ?2037 ?2038) ?2039 =?= multiply ?2039 (multiply ?2037 ?2038) [2039, 2038, 2037] by Demod 1286 with 21 at 1,2
% 7.40/2.21 Id : 1193, {_}: multiply ?942 (divide ?943 ?942) =>= ?943 [943, 942] by Demod 690 with 871 at 2
% 7.40/2.21 Id : 104, {_}: divide (inverse (divide (inverse ?232) identity)) ?233 =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Super 99 with 21 at 1,1,3
% 7.40/2.21 Id : 841, {_}: inverse (divide ?1235 (inverse ?1236)) =>= divide (inverse ?1235) ?1236 [1236, 1235] by Super 836 with 412 at 1,1,2
% 7.40/2.21 Id : 859, {_}: inverse (multiply ?1235 ?1236) =<= divide (inverse ?1235) ?1236 [1236, 1235] by Demod 841 with 21 at 1,2
% 7.40/2.21 Id : 2053, {_}: inverse (multiply (divide (inverse ?232) identity) ?233) =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Demod 104 with 859 at 2
% 7.40/2.21 Id : 1035, {_}: inverse (multiply ?229 ?230) =<= divide (inverse ?230) ?229 [230, 229] by Demod 407 with 859 at 2
% 7.40/2.21 Id : 1036, {_}: inverse (multiply ?229 ?230) =?= inverse (multiply ?230 ?229) [230, 229] by Demod 1035 with 859 at 3
% 7.40/2.21 Id : 873, {_}: divide (inverse ?1279) (divide ?1280 ?1281) =>= divide (divide ?1281 ?1280) ?1279 [1281, 1280, 1279] by Super 407 with 843 at 1,3
% 7.40/2.21 Id : 1528, {_}: inverse (multiply ?1279 (divide ?1280 ?1281)) =>= divide (divide ?1281 ?1280) ?1279 [1281, 1280, 1279] by Demod 873 with 859 at 2
% 7.40/2.21 Id : 1542, {_}: inverse (multiply (divide ?2352 ?2353) ?2354) =>= divide (divide ?2353 ?2352) ?2354 [2354, 2353, 2352] by Super 1036 with 1528 at 3
% 7.40/2.21 Id : 2054, {_}: divide (divide identity (inverse ?232)) ?233 =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Demod 2053 with 1542 at 2
% 7.40/2.21 Id : 2055, {_}: divide (inverse (inverse ?232)) ?233 =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Demod 2054 with 4 at 1,2
% 7.40/2.21 Id : 2056, {_}: inverse (multiply (inverse ?232) ?233) =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Demod 2055 with 859 at 2
% 7.40/2.21 Id : 2057, {_}: inverse (divide ?233 ?232) =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 232, 233] by Demod 2056 with 661 at 1,2
% 7.40/2.21 Id : 2058, {_}: divide ?232 ?233 =<= divide (divide (multiply ?234 ?232) ?233) ?234 [234, 233, 232] by Demod 2057 with 843 at 2
% 7.40/2.21 Id : 2066, {_}: multiply ?3167 (divide ?3168 ?3169) =<= divide (multiply ?3167 ?3168) ?3169 [3169, 3168, 3167] by Super 1193 with 2058 at 2,2
% 7.40/2.21 Id : 2182, {_}: multiply (multiply ?3345 ?3346) ?3347 =<= multiply ?3345 (divide ?3346 (inverse ?3347)) [3347, 3346, 3345] by Super 21 with 2066 at 3
% 7.40/2.21 Id : 2220, {_}: multiply (multiply ?3345 ?3346) ?3347 =>= multiply ?3345 (multiply ?3346 ?3347) [3347, 3346, 3345] by Demod 2182 with 21 at 2,3
% 7.40/2.21 Id : 15932, {_}: multiply ?2037 (multiply ?2038 ?2039) =?= multiply ?2039 (multiply ?2037 ?2038) [2039, 2038, 2037] by Demod 1334 with 2220 at 2
% 7.40/2.21 Id : 16459, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 16458 with 15932 at 2
% 7.40/2.21 Id : 16458, {_}: multiply b3 (multiply c3 a3) =>= multiply a3 (multiply b3 c3) [] by Demod 16457 with 15932 at 2
% 7.40/2.21 Id : 16457, {_}: multiply c3 (multiply a3 b3) =>= multiply a3 (multiply b3 c3) [] by Demod 1 with 682 at 2
% 7.40/2.21 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 7.40/2.21 % SZS output end CNFRefutation for theBenchmark.p
% 7.40/2.21 14916: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 1.873507 using kbo
%------------------------------------------------------------------------------