%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP592-1 : TPTP v8.1.0. Bugfixed v2.7.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:54 EDT 2022
% Result : Unsatisfiable 0.19s 0.43s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP592-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.06/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jun 14 12:16:36 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 19946: Facts:
% 0.12/0.34 19946: Id : 2, {_}:
% 0.12/0.34 double_divide
% 0.12/0.34 (inverse
% 0.12/0.34 (double_divide (double_divide ?2 ?3)
% 0.12/0.34 (inverse (double_divide ?2 (inverse ?4))))) ?3
% 0.12/0.34 =>=
% 0.12/0.34 ?4
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 19946: Id : 3, {_}:
% 0.12/0.34 multiply ?6 ?7 =<= inverse (double_divide ?7 ?6)
% 0.12/0.34 [7, 6] by multiply ?6 ?7
% 0.12/0.34 19946: Goal:
% 0.12/0.34 19946: Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.19/0.43 Statistics :
% 0.19/0.43 Max weight : 26
% 0.19/0.43 Found proof, 0.091092s
% 0.19/0.43 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.43 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.43 Id : 4, {_}: double_divide (inverse (double_divide (double_divide ?9 ?10) (inverse (double_divide ?9 (inverse ?11))))) ?10 =>= ?11 [11, 10, 9] by single_axiom ?9 ?10 ?11
% 0.19/0.43 Id : 11, {_}: multiply ?30 ?31 =<= inverse (double_divide ?31 ?30) [31, 30] by multiply ?30 ?31
% 0.19/0.43 Id : 3, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by multiply ?6 ?7
% 0.19/0.43 Id : 2, {_}: double_divide (inverse (double_divide (double_divide ?2 ?3) (inverse (double_divide ?2 (inverse ?4))))) ?3 =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.19/0.43 Id : 8, {_}: double_divide (multiply (inverse (double_divide ?2 (inverse ?4))) (double_divide ?2 ?3)) ?3 =>= ?4 [3, 4, 2] by Demod 2 with 3 at 1,2
% 0.19/0.43 Id : 9, {_}: double_divide (multiply (multiply (inverse ?4) ?2) (double_divide ?2 ?3)) ?3 =>= ?4 [3, 2, 4] by Demod 8 with 3 at 1,1,2
% 0.19/0.43 Id : 10, {_}: double_divide (multiply (multiply (multiply ?25 ?26) ?27) (double_divide ?27 ?28)) ?28 =>= double_divide ?26 ?25 [28, 27, 26, 25] by Super 9 with 3 at 1,1,1,2
% 0.19/0.43 Id : 165, {_}: multiply ?553 (multiply (multiply (inverse ?554) ?555) (double_divide ?555 ?553)) =>= inverse ?554 [555, 554, 553] by Super 11 with 9 at 1,3
% 0.19/0.43 Id : 5, {_}: double_divide (inverse (double_divide (double_divide (inverse (double_divide (double_divide ?13 (inverse ?14)) (inverse (double_divide ?13 (inverse ?15))))) ?16) (inverse ?15))) ?16 =>= ?14 [16, 15, 14, 13] by Super 4 with 2 at 1,2,1,1,2
% 0.19/0.43 Id : 14, {_}: double_divide (multiply (inverse ?15) (double_divide (inverse (double_divide (double_divide ?13 (inverse ?14)) (inverse (double_divide ?13 (inverse ?15))))) ?16)) ?16 =>= ?14 [16, 14, 13, 15] by Demod 5 with 3 at 1,2
% 0.19/0.43 Id : 15, {_}: double_divide (multiply (inverse ?15) (double_divide (multiply (inverse (double_divide ?13 (inverse ?15))) (double_divide ?13 (inverse ?14))) ?16)) ?16 =>= ?14 [16, 14, 13, 15] by Demod 14 with 3 at 1,2,1,2
% 0.19/0.43 Id : 19, {_}: double_divide (multiply (inverse ?51) (double_divide (multiply (multiply (inverse ?51) ?52) (double_divide ?52 (inverse ?53))) ?54)) ?54 =>= ?53 [54, 53, 52, 51] by Demod 15 with 3 at 1,1,2,1,2
% 0.19/0.43 Id : 24, {_}: double_divide (multiply (inverse ?81) ?81) (inverse ?82) =>= ?82 [82, 81] by Super 19 with 9 at 2,1,2
% 0.19/0.43 Id : 169, {_}: multiply (inverse ?574) (multiply (multiply (inverse ?575) (multiply (inverse ?576) ?576)) ?574) =>= inverse ?575 [576, 575, 574] by Super 165 with 24 at 2,2,2
% 0.19/0.43 Id : 30, {_}: multiply (inverse ?96) (multiply (inverse ?97) ?97) =>= inverse ?96 [97, 96] by Super 3 with 24 at 1,3
% 0.19/0.43 Id : 187, {_}: multiply (inverse ?574) (multiply (inverse ?575) ?574) =>= inverse ?575 [575, 574] by Demod 169 with 30 at 1,2,2
% 0.19/0.43 Id : 196, {_}: double_divide (multiply (multiply (inverse ?637) ?638) (double_divide ?638 ?639)) ?639 =?= double_divide (multiply (inverse ?637) ?640) (inverse ?640) [640, 639, 638, 637] by Super 10 with 187 at 1,1,1,2
% 0.19/0.43 Id : 210, {_}: ?637 =<= double_divide (multiply (inverse ?637) ?640) (inverse ?640) [640, 637] by Demod 196 with 9 at 2
% 0.19/0.43 Id : 199, {_}: multiply (inverse ?650) (multiply (inverse ?651) ?650) =>= inverse ?651 [651, 650] by Demod 169 with 30 at 1,2,2
% 0.19/0.43 Id : 204, {_}: multiply (inverse (multiply (inverse ?667) ?668)) (inverse ?667) =>= inverse ?668 [668, 667] by Super 199 with 187 at 2,2
% 0.19/0.43 Id : 340, {_}: multiply (inverse ?1092) ?1093 =<= double_divide (inverse ?1093) (inverse (inverse ?1092)) [1093, 1092] by Super 210 with 204 at 1,3
% 0.19/0.43 Id : 341, {_}: multiply (inverse (double_divide ?1095 ?1096)) ?1097 =<= double_divide (inverse ?1097) (inverse (multiply ?1096 ?1095)) [1097, 1096, 1095] by Super 340 with 3 at 1,2,3
% 0.19/0.43 Id : 348, {_}: multiply (multiply ?1096 ?1095) ?1097 =<= double_divide (inverse ?1097) (inverse (multiply ?1096 ?1095)) [1097, 1095, 1096] by Demod 341 with 3 at 1,2
% 0.19/0.43 Id : 342, {_}: multiply (inverse ?1099) (double_divide ?1100 ?1101) =<= double_divide (multiply ?1101 ?1100) (inverse (inverse ?1099)) [1101, 1100, 1099] by Super 340 with 3 at 1,3
% 0.19/0.43 Id : 401, {_}: multiply (inverse ?1222) (double_divide ?1223 (inverse ?1223)) =>= inverse ?1222 [1223, 1222] by Super 24 with 342 at 2
% 0.19/0.43 Id : 715, {_}: ?2139 =<= double_divide (inverse ?2139) (inverse (double_divide ?2140 (inverse ?2140))) [2140, 2139] by Super 210 with 401 at 1,3
% 0.19/0.43 Id : 779, {_}: ?2219 =<= double_divide (inverse ?2219) (multiply (inverse ?2220) ?2220) [2220, 2219] by Demod 715 with 3 at 2,3
% 0.19/0.43 Id : 783, {_}: ?2234 =<= double_divide (inverse ?2234) (inverse (multiply (inverse ?2235) ?2235)) [2235, 2234] by Super 779 with 30 at 2,3
% 0.19/0.43 Id : 791, {_}: ?2234 =<= multiply (multiply (inverse ?2235) ?2235) ?2234 [2235, 2234] by Demod 783 with 348 at 3
% 0.19/0.43 Id : 802, {_}: multiply (multiply (multiply (inverse ?2272) ?2272) ?2273) ?2274 =>= double_divide (inverse ?2274) (inverse ?2273) [2274, 2273, 2272] by Super 348 with 791 at 1,2,3
% 0.19/0.43 Id : 832, {_}: multiply ?2273 ?2274 =<= double_divide (inverse ?2274) (inverse ?2273) [2274, 2273] by Demod 802 with 791 at 1,2
% 0.19/0.43 Id : 1004, {_}: double_divide (double_divide ?2903 ?2904) ?2904 =>= ?2903 [2904, 2903] by Super 9 with 791 at 1,2
% 0.19/0.43 Id : 1014, {_}: double_divide ?2947 (inverse ?2948) =>= multiply (inverse ?2947) ?2948 [2948, 2947] by Super 1004 with 210 at 1,2
% 0.19/0.43 Id : 1020, {_}: multiply ?2273 ?2274 =<= multiply (inverse (inverse ?2274)) ?2273 [2274, 2273] by Demod 832 with 1014 at 3
% 0.19/0.43 Id : 1114, {_}: multiply (inverse ?3204) ?3205 =<= inverse (multiply (inverse ?3205) ?3204) [3205, 3204] by Super 3 with 1014 at 1,3
% 0.19/0.43 Id : 1119, {_}: multiply (inverse (multiply (inverse ?3224) ?3225)) ?3225 =>= inverse (inverse ?3224) [3225, 3224] by Super 1114 with 187 at 1,3
% 0.19/0.43 Id : 1045, {_}: multiply (inverse ?2995) ?2996 =<= inverse (multiply (inverse ?2996) ?2995) [2996, 2995] by Super 3 with 1014 at 1,3
% 0.19/0.43 Id : 1134, {_}: multiply (multiply (inverse ?3225) ?3224) ?3225 =>= inverse (inverse ?3224) [3224, 3225] by Demod 1119 with 1045 at 1,2
% 0.19/0.43 Id : 1022, {_}: ?637 =<= multiply (inverse (multiply (inverse ?637) ?640)) ?640 [640, 637] by Demod 210 with 1014 at 3
% 0.19/0.43 Id : 1083, {_}: ?637 =<= multiply (multiply (inverse ?640) ?637) ?640 [640, 637] by Demod 1022 with 1045 at 1,3
% 0.19/0.43 Id : 1135, {_}: ?3224 =<= inverse (inverse ?3224) [3224] by Demod 1134 with 1083 at 2
% 0.19/0.43 Id : 1144, {_}: multiply ?2273 ?2274 =?= multiply ?2274 ?2273 [2274, 2273] by Demod 1020 with 1135 at 1,3
% 0.19/0.43 Id : 1195, {_}: multiply a b === multiply a b [] by Demod 1 with 1144 at 3
% 0.19/0.43 Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.19/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.43 19946: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.094975 using nrkbo
% 0.19/0.43 Statistics :
% 0.19/0.43 Max weight : 39
% 0.19/0.43 Found proof, 0.094898s
% 0.19/0.43 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.43 % SZS output start CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------