%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP497-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 : n005.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:32 EDT 2022
% Result : Unsatisfiable 0.12s 0.37s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP497-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 : n005.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 : Tue Jun 14 08:04:54 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 20886: Facts:
% 0.12/0.34 20886: Id : 2, {_}:
% 0.12/0.34 double_divide
% 0.12/0.34 (double_divide identity
% 0.12/0.34 (double_divide ?2 (double_divide ?3 identity)))
% 0.12/0.34 (double_divide (double_divide ?3 (double_divide ?4 ?2)) identity)
% 0.12/0.34 =>=
% 0.12/0.34 ?4
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 20886: Id : 3, {_}:
% 0.12/0.34 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.12/0.34 [7, 6] by multiply ?6 ?7
% 0.12/0.34 20886: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.34 20886: Id : 5, {_}:
% 0.12/0.34 identity =<= double_divide ?11 (inverse ?11)
% 0.12/0.34 [11] by identity ?11
% 0.12/0.34 20886: Goal:
% 0.12/0.34 20886: Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.12/0.37 Statistics :
% 0.12/0.37 Max weight : 20
% 0.12/0.37 Found proof, 0.030984s
% 0.12/0.37 % SZS status Unsatisfiable for theBenchmark.p
% 0.12/0.37 % SZS output start CNFRefutation for theBenchmark.p
% 0.12/0.37 Id : 6, {_}: double_divide (double_divide identity (double_divide ?13 (double_divide ?14 identity))) (double_divide (double_divide ?14 (double_divide ?15 ?13)) identity) =>= ?15 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 0.12/0.37 Id : 27, {_}: identity =<= double_divide ?72 (inverse ?72) [72] by identity ?72
% 0.12/0.37 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.12/0.37 Id : 2, {_}: double_divide (double_divide identity (double_divide ?2 (double_divide ?3 identity))) (double_divide (double_divide ?3 (double_divide ?4 ?2)) identity) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.37 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.37 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.12/0.37 Id : 18, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.12/0.37 Id : 20, {_}: multiply identity ?55 =>= inverse (inverse ?55) [55] by Super 18 with 4 at 1,3
% 0.12/0.37 Id : 11, {_}: double_divide (double_divide identity (double_divide ?2 (double_divide ?3 identity))) (multiply (double_divide ?4 ?2) ?3) =>= ?4 [4, 3, 2] by Demod 2 with 3 at 2,2
% 0.12/0.37 Id : 19, {_}: double_divide (double_divide identity (double_divide ?2 (inverse ?3))) (multiply (double_divide ?4 ?2) ?3) =>= ?4 [4, 3, 2] by Demod 11 with 4 at 2,2,1,2
% 0.12/0.37 Id : 25, {_}: double_divide (double_divide identity identity) (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Super 19 with 5 at 2,1,2
% 0.12/0.37 Id : 30, {_}: double_divide (inverse identity) (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 25 with 4 at 1,2
% 0.12/0.37 Id : 28, {_}: identity =<= double_divide (double_divide ?74 ?75) (multiply ?75 ?74) [75, 74] by Super 27 with 18 at 2,3
% 0.12/0.37 Id : 66, {_}: identity =<= inverse identity [] by Super 19 with 28 at 2
% 0.12/0.37 Id : 129, {_}: double_divide identity (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 30 with 66 at 1,2
% 0.12/0.37 Id : 134, {_}: double_divide identity (multiply (double_divide ?272 ?273) ?273) =>= ?272 [273, 272] by Demod 30 with 66 at 1,2
% 0.12/0.37 Id : 139, {_}: double_divide identity (multiply (inverse ?291) identity) =>= ?291 [291] by Super 134 with 4 at 1,2,2
% 0.12/0.37 Id : 140, {_}: double_divide identity (multiply identity (inverse ?293)) =>= ?293 [293] by Super 134 with 5 at 1,2,2
% 0.12/0.37 Id : 148, {_}: double_divide identity (inverse (inverse (inverse ?293))) =>= ?293 [293] by Demod 140 with 20 at 2,2
% 0.12/0.37 Id : 215, {_}: multiply (inverse (inverse (inverse ?455))) identity =>= inverse ?455 [455] by Super 18 with 148 at 1,3
% 0.12/0.37 Id : 284, {_}: double_divide identity (inverse ?550) =>= inverse (inverse ?550) [550] by Super 139 with 215 at 2,2
% 0.12/0.37 Id : 257, {_}: double_divide identity (inverse ?505) =>= inverse (inverse ?505) [505] by Super 139 with 215 at 2,2
% 0.12/0.37 Id : 272, {_}: inverse (inverse (inverse (inverse ?293))) =>= ?293 [293] by Demod 148 with 257 at 2
% 0.12/0.37 Id : 285, {_}: double_divide identity ?552 =<= inverse (inverse (inverse (inverse (inverse ?552)))) [552] by Super 284 with 272 at 2,2
% 0.12/0.37 Id : 305, {_}: double_divide identity ?552 =>= inverse ?552 [552] by Demod 285 with 272 at 3
% 0.12/0.37 Id : 353, {_}: inverse (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 129 with 305 at 2
% 0.12/0.37 Id : 8, {_}: double_divide (double_divide identity (double_divide identity (double_divide (double_divide identity (double_divide ?22 (double_divide ?23 identity))) identity))) (double_divide ?24 identity) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Super 6 with 2 at 1,2,2
% 0.12/0.37 Id : 88, {_}: double_divide (double_divide identity (double_divide identity (inverse (double_divide identity (double_divide ?22 (double_divide ?23 identity)))))) (double_divide ?24 identity) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 8 with 4 at 2,2,1,2
% 0.12/0.37 Id : 89, {_}: double_divide (double_divide identity (double_divide identity (inverse (double_divide identity (double_divide ?22 (double_divide ?23 identity)))))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 88 with 4 at 2,2
% 0.12/0.37 Id : 90, {_}: double_divide (double_divide identity (double_divide identity (multiply (double_divide ?22 (double_divide ?23 identity)) identity))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 89 with 18 at 2,2,1,2
% 0.12/0.37 Id : 91, {_}: double_divide (double_divide identity (double_divide identity (multiply (double_divide ?22 (inverse ?23)) identity))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 90 with 4 at 2,1,2,2,1,2
% 0.12/0.37 Id : 354, {_}: double_divide (inverse (double_divide identity (multiply (double_divide ?22 (inverse ?23)) identity))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 91 with 305 at 1,2
% 0.12/0.37 Id : 355, {_}: double_divide (inverse (inverse (multiply (double_divide ?22 (inverse ?23)) identity))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 354 with 305 at 1,1,2
% 0.12/0.37 Id : 376, {_}: double_divide (inverse (inverse (multiply (inverse (inverse ?658)) identity))) (inverse ?659) =>= double_divide ?658 (double_divide ?659 identity) [659, 658] by Super 355 with 305 at 1,1,1,1,2
% 0.12/0.37 Id : 359, {_}: inverse (multiply (inverse ?291) identity) =>= ?291 [291] by Demod 139 with 305 at 2
% 0.12/0.37 Id : 381, {_}: double_divide (inverse (inverse ?658)) (inverse ?659) =>= double_divide ?658 (double_divide ?659 identity) [659, 658] by Demod 376 with 359 at 1,1,2
% 0.12/0.37 Id : 382, {_}: double_divide (inverse (inverse ?658)) (inverse ?659) =>= double_divide ?658 (inverse ?659) [659, 658] by Demod 381 with 4 at 2,3
% 0.12/0.37 Id : 457, {_}: inverse (multiply (double_divide ?725 (inverse ?726)) (inverse ?726)) =>= inverse (inverse ?725) [726, 725] by Super 353 with 382 at 1,1,2
% 0.12/0.37 Id : 472, {_}: ?725 =<= inverse (inverse ?725) [725] by Demod 457 with 353 at 2
% 0.12/0.37 Id : 491, {_}: multiply identity ?55 =>= ?55 [55] by Demod 20 with 472 at 3
% 0.12/0.37 Id : 509, {_}: a2 === a2 [] by Demod 1 with 491 at 2
% 0.12/0.37 Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.12/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.37 20886: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.034729 using nrkbo
%------------------------------------------------------------------------------