%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP577-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 : n015.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:51 EDT 2022
% Result : Unsatisfiable 0.19s 0.38s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GRP577-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n015.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 06:26:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 2539: Facts:
% 0.12/0.33 2539: Id : 2, {_}:
% 0.12/0.33 double_divide
% 0.12/0.33 (double_divide ?2
% 0.12/0.33 (double_divide (double_divide (double_divide ?3 ?2) ?4)
% 0.12/0.33 (double_divide ?3 identity))) (double_divide identity identity)
% 0.12/0.33 =>=
% 0.12/0.33 ?4
% 0.12/0.33 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.33 2539: Id : 3, {_}:
% 0.12/0.33 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.12/0.33 [7, 6] by multiply ?6 ?7
% 0.12/0.33 2539: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.33 2539: Id : 5, {_}:
% 0.12/0.33 identity =<= double_divide ?11 (inverse ?11)
% 0.12/0.33 [11] by identity ?11
% 0.12/0.33 2539: Goal:
% 0.12/0.33 2539: Id : 1, {_}: multiply (inverse a1) a1 =>= identity [] by prove_these_axioms_1
% 0.19/0.38 Statistics :
% 0.19/0.38 Max weight : 20
% 0.19/0.38 Found proof, 0.052083s
% 0.19/0.38 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.38 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.38 Id : 2, {_}: double_divide (double_divide ?2 (double_divide (double_divide (double_divide ?3 ?2) ?4) (double_divide ?3 identity))) (double_divide identity identity) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.19/0.39 Id : 6, {_}: double_divide (double_divide ?13 (double_divide (double_divide (double_divide ?14 ?13) ?15) (double_divide ?14 identity))) (double_divide identity identity) =>= ?15 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 0.19/0.39 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.19/0.39 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.19/0.39 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.19/0.39 Id : 19, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.19/0.39 Id : 30, {_}: multiply (inverse ?75) ?75 =>= inverse identity [75] by Super 19 with 5 at 1,3
% 0.19/0.39 Id : 9, {_}: double_divide (double_divide ?26 ?27) (double_divide identity identity) =<= double_divide (double_divide (double_divide ?28 (double_divide identity ?26)) ?27) (double_divide ?28 identity) [28, 27, 26] by Super 6 with 2 at 2,1,2
% 0.19/0.39 Id : 214, {_}: double_divide (double_divide ?26 ?27) (inverse identity) =<= double_divide (double_divide (double_divide ?28 (double_divide identity ?26)) ?27) (double_divide ?28 identity) [28, 27, 26] by Demod 9 with 4 at 2,2
% 0.19/0.39 Id : 231, {_}: double_divide (double_divide ?556 ?557) (inverse identity) =<= double_divide (double_divide (double_divide ?558 (double_divide identity ?556)) ?557) (inverse ?558) [558, 557, 556] by Demod 214 with 4 at 2,3
% 0.19/0.39 Id : 20, {_}: double_divide (double_divide ?2 (double_divide (double_divide (double_divide ?3 ?2) ?4) (inverse ?3))) (double_divide identity identity) =>= ?4 [4, 3, 2] by Demod 2 with 4 at 2,2,1,2
% 0.19/0.39 Id : 21, {_}: double_divide (double_divide ?2 (double_divide (double_divide (double_divide ?3 ?2) ?4) (inverse ?3))) (inverse identity) =>= ?4 [4, 3, 2] by Demod 20 with 4 at 2,2
% 0.19/0.39 Id : 29, {_}: double_divide (double_divide ?72 (double_divide identity (inverse ?73))) (inverse identity) =>= inverse (double_divide ?73 ?72) [73, 72] by Super 21 with 5 at 1,2,1,2
% 0.19/0.39 Id : 34, {_}: double_divide (double_divide ?72 (double_divide identity (inverse ?73))) (inverse identity) =>= multiply ?72 ?73 [73, 72] by Demod 29 with 19 at 3
% 0.19/0.39 Id : 235, {_}: double_divide (double_divide (inverse ?571) (inverse identity)) (inverse identity) =?= double_divide (multiply ?572 ?571) (inverse ?572) [572, 571] by Super 231 with 34 at 1,3
% 0.19/0.39 Id : 167, {_}: double_divide (double_divide ?410 (double_divide identity (inverse ?411))) (inverse identity) =>= multiply ?410 ?411 [411, 410] by Demod 29 with 19 at 3
% 0.19/0.39 Id : 169, {_}: double_divide (double_divide ?417 identity) (inverse identity) =>= multiply ?417 identity [417] by Super 167 with 5 at 2,1,2
% 0.19/0.39 Id : 179, {_}: double_divide (inverse ?417) (inverse identity) =>= multiply ?417 identity [417] by Demod 169 with 4 at 1,2
% 0.19/0.39 Id : 256, {_}: double_divide (multiply ?571 identity) (inverse identity) =?= double_divide (multiply ?572 ?571) (inverse ?572) [572, 571] by Demod 235 with 179 at 1,2
% 0.19/0.39 Id : 190, {_}: double_divide (inverse ?446) (inverse identity) =>= multiply ?446 identity [446] by Demod 169 with 4 at 1,2
% 0.19/0.39 Id : 191, {_}: double_divide (multiply ?448 ?449) (inverse identity) =>= multiply (double_divide ?449 ?448) identity [449, 448] by Super 190 with 19 at 1,2
% 0.19/0.39 Id : 257, {_}: multiply (double_divide identity ?571) identity =<= double_divide (multiply ?572 ?571) (inverse ?572) [572, 571] by Demod 256 with 191 at 2
% 0.19/0.39 Id : 436, {_}: multiply (double_divide identity ?1014) identity =?= multiply (double_divide ?1014 identity) identity [1014] by Super 191 with 257 at 2
% 0.19/0.39 Id : 459, {_}: multiply (double_divide identity ?1014) identity =>= multiply (inverse ?1014) identity [1014] by Demod 436 with 4 at 1,3
% 0.19/0.39 Id : 466, {_}: multiply (inverse ?571) identity =<= double_divide (multiply ?572 ?571) (inverse ?572) [572, 571] by Demod 257 with 459 at 2
% 0.19/0.39 Id : 474, {_}: multiply (double_divide identity ?1091) identity =>= multiply (inverse ?1091) identity [1091] by Demod 436 with 4 at 1,3
% 0.19/0.39 Id : 476, {_}: multiply identity identity =<= multiply (inverse (inverse identity)) identity [] by Super 474 with 5 at 1,2
% 0.19/0.39 Id : 22, {_}: multiply identity ?57 =>= inverse (inverse ?57) [57] by Super 19 with 4 at 1,3
% 0.19/0.39 Id : 488, {_}: inverse (inverse identity) =<= multiply (inverse (inverse identity)) identity [] by Demod 476 with 22 at 2
% 0.19/0.39 Id : 492, {_}: multiply (inverse identity) identity =<= double_divide (inverse (inverse identity)) (inverse (inverse (inverse identity))) [] by Super 466 with 488 at 1,3
% 0.19/0.39 Id : 505, {_}: inverse identity =<= double_divide (inverse (inverse identity)) (inverse (inverse (inverse identity))) [] by Demod 492 with 30 at 2
% 0.19/0.39 Id : 506, {_}: inverse identity =>= identity [] by Demod 505 with 5 at 3
% 0.19/0.39 Id : 528, {_}: multiply (inverse ?75) ?75 =>= identity [75] by Demod 30 with 506 at 3
% 0.19/0.39 Id : 619, {_}: identity === identity [] by Demod 1 with 528 at 2
% 0.19/0.39 Id : 1, {_}: multiply (inverse a1) a1 =>= identity [] by prove_these_axioms_1
% 0.19/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.39 2541: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.059459 using lpo
%------------------------------------------------------------------------------