%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP498-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 : n025.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.19s 0.42s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP498-1 : TPTP v8.1.0. Released v2.6.0.
% 0.07/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.34 % Computer : n025.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 : Mon Jun 13 15:15:54 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 1050: Facts:
% 0.13/0.35 1050: Id : 2, {_}:
% 0.13/0.35 double_divide
% 0.13/0.35 (double_divide identity
% 0.13/0.35 (double_divide ?2 (double_divide ?3 identity)))
% 0.13/0.35 (double_divide (double_divide ?3 (double_divide ?4 ?2)) identity)
% 0.13/0.35 =>=
% 0.13/0.35 ?4
% 0.13/0.35 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.13/0.35 1050: Id : 3, {_}:
% 0.13/0.35 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.13/0.35 [7, 6] by multiply ?6 ?7
% 0.13/0.35 1050: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.13/0.35 1050: Id : 5, {_}:
% 0.13/0.35 identity =<= double_divide ?11 (inverse ?11)
% 0.13/0.35 [11] by identity ?11
% 0.13/0.35 1050: Goal:
% 0.13/0.35 1050: Id : 1, {_}:
% 0.13/0.35 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.13/0.35 [] by prove_these_axioms_3
% 0.19/0.42 Statistics :
% 0.19/0.42 Max weight : 20
% 0.19/0.42 Found proof, 0.070323s
% 0.19/0.42 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.42 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.42 Id : 27, {_}: identity =<= double_divide ?72 (inverse ?72) [72] by identity ?72
% 0.19/0.42 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 0.19/0.42 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 0.19/0.42 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.19/0.42 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.19/0.42 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.19/0.42 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.19/0.42 Id : 84, {_}: 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.19/0.42 Id : 85, {_}: 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 84 with 4 at 2,2
% 0.19/0.42 Id : 18, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 0.19/0.42 Id : 86, {_}: 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 85 with 18 at 2,2,1,2
% 0.19/0.42 Id : 87, {_}: 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 86 with 4 at 2,1,2,2,1,2
% 0.19/0.42 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.19/0.42 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.19/0.42 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.19/0.42 Id : 30, {_}: double_divide (inverse identity) (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 25 with 4 at 1,2
% 0.19/0.42 Id : 28, {_}: identity =<= double_divide (double_divide ?74 ?75) (multiply ?75 ?74) [75, 74] by Super 27 with 18 at 2,3
% 0.19/0.42 Id : 63, {_}: identity =<= inverse identity [] by Super 19 with 28 at 2
% 0.19/0.42 Id : 128, {_}: double_divide identity (multiply (double_divide ?272 ?273) ?273) =>= ?272 [273, 272] by Demod 30 with 63 at 1,2
% 0.19/0.42 Id : 133, {_}: double_divide identity (multiply (inverse ?291) identity) =>= ?291 [291] by Super 128 with 4 at 1,2,2
% 0.19/0.42 Id : 134, {_}: double_divide identity (multiply identity (inverse ?293)) =>= ?293 [293] by Super 128 with 5 at 1,2,2
% 0.19/0.42 Id : 20, {_}: multiply identity ?55 =>= inverse (inverse ?55) [55] by Super 18 with 4 at 1,3
% 0.19/0.42 Id : 142, {_}: double_divide identity (inverse (inverse (inverse ?293))) =>= ?293 [293] by Demod 134 with 20 at 2,2
% 0.19/0.42 Id : 206, {_}: multiply (inverse (inverse (inverse ?455))) identity =>= inverse ?455 [455] by Super 18 with 142 at 1,3
% 0.19/0.42 Id : 272, {_}: double_divide identity (inverse ?550) =>= inverse (inverse ?550) [550] by Super 133 with 206 at 2,2
% 0.19/0.42 Id : 246, {_}: double_divide identity (inverse ?505) =>= inverse (inverse ?505) [505] by Super 133 with 206 at 2,2
% 0.19/0.42 Id : 260, {_}: inverse (inverse (inverse (inverse ?293))) =>= ?293 [293] by Demod 142 with 246 at 2
% 0.19/0.42 Id : 273, {_}: double_divide identity ?552 =<= inverse (inverse (inverse (inverse (inverse ?552)))) [552] by Super 272 with 260 at 2,2
% 0.19/0.42 Id : 293, {_}: double_divide identity ?552 =>= inverse ?552 [552] by Demod 273 with 260 at 3
% 0.19/0.42 Id : 340, {_}: 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 87 with 293 at 1,2
% 0.19/0.42 Id : 341, {_}: 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 340 with 293 at 1,1,2
% 0.19/0.42 Id : 355, {_}: multiply ?638 identity =>= inverse (inverse ?638) [638] by Super 18 with 293 at 1,3
% 0.19/0.42 Id : 385, {_}: double_divide (inverse (inverse (inverse (inverse (double_divide ?22 (inverse ?23)))))) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 341 with 355 at 1,1,1,2
% 0.19/0.42 Id : 386, {_}: double_divide (double_divide ?22 (inverse ?23)) (inverse ?24) =>= double_divide ?23 (double_divide ?24 ?22) [24, 23, 22] by Demod 385 with 260 at 1,2
% 0.19/0.42 Id : 123, {_}: double_divide identity (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 30 with 63 at 1,2
% 0.19/0.42 Id : 339, {_}: inverse (multiply (double_divide ?67 ?68) ?68) =>= ?67 [68, 67] by Demod 123 with 293 at 2
% 0.19/0.42 Id : 362, {_}: double_divide (inverse (inverse (multiply (inverse (inverse ?658)) identity))) (inverse ?659) =>= double_divide ?658 (double_divide ?659 identity) [659, 658] by Super 341 with 293 at 1,1,1,1,2
% 0.19/0.42 Id : 345, {_}: inverse (multiply (inverse ?291) identity) =>= ?291 [291] by Demod 133 with 293 at 2
% 0.19/0.42 Id : 367, {_}: double_divide (inverse (inverse ?658)) (inverse ?659) =>= double_divide ?658 (double_divide ?659 identity) [659, 658] by Demod 362 with 345 at 1,1,2
% 0.19/0.42 Id : 368, {_}: double_divide (inverse (inverse ?658)) (inverse ?659) =>= double_divide ?658 (inverse ?659) [659, 658] by Demod 367 with 4 at 2,3
% 0.19/0.42 Id : 441, {_}: inverse (multiply (double_divide ?725 (inverse ?726)) (inverse ?726)) =>= inverse (inverse ?725) [726, 725] by Super 339 with 368 at 1,1,2
% 0.19/0.42 Id : 456, {_}: ?725 =<= inverse (inverse ?725) [725] by Demod 441 with 339 at 2
% 0.19/0.42 Id : 484, {_}: double_divide (double_divide ?800 ?801) (inverse ?802) =>= double_divide (inverse ?801) (double_divide ?802 ?800) [802, 801, 800] by Super 386 with 456 at 2,1,2
% 0.19/0.42 Id : 12, {_}: double_divide (double_divide identity (double_divide identity (double_divide ?33 identity))) (multiply (multiply ?34 ?35) ?33) =>= double_divide ?35 ?34 [35, 34, 33] by Super 11 with 3 at 1,2,2
% 0.19/0.42 Id : 301, {_}: double_divide (double_divide identity (double_divide identity (inverse ?33))) (multiply (multiply ?34 ?35) ?33) =>= double_divide ?35 ?34 [35, 34, 33] by Demod 12 with 4 at 2,2,1,2
% 0.19/0.42 Id : 302, {_}: double_divide (double_divide identity (inverse (inverse ?33))) (multiply (multiply ?34 ?35) ?33) =>= double_divide ?35 ?34 [35, 34, 33] by Demod 301 with 246 at 2,1,2
% 0.19/0.42 Id : 303, {_}: double_divide (inverse (inverse (inverse ?33))) (multiply (multiply ?34 ?35) ?33) =>= double_divide ?35 ?34 [35, 34, 33] by Demod 302 with 246 at 1,2
% 0.19/0.42 Id : 471, {_}: double_divide (inverse ?33) (multiply (multiply ?34 ?35) ?33) =>= double_divide ?35 ?34 [35, 34, 33] by Demod 303 with 456 at 1,2
% 0.19/0.42 Id : 26, {_}: multiply (inverse ?70) ?70 =>= inverse identity [70] by Super 18 with 5 at 1,3
% 0.19/0.42 Id : 103, {_}: multiply (inverse ?70) ?70 =>= identity [70] by Demod 26 with 63 at 3
% 0.19/0.42 Id : 480, {_}: multiply ?787 (inverse ?787) =>= identity [787] by Super 103 with 456 at 1,2
% 0.19/0.42 Id : 501, {_}: double_divide (inverse (inverse (multiply ?841 ?842))) identity =>= double_divide ?842 ?841 [842, 841] by Super 471 with 480 at 2,2
% 0.19/0.42 Id : 510, {_}: inverse (inverse (inverse (multiply ?841 ?842))) =>= double_divide ?842 ?841 [842, 841] by Demod 501 with 4 at 2
% 0.19/0.42 Id : 511, {_}: inverse (multiply ?841 ?842) =>= double_divide ?842 ?841 [842, 841] by Demod 510 with 456 at 2
% 0.19/0.42 Id : 630, {_}: double_divide ?68 (double_divide ?67 ?68) =>= ?67 [67, 68] by Demod 339 with 511 at 2
% 0.19/0.42 Id : 344, {_}: double_divide (inverse (double_divide ?2 (inverse ?3))) (multiply (double_divide ?4 ?2) ?3) =>= ?4 [4, 3, 2] by Demod 19 with 293 at 1,2
% 0.19/0.42 Id : 349, {_}: double_divide (multiply (inverse ?3) ?2) (multiply (double_divide ?4 ?2) ?3) =>= ?4 [4, 2, 3] by Demod 344 with 18 at 1,2
% 0.19/0.42 Id : 481, {_}: identity =<= double_divide (inverse ?789) ?789 [789] by Super 5 with 456 at 2,3
% 0.19/0.42 Id : 586, {_}: double_divide (multiply (inverse ?1035) ?1036) (multiply identity ?1035) =>= inverse ?1036 [1036, 1035] by Super 349 with 481 at 1,2,2
% 0.19/0.42 Id : 474, {_}: multiply identity ?55 =>= ?55 [55] by Demod 20 with 456 at 3
% 0.19/0.42 Id : 625, {_}: double_divide (multiply (inverse ?1035) ?1036) ?1035 =>= inverse ?1036 [1036, 1035] by Demod 586 with 474 at 2,2
% 0.19/0.42 Id : 738, {_}: double_divide ?1277 (inverse ?1278) =>= multiply (inverse ?1277) ?1278 [1278, 1277] by Super 630 with 625 at 2,2
% 0.19/0.42 Id : 780, {_}: multiply (inverse (double_divide ?800 ?801)) ?802 =<= double_divide (inverse ?801) (double_divide ?802 ?800) [802, 801, 800] by Demod 484 with 738 at 2
% 0.19/0.42 Id : 781, {_}: multiply (multiply ?801 ?800) ?802 =<= double_divide (inverse ?801) (double_divide ?802 ?800) [802, 800, 801] by Demod 780 with 18 at 1,2
% 0.19/0.42 Id : 795, {_}: double_divide ?1396 (inverse ?1397) =>= multiply (inverse ?1396) ?1397 [1397, 1396] by Super 630 with 625 at 2,2
% 0.19/0.42 Id : 832, {_}: double_divide ?1458 ?1459 =<= multiply (inverse ?1458) (inverse ?1459) [1459, 1458] by Super 795 with 456 at 2,2
% 0.19/0.42 Id : 840, {_}: double_divide (inverse ?1484) ?1485 =>= multiply ?1484 (inverse ?1485) [1485, 1484] by Super 832 with 456 at 1,3
% 0.19/0.42 Id : 953, {_}: multiply (multiply ?801 ?800) ?802 =<= multiply ?801 (inverse (double_divide ?802 ?800)) [802, 800, 801] by Demod 781 with 840 at 3
% 0.19/0.42 Id : 954, {_}: multiply (multiply ?801 ?800) ?802 =?= multiply ?801 (multiply ?800 ?802) [802, 800, 801] by Demod 953 with 18 at 2,3
% 0.19/0.42 Id : 1007, {_}: multiply a3 (multiply b3 c3) === multiply a3 (multiply b3 c3) [] by Demod 1 with 954 at 2
% 0.19/0.42 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 0.19/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.42 1050: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.075889 using nrkbo
%------------------------------------------------------------------------------