%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP531-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 : n028.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:39 EDT 2022
% Result : Unsatisfiable 0.19s 0.37s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP531-1 : TPTP v8.1.0. Released v2.6.0.
% 0.11/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.12/0.33 % Computer : n028.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 09:44:53 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.34 31319: Facts:
% 0.19/0.34 31319: Id : 2, {_}:
% 0.19/0.34 divide (divide ?2 (divide ?3 ?4)) (divide ?2 ?3) =>= ?4
% 0.19/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.19/0.34 31319: Id : 3, {_}:
% 0.19/0.34 multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
% 0.19/0.34 [8, 7, 6] by multiply ?6 ?7 ?8
% 0.19/0.34 31319: Id : 4, {_}:
% 0.19/0.34 inverse ?10 =<= divide (divide ?11 ?11) ?10
% 0.19/0.34 [11, 10] by inverse ?10 ?11
% 0.19/0.34 31319: Goal:
% 0.19/0.34 31319: Id : 1, {_}:
% 0.19/0.34 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
% 0.19/0.34 [] by prove_these_axioms_3
% 0.19/0.37 Statistics :
% 0.19/0.37 Max weight : 14
% 0.19/0.37 Found proof, 0.029368s
% 0.19/0.37 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.37 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.37 Id : 3, {_}: multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7) [8, 7, 6] by multiply ?6 ?7 ?8
% 0.19/0.37 Id : 4, {_}: inverse ?10 =<= divide (divide ?11 ?11) ?10 [11, 10] by inverse ?10 ?11
% 0.19/0.37 Id : 2, {_}: divide (divide ?2 (divide ?3 ?4)) (divide ?2 ?3) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.19/0.37 Id : 5, {_}: divide (divide ?13 (divide ?14 ?15)) (divide ?13 ?14) =>= ?15 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 0.19/0.37 Id : 8, {_}: divide ?27 (divide (divide ?28 (divide ?29 ?27)) ?28) =>= ?29 [29, 28, 27] by Super 5 with 2 at 1,2
% 0.19/0.37 Id : 43, {_}: inverse (divide (divide ?126 ?127) ?126) =>= ?127 [127, 126] by Super 2 with 4 at 2
% 0.19/0.37 Id : 83, {_}: inverse (inverse ?276) =>= ?276 [276] by Super 43 with 4 at 1,2
% 0.19/0.37 Id : 25, {_}: inverse (divide (divide ?91 ?92) ?91) =>= ?92 [92, 91] by Super 2 with 4 at 2
% 0.19/0.37 Id : 84, {_}: inverse ?278 =<= divide (divide ?279 ?278) ?279 [279, 278] by Super 83 with 25 at 1,2
% 0.19/0.37 Id : 205, {_}: divide ?27 (inverse (divide ?29 ?27)) =>= ?29 [29, 27] by Demod 8 with 84 at 2,2
% 0.19/0.37 Id : 20, {_}: multiply ?6 ?7 =<= divide ?6 (inverse ?7) [7, 6] by Demod 3 with 4 at 2,3
% 0.19/0.37 Id : 210, {_}: multiply ?691 (divide ?692 ?691) =>= ?692 [692, 691] by Demod 205 with 20 at 2
% 0.19/0.37 Id : 405, {_}: multiply (divide ?1010 ?1011) ?1012 =<= divide ?1010 (divide ?1011 ?1012) [1012, 1011, 1010] by Super 210 with 2 at 2,2
% 0.19/0.37 Id : 150, {_}: inverse ?529 =<= divide (divide ?530 ?529) ?530 [530, 529] by Super 83 with 25 at 1,2
% 0.19/0.37 Id : 155, {_}: inverse (inverse ?549) =<= divide (multiply ?550 ?549) ?550 [550, 549] by Super 150 with 20 at 1,3
% 0.19/0.37 Id : 47, {_}: inverse (inverse ?139) =>= ?139 [139] by Super 43 with 4 at 1,2
% 0.19/0.37 Id : 167, {_}: ?549 =<= divide (multiply ?550 ?549) ?550 [550, 549] by Demod 155 with 47 at 2
% 0.19/0.37 Id : 179, {_}: inverse ?612 =<= divide ?613 (multiply ?612 ?613) [613, 612] by Super 84 with 167 at 1,3
% 0.19/0.37 Id : 186, {_}: inverse (multiply ?629 ?630) =<= divide (inverse ?629) ?630 [630, 629] by Super 84 with 179 at 1,3
% 0.19/0.37 Id : 411, {_}: multiply (divide ?1034 (inverse ?1035)) ?1036 =<= divide ?1034 (inverse (multiply ?1035 ?1036)) [1036, 1035, 1034] by Super 405 with 186 at 2,3
% 0.19/0.37 Id : 439, {_}: multiply (multiply ?1034 ?1035) ?1036 =<= divide ?1034 (inverse (multiply ?1035 ?1036)) [1036, 1035, 1034] by Demod 411 with 20 at 1,2
% 0.19/0.37 Id : 440, {_}: multiply (multiply ?1034 ?1035) ?1036 =>= multiply ?1034 (multiply ?1035 ?1036) [1036, 1035, 1034] by Demod 439 with 20 at 3
% 0.19/0.37 Id : 602, {_}: multiply a3 (multiply b3 c3) =?= multiply a3 (multiply b3 c3) [] by Demod 1 with 440 at 2
% 0.19/0.37 Id : 1, {_}: multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3) [] by prove_these_axioms_3
% 0.19/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.37 31320: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 0.030902 using kbo
%------------------------------------------------------------------------------