%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP611-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 : n023.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:59 EDT 2022
% Result : Unsatisfiable 0.19s 0.54s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP611-1 : TPTP v8.1.0. Released v2.6.0.
% 0.11/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.34 % Computer : n023.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 : Tue Jun 14 02:34:06 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 19478: Facts:
% 0.13/0.34 19478: Id : 2, {_}:
% 0.13/0.34 inverse
% 0.13/0.34 (double_divide
% 0.13/0.34 (inverse (double_divide (inverse (double_divide ?2 ?3)) ?4))
% 0.13/0.34 (double_divide ?2 ?4))
% 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 19478: Id : 3, {_}:
% 0.13/0.34 multiply ?6 ?7 =<= inverse (double_divide ?7 ?6)
% 0.13/0.34 [7, 6] by multiply ?6 ?7
% 0.13/0.34 19478: Goal:
% 0.13/0.34 19478: 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
% 0.19/0.54 Statistics :
% 0.19/0.54 Max weight : 23
% 0.19/0.54 Found proof, 0.203343s
% 0.19/0.54 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.54 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.54 Id : 2, {_}: inverse (double_divide (inverse (double_divide (inverse (double_divide ?2 ?3)) ?4)) (double_divide ?2 ?4)) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.19/0.54 Id : 4, {_}: inverse (double_divide (inverse (double_divide (inverse (double_divide ?9 ?10)) ?11)) (double_divide ?9 ?11)) =>= ?10 [11, 10, 9] by single_axiom ?9 ?10 ?11
% 0.19/0.54 Id : 3, {_}: multiply ?6 ?7 =<= inverse (double_divide ?7 ?6) [7, 6] by multiply ?6 ?7
% 0.19/0.54 Id : 5, {_}: inverse (double_divide (inverse (double_divide ?13 ?14)) (double_divide (inverse (double_divide (inverse (double_divide ?15 ?13)) ?16)) ?14)) =>= double_divide ?15 ?16 [16, 15, 14, 13] by Super 4 with 2 at 1,1,1,1,2
% 0.19/0.54 Id : 13, {_}: multiply (double_divide (inverse (double_divide (inverse (double_divide ?15 ?13)) ?16)) ?14) (inverse (double_divide ?13 ?14)) =>= double_divide ?15 ?16 [14, 16, 13, 15] by Demod 5 with 3 at 2
% 0.19/0.54 Id : 14, {_}: multiply (double_divide (multiply ?16 (inverse (double_divide ?15 ?13))) ?14) (inverse (double_divide ?13 ?14)) =>= double_divide ?15 ?16 [14, 13, 15, 16] by Demod 13 with 3 at 1,1,2
% 0.19/0.54 Id : 15, {_}: multiply (double_divide (multiply ?16 (inverse (double_divide ?15 ?13))) ?14) (multiply ?14 ?13) =>= double_divide ?15 ?16 [14, 13, 15, 16] by Demod 14 with 3 at 2,2
% 0.19/0.54 Id : 16, {_}: multiply (double_divide (multiply ?16 (multiply ?13 ?15)) ?14) (multiply ?14 ?13) =>= double_divide ?15 ?16 [14, 15, 13, 16] by Demod 15 with 3 at 2,1,1,2
% 0.19/0.54 Id : 6, {_}: inverse (double_divide ?18 (double_divide (inverse (double_divide ?19 ?18)) (double_divide ?19 ?20))) =>= ?20 [20, 19, 18] by Super 4 with 2 at 1,1,2
% 0.19/0.54 Id : 27, {_}: multiply (double_divide (inverse (double_divide ?19 ?18)) (double_divide ?19 ?20)) ?18 =>= ?20 [20, 18, 19] by Demod 6 with 3 at 2
% 0.19/0.54 Id : 28, {_}: multiply (double_divide (multiply ?18 ?19) (double_divide ?19 ?20)) ?18 =>= ?20 [20, 19, 18] by Demod 27 with 3 at 1,1,2
% 0.19/0.54 Id : 32, {_}: ?104 =<= double_divide ?105 (multiply (double_divide (multiply ?106 ?105) ?104) ?106) [106, 105, 104] by Super 16 with 28 at 2
% 0.19/0.54 Id : 42, {_}: multiply (multiply (double_divide (multiply ?149 ?150) ?151) ?149) ?150 =>= inverse ?151 [151, 150, 149] by Super 3 with 32 at 1,3
% 0.19/0.54 Id : 8, {_}: multiply (double_divide ?2 ?4) (inverse (double_divide (inverse (double_divide ?2 ?3)) ?4)) =>= ?3 [3, 4, 2] by Demod 2 with 3 at 2
% 0.19/0.54 Id : 9, {_}: multiply (double_divide ?2 ?4) (multiply ?4 (inverse (double_divide ?2 ?3))) =>= ?3 [3, 4, 2] by Demod 8 with 3 at 2,2
% 0.19/0.54 Id : 10, {_}: multiply (double_divide ?2 ?4) (multiply ?4 (multiply ?3 ?2)) =>= ?3 [3, 4, 2] by Demod 9 with 3 at 2,2,2
% 0.19/0.54 Id : 103, {_}: multiply (multiply (double_divide (multiply ?512 ?513) ?514) ?512) ?513 =>= inverse ?514 [514, 513, 512] by Super 3 with 32 at 1,3
% 0.19/0.54 Id : 111, {_}: multiply (double_divide ?555 (multiply ?556 ?557)) (multiply ?557 ?555) =>= inverse ?556 [557, 556, 555] by Super 103 with 16 at 1,2
% 0.19/0.54 Id : 281, {_}: multiply (double_divide ?1397 (double_divide ?1397 (multiply ?1398 ?1399))) (inverse ?1398) =>= ?1399 [1399, 1398, 1397] by Super 10 with 111 at 2,2
% 0.19/0.54 Id : 417, {_}: multiply ?2064 ?2065 =<= inverse (double_divide (multiply (inverse ?2066) ?2065) (multiply ?2066 ?2064)) [2066, 2065, 2064] by Super 42 with 281 at 1,2
% 0.19/0.54 Id : 439, {_}: multiply ?2064 ?2065 =<= multiply (multiply ?2066 ?2064) (multiply (inverse ?2066) ?2065) [2066, 2065, 2064] by Demod 417 with 3 at 3
% 0.19/0.54 Id : 484, {_}: multiply ?2325 ?2326 =<= multiply (multiply ?2327 ?2325) (multiply (inverse ?2327) ?2326) [2327, 2326, 2325] by Demod 417 with 3 at 3
% 0.19/0.54 Id : 486, {_}: multiply (multiply ?2334 (multiply ?2335 ?2336)) ?2337 =?= multiply ?2335 (multiply (inverse (double_divide ?2336 ?2334)) ?2337) [2337, 2336, 2335, 2334] by Super 484 with 10 at 1,3
% 0.19/0.54 Id : 508, {_}: multiply (multiply ?2334 (multiply ?2335 ?2336)) ?2337 =>= multiply ?2335 (multiply (multiply ?2334 ?2336) ?2337) [2337, 2336, 2335, 2334] by Demod 486 with 3 at 1,2,3
% 0.19/0.54 Id : 523, {_}: multiply (multiply ?2436 ?2437) ?2438 =?= multiply ?2436 (multiply (multiply ?2439 ?2437) (multiply (inverse ?2439) ?2438)) [2439, 2438, 2437, 2436] by Super 439 with 508 at 3
% 0.19/0.54 Id : 584, {_}: multiply (multiply ?2436 ?2437) ?2438 =>= multiply ?2436 (multiply ?2437 ?2438) [2438, 2437, 2436] by Demod 523 with 439 at 2,3
% 0.19/0.54 Id : 716, {_}: multiply a3 (multiply b3 c3) === multiply a3 (multiply b3 c3) [] by Demod 1 with 584 at 2
% 0.19/0.54 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 0.19/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.54 19480: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.204888 using lpo
%------------------------------------------------------------------------------