%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP434-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 : n013.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:16 EDT 2022
% Result : Unsatisfiable 1.30s 0.71s
% Output : CNFRefutation 1.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP434-1 : TPTP v8.1.0. Released v2.6.0.
% 0.07/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n013.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 : Mon Jun 13 21:40:59 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 13363: Facts:
% 0.12/0.34 13363: Id : 2, {_}:
% 0.12/0.34 inverse
% 0.12/0.34 (multiply
% 0.12/0.34 (multiply (multiply (inverse (multiply (multiply ?2 ?3) ?4)) ?2)
% 0.12/0.34 ?3) (multiply ?5 (inverse ?5)))
% 0.12/0.34 =>=
% 0.12/0.34 ?4
% 0.12/0.34 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
% 0.12/0.34 13363: Goal:
% 0.12/0.34 13363: Id : 1, {_}:
% 0.12/0.34 multiply (multiply (inverse b2) b2) a2 =>= a2
% 0.12/0.34 [] by prove_these_axioms_2
% 1.30/0.71 Statistics :
% 1.30/0.71 Max weight : 41
% 1.30/0.71 Found proof, 0.372003s
% 1.30/0.71 % SZS status Unsatisfiable for theBenchmark.p
% 1.30/0.71 % SZS output start CNFRefutation for theBenchmark.p
% 1.30/0.71 Id : 3, {_}: inverse (multiply (multiply (multiply (inverse (multiply (multiply ?7 ?8) ?9)) ?7) ?8) (multiply ?10 (inverse ?10))) =>= ?9 [10, 9, 8, 7] by single_axiom ?7 ?8 ?9 ?10
% 1.30/0.71 Id : 2, {_}: inverse (multiply (multiply (multiply (inverse (multiply (multiply ?2 ?3) ?4)) ?2) ?3) (multiply ?5 (inverse ?5))) =>= ?4 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
% 1.30/0.71 Id : 5, {_}: inverse (multiply (multiply (multiply ?20 (multiply (inverse (multiply (multiply ?21 ?22) ?20)) ?21)) ?22) (multiply ?23 (inverse ?23))) =?= multiply ?24 (inverse ?24) [24, 23, 22, 21, 20] by Super 3 with 2 at 1,1,1,1,2
% 1.30/0.71 Id : 45, {_}: inverse (multiply (multiply (multiply (inverse (inverse (multiply (multiply (multiply ?402 (multiply (inverse (multiply (multiply ?403 ?404) ?402)) ?403)) ?404) (multiply ?405 (inverse ?405))))) ?406) ?407) (multiply ?408 (inverse ?408))) =>= inverse (multiply ?406 ?407) [408, 407, 406, 405, 404, 403, 402] by Super 2 with 5 at 1,1,1,1,1,2
% 1.30/0.71 Id : 85, {_}: inverse (multiply (multiply (multiply (inverse (multiply ?809 (inverse ?809))) ?810) ?811) (multiply ?812 (inverse ?812))) =>= inverse (multiply ?810 ?811) [812, 811, 810, 809] by Super 45 with 5 at 1,1,1,1,1,2
% 1.30/0.71 Id : 136, {_}: multiply ?1227 (inverse ?1227) =?= inverse (multiply (multiply (inverse (multiply (multiply ?1228 ?1229) (inverse (multiply ?1230 (inverse ?1230))))) ?1228) ?1229) [1230, 1229, 1228, 1227] by Super 85 with 5 at 2
% 1.30/0.71 Id : 105, {_}: multiply ?977 (inverse ?977) =?= inverse (multiply (multiply (inverse (multiply (multiply ?978 ?979) (inverse (multiply ?980 (inverse ?980))))) ?978) ?979) [980, 979, 978, 977] by Super 85 with 5 at 2
% 1.30/0.71 Id : 153, {_}: multiply ?1361 (inverse ?1361) =?= multiply ?1362 (inverse ?1362) [1362, 1361] by Super 136 with 105 at 3
% 1.30/0.71 Id : 189, {_}: inverse (multiply (multiply (multiply (inverse (multiply (multiply ?1574 (inverse ?1574)) ?1575)) ?1576) (inverse ?1576)) (multiply ?1577 (inverse ?1577))) =>= ?1575 [1577, 1576, 1575, 1574] by Super 2 with 153 at 1,1,1,1,1,1,2
% 1.30/0.71 Id : 213, {_}: multiply ?1734 (inverse ?1734) =?= inverse (multiply (multiply (inverse (multiply ?1735 (inverse ?1735))) ?1736) (inverse ?1736)) [1736, 1735, 1734] by Super 105 with 153 at 1,1,1,1,3
% 1.30/0.71 Id : 1364, {_}: inverse (multiply (multiply (multiply (multiply ?8356 (inverse ?8356)) (inverse (multiply ?8357 (inverse ?8357)))) ?8358) (multiply ?8359 (inverse ?8359))) =>= inverse ?8358 [8359, 8358, 8357, 8356] by Super 2 with 213 at 1,1,1,1,2
% 1.30/0.71 Id : 1446, {_}: inverse (multiply (multiply (multiply ?8937 (inverse ?8937)) ?8938) (multiply ?8939 (inverse ?8939))) =>= inverse ?8938 [8939, 8938, 8937] by Super 1364 with 153 at 1,1,1,2
% 1.30/0.71 Id : 1493, {_}: inverse (inverse (inverse (inverse (multiply (multiply ?9111 (inverse ?9111)) ?9112)))) =>= ?9112 [9112, 9111] by Super 189 with 1446 at 2
% 1.30/0.71 Id : 1768, {_}: inverse (inverse (inverse (inverse (multiply (multiply ?10497 (inverse ?10497)) ?10498)))) =>= ?10498 [10498, 10497] by Super 189 with 1446 at 2
% 1.30/0.71 Id : 285, {_}: inverse (multiply (multiply (multiply (multiply ?2106 (inverse ?2106)) (inverse (multiply ?2107 (inverse ?2107)))) ?2108) (multiply ?2109 (inverse ?2109))) =>= inverse ?2108 [2109, 2108, 2107, 2106] by Super 2 with 213 at 1,1,1,1,2
% 1.30/0.71 Id : 1808, {_}: inverse (inverse (inverse (inverse (inverse (multiply (multiply ?10694 (inverse ?10694)) (inverse (multiply ?10695 (inverse ?10695)))))))) =?= multiply ?10696 (inverse ?10696) [10696, 10695, 10694] by Super 1768 with 285 at 1,1,1,2
% 1.30/0.71 Id : 1824, {_}: inverse (inverse (multiply ?10695 (inverse ?10695))) =?= multiply ?10696 (inverse ?10696) [10696, 10695] by Demod 1808 with 1493 at 1,2
% 1.30/0.71 Id : 1940, {_}: inverse (inverse (inverse (inverse (multiply (inverse (inverse (multiply ?11291 (inverse ?11291)))) ?11292)))) =>= ?11292 [11292, 11291] by Super 1493 with 1824 at 1,1,1,1,1,2
% 1.30/0.71 Id : 66, {_}: inverse (multiply (multiply (multiply (inverse (multiply ?644 (inverse ?644))) ?645) ?646) (multiply ?647 (inverse ?647))) =>= inverse (multiply ?645 ?646) [647, 646, 645, 644] by Super 45 with 5 at 1,1,1,1,1,2
% 1.30/0.71 Id : 1512, {_}: inverse ?9246 =<= inverse (multiply (inverse (inverse (multiply ?9247 (inverse ?9247)))) ?9246) [9247, 9246] by Super 66 with 1446 at 2
% 1.30/0.71 Id : 2004, {_}: inverse (inverse (inverse (inverse ?11292))) =>= ?11292 [11292] by Demod 1940 with 1512 at 1,1,1,2
% 1.30/0.71 Id : 2024, {_}: multiply (multiply ?9111 (inverse ?9111)) ?9112 =>= ?9112 [9112, 9111] by Demod 1493 with 2004 at 2
% 1.30/0.71 Id : 2025, {_}: inverse (multiply ?8938 (multiply ?8939 (inverse ?8939))) =>= inverse ?8938 [8939, 8938] by Demod 1446 with 2024 at 1,1,2
% 1.30/0.71 Id : 2034, {_}: inverse (multiply (multiply (inverse (multiply (multiply ?2 ?3) ?4)) ?2) ?3) =>= ?4 [4, 3, 2] by Demod 2 with 2025 at 2
% 1.30/0.71 Id : 2062, {_}: inverse (inverse (inverse (inverse ?11667))) =>= ?11667 [11667] by Demod 1940 with 1512 at 1,1,1,2
% 1.30/0.71 Id : 2066, {_}: inverse (inverse (inverse (inverse ?11677))) =<= multiply ?11677 (multiply ?11678 (inverse ?11678)) [11678, 11677] by Super 2062 with 2025 at 1,1,1,2
% 1.30/0.71 Id : 2084, {_}: ?11677 =<= multiply ?11677 (multiply ?11678 (inverse ?11678)) [11678, 11677] by Demod 2066 with 2004 at 2
% 1.30/0.71 Id : 2093, {_}: inverse (multiply (multiply (inverse (multiply ?11732 ?11733)) ?11732) (multiply ?11734 (inverse ?11734))) =>= ?11733 [11734, 11733, 11732] by Super 2034 with 2084 at 1,1,1,1,1,2
% 1.30/0.71 Id : 2371, {_}: inverse (multiply (inverse (multiply ?12486 ?12487)) ?12486) =>= ?12487 [12487, 12486] by Demod 2093 with 2084 at 1,2
% 1.30/0.71 Id : 2373, {_}: inverse (multiply (inverse ?12492) (multiply ?12493 (inverse ?12493))) =>= ?12492 [12493, 12492] by Super 2371 with 2024 at 1,1,1,2
% 1.30/0.71 Id : 2394, {_}: inverse (inverse ?12492) =>= ?12492 [12492] by Demod 2373 with 2084 at 1,2
% 1.30/0.71 Id : 2419, {_}: multiply (multiply (inverse ?12586) ?12586) ?12587 =>= ?12587 [12587, 12586] by Super 2024 with 2394 at 2,1,2
% 1.30/0.71 Id : 2540, {_}: a2 === a2 [] by Demod 1 with 2419 at 2
% 1.30/0.71 Id : 1, {_}: multiply (multiply (inverse b2) b2) a2 =>= a2 [] by prove_these_axioms_2
% 1.30/0.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.71 13366: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.373937 using nrkbo
%------------------------------------------------------------------------------