%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP571-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 : n013.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:49 EDT 2022
% Result : Unsatisfiable 34.91s 9.06s
% Output : CNFRefutation 34.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP571-1 : TPTP v8.1.0. Released v2.6.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Mon Jun 13 12:21:43 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.13/0.34 29662: Facts:
% 0.13/0.34 29662: Id : 2, {_}:
% 0.13/0.34 double_divide
% 0.13/0.34 (double_divide ?2
% 0.13/0.34 (double_divide (double_divide ?3 (double_divide ?2 ?4))
% 0.13/0.34 (double_divide ?4 identity))) (double_divide identity identity)
% 0.13/0.34 =>=
% 0.13/0.34 ?3
% 0.13/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.13/0.34 29662: Id : 3, {_}:
% 0.13/0.34 multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity
% 0.13/0.34 [7, 6] by multiply ?6 ?7
% 0.13/0.34 29662: Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 0.13/0.34 29662: Id : 5, {_}:
% 0.13/0.34 identity =<= double_divide ?11 (inverse ?11)
% 0.13/0.34 [11] by identity ?11
% 0.13/0.34 29662: Goal:
% 0.13/0.34 29662: Id : 1, {_}:
% 0.13/0.34 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.13/0.34 [] by prove_these_axioms_3
% 34.91/9.06 Statistics :
% 34.91/9.06 Max weight : 32
% 34.91/9.06 Found proof, 8.726238s
% 34.91/9.06 % SZS status Unsatisfiable for theBenchmark.p
% 34.91/9.06 % SZS output start CNFRefutation for theBenchmark.p
% 34.91/9.06 Id : 5, {_}: identity =<= double_divide ?11 (inverse ?11) [11] by identity ?11
% 34.91/9.06 Id : 2, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (double_divide ?4 identity))) (double_divide identity identity) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 34.91/9.06 Id : 6, {_}: double_divide (double_divide ?13 (double_divide (double_divide ?14 (double_divide ?13 ?15)) (double_divide ?15 identity))) (double_divide identity identity) =>= ?14 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 34.91/9.06 Id : 4, {_}: inverse ?9 =<= double_divide ?9 identity [9] by inverse ?9
% 34.91/9.06 Id : 3, {_}: multiply ?6 ?7 =<= double_divide (double_divide ?7 ?6) identity [7, 6] by multiply ?6 ?7
% 34.91/9.06 Id : 16, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by Demod 3 with 4 at 3
% 34.91/9.06 Id : 7, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (double_divide ?19 identity))) (double_divide (double_divide ?20 ?18) (double_divide (double_divide identity identity) identity))) (double_divide identity identity) =>= ?20 [20, 19, 18, 17] by Super 6 with 2 at 2,1,2,1,2
% 34.91/9.06 Id : 42, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (double_divide (double_divide identity identity) identity))) (double_divide identity identity) =>= ?20 [20, 19, 18, 17] by Demod 7 with 4 at 2,2,1,1,2
% 34.91/9.06 Id : 43, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (inverse (double_divide identity identity)))) (double_divide identity identity) =>= ?20 [20, 19, 18, 17] by Demod 42 with 4 at 2,2,1,2
% 34.91/9.06 Id : 44, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (inverse (double_divide identity identity)))) (inverse identity) =>= ?20 [20, 19, 18, 17] by Demod 43 with 4 at 2,2
% 34.91/9.06 Id : 45, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (multiply identity identity))) (inverse identity) =>= ?20 [20, 19, 18, 17] by Demod 44 with 16 at 2,2,1,2
% 34.91/9.06 Id : 19, {_}: multiply identity ?50 =>= inverse (inverse ?50) [50] by Super 16 with 4 at 1,3
% 34.91/9.06 Id : 72, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (inverse (inverse identity)))) (inverse identity) =>= ?20 [20, 19, 18, 17] by Demod 45 with 19 at 2,2,1,2
% 34.91/9.06 Id : 17, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) (double_divide identity identity) =>= ?3 [4, 3, 2] by Demod 2 with 4 at 2,2,1,2
% 34.91/9.06 Id : 18, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) (inverse identity) =>= ?3 [4, 3, 2] by Demod 17 with 4 at 2,2
% 34.91/9.06 Id : 8, {_}: double_divide (double_divide identity (double_divide ?22 (double_divide identity identity))) (double_divide identity identity) =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (double_divide ?24 identity)) [24, 23, 22] by Super 6 with 2 at 1,2,1,2
% 34.91/9.06 Id : 82, {_}: double_divide (double_divide identity (double_divide ?22 (inverse identity))) (double_divide identity identity) =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (double_divide ?24 identity)) [24, 23, 22] by Demod 8 with 4 at 2,2,1,2
% 34.91/9.06 Id : 83, {_}: double_divide (double_divide identity (double_divide ?22 (inverse identity))) (inverse identity) =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (double_divide ?24 identity)) [24, 23, 22] by Demod 82 with 4 at 2,2
% 34.91/9.06 Id : 84, {_}: double_divide (double_divide identity (double_divide ?22 (inverse identity))) (inverse identity) =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 83 with 4 at 2,2,3
% 34.91/9.06 Id : 88, {_}: double_divide (double_divide (double_divide identity (double_divide ?211 (inverse identity))) (inverse identity)) (inverse identity) =>= ?211 [211] by Super 18 with 84 at 1,2
% 34.91/9.06 Id : 273, {_}: double_divide (double_divide (double_divide identity (double_divide ?625 (inverse identity))) (inverse identity)) (inverse identity) =>= ?625 [625] by Super 18 with 84 at 1,2
% 34.91/9.06 Id : 291, {_}: double_divide (double_divide (double_divide identity identity) (inverse identity)) (inverse identity) =>= identity [] by Super 273 with 5 at 2,1,1,2
% 34.91/9.06 Id : 310, {_}: double_divide (double_divide (inverse identity) (inverse identity)) (inverse identity) =>= identity [] by Demod 291 with 4 at 1,1,2
% 34.91/9.06 Id : 325, {_}: double_divide (double_divide (double_divide identity identity) (inverse identity)) (inverse identity) =>= double_divide (inverse identity) (inverse identity) [] by Super 88 with 310 at 2,1,1,2
% 34.91/9.06 Id : 340, {_}: double_divide (double_divide (inverse identity) (inverse identity)) (inverse identity) =>= double_divide (inverse identity) (inverse identity) [] by Demod 325 with 4 at 1,1,2
% 34.91/9.06 Id : 341, {_}: identity =<= double_divide (inverse identity) (inverse identity) [] by Demod 340 with 310 at 2
% 34.91/9.06 Id : 360, {_}: double_divide (double_divide (double_divide identity identity) (inverse identity)) (inverse identity) =>= inverse identity [] by Super 88 with 341 at 2,1,1,2
% 34.91/9.06 Id : 383, {_}: double_divide (double_divide (inverse identity) (inverse identity)) (inverse identity) =>= inverse identity [] by Demod 360 with 4 at 1,1,2
% 34.91/9.06 Id : 384, {_}: double_divide identity (inverse identity) =>= inverse identity [] by Demod 383 with 341 at 1,2
% 34.91/9.06 Id : 385, {_}: identity =<= inverse identity [] by Demod 384 with 5 at 2
% 34.91/9.06 Id : 403, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (inverse identity))) (inverse identity) =>= ?20 [20, 19, 18, 17] by Demod 72 with 385 at 1,2,2,1,2
% 34.91/9.06 Id : 404, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) (inverse identity))) identity =>= ?20 [20, 19, 18, 17] by Demod 403 with 385 at 2,2
% 34.91/9.06 Id : 405, {_}: double_divide (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) identity)) identity =>= ?20 [20, 19, 18, 17] by Demod 404 with 385 at 2,2,1,2
% 34.91/9.06 Id : 412, {_}: inverse (double_divide (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) (double_divide (double_divide ?20 ?18) identity)) =>= ?20 [20, 19, 18, 17] by Demod 405 with 4 at 2
% 34.91/9.06 Id : 413, {_}: multiply (double_divide (double_divide ?20 ?18) identity) (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) =>= ?20 [19, 17, 18, 20] by Demod 412 with 16 at 2
% 34.91/9.06 Id : 414, {_}: multiply (inverse (double_divide ?20 ?18)) (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) =>= ?20 [19, 17, 18, 20] by Demod 413 with 4 at 1,2
% 34.91/9.06 Id : 415, {_}: multiply (multiply ?18 ?20) (double_divide ?17 (double_divide (double_divide ?18 (double_divide ?17 ?19)) (inverse ?19))) =>= ?20 [19, 17, 20, 18] by Demod 414 with 16 at 1,2
% 34.91/9.06 Id : 399, {_}: double_divide (double_divide identity (double_divide ?22 identity)) (inverse identity) =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 84 with 385 at 2,2,1,2
% 34.91/9.06 Id : 400, {_}: double_divide (double_divide identity (double_divide ?22 identity)) identity =?= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 399 with 385 at 2,2
% 34.91/9.06 Id : 418, {_}: inverse (double_divide identity (double_divide ?22 identity)) =<= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 400 with 4 at 2
% 34.91/9.06 Id : 419, {_}: multiply (double_divide ?22 identity) identity =<= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 418 with 16 at 2
% 34.91/9.06 Id : 420, {_}: multiply (inverse ?22) identity =<= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 419 with 4 at 1,2
% 34.91/9.06 Id : 421, {_}: multiply (multiply ?18 ?20) (multiply (inverse ?18) identity) =>= ?20 [20, 18] by Demod 415 with 420 at 2,2
% 34.91/9.06 Id : 434, {_}: multiply (multiply identity ?753) (multiply identity identity) =>= ?753 [753] by Super 421 with 385 at 1,2,2
% 34.91/9.06 Id : 439, {_}: multiply (inverse (inverse ?753)) (multiply identity identity) =>= ?753 [753] by Demod 434 with 19 at 1,2
% 34.91/9.06 Id : 440, {_}: multiply (inverse (inverse ?753)) (inverse (inverse identity)) =>= ?753 [753] by Demod 439 with 19 at 2,2
% 34.91/9.06 Id : 441, {_}: multiply (inverse (inverse ?753)) (inverse identity) =>= ?753 [753] by Demod 440 with 385 at 1,2,2
% 34.91/9.06 Id : 442, {_}: multiply (inverse (inverse ?753)) identity =>= ?753 [753] by Demod 441 with 385 at 2,2
% 34.91/9.06 Id : 396, {_}: double_divide (double_divide (double_divide identity (double_divide ?211 identity)) (inverse identity)) (inverse identity) =>= ?211 [211] by Demod 88 with 385 at 2,2,1,1,2
% 34.91/9.06 Id : 397, {_}: double_divide (double_divide (double_divide identity (double_divide ?211 identity)) identity) (inverse identity) =>= ?211 [211] by Demod 396 with 385 at 2,1,2
% 34.91/9.06 Id : 398, {_}: double_divide (double_divide (double_divide identity (double_divide ?211 identity)) identity) identity =>= ?211 [211] by Demod 397 with 385 at 2,2
% 34.91/9.06 Id : 422, {_}: inverse (double_divide (double_divide identity (double_divide ?211 identity)) identity) =>= ?211 [211] by Demod 398 with 4 at 2
% 34.91/9.06 Id : 423, {_}: multiply identity (double_divide identity (double_divide ?211 identity)) =>= ?211 [211] by Demod 422 with 16 at 2
% 34.91/9.06 Id : 424, {_}: inverse (inverse (double_divide identity (double_divide ?211 identity))) =>= ?211 [211] by Demod 423 with 19 at 2
% 34.91/9.06 Id : 425, {_}: inverse (multiply (double_divide ?211 identity) identity) =>= ?211 [211] by Demod 424 with 16 at 1,2
% 34.91/9.06 Id : 426, {_}: inverse (multiply (inverse ?211) identity) =>= ?211 [211] by Demod 425 with 4 at 1,1,2
% 34.91/9.06 Id : 11, {_}: double_divide (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) (double_divide identity identity))) (double_divide identity identity) =>= ?35 [35, 34, 33] by Super 2 with 3 at 2,1,2,1,2
% 34.91/9.06 Id : 460, {_}: double_divide (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) (inverse identity))) (double_divide identity identity) =>= ?35 [35, 34, 33] by Demod 11 with 4 at 2,2,1,2
% 34.91/9.06 Id : 461, {_}: double_divide (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) (inverse identity))) (inverse identity) =>= ?35 [35, 34, 33] by Demod 460 with 4 at 2,2
% 34.91/9.06 Id : 462, {_}: double_divide (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) identity)) (inverse identity) =>= ?35 [35, 34, 33] by Demod 461 with 385 at 2,2,1,2
% 34.91/9.06 Id : 463, {_}: double_divide (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) identity)) identity =>= ?35 [35, 34, 33] by Demod 462 with 385 at 2,2
% 34.91/9.06 Id : 464, {_}: inverse (double_divide (double_divide ?33 ?34) (double_divide (double_divide ?35 (multiply ?34 ?33)) identity)) =>= ?35 [35, 34, 33] by Demod 463 with 4 at 2
% 34.91/9.06 Id : 465, {_}: multiply (double_divide (double_divide ?35 (multiply ?34 ?33)) identity) (double_divide ?33 ?34) =>= ?35 [33, 34, 35] by Demod 464 with 16 at 2
% 34.91/9.06 Id : 466, {_}: multiply (inverse (double_divide ?35 (multiply ?34 ?33))) (double_divide ?33 ?34) =>= ?35 [33, 34, 35] by Demod 465 with 4 at 1,2
% 34.91/9.06 Id : 472, {_}: multiply (multiply (multiply ?777 ?778) ?779) (double_divide ?778 ?777) =>= ?779 [779, 778, 777] by Demod 466 with 16 at 1,2
% 34.91/9.06 Id : 79, {_}: multiply (inverse ?191) ?191 =>= inverse identity [191] by Super 16 with 5 at 1,3
% 34.91/9.06 Id : 80, {_}: multiply (multiply ?193 ?194) (double_divide ?194 ?193) =>= inverse identity [194, 193] by Super 79 with 16 at 1,2
% 34.91/9.06 Id : 408, {_}: multiply (multiply ?193 ?194) (double_divide ?194 ?193) =>= identity [194, 193] by Demod 80 with 385 at 3
% 34.91/9.06 Id : 484, {_}: multiply identity (double_divide ?826 ?827) =>= double_divide ?826 ?827 [827, 826] by Super 472 with 408 at 1,2
% 34.91/9.06 Id : 502, {_}: inverse (inverse (double_divide ?826 ?827)) =>= double_divide ?826 ?827 [827, 826] by Demod 484 with 19 at 2
% 34.91/9.06 Id : 503, {_}: inverse (multiply ?827 ?826) =>= double_divide ?826 ?827 [826, 827] by Demod 502 with 16 at 1,2
% 34.91/9.06 Id : 532, {_}: double_divide identity (inverse ?211) =>= ?211 [211] by Demod 426 with 503 at 2
% 34.91/9.07 Id : 540, {_}: inverse (multiply ?896 ?897) =>= double_divide ?897 ?896 [897, 896] by Demod 502 with 16 at 1,2
% 34.91/9.07 Id : 541, {_}: inverse (inverse (inverse ?899)) =>= double_divide ?899 identity [899] by Super 540 with 19 at 1,2
% 34.91/9.07 Id : 551, {_}: inverse (inverse (inverse ?899)) =>= inverse ?899 [899] by Demod 541 with 4 at 3
% 34.91/9.07 Id : 565, {_}: double_divide identity (inverse ?946) =>= inverse (inverse ?946) [946] by Super 532 with 551 at 2,2
% 34.91/9.07 Id : 573, {_}: ?946 =<= inverse (inverse ?946) [946] by Demod 565 with 532 at 2
% 34.91/9.07 Id : 586, {_}: multiply ?753 identity =>= ?753 [753] by Demod 442 with 573 at 1,2
% 34.91/9.07 Id : 587, {_}: multiply (multiply ?18 ?20) (inverse ?18) =>= ?20 [20, 18] by Demod 421 with 586 at 2,2
% 34.91/9.07 Id : 467, {_}: multiply (multiply (multiply ?34 ?33) ?35) (double_divide ?33 ?34) =>= ?35 [35, 33, 34] by Demod 466 with 16 at 1,2
% 34.91/9.07 Id : 20, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) (inverse identity))) (inverse identity) =>= ?53 [53, 52] by Super 18 with 4 at 2,1,2,1,2
% 34.91/9.07 Id : 661, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) (inverse identity) =>= ?53 [53, 52] by Demod 20 with 385 at 2,2,1,2
% 34.91/9.07 Id : 662, {_}: double_divide (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) identity =>= ?53 [53, 52] by Demod 661 with 385 at 2,2
% 34.91/9.07 Id : 663, {_}: inverse (double_divide ?52 (double_divide (double_divide ?53 (inverse ?52)) identity)) =>= ?53 [53, 52] by Demod 662 with 4 at 2
% 34.91/9.07 Id : 664, {_}: multiply (double_divide (double_divide ?53 (inverse ?52)) identity) ?52 =>= ?53 [52, 53] by Demod 663 with 16 at 2
% 34.91/9.07 Id : 665, {_}: multiply (inverse (double_divide ?53 (inverse ?52))) ?52 =>= ?53 [52, 53] by Demod 664 with 4 at 1,2
% 34.91/9.07 Id : 666, {_}: multiply (multiply (inverse ?52) ?53) ?52 =>= ?53 [53, 52] by Demod 665 with 16 at 1,2
% 34.91/9.07 Id : 670, {_}: multiply ?1053 (double_divide ?1053 (inverse ?1054)) =>= ?1054 [1054, 1053] by Super 467 with 666 at 1,2
% 34.91/9.07 Id : 870, {_}: multiply ?1253 (inverse ?1254) =<= double_divide ?1254 (inverse ?1253) [1254, 1253] by Super 587 with 670 at 1,2
% 34.91/9.07 Id : 905, {_}: multiply (inverse ?1300) ?1301 =<= inverse (multiply ?1300 (inverse ?1301)) [1301, 1300] by Super 16 with 870 at 1,3
% 34.91/9.07 Id : 924, {_}: multiply (inverse ?1300) ?1301 =<= double_divide (inverse ?1301) ?1300 [1301, 1300] by Demod 905 with 503 at 3
% 34.91/9.07 Id : 588, {_}: inverse ?22 =<= double_divide ?23 (double_divide (double_divide ?22 (double_divide ?23 ?24)) (inverse ?24)) [24, 23, 22] by Demod 420 with 586 at 2
% 34.91/9.07 Id : 896, {_}: inverse ?22 =<= double_divide ?23 (multiply ?24 (inverse (double_divide ?22 (double_divide ?23 ?24)))) [24, 23, 22] by Demod 588 with 870 at 2,3
% 34.91/9.07 Id : 901, {_}: inverse ?22 =<= double_divide ?23 (multiply ?24 (multiply (double_divide ?23 ?24) ?22)) [24, 23, 22] by Demod 896 with 16 at 2,2,3
% 34.91/9.07 Id : 46, {_}: multiply (inverse identity) (double_divide (double_divide ?87 (double_divide (double_divide ?88 (double_divide ?87 ?89)) (inverse ?89))) (double_divide (double_divide ?90 ?88) (multiply identity identity))) =>= inverse ?90 [90, 89, 88, 87] by Super 16 with 45 at 1,3
% 34.91/9.07 Id : 991, {_}: multiply identity (double_divide (double_divide ?87 (double_divide (double_divide ?88 (double_divide ?87 ?89)) (inverse ?89))) (double_divide (double_divide ?90 ?88) (multiply identity identity))) =>= inverse ?90 [90, 89, 88, 87] by Demod 46 with 385 at 1,2
% 34.91/9.07 Id : 992, {_}: multiply identity (double_divide (double_divide ?87 (multiply ?89 (inverse (double_divide ?88 (double_divide ?87 ?89))))) (double_divide (double_divide ?90 ?88) (multiply identity identity))) =>= inverse ?90 [90, 88, 89, 87] by Demod 991 with 870 at 2,1,2,2
% 34.91/9.07 Id : 585, {_}: multiply identity ?50 =>= ?50 [50] by Demod 19 with 573 at 3
% 34.91/9.07 Id : 993, {_}: multiply identity (double_divide (double_divide ?87 (multiply ?89 (inverse (double_divide ?88 (double_divide ?87 ?89))))) (double_divide (double_divide ?90 ?88) identity)) =>= inverse ?90 [90, 88, 89, 87] by Demod 992 with 585 at 2,2,2,2
% 34.91/9.07 Id : 994, {_}: double_divide (double_divide ?87 (multiply ?89 (inverse (double_divide ?88 (double_divide ?87 ?89))))) (double_divide (double_divide ?90 ?88) identity) =>= inverse ?90 [90, 88, 89, 87] by Demod 993 with 585 at 2
% 34.91/9.07 Id : 995, {_}: double_divide (double_divide ?87 (multiply ?89 (multiply (double_divide ?87 ?89) ?88))) (double_divide (double_divide ?90 ?88) identity) =>= inverse ?90 [90, 88, 89, 87] by Demod 994 with 16 at 2,2,1,2
% 34.91/9.07 Id : 996, {_}: double_divide (double_divide ?87 (multiply ?89 (multiply (double_divide ?87 ?89) ?88))) (inverse (double_divide ?90 ?88)) =>= inverse ?90 [90, 88, 89, 87] by Demod 995 with 4 at 2,2
% 34.91/9.07 Id : 997, {_}: multiply (double_divide ?90 ?88) (inverse (double_divide ?87 (multiply ?89 (multiply (double_divide ?87 ?89) ?88)))) =>= inverse ?90 [89, 87, 88, 90] by Demod 996 with 870 at 2
% 34.91/9.07 Id : 998, {_}: multiply (double_divide ?90 ?88) (multiply (multiply ?89 (multiply (double_divide ?87 ?89) ?88)) ?87) =>= inverse ?90 [87, 89, 88, 90] by Demod 997 with 16 at 2,2
% 34.91/9.07 Id : 402, {_}: double_divide (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) identity =>= ?3 [4, 3, 2] by Demod 18 with 385 at 2,2
% 34.91/9.07 Id : 416, {_}: inverse (double_divide ?2 (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4))) =>= ?3 [4, 3, 2] by Demod 402 with 4 at 2
% 34.91/9.07 Id : 417, {_}: multiply (double_divide (double_divide ?3 (double_divide ?2 ?4)) (inverse ?4)) ?2 =>= ?3 [4, 2, 3] by Demod 416 with 16 at 2
% 34.91/9.07 Id : 898, {_}: multiply (multiply ?4 (inverse (double_divide ?3 (double_divide ?2 ?4)))) ?2 =>= ?3 [2, 3, 4] by Demod 417 with 870 at 1,2
% 34.91/9.07 Id : 899, {_}: multiply (multiply ?4 (multiply (double_divide ?2 ?4) ?3)) ?2 =>= ?3 [3, 2, 4] by Demod 898 with 16 at 2,1,2
% 34.91/9.07 Id : 999, {_}: multiply (double_divide ?90 ?88) ?88 =>= inverse ?90 [88, 90] by Demod 998 with 899 at 2,2
% 34.91/9.07 Id : 1000, {_}: inverse ?1420 =<= double_divide ?1421 (multiply ?1420 (inverse ?1421)) [1421, 1420] by Super 901 with 999 at 2,2,3
% 34.91/9.07 Id : 1914, {_}: multiply (inverse (multiply ?2779 (inverse (inverse ?2780)))) ?2780 =>= inverse ?2779 [2780, 2779] by Super 924 with 1000 at 3
% 34.91/9.07 Id : 1946, {_}: multiply (double_divide (inverse (inverse ?2780)) ?2779) ?2780 =>= inverse ?2779 [2779, 2780] by Demod 1914 with 503 at 1,2
% 34.91/9.07 Id : 1947, {_}: multiply (multiply (inverse ?2779) (inverse ?2780)) ?2780 =>= inverse ?2779 [2780, 2779] by Demod 1946 with 924 at 1,2
% 34.91/9.07 Id : 430, {_}: multiply (inverse ?745) identity =<= double_divide ?746 (double_divide (double_divide ?745 (double_divide ?746 identity)) identity) [746, 745] by Super 420 with 385 at 2,2,3
% 34.91/9.07 Id : 451, {_}: multiply (inverse ?745) identity =<= double_divide ?746 (inverse (double_divide ?745 (double_divide ?746 identity))) [746, 745] by Demod 430 with 4 at 2,3
% 34.91/9.07 Id : 452, {_}: multiply (inverse ?745) identity =<= double_divide ?746 (multiply (double_divide ?746 identity) ?745) [746, 745] by Demod 451 with 16 at 2,3
% 34.91/9.07 Id : 453, {_}: multiply (inverse ?745) identity =<= double_divide ?746 (multiply (inverse ?746) ?745) [746, 745] by Demod 452 with 4 at 1,2,3
% 34.91/9.07 Id : 811, {_}: inverse ?745 =<= double_divide ?746 (multiply (inverse ?746) ?745) [746, 745] by Demod 453 with 586 at 2
% 34.91/9.07 Id : 872, {_}: inverse (double_divide (inverse ?1259) (inverse ?1260)) =>= double_divide ?1259 ?1260 [1260, 1259] by Super 811 with 670 at 2,3
% 34.91/9.07 Id : 883, {_}: multiply (inverse ?1260) (inverse ?1259) =>= double_divide ?1259 ?1260 [1259, 1260] by Demod 872 with 16 at 2
% 34.91/9.07 Id : 2013, {_}: multiply (double_divide ?2913 ?2914) ?2913 =>= inverse ?2914 [2914, 2913] by Demod 1947 with 883 at 1,2
% 34.91/9.07 Id : 1008, {_}: inverse (inverse ?1447) =<= double_divide ?1448 (double_divide ?1447 ?1448) [1448, 1447] by Super 503 with 999 at 1,2
% 34.91/9.07 Id : 1023, {_}: ?1447 =<= double_divide ?1448 (double_divide ?1447 ?1448) [1448, 1447] by Demod 1008 with 573 at 2
% 34.91/9.07 Id : 2022, {_}: multiply ?2939 ?2940 =<= inverse (double_divide ?2939 ?2940) [2940, 2939] by Super 2013 with 1023 at 1,2
% 34.91/9.07 Id : 2068, {_}: multiply ?2939 ?2940 =?= multiply ?2940 ?2939 [2940, 2939] by Demod 2022 with 16 at 3
% 34.91/9.07 Id : 873, {_}: multiply ?1262 (double_divide ?1262 (inverse ?1263)) =>= ?1263 [1263, 1262] by Super 467 with 666 at 1,2
% 34.91/9.07 Id : 877, {_}: multiply ?1275 (double_divide ?1275 ?1276) =>= inverse ?1276 [1276, 1275] by Super 873 with 573 at 2,2,2
% 34.91/9.07 Id : 1108, {_}: inverse (inverse ?1589) =<= double_divide (double_divide ?1590 ?1589) ?1590 [1590, 1589] by Super 503 with 877 at 1,2
% 34.91/9.07 Id : 1226, {_}: ?1757 =<= double_divide (double_divide ?1758 ?1757) ?1758 [1758, 1757] by Demod 1108 with 573 at 2
% 34.91/9.07 Id : 1232, {_}: multiply ?1773 (multiply (double_divide ?1774 ?1773) ?1775) =>= double_divide (inverse ?1775) ?1774 [1775, 1774, 1773] by Super 1226 with 901 at 1,3
% 34.91/9.07 Id : 5586, {_}: multiply ?7908 (multiply (double_divide ?7909 ?7908) ?7910) =>= multiply (inverse ?7909) ?7910 [7910, 7909, 7908] by Demod 1232 with 924 at 3
% 34.91/9.07 Id : 1099, {_}: inverse (double_divide (double_divide ?1557 ?1558) ?1559) =<= double_divide ?1557 (multiply ?1558 (inverse ?1559)) [1559, 1558, 1557] by Super 901 with 877 at 2,2,3
% 34.91/9.07 Id : 1133, {_}: multiply ?1559 (double_divide ?1557 ?1558) =<= double_divide ?1557 (multiply ?1558 (inverse ?1559)) [1558, 1557, 1559] by Demod 1099 with 16 at 2
% 34.91/9.07 Id : 3884, {_}: multiply ?5467 (double_divide ?5468 ?5469) =<= double_divide ?5468 (multiply (inverse ?5467) ?5469) [5469, 5468, 5467] by Super 1133 with 2068 at 2,3
% 34.91/9.07 Id : 4029, {_}: multiply (inverse (multiply (inverse ?5751) ?5752)) ?5753 =>= multiply ?5751 (double_divide (inverse ?5753) ?5752) [5753, 5752, 5751] by Super 924 with 3884 at 3
% 34.91/9.07 Id : 4081, {_}: multiply (double_divide ?5752 (inverse ?5751)) ?5753 =>= multiply ?5751 (double_divide (inverse ?5753) ?5752) [5753, 5751, 5752] by Demod 4029 with 503 at 1,2
% 34.91/9.07 Id : 4082, {_}: multiply (double_divide ?5752 (inverse ?5751)) ?5753 =>= multiply ?5751 (multiply (inverse ?5752) ?5753) [5753, 5751, 5752] by Demod 4081 with 924 at 2,3
% 34.91/9.07 Id : 4083, {_}: multiply (multiply ?5751 (inverse ?5752)) ?5753 =>= multiply ?5751 (multiply (inverse ?5752) ?5753) [5753, 5752, 5751] by Demod 4082 with 870 at 1,2
% 34.91/9.07 Id : 2468, {_}: multiply (multiply ?3562 (inverse ?3563)) ?3564 =>= double_divide (double_divide ?3564 ?3562) ?3563 [3564, 3563, 3562] by Super 899 with 877 at 2,1,2
% 34.91/9.07 Id : 2472, {_}: multiply (multiply ?3579 ?3580) ?3581 =<= double_divide (double_divide ?3581 ?3579) (inverse ?3580) [3581, 3580, 3579] by Super 2468 with 573 at 2,1,2
% 34.91/9.07 Id : 2526, {_}: multiply (multiply ?3579 ?3580) ?3581 =<= multiply ?3580 (inverse (double_divide ?3581 ?3579)) [3581, 3580, 3579] by Demod 2472 with 870 at 3
% 34.91/9.07 Id : 2527, {_}: multiply (multiply ?3579 ?3580) ?3581 =>= multiply ?3580 (multiply ?3579 ?3581) [3581, 3580, 3579] by Demod 2526 with 16 at 2,3
% 34.91/9.07 Id : 4084, {_}: multiply (inverse ?5752) (multiply ?5751 ?5753) =?= multiply ?5751 (multiply (inverse ?5752) ?5753) [5753, 5751, 5752] by Demod 4083 with 2527 at 2
% 34.91/9.07 Id : 947, {_}: multiply (inverse ?1389) ?1390 =<= double_divide (inverse ?1390) ?1389 [1390, 1389] by Demod 905 with 503 at 3
% 34.91/9.07 Id : 948, {_}: multiply (inverse ?1392) (multiply ?1393 ?1394) =>= double_divide (double_divide ?1394 ?1393) ?1392 [1394, 1393, 1392] by Super 947 with 503 at 1,3
% 34.91/9.07 Id : 4085, {_}: double_divide (double_divide ?5753 ?5751) ?5752 =<= multiply ?5751 (multiply (inverse ?5752) ?5753) [5752, 5751, 5753] by Demod 4084 with 948 at 2
% 34.91/9.07 Id : 911, {_}: multiply ?1318 (inverse ?1319) =<= double_divide ?1319 (inverse ?1318) [1319, 1318] by Super 587 with 670 at 1,2
% 34.91/9.07 Id : 912, {_}: multiply (multiply ?1321 ?1322) (inverse ?1323) =>= double_divide ?1323 (double_divide ?1322 ?1321) [1323, 1322, 1321] by Super 911 with 503 at 2,3
% 34.91/9.07 Id : 2565, {_}: multiply ?1322 (multiply ?1321 (inverse ?1323)) =>= double_divide ?1323 (double_divide ?1322 ?1321) [1323, 1321, 1322] by Demod 912 with 2527 at 2
% 34.91/9.07 Id : 3886, {_}: multiply ?5475 (multiply (inverse ?5476) ?5477) =>= double_divide ?5476 (double_divide ?5475 ?5477) [5477, 5476, 5475] by Super 2565 with 2068 at 2,2
% 34.91/9.07 Id : 4309, {_}: double_divide (double_divide ?5753 ?5751) ?5752 =?= double_divide ?5752 (double_divide ?5751 ?5753) [5752, 5751, 5753] by Demod 4085 with 3886 at 3
% 34.91/9.07 Id : 5590, {_}: multiply ?7924 (multiply (double_divide ?7924 (double_divide ?7925 ?7926)) ?7927) =>= multiply (inverse (double_divide ?7926 ?7925)) ?7927 [7927, 7926, 7925, 7924] by Super 5586 with 4309 at 1,2,2
% 34.91/9.07 Id : 5683, {_}: multiply ?7924 (multiply (double_divide ?7924 (double_divide ?7925 ?7926)) ?7927) =>= multiply (multiply ?7925 ?7926) ?7927 [7927, 7926, 7925, 7924] by Demod 5590 with 16 at 1,3
% 34.91/9.07 Id : 5684, {_}: multiply ?7924 (multiply (double_divide ?7924 (double_divide ?7925 ?7926)) ?7927) =>= multiply ?7926 (multiply ?7925 ?7927) [7927, 7926, 7925, 7924] by Demod 5683 with 2527 at 3
% 34.91/9.07 Id : 2599, {_}: multiply (multiply ?3759 ?3760) ?3761 =>= multiply ?3760 (multiply ?3759 ?3761) [3761, 3760, 3759] by Demod 2526 with 16 at 2,3
% 34.91/9.07 Id : 1948, {_}: multiply (double_divide ?2780 ?2779) ?2780 =>= inverse ?2779 [2779, 2780] by Demod 1947 with 883 at 1,2
% 34.91/9.07 Id : 2611, {_}: multiply (inverse ?3808) ?3809 =<= multiply ?3810 (multiply (double_divide ?3810 ?3808) ?3809) [3810, 3809, 3808] by Super 2599 with 1948 at 1,2
% 34.91/9.07 Id : 67119, {_}: multiply (inverse (double_divide ?7925 ?7926)) ?7927 =>= multiply ?7926 (multiply ?7925 ?7927) [7927, 7926, 7925] by Demod 5684 with 2611 at 2
% 34.91/9.07 Id : 67120, {_}: multiply (multiply ?7926 ?7925) ?7927 =>= multiply ?7926 (multiply ?7925 ?7927) [7927, 7925, 7926] by Demod 67119 with 16 at 1,2
% 34.91/9.07 Id : 67121, {_}: multiply ?7925 (multiply ?7926 ?7927) =?= multiply ?7926 (multiply ?7925 ?7927) [7927, 7926, 7925] by Demod 67120 with 2527 at 2
% 34.91/9.07 Id : 68038, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 68037 with 2068 at 2,2
% 34.91/9.07 Id : 68037, {_}: multiply a3 (multiply c3 b3) =?= multiply a3 (multiply b3 c3) [] by Demod 68036 with 67121 at 2
% 34.91/9.07 Id : 68036, {_}: multiply c3 (multiply a3 b3) =>= multiply a3 (multiply b3 c3) [] by Demod 1 with 2068 at 2
% 34.91/9.07 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 34.91/9.07 % SZS output end CNFRefutation for theBenchmark.p
% 34.91/9.07 29663: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 8.73123 using kbo
%------------------------------------------------------------------------------