%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP563-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 : n014.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:47 EDT 2022
% Result : Unsatisfiable 2.25s 0.90s
% Output : CNFRefutation 2.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GRP563-1 : TPTP v8.1.0. Released v2.6.0.
% 0.08/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.14/0.34 % Computer : n014.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Mon Jun 13 17:28:52 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.14/0.35 6528: Facts:
% 0.14/0.35 6528: Id : 2, {_}:
% 0.14/0.35 divide (divide (divide ?2 (inverse ?3)) ?4) (divide ?2 ?4) =>= ?3
% 0.14/0.35 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.14/0.35 6528: Id : 3, {_}:
% 0.14/0.35 multiply ?6 ?7 =<= divide ?6 (inverse ?7)
% 0.14/0.35 [7, 6] by multiply ?6 ?7
% 0.14/0.35 6528: Goal:
% 0.14/0.35 6528: Id : 1, {_}:
% 0.14/0.35 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.14/0.35 [] by prove_these_axioms_3
% 2.25/0.90 Statistics :
% 2.25/0.90 Max weight : 22
% 2.25/0.90 Found proof, 0.551862s
% 2.25/0.90 % SZS status Unsatisfiable for theBenchmark.p
% 2.25/0.90 % SZS output start CNFRefutation for theBenchmark.p
% 2.25/0.90 Id : 4, {_}: divide (divide (divide ?9 (inverse ?10)) ?11) (divide ?9 ?11) =>= ?10 [11, 10, 9] by single_axiom ?9 ?10 ?11
% 2.25/0.90 Id : 3, {_}: multiply ?6 ?7 =<= divide ?6 (inverse ?7) [7, 6] by multiply ?6 ?7
% 2.25/0.90 Id : 2, {_}: divide (divide (divide ?2 (inverse ?3)) ?4) (divide ?2 ?4) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 2.25/0.90 Id : 8, {_}: divide (divide (multiply ?2 ?3) ?4) (divide ?2 ?4) =>= ?3 [4, 3, 2] by Demod 2 with 3 at 1,1,2
% 2.25/0.90 Id : 9, {_}: divide (divide (multiply ?24 ?25) (inverse ?26)) (multiply ?24 ?26) =>= ?25 [26, 25, 24] by Super 8 with 3 at 2,2
% 2.25/0.90 Id : 13, {_}: divide (multiply (multiply ?24 ?25) ?26) (multiply ?24 ?26) =>= ?25 [26, 25, 24] by Demod 9 with 3 at 1,2
% 2.25/0.90 Id : 29, {_}: divide ?89 (divide (multiply ?90 ?89) (multiply ?90 ?91)) =>= ?91 [91, 90, 89] by Super 8 with 13 at 1,2
% 2.25/0.90 Id : 5, {_}: divide (divide (divide (divide (divide ?13 (inverse ?14)) ?15) (inverse ?16)) (divide ?13 ?15)) ?14 =>= ?16 [16, 15, 14, 13] by Super 4 with 2 at 2,2
% 2.25/0.90 Id : 15, {_}: divide (divide (multiply (divide (divide ?13 (inverse ?14)) ?15) ?16) (divide ?13 ?15)) ?14 =>= ?16 [16, 15, 14, 13] by Demod 5 with 3 at 1,1,2
% 2.25/0.90 Id : 16, {_}: divide (divide (multiply (divide (multiply ?13 ?14) ?15) ?16) (divide ?13 ?15)) ?14 =>= ?16 [16, 15, 14, 13] by Demod 15 with 3 at 1,1,1,1,2
% 2.25/0.90 Id : 17, {_}: multiply (divide (multiply (divide (multiply ?38 (inverse ?39)) ?40) ?41) (divide ?38 ?40)) ?39 =>= ?41 [41, 40, 39, 38] by Super 3 with 16 at 3
% 2.25/0.90 Id : 48, {_}: divide (divide ?163 (divide (divide (multiply ?164 (inverse ?165)) ?166) (divide ?164 ?166))) ?163 =>= ?165 [166, 165, 164, 163] by Super 16 with 17 at 1,1,2
% 2.25/0.90 Id : 63, {_}: divide (divide ?163 (inverse ?165)) ?163 =>= ?165 [165, 163] by Demod 48 with 8 at 2,1,2
% 2.25/0.90 Id : 64, {_}: divide (multiply ?163 ?165) ?163 =>= ?165 [165, 163] by Demod 63 with 3 at 1,2
% 2.25/0.90 Id : 73, {_}: divide ?261 (divide ?262 ?262) =>= ?261 [262, 261] by Super 8 with 64 at 1,2
% 2.25/0.90 Id : 93, {_}: multiply (divide ?336 ?336) ?337 =>= ?337 [337, 336] by Super 64 with 73 at 2
% 2.25/0.90 Id : 161, {_}: divide ?568 (divide (multiply (divide ?569 ?569) ?568) ?570) =>= ?570 [570, 569, 568] by Super 29 with 93 at 2,2,2
% 2.25/0.90 Id : 186, {_}: divide ?643 (divide ?643 ?644) =>= ?644 [644, 643] by Demod 161 with 93 at 1,2,2
% 2.25/0.90 Id : 292, {_}: divide ?1133 (multiply ?1133 ?1134) =>= inverse ?1134 [1134, 1133] by Super 186 with 3 at 2,2
% 2.25/0.90 Id : 294, {_}: divide (divide ?1141 ?1141) ?1142 =>= inverse ?1142 [1142, 1141] by Super 292 with 93 at 2,2
% 2.25/0.90 Id : 366, {_}: divide (divide (multiply (divide ?1284 ?1284) ?1285) ?1286) (inverse ?1286) =>= ?1285 [1286, 1285, 1284] by Super 8 with 294 at 2,2
% 2.25/0.90 Id : 398, {_}: multiply (divide (multiply (divide ?1284 ?1284) ?1285) ?1286) ?1286 =>= ?1285 [1286, 1285, 1284] by Demod 366 with 3 at 2
% 2.25/0.90 Id : 540, {_}: multiply (divide ?1733 ?1734) ?1734 =>= ?1733 [1734, 1733] by Demod 398 with 93 at 1,1,2
% 2.25/0.90 Id : 548, {_}: multiply ?1771 ?1772 =?= multiply ?1772 ?1771 [1772, 1771] by Super 540 with 64 at 1,2
% 2.25/0.90 Id : 399, {_}: multiply (divide ?1285 ?1286) ?1286 =>= ?1285 [1286, 1285] by Demod 398 with 93 at 1,1,2
% 2.25/0.90 Id : 541, {_}: multiply ?1736 (divide ?1737 ?1738) =<= divide (multiply ?1737 ?1736) ?1738 [1738, 1737, 1736] by Super 540 with 8 at 1,2
% 2.25/0.90 Id : 924, {_}: multiply (multiply ?2495 (divide ?2496 ?2497)) ?2497 =>= multiply ?2496 ?2495 [2497, 2496, 2495] by Super 399 with 541 at 1,2
% 2.25/0.90 Id : 2785, {_}: multiply ?4916 (multiply ?4917 (divide ?4918 ?4916)) =>= multiply ?4918 ?4917 [4918, 4917, 4916] by Demod 924 with 548 at 2
% 2.25/0.90 Id : 2793, {_}: multiply ?4949 (multiply ?4950 (multiply ?4951 (divide ?4952 ?4949))) =>= multiply (multiply ?4952 ?4951) ?4950 [4952, 4951, 4950, 4949] by Super 2785 with 541 at 2,2,2
% 2.25/0.90 Id : 542, {_}: multiply ?1740 (multiply ?1741 ?1742) =<= multiply (multiply ?1741 ?1740) ?1742 [1742, 1741, 1740] by Super 540 with 13 at 1,2
% 2.25/0.90 Id : 2872, {_}: multiply ?4949 (multiply ?4950 (multiply ?4951 (divide ?4952 ?4949))) =>= multiply ?4951 (multiply ?4952 ?4950) [4952, 4951, 4950, 4949] by Demod 2793 with 542 at 3
% 2.25/0.90 Id : 2804, {_}: multiply ?4995 (multiply ?4996 (multiply ?4997 (divide ?4998 ?4995))) =>= multiply ?4998 (multiply ?4997 ?4996) [4998, 4997, 4996, 4995] by Super 2785 with 542 at 2,2
% 2.25/0.90 Id : 8471, {_}: multiply ?4952 (multiply ?4951 ?4950) =?= multiply ?4951 (multiply ?4952 ?4950) [4950, 4951, 4952] by Demod 2872 with 2804 at 2
% 2.25/0.90 Id : 8781, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 8780 with 548 at 2,2
% 2.25/0.90 Id : 8780, {_}: multiply a3 (multiply c3 b3) =?= multiply a3 (multiply b3 c3) [] by Demod 8779 with 8471 at 2
% 2.25/0.90 Id : 8779, {_}: multiply c3 (multiply a3 b3) =>= multiply a3 (multiply b3 c3) [] by Demod 1 with 548 at 2
% 2.25/0.90 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 2.25/0.90 % SZS output end CNFRefutation for theBenchmark.p
% 2.25/0.90 6529: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.55331 using kbo
%------------------------------------------------------------------------------