%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n027.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.27s 0.67s
% Output : CNFRefutation 1.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% 0.07/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 1 19:58:34 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 12782: Facts:
% 0.13/0.34 12782: Id : 2, {_}:
% 0.13/0.34 multiply (multiply ?2 ?3 ?4) ?5 (multiply ?2 ?3 ?6)
% 0.13/0.34 =>=
% 0.13/0.34 multiply ?2 ?3 (multiply ?4 ?5 ?6)
% 0.13/0.34 [6, 5, 4, 3, 2] by associativity ?2 ?3 ?4 ?5 ?6
% 0.13/0.34 12782: Id : 3, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
% 0.13/0.34 12782: Id : 4, {_}:
% 0.13/0.34 multiply ?11 ?11 ?12 =>= ?11
% 0.13/0.34 [12, 11] by ternary_multiply_2 ?11 ?12
% 0.13/0.34 12782: Id : 5, {_}:
% 0.13/0.34 multiply (inverse ?14) ?14 ?15 =>= ?15
% 0.13/0.34 [15, 14] by left_inverse ?14 ?15
% 0.13/0.34 12782: Id : 6, {_}: multiply ?17 ?18 ?17 =>= ?17 [18, 17] by extra_lemma ?17 ?18
% 0.13/0.34 12782: Goal:
% 0.13/0.34 12782: Id : 1, {_}: multiply a (inverse a) b =>= b [] by prove_equation
% 1.27/0.67 Statistics :
% 1.27/0.67 Max weight : 24
% 1.27/0.67 Found proof, 0.321686s
% 1.27/0.67 % SZS status Unsatisfiable for theBenchmark.p
% 1.27/0.67 % SZS output start CNFRefutation for theBenchmark.p
% 1.27/0.67 Id : 6, {_}: multiply ?17 ?18 ?17 =>= ?17 [18, 17] by extra_lemma ?17 ?18
% 1.27/0.67 Id : 4, {_}: multiply ?11 ?11 ?12 =>= ?11 [12, 11] by ternary_multiply_2 ?11 ?12
% 1.27/0.67 Id : 5, {_}: multiply (inverse ?14) ?14 ?15 =>= ?15 [15, 14] by left_inverse ?14 ?15
% 1.27/0.67 Id : 3, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
% 1.27/0.67 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.27/0.67 Id : 668, {_}: multiply (multiply ?2321 ?2322 ?2323) ?2324 ?2322 =?= multiply ?2321 ?2322 (multiply ?2323 ?2324 ?2322) [2324, 2323, 2322, 2321] by Super 2 with 3 at 3,2
% 1.27/0.67 Id : 672, {_}: multiply (multiply ?2341 ?2342 (inverse ?2343)) ?2343 ?2342 =>= multiply ?2341 ?2342 ?2342 [2343, 2342, 2341] by Super 668 with 5 at 3,3
% 1.27/0.67 Id : 1012, {_}: multiply (multiply ?3241 ?3242 (inverse ?3243)) ?3243 ?3242 =>= ?3242 [3243, 3242, 3241] by Demod 672 with 3 at 3
% 1.27/0.67 Id : 671, {_}: multiply (multiply ?2337 ?2338 ?2339) ?2339 ?2338 =>= multiply ?2337 ?2338 ?2339 [2339, 2338, 2337] by Super 668 with 4 at 3,3
% 1.27/0.67 Id : 1018, {_}: multiply (multiply ?3261 (inverse ?3262) ?3263) ?3262 ?3263 =>= ?3263 [3263, 3262, 3261] by Super 1012 with 671 at 1,2
% 1.27/0.67 Id : 2161, {_}: multiply (multiply ?6586 ?6587 ?6588) ?6589 ?6586 =?= multiply ?6586 ?6587 (multiply ?6588 ?6589 ?6586) [6589, 6588, 6587, 6586] by Super 2 with 6 at 3,2
% 1.27/0.67 Id : 2164, {_}: multiply (multiply ?6602 ?6603 ?6604) ?6604 ?6602 =>= multiply ?6602 ?6603 ?6604 [6604, 6603, 6602] by Super 2161 with 4 at 3,3
% 1.27/0.67 Id : 2561, {_}: multiply (multiply ?7465 ?7466 ?7467) ?7465 ?7467 =?= multiply (multiply ?7465 ?7466 ?7467) ?7467 ?7465 [7467, 7466, 7465] by Super 671 with 2164 at 1,2
% 1.27/0.67 Id : 2663, {_}: multiply (multiply ?7465 ?7466 ?7467) ?7465 ?7467 =>= multiply ?7465 ?7466 ?7467 [7467, 7466, 7465] by Demod 2561 with 2164 at 3
% 1.27/0.67 Id : 3416, {_}: multiply ?9316 (inverse ?9316) ?9317 =>= ?9317 [9317, 9316] by Super 1018 with 2663 at 2
% 1.27/0.67 Id : 4197, {_}: b === b [] by Demod 1 with 3416 at 2
% 1.27/0.67 Id : 1, {_}: multiply a (inverse a) b =>= b [] by prove_equation
% 1.27/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.27/0.67 12782: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.311582 using nrkbo
%------------------------------------------------------------------------------