%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP532-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n032.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:40 EDT 2022
% Result : Unsatisfiable 0.16s 0.35s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRP532-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.11/0.11 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 600
% 0.11/0.31 % DateTime : Mon Jun 13 23:48:42 EDT 2022
% 0.11/0.31 % CPUTime :
% 0.11/0.31 29508: Facts:
% 0.11/0.31 29508: Id : 2, {_}:
% 0.11/0.31 divide (divide ?2 (divide ?3 ?4)) (divide ?2 ?3) =>= ?4
% 0.11/0.31 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.11/0.31 29508: Id : 3, {_}:
% 0.11/0.31 multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
% 0.11/0.31 [8, 7, 6] by multiply ?6 ?7 ?8
% 0.11/0.31 29508: Id : 4, {_}:
% 0.11/0.31 inverse ?10 =<= divide (divide ?11 ?11) ?10
% 0.11/0.31 [11, 10] by inverse ?10 ?11
% 0.11/0.31 29508: Goal:
% 0.11/0.31 29508: Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.16/0.35 Statistics :
% 0.16/0.35 Max weight : 14
% 0.16/0.35 Found proof, 0.037850s
% 0.16/0.35 % SZS status Unsatisfiable for theBenchmark.p
% 0.16/0.35 % SZS output start CNFRefutation for theBenchmark.p
% 0.16/0.35 Id : 5, {_}: divide (divide ?13 (divide ?14 ?15)) (divide ?13 ?14) =>= ?15 [15, 14, 13] by single_axiom ?13 ?14 ?15
% 0.16/0.35 Id : 2, {_}: divide (divide ?2 (divide ?3 ?4)) (divide ?2 ?3) =>= ?4 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.16/0.35 Id : 4, {_}: inverse ?10 =<= divide (divide ?11 ?11) ?10 [11, 10] by inverse ?10 ?11
% 0.16/0.35 Id : 3, {_}: multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7) [8, 7, 6] by multiply ?6 ?7 ?8
% 0.16/0.35 Id : 20, {_}: multiply ?6 ?7 =<= divide ?6 (inverse ?7) [7, 6] by Demod 3 with 4 at 2,3
% 0.16/0.35 Id : 21, {_}: multiply (divide ?76 ?76) ?77 =>= inverse (inverse ?77) [77, 76] by Super 20 with 4 at 3
% 0.16/0.35 Id : 43, {_}: inverse (divide (divide ?126 ?127) ?126) =>= ?127 [127, 126] by Super 2 with 4 at 2
% 0.16/0.35 Id : 47, {_}: inverse (inverse ?139) =>= ?139 [139] by Super 43 with 4 at 1,2
% 0.16/0.35 Id : 81, {_}: multiply (divide ?76 ?76) ?77 =>= ?77 [77, 76] by Demod 21 with 47 at 3
% 0.16/0.35 Id : 88, {_}: multiply ?288 (inverse ?289) =>= divide ?288 ?289 [289, 288] by Super 20 with 47 at 2,3
% 0.16/0.35 Id : 25, {_}: inverse (divide (divide ?91 ?92) ?91) =>= ?92 [92, 91] by Super 2 with 4 at 2
% 0.16/0.35 Id : 89, {_}: multiply ?291 ?292 =<= divide ?291 (divide (divide ?293 ?292) ?293) [293, 292, 291] by Super 88 with 25 at 2,2
% 0.16/0.35 Id : 8, {_}: divide ?27 (divide (divide ?28 (divide ?29 ?27)) ?28) =>= ?29 [29, 28, 27] by Super 5 with 2 at 1,2
% 0.16/0.35 Id : 83, {_}: inverse (inverse ?276) =>= ?276 [276] by Super 43 with 4 at 1,2
% 0.16/0.35 Id : 84, {_}: inverse ?278 =<= divide (divide ?279 ?278) ?279 [279, 278] by Super 83 with 25 at 1,2
% 0.16/0.35 Id : 205, {_}: divide ?27 (inverse (divide ?29 ?27)) =>= ?29 [29, 27] by Demod 8 with 84 at 2,2
% 0.16/0.35 Id : 210, {_}: multiply ?691 (divide ?692 ?691) =>= ?692 [692, 691] by Demod 205 with 20 at 2
% 0.16/0.35 Id : 211, {_}: multiply (divide ?694 ?695) ?696 =<= divide ?694 (divide ?695 ?696) [696, 695, 694] by Super 210 with 2 at 2,2
% 0.16/0.35 Id : 860, {_}: multiply ?291 ?292 =<= multiply (divide ?291 (divide ?293 ?292)) ?293 [293, 292, 291] by Demod 89 with 211 at 3
% 0.16/0.35 Id : 861, {_}: multiply ?291 ?292 =<= multiply (multiply (divide ?291 ?293) ?292) ?293 [293, 292, 291] by Demod 860 with 211 at 1,3
% 0.16/0.35 Id : 405, {_}: multiply (divide ?1010 ?1011) ?1012 =<= divide ?1010 (divide ?1011 ?1012) [1012, 1011, 1010] by Super 210 with 2 at 2,2
% 0.16/0.35 Id : 150, {_}: inverse ?529 =<= divide (divide ?530 ?529) ?530 [530, 529] by Super 83 with 25 at 1,2
% 0.16/0.35 Id : 155, {_}: inverse (inverse ?549) =<= divide (multiply ?550 ?549) ?550 [550, 549] by Super 150 with 20 at 1,3
% 0.16/0.35 Id : 167, {_}: ?549 =<= divide (multiply ?550 ?549) ?550 [550, 549] by Demod 155 with 47 at 2
% 0.16/0.35 Id : 179, {_}: inverse ?612 =<= divide ?613 (multiply ?612 ?613) [613, 612] by Super 84 with 167 at 1,3
% 0.16/0.35 Id : 186, {_}: inverse (multiply ?629 ?630) =<= divide (inverse ?629) ?630 [630, 629] by Super 84 with 179 at 1,3
% 0.16/0.35 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.16/0.35 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.16/0.35 Id : 440, {_}: multiply (multiply ?1034 ?1035) ?1036 =>= multiply ?1034 (multiply ?1035 ?1036) [1036, 1035, 1034] by Demod 439 with 20 at 3
% 0.16/0.35 Id : 862, {_}: multiply ?291 ?292 =<= multiply (divide ?291 ?293) (multiply ?292 ?293) [293, 292, 291] by Demod 861 with 440 at 3
% 0.16/0.35 Id : 867, {_}: multiply ?1560 ?1561 =?= multiply ?1561 ?1560 [1561, 1560] by Super 81 with 862 at 2
% 0.16/0.35 Id : 1432, {_}: multiply a b =?= multiply a b [] by Demod 1 with 867 at 3
% 0.16/0.35 Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.16/0.35 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.35 29509: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.038981 using kbo
%------------------------------------------------------------------------------