%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : BOO068-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n032.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:19 EDT 2022
% Result : Unsatisfiable 0.15s 0.41s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : BOO068-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.10 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 600
% 0.11/0.30 % DateTime : Wed Jun 1 16:54:29 EDT 2022
% 0.11/0.30 % CPUTime :
% 0.11/0.30 26547: Facts:
% 0.11/0.30 26547: Id : 2, {_}:
% 0.11/0.30 multiply (multiply ?2 (inverse ?2) ?3)
% 0.11/0.30 (inverse (multiply (multiply ?4 ?5 ?6) ?7 (multiply ?4 ?5 ?8)))
% 0.11/0.30 (multiply ?5 (multiply ?8 ?7 ?6) ?4)
% 0.11/0.30 =>=
% 0.11/0.30 ?3
% 0.11/0.30 [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
% 0.11/0.30 26547: Goal:
% 0.11/0.30 26547: Id : 1, {_}: multiply b a a =>= a [] by prove_tba_axioms_2
% 0.15/0.41 Statistics :
% 0.15/0.41 Max weight : 63
% 0.15/0.41 Found proof, 0.111796s
% 0.15/0.41 % SZS status Unsatisfiable for theBenchmark.p
% 0.15/0.41 % SZS output start CNFRefutation for theBenchmark.p
% 0.15/0.41 Id : 3, {_}: multiply (multiply ?10 (inverse ?10) ?11) (inverse (multiply (multiply ?12 ?13 ?14) ?15 (multiply ?12 ?13 ?16))) (multiply ?13 (multiply ?16 ?15 ?14) ?12) =>= ?11 [16, 15, 14, 13, 12, 11, 10] by single_axiom ?10 ?11 ?12 ?13 ?14 ?15 ?16
% 0.15/0.42 Id : 2, {_}: multiply (multiply ?2 (inverse ?2) ?3) (inverse (multiply (multiply ?4 ?5 ?6) ?7 (multiply ?4 ?5 ?8))) (multiply ?5 (multiply ?8 ?7 ?6) ?4) =>= ?3 [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
% 0.15/0.42 Id : 7, {_}: multiply (multiply ?54 ?55 ?56) (inverse (multiply (multiply ?57 ?58 ?59) ?60 (multiply ?57 ?58 ?61))) (multiply ?58 (multiply ?61 ?60 ?59) ?57) =?= multiply ?55 (multiply ?56 (inverse (multiply ?54 ?55 ?62)) ?62) ?54 [62, 61, 60, 59, 58, 57, 56, 55, 54] by Super 3 with 2 at 1,2
% 0.15/0.42 Id : 19, {_}: multiply (inverse ?198) (multiply ?199 (inverse (multiply ?198 (inverse ?198) ?200)) ?200) ?198 =>= ?199 [200, 199, 198] by Super 2 with 7 at 2
% 0.15/0.42 Id : 53, {_}: multiply (multiply ?501 (inverse ?501) ?502) (inverse (multiply (multiply ?503 (inverse ?503) ?504) (inverse (multiply ?503 (inverse ?503) ?504)) (multiply ?503 (inverse ?503) ?505))) ?505 =>= ?502 [505, 504, 503, 502, 501] by Super 2 with 19 at 3,2
% 0.15/0.42 Id : 30, {_}: multiply (multiply ?340 (inverse ?340) ?341) (inverse (multiply (multiply ?342 (inverse ?342) ?343) (inverse (multiply ?342 (inverse ?342) ?343)) (multiply ?342 (inverse ?342) ?344))) ?344 =>= ?341 [344, 343, 342, 341, 340] by Super 2 with 19 at 3,2
% 0.15/0.42 Id : 87, {_}: multiply (multiply ?724 (inverse ?724) ?725) (inverse (multiply ?726 (inverse ?726) (multiply (multiply ?726 (inverse ?726) ?727) (inverse (multiply ?726 (inverse ?726) ?727)) ?728))) ?728 =>= ?725 [728, 727, 726, 725, 724] by Super 53 with 30 at 1,2,2
% 0.15/0.42 Id : 100, {_}: multiply (multiply ?821 ?822 ?823) (inverse (multiply ?824 (inverse ?824) (multiply (multiply ?824 (inverse ?824) ?825) (inverse (multiply ?824 (inverse ?824) ?825)) ?826))) ?826 =?= multiply ?822 (multiply ?823 (inverse (multiply ?821 ?822 ?827)) ?827) ?821 [827, 826, 825, 824, 823, 822, 821] by Super 87 with 2 at 1,2
% 0.15/0.42 Id : 29, {_}: multiply (multiply ?332 (inverse ?332) ?333) (inverse (multiply (multiply ?334 ?335 ?336) (multiply ?337 (inverse (multiply ?336 (inverse ?336) ?338)) ?338) (multiply ?334 ?335 (inverse ?336)))) (multiply ?335 ?337 ?334) =>= ?333 [338, 337, 336, 335, 334, 333, 332] by Super 2 with 19 at 2,3,2
% 0.15/0.42 Id : 376, {_}: multiply (multiply ?2952 (inverse ?2952) ?2953) (inverse ?2954) (multiply (inverse ?2955) (multiply ?2956 (inverse (multiply (multiply ?2956 ?2955 ?2957) (multiply (inverse ?2955) (inverse (multiply ?2957 (inverse ?2957) ?2958)) ?2958) (multiply ?2956 ?2955 (inverse ?2957)))) ?2954) ?2955) =>= ?2953 [2958, 2957, 2956, 2955, 2954, 2953, 2952] by Super 2 with 29 at 1,2,2
% 0.15/0.42 Id : 406, {_}: multiply (multiply ?3280 (inverse ?3280) ?3281) (inverse (multiply ?3282 (inverse ?3282) (multiply ?3283 (inverse ?3283) ?3284))) (multiply (inverse ?3282) ?3284 ?3282) =>= ?3281 [3284, 3283, 3282, 3281, 3280] by Super 376 with 29 at 2,3,2
% 0.15/0.42 Id : 130, {_}: multiply (multiply ?938 (inverse ?938) ?939) (inverse ?940) (multiply (inverse ?941) (multiply ?942 (inverse (multiply (multiply ?942 ?941 ?943) (multiply (inverse ?941) (inverse (multiply ?943 (inverse ?943) ?944)) ?944) (multiply ?942 ?941 (inverse ?943)))) ?940) ?941) =>= ?939 [944, 943, 942, 941, 940, 939, 938] by Super 2 with 29 at 1,2,2
% 0.15/0.42 Id : 457, {_}: multiply (multiply ?3597 (inverse ?3597) ?3598) (inverse ?3599) (multiply (inverse ?3600) (multiply ?3601 (inverse (multiply (multiply ?3601 ?3600 ?3602) (multiply (inverse ?3600) (inverse (multiply ?3602 (inverse ?3602) ?3603)) ?3603) (multiply ?3601 ?3600 (inverse ?3602)))) ?3599) ?3600) =?= multiply (inverse ?3604) ?3598 ?3604 [3604, 3603, 3602, 3601, 3600, 3599, 3598, 3597] by Super 130 with 406 at 1,2
% 0.15/0.42 Id : 485, {_}: ?3598 =<= multiply (inverse ?3604) ?3598 ?3604 [3604, 3598] by Demod 457 with 130 at 2
% 0.15/0.42 Id : 513, {_}: multiply (multiply ?3280 (inverse ?3280) ?3281) (inverse (multiply ?3282 (inverse ?3282) (multiply ?3283 (inverse ?3283) ?3284))) ?3284 =>= ?3281 [3284, 3283, 3282, 3281, 3280] by Demod 406 with 485 at 3,2
% 0.15/0.42 Id : 514, {_}: multiply ?199 (inverse (multiply ?198 (inverse ?198) ?200)) ?200 =>= ?199 [200, 198, 199] by Demod 19 with 485 at 2
% 0.15/0.42 Id : 550, {_}: multiply ?4028 (inverse (inverse (inverse ?4029))) ?4029 =>= ?4028 [4029, 4028] by Super 514 with 485 at 1,2,2
% 0.15/0.42 Id : 633, {_}: inverse (inverse (inverse ?4236)) =>= inverse ?4236 [4236] by Super 485 with 550 at 3
% 0.15/0.42 Id : 651, {_}: ?4320 =<= multiply (inverse ?4321) ?4320 (inverse (inverse ?4321)) [4321, 4320] by Super 485 with 633 at 1,3
% 0.15/0.42 Id : 729, {_}: multiply (multiply ?4713 (inverse ?4713) ?4714) (inverse (multiply ?4715 (inverse ?4715) (inverse (inverse ?4716)))) (inverse (inverse ?4716)) =>= ?4714 [4716, 4715, 4714, 4713] by Super 513 with 651 at 3,1,2,2
% 0.15/0.42 Id : 743, {_}: multiply ?4713 (inverse ?4713) ?4714 =>= ?4714 [4714, 4713] by Demod 729 with 514 at 2
% 0.15/0.42 Id : 760, {_}: multiply (multiply ?821 ?822 ?823) (inverse (multiply (multiply ?824 (inverse ?824) ?825) (inverse (multiply ?824 (inverse ?824) ?825)) ?826)) ?826 =?= multiply ?822 (multiply ?823 (inverse (multiply ?821 ?822 ?827)) ?827) ?821 [827, 826, 825, 824, 823, 822, 821] by Demod 100 with 743 at 1,2,2
% 0.15/0.42 Id : 761, {_}: multiply (multiply ?821 ?822 ?823) (inverse ?826) ?826 =?= multiply ?822 (multiply ?823 (inverse (multiply ?821 ?822 ?827)) ?827) ?821 [827, 826, 823, 822, 821] by Demod 760 with 743 at 1,2,2
% 0.15/0.42 Id : 638, {_}: multiply ?4028 (inverse ?4029) ?4029 =>= ?4028 [4029, 4028] by Demod 550 with 633 at 2,2
% 0.15/0.42 Id : 767, {_}: multiply ?821 ?822 ?823 =<= multiply ?822 (multiply ?823 (inverse (multiply ?821 ?822 ?827)) ?827) ?821 [827, 823, 822, 821] by Demod 761 with 638 at 2
% 0.15/0.42 Id : 964, {_}: multiply ?5270 ?5271 (multiply ?5270 ?5271 ?5272) =>= multiply ?5271 ?5272 ?5270 [5272, 5271, 5270] by Super 767 with 743 at 2,3
% 0.15/0.42 Id : 783, {_}: inverse (inverse ?4813) =>= ?4813 [4813] by Super 485 with 743 at 3
% 0.15/0.42 Id : 822, {_}: ?4887 =<= multiply ?4888 ?4887 (inverse ?4888) [4888, 4887] by Super 485 with 783 at 1,3
% 0.15/0.42 Id : 975, {_}: multiply ?5317 ?5318 ?5318 =?= multiply ?5318 (inverse ?5317) ?5317 [5318, 5317] by Super 964 with 822 at 3,2
% 0.15/0.42 Id : 992, {_}: multiply ?5317 ?5318 ?5318 =>= ?5318 [5318, 5317] by Demod 975 with 638 at 3
% 0.15/0.42 Id : 1086, {_}: a === a [] by Demod 1 with 992 at 2
% 0.15/0.42 Id : 1, {_}: multiply b a a =>= a [] by prove_tba_axioms_2
% 0.15/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.42 26550: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.113842 using nrkbo
%------------------------------------------------------------------------------