%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n023.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:09 EDT 2022
% Result : Unsatisfiable 1.29s 0.65s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n023.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 : Wed Jun 1 19:56:56 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 4899: Facts:
% 0.12/0.33 4899: Id : 2, {_}:
% 0.12/0.33 multiply (multiply ?2 ?3 ?4) ?5 (multiply ?2 ?3 ?6)
% 0.12/0.33 =>=
% 0.12/0.33 multiply ?2 ?3 (multiply ?4 ?5 ?6)
% 0.12/0.33 [6, 5, 4, 3, 2] by associativity ?2 ?3 ?4 ?5 ?6
% 0.12/0.33 4899: Id : 3, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
% 0.12/0.33 4899: Id : 4, {_}:
% 0.12/0.33 multiply ?11 ?11 ?12 =>= ?11
% 0.12/0.33 [12, 11] by ternary_multiply_2 ?11 ?12
% 0.12/0.33 4899: Id : 5, {_}:
% 0.12/0.33 multiply (inverse ?14) ?14 ?15 =>= ?15
% 0.12/0.33 [15, 14] by left_inverse ?14 ?15
% 0.12/0.33 4899: Goal:
% 0.12/0.33 4899: Id : 1, {_}: multiply a (inverse a) b =>= b [] by prove_equation
% 1.29/0.65 Statistics :
% 1.29/0.65 Max weight : 24
% 1.29/0.65 Found proof, 0.317224s
% 1.29/0.65 % SZS status Unsatisfiable for theBenchmark.p
% 1.29/0.65 % SZS output start CNFRefutation for theBenchmark.p
% 1.29/0.65 Id : 4, {_}: multiply ?11 ?11 ?12 =>= ?11 [12, 11] by ternary_multiply_2 ?11 ?12
% 1.29/0.65 Id : 5, {_}: multiply (inverse ?14) ?14 ?15 =>= ?15 [15, 14] by left_inverse ?14 ?15
% 1.29/0.65 Id : 3, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
% 1.29/0.65 Id : 2, {_}: multiply (multiply ?2 ?3 ?4) ?5 (multiply ?2 ?3 ?6) =>= multiply ?2 ?3 (multiply ?4 ?5 ?6) [6, 5, 4, 3, 2] by associativity ?2 ?3 ?4 ?5 ?6
% 1.29/0.65 Id : 666, {_}: multiply (multiply ?2318 ?2319 ?2320) ?2321 ?2319 =?= multiply ?2318 ?2319 (multiply ?2320 ?2321 ?2319) [2321, 2320, 2319, 2318] by Super 2 with 3 at 3,2
% 1.29/0.65 Id : 670, {_}: multiply (multiply ?2338 ?2339 (inverse ?2340)) ?2340 ?2339 =>= multiply ?2338 ?2339 ?2339 [2340, 2339, 2338] by Super 666 with 5 at 3,3
% 1.29/0.65 Id : 1010, {_}: multiply (multiply ?3238 ?3239 (inverse ?3240)) ?3240 ?3239 =>= ?3239 [3240, 3239, 3238] by Demod 670 with 3 at 3
% 1.29/0.65 Id : 669, {_}: multiply (multiply ?2334 ?2335 ?2336) ?2336 ?2335 =>= multiply ?2334 ?2335 ?2336 [2336, 2335, 2334] by Super 666 with 4 at 3,3
% 1.29/0.65 Id : 1016, {_}: multiply (multiply ?3258 (inverse ?3259) ?3260) ?3259 ?3260 =>= ?3260 [3260, 3259, 3258] by Super 1010 with 669 at 1,2
% 1.29/0.65 Id : 16, {_}: multiply (multiply ?70 ?70 ?71) ?72 ?70 =?= multiply ?70 ?70 (multiply ?71 ?72 ?73) [73, 72, 71, 70] by Super 2 with 4 at 3,2
% 1.29/0.65 Id : 24, {_}: multiply ?70 ?72 ?70 =<= multiply ?70 ?70 (multiply ?71 ?72 ?73) [73, 71, 72, 70] by Demod 16 with 4 at 1,2
% 1.29/0.65 Id : 25, {_}: multiply ?70 ?72 ?70 =>= ?70 [72, 70] by Demod 24 with 4 at 3
% 1.29/0.65 Id : 2159, {_}: multiply (multiply ?6583 ?6584 ?6585) ?6586 ?6583 =?= multiply ?6583 ?6584 (multiply ?6585 ?6586 ?6583) [6586, 6585, 6584, 6583] by Super 2 with 25 at 3,2
% 1.29/0.65 Id : 2162, {_}: multiply (multiply ?6599 ?6600 ?6601) ?6601 ?6599 =>= multiply ?6599 ?6600 ?6601 [6601, 6600, 6599] by Super 2159 with 4 at 3,3
% 1.29/0.65 Id : 2559, {_}: multiply (multiply ?7462 ?7463 ?7464) ?7462 ?7464 =?= multiply (multiply ?7462 ?7463 ?7464) ?7464 ?7462 [7464, 7463, 7462] by Super 669 with 2162 at 1,2
% 1.29/0.65 Id : 2661, {_}: multiply (multiply ?7462 ?7463 ?7464) ?7462 ?7464 =>= multiply ?7462 ?7463 ?7464 [7464, 7463, 7462] by Demod 2559 with 2162 at 3
% 1.29/0.65 Id : 3414, {_}: multiply ?9313 (inverse ?9313) ?9314 =>= ?9314 [9314, 9313] by Super 1016 with 2661 at 2
% 1.29/0.65 Id : 4195, {_}: b === b [] by Demod 1 with 3414 at 2
% 1.29/0.65 Id : 1, {_}: multiply a (inverse a) b =>= b [] by prove_equation
% 1.29/0.65 % SZS output end CNFRefutation for theBenchmark.p
% 1.29/0.65 4899: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.308024 using nrkbo
%------------------------------------------------------------------------------