%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP582-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 : n020.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:52 EDT 2022
% Result : Unsatisfiable 0.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GRP582-1 : TPTP v8.1.0. Released v2.6.0.
% 0.10/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n020.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 10:05:50 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 5729: Facts:
% 0.12/0.33 5729: Id : 2, {_}:
% 0.12/0.33 double_divide
% 0.12/0.33 (double_divide ?2
% 0.12/0.33 (double_divide (double_divide identity ?3)
% 0.12/0.33 (double_divide ?4 (double_divide ?3 ?2))))
% 0.12/0.33 (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 5729: 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 5729: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.33 5729: Id : 5, {_}:
% 0.12/0.33 identity =<= double_divide ?11 (inverse ?11)
% 0.12/0.33 [11] by identity ?11
% 0.12/0.33 5729: Goal:
% 0.12/0.33 5729: Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.12/0.39 Statistics :
% 0.12/0.39 Max weight : 20
% 0.12/0.39 Found proof, 0.055868s
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark.p
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark.p
% 0.12/0.39 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.12/0.39 Id : 2, {_}: double_divide (double_divide ?2 (double_divide (double_divide identity ?3) (double_divide ?4 (double_divide ?3 ?2)))) (double_divide identity identity) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.39 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.12/0.39 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.12/0.39 Id : 15, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.12/0.39 Id : 17, {_}: multiply identity ?45 =>= inverse (inverse ?45) [45] by Super 15 with 4 at 1,3
% 0.12/0.39 Id : 16, {_}: double_divide (double_divide ?2 (double_divide (double_divide identity ?3) (double_divide ?4 (double_divide ?3 ?2)))) (inverse identity) =>= ?4 [4, 3, 2] by Demod 2 with 4 at 2,2
% 0.12/0.39 Id : 443, {_}: double_divide (double_divide identity (double_divide (double_divide identity ?542) (double_divide ?543 (inverse ?542)))) (inverse identity) =>= ?543 [543, 542] by Super 16 with 4 at 2,2,2,1,2
% 0.12/0.39 Id : 454, {_}: double_divide (double_divide identity (double_divide (double_divide identity ?574) identity)) (inverse identity) =>= ?574 [574] by Super 443 with 5 at 2,2,1,2
% 0.12/0.39 Id : 469, {_}: double_divide (double_divide identity (inverse (double_divide identity ?574))) (inverse identity) =>= ?574 [574] by Demod 454 with 4 at 2,1,2
% 0.12/0.39 Id : 479, {_}: double_divide (double_divide identity (multiply ?597 identity)) (inverse identity) =>= ?597 [597] by Demod 469 with 15 at 2,1,2
% 0.12/0.39 Id : 24, {_}: multiply (inverse ?63) ?63 =>= inverse identity [63] by Super 15 with 5 at 1,3
% 0.12/0.39 Id : 481, {_}: double_divide (double_divide identity (inverse identity)) (inverse identity) =>= inverse identity [] by Super 479 with 24 at 2,1,2
% 0.12/0.39 Id : 484, {_}: double_divide identity (inverse identity) =>= inverse identity [] by Demod 481 with 5 at 1,2
% 0.12/0.39 Id : 485, {_}: identity =<= inverse identity [] by Demod 484 with 5 at 2
% 0.12/0.39 Id : 505, {_}: double_divide (double_divide ?2 (double_divide (double_divide identity ?3) (double_divide ?4 (double_divide ?3 ?2)))) identity =>= ?4 [4, 3, 2] by Demod 16 with 485 at 2,2
% 0.12/0.39 Id : 539, {_}: inverse (double_divide ?2 (double_divide (double_divide identity ?3) (double_divide ?4 (double_divide ?3 ?2)))) =>= ?4 [4, 3, 2] by Demod 505 with 4 at 2
% 0.12/0.39 Id : 540, {_}: multiply (double_divide (double_divide identity ?3) (double_divide ?4 (double_divide ?3 ?2))) ?2 =>= ?4 [2, 4, 3] by Demod 539 with 15 at 2
% 0.12/0.39 Id : 22, {_}: double_divide (double_divide (inverse ?57) (double_divide (double_divide identity ?57) (double_divide ?58 identity))) (inverse identity) =>= ?58 [58, 57] by Super 16 with 5 at 2,2,2,1,2
% 0.12/0.39 Id : 91, {_}: double_divide (double_divide (inverse ?145) (double_divide (double_divide identity ?145) (inverse ?146))) (inverse identity) =>= ?146 [146, 145] by Demod 22 with 4 at 2,2,1,2
% 0.12/0.39 Id : 94, {_}: double_divide (double_divide (inverse (inverse identity)) (double_divide identity (inverse ?154))) (inverse identity) =>= ?154 [154] by Super 91 with 5 at 1,2,1,2
% 0.12/0.39 Id : 509, {_}: double_divide (double_divide (inverse identity) (double_divide identity (inverse ?154))) (inverse identity) =>= ?154 [154] by Demod 94 with 485 at 1,1,1,2
% 0.12/0.39 Id : 510, {_}: double_divide (double_divide (inverse identity) (double_divide identity (inverse ?154))) identity =>= ?154 [154] by Demod 509 with 485 at 2,2
% 0.12/0.39 Id : 511, {_}: double_divide (double_divide identity (double_divide identity (inverse ?154))) identity =>= ?154 [154] by Demod 510 with 485 at 1,1,2
% 0.12/0.39 Id : 532, {_}: inverse (double_divide identity (double_divide identity (inverse ?154))) =>= ?154 [154] by Demod 511 with 4 at 2
% 0.12/0.39 Id : 533, {_}: multiply (double_divide identity (inverse ?154)) identity =>= ?154 [154] by Demod 532 with 15 at 2
% 0.12/0.39 Id : 96, {_}: double_divide (double_divide (inverse ?159) identity) (inverse identity) =>= double_divide identity ?159 [159] by Super 91 with 5 at 2,1,2
% 0.12/0.39 Id : 101, {_}: double_divide (inverse (inverse ?159)) (inverse identity) =>= double_divide identity ?159 [159] by Demod 96 with 4 at 1,2
% 0.12/0.39 Id : 105, {_}: multiply (inverse identity) (inverse (inverse ?172)) =>= inverse (double_divide identity ?172) [172] by Super 15 with 101 at 1,3
% 0.12/0.39 Id : 110, {_}: multiply (inverse identity) (inverse (inverse ?172)) =>= multiply ?172 identity [172] by Demod 105 with 15 at 3
% 0.12/0.39 Id : 507, {_}: multiply identity (inverse (inverse ?172)) =>= multiply ?172 identity [172] by Demod 110 with 485 at 1,2
% 0.12/0.39 Id : 536, {_}: inverse (inverse (inverse (inverse ?172))) =>= multiply ?172 identity [172] by Demod 507 with 17 at 2
% 0.12/0.39 Id : 502, {_}: double_divide (inverse (inverse ?159)) identity =>= double_divide identity ?159 [159] by Demod 101 with 485 at 2,2
% 0.12/0.39 Id : 541, {_}: inverse (inverse (inverse ?159)) =>= double_divide identity ?159 [159] by Demod 502 with 4 at 2
% 0.12/0.39 Id : 542, {_}: double_divide identity (inverse ?172) =>= multiply ?172 identity [172] by Demod 536 with 541 at 2
% 0.12/0.39 Id : 545, {_}: multiply (multiply ?154 identity) identity =>= ?154 [154] by Demod 533 with 542 at 1,2
% 0.12/0.39 Id : 114, {_}: multiply (inverse identity) (inverse (inverse ?187)) =>= multiply ?187 identity [187] by Demod 105 with 15 at 3
% 0.12/0.39 Id : 115, {_}: multiply (inverse identity) (inverse (multiply ?189 ?190)) =>= multiply (double_divide ?190 ?189) identity [190, 189] by Super 114 with 15 at 1,2,2
% 0.12/0.39 Id : 508, {_}: multiply identity (inverse (multiply ?189 ?190)) =>= multiply (double_divide ?190 ?189) identity [190, 189] by Demod 115 with 485 at 1,2
% 0.12/0.39 Id : 535, {_}: inverse (inverse (inverse (multiply ?189 ?190))) =>= multiply (double_divide ?190 ?189) identity [190, 189] by Demod 508 with 17 at 2
% 0.12/0.39 Id : 543, {_}: double_divide identity (multiply ?189 ?190) =>= multiply (double_divide ?190 ?189) identity [190, 189] by Demod 535 with 541 at 2
% 0.12/0.39 Id : 28, {_}: double_divide (double_divide (inverse ?57) (double_divide (double_divide identity ?57) (inverse ?58))) (inverse identity) =>= ?58 [58, 57] by Demod 22 with 4 at 2,2,1,2
% 0.12/0.39 Id : 506, {_}: double_divide (double_divide (inverse ?57) (double_divide (double_divide identity ?57) (inverse ?58))) identity =>= ?58 [58, 57] by Demod 28 with 485 at 2,2
% 0.12/0.39 Id : 537, {_}: inverse (double_divide (inverse ?57) (double_divide (double_divide identity ?57) (inverse ?58))) =>= ?58 [58, 57] by Demod 506 with 4 at 2
% 0.12/0.39 Id : 538, {_}: multiply (double_divide (double_divide identity ?57) (inverse ?58)) (inverse ?57) =>= ?58 [58, 57] by Demod 537 with 15 at 2
% 0.12/0.39 Id : 575, {_}: multiply (double_divide (double_divide identity ?609) identity) (inverse ?609) =>= identity [609] by Super 538 with 485 at 2,1,2
% 0.12/0.39 Id : 591, {_}: multiply (inverse (double_divide identity ?609)) (inverse ?609) =>= identity [609] by Demod 575 with 4 at 1,2
% 0.12/0.39 Id : 614, {_}: multiply (multiply ?621 identity) (inverse ?621) =>= identity [621] by Demod 591 with 15 at 1,2
% 0.12/0.39 Id : 622, {_}: multiply ?637 (inverse (multiply ?637 identity)) =>= identity [637] by Super 614 with 545 at 1,2
% 0.12/0.39 Id : 470, {_}: double_divide (double_divide identity (multiply ?574 identity)) (inverse identity) =>= ?574 [574] by Demod 469 with 15 at 2,1,2
% 0.12/0.39 Id : 475, {_}: multiply (inverse identity) (double_divide identity (multiply ?589 identity)) =>= inverse ?589 [589] by Super 15 with 470 at 1,3
% 0.12/0.39 Id : 686, {_}: multiply identity (double_divide identity (multiply ?589 identity)) =>= inverse ?589 [589] by Demod 475 with 485 at 1,2
% 0.12/0.39 Id : 687, {_}: multiply identity (multiply (double_divide identity ?589) identity) =>= inverse ?589 [589] by Demod 686 with 543 at 2,2
% 0.12/0.39 Id : 688, {_}: inverse (inverse (multiply (double_divide identity ?589) identity)) =>= inverse ?589 [589] by Demod 687 with 17 at 2
% 0.12/0.39 Id : 693, {_}: multiply (double_divide (double_divide identity ?671) (inverse ?672)) (inverse ?671) =>= inverse (multiply (double_divide identity ?672) identity) [672, 671] by Super 538 with 688 at 2,1,2
% 0.12/0.39 Id : 713, {_}: ?672 =<= inverse (multiply (double_divide identity ?672) identity) [672] by Demod 693 with 538 at 2
% 0.12/0.39 Id : 744, {_}: multiply (double_divide identity ?715) ?715 =>= identity [715] by Super 622 with 713 at 2,2
% 0.12/0.39 Id : 772, {_}: double_divide identity identity =<= multiply (double_divide ?732 (double_divide identity ?732)) identity [732] by Super 543 with 744 at 2,2
% 0.12/0.39 Id : 807, {_}: inverse identity =<= multiply (double_divide ?732 (double_divide identity ?732)) identity [732] by Demod 772 with 4 at 2
% 0.12/0.39 Id : 808, {_}: identity =<= multiply (double_divide ?732 (double_divide identity ?732)) identity [732] by Demod 807 with 485 at 2
% 0.12/0.39 Id : 1010, {_}: multiply identity identity =<= double_divide ?881 (double_divide identity ?881) [881] by Super 545 with 808 at 1,2
% 0.12/0.39 Id : 1033, {_}: inverse (inverse identity) =<= double_divide ?881 (double_divide identity ?881) [881] by Demod 1010 with 17 at 2
% 0.12/0.39 Id : 1034, {_}: inverse identity =<= double_divide ?881 (double_divide identity ?881) [881] by Demod 1033 with 485 at 1,2
% 0.12/0.39 Id : 1035, {_}: identity =<= double_divide ?881 (double_divide identity ?881) [881] by Demod 1034 with 485 at 2
% 0.12/0.39 Id : 1082, {_}: multiply (double_divide (double_divide identity identity) identity) ?915 =>= ?915 [915] by Super 540 with 1035 at 2,1,2
% 0.12/0.39 Id : 1120, {_}: multiply (inverse (double_divide identity identity)) ?915 =>= ?915 [915] by Demod 1082 with 4 at 1,2
% 0.12/0.39 Id : 1121, {_}: multiply (multiply identity identity) ?915 =>= ?915 [915] by Demod 1120 with 15 at 1,2
% 0.12/0.39 Id : 1122, {_}: multiply (inverse (inverse identity)) ?915 =>= ?915 [915] by Demod 1121 with 17 at 1,2
% 0.12/0.39 Id : 1123, {_}: multiply (inverse identity) ?915 =>= ?915 [915] by Demod 1122 with 485 at 1,1,2
% 0.12/0.39 Id : 1124, {_}: multiply identity ?915 =>= ?915 [915] by Demod 1123 with 485 at 1,2
% 0.12/0.39 Id : 1125, {_}: inverse (inverse ?915) =>= ?915 [915] by Demod 1124 with 17 at 2
% 0.12/0.39 Id : 1186, {_}: multiply identity ?45 =>= ?45 [45] by Demod 17 with 1125 at 3
% 0.12/0.39 Id : 1237, {_}: a2 === a2 [] by Demod 1 with 1186 at 2
% 0.12/0.39 Id : 1, {_}: multiply identity a2 =>= a2 [] by prove_these_axioms_2
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.39 5732: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.060015 using nrkbo
%------------------------------------------------------------------------------