%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP560-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 : n012.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:47 EDT 2022
% Result : Unsatisfiable 0.12s 0.38s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP560-1 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.10/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n012.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 : Mon Jun 13 23:47:55 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 8756: Facts:
% 0.12/0.34 8756: Id : 2, {_}:
% 0.12/0.34 divide ?2 (inverse (divide (divide ?3 ?4) (divide ?2 ?4))) =>= ?3
% 0.12/0.34 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.34 8756: Id : 3, {_}:
% 0.12/0.34 multiply ?6 ?7 =<= divide ?6 (inverse ?7)
% 0.12/0.34 [7, 6] by multiply ?6 ?7
% 0.12/0.34 8756: Goal:
% 0.12/0.34 8756: Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.12/0.38 Statistics :
% 0.12/0.38 Max weight : 22
% 0.12/0.38 Found proof, 0.041770s
% 0.12/0.38 % SZS status Unsatisfiable for theBenchmark.p
% 0.12/0.38 % SZS output start CNFRefutation for theBenchmark.p
% 0.12/0.38 Id : 2, {_}: divide ?2 (inverse (divide (divide ?3 ?4) (divide ?2 ?4))) =>= ?3 [4, 3, 2] by single_axiom ?2 ?3 ?4
% 0.12/0.38 Id : 4, {_}: divide ?9 (inverse (divide (divide ?10 ?11) (divide ?9 ?11))) =>= ?10 [11, 10, 9] by single_axiom ?9 ?10 ?11
% 0.12/0.38 Id : 3, {_}: multiply ?6 ?7 =<= divide ?6 (inverse ?7) [7, 6] by multiply ?6 ?7
% 0.12/0.38 Id : 5, {_}: divide ?13 (inverse (divide (divide ?14 (inverse (divide (divide ?15 ?16) (divide ?13 ?16)))) ?15)) =>= ?14 [16, 15, 14, 13] by Super 4 with 2 at 2,1,2,2
% 0.12/0.38 Id : 15, {_}: multiply ?13 (divide (divide ?14 (inverse (divide (divide ?15 ?16) (divide ?13 ?16)))) ?15) =>= ?14 [16, 15, 14, 13] by Demod 5 with 3 at 2
% 0.12/0.38 Id : 16, {_}: multiply ?13 (divide (multiply ?14 (divide (divide ?15 ?16) (divide ?13 ?16))) ?15) =>= ?14 [16, 15, 14, 13] by Demod 15 with 3 at 1,2,2
% 0.12/0.38 Id : 17, {_}: multiply ?39 (divide (multiply ?40 (divide (divide ?41 ?42) (divide ?39 ?42))) ?41) =>= ?40 [42, 41, 40, 39] by Demod 15 with 3 at 1,2,2
% 0.12/0.38 Id : 8, {_}: multiply ?2 (divide (divide ?3 ?4) (divide ?2 ?4)) =>= ?3 [4, 3, 2] by Demod 2 with 3 at 2
% 0.12/0.38 Id : 20, {_}: multiply ?54 (divide ?55 ?55) =>= ?54 [55, 54] by Super 17 with 8 at 1,2,2
% 0.12/0.38 Id : 34, {_}: multiply ?89 (divide ?90 ?89) =>= ?90 [90, 89] by Super 16 with 20 at 1,2,2
% 0.12/0.38 Id : 35, {_}: multiply (inverse ?92) (multiply ?93 ?92) =>= ?93 [93, 92] by Super 34 with 3 at 2,2
% 0.12/0.38 Id : 9, {_}: multiply ?25 (divide (divide ?26 (inverse ?27)) (multiply ?25 ?27)) =>= ?26 [27, 26, 25] by Super 8 with 3 at 2,2,2
% 0.12/0.38 Id : 13, {_}: multiply ?25 (divide (multiply ?26 ?27) (multiply ?25 ?27)) =>= ?26 [27, 26, 25] by Demod 9 with 3 at 1,2,2
% 0.12/0.38 Id : 59, {_}: multiply (inverse ?143) (multiply ?144 ?143) =>= ?144 [144, 143] by Super 34 with 3 at 2,2
% 0.12/0.38 Id : 62, {_}: multiply (inverse (divide ?155 ?155)) ?156 =>= ?156 [156, 155] by Super 59 with 20 at 2,2
% 0.12/0.38 Id : 111, {_}: multiply (inverse (divide ?288 ?288)) (divide (multiply ?289 ?290) ?290) =>= ?289 [290, 289, 288] by Super 13 with 62 at 2,2,2
% 0.12/0.38 Id : 159, {_}: divide (multiply ?420 ?421) ?421 =>= ?420 [421, 420] by Demod 111 with 62 at 2
% 0.12/0.38 Id : 26, {_}: multiply ?66 (divide ?67 ?66) =>= ?67 [67, 66] by Super 16 with 20 at 1,2,2
% 0.12/0.38 Id : 164, {_}: divide ?439 (divide ?439 ?440) =>= ?440 [440, 439] by Super 159 with 26 at 1,2
% 0.12/0.38 Id : 248, {_}: multiply (divide ?665 ?666) ?666 =>= ?665 [666, 665] by Super 8 with 164 at 2,2
% 0.12/0.38 Id : 471, {_}: multiply (inverse ?1320) ?1321 =<= divide ?1321 ?1320 [1321, 1320] by Super 35 with 248 at 2,2
% 0.12/0.38 Id : 511, {_}: multiply ?6 ?7 =?= multiply (inverse (inverse ?7)) ?6 [7, 6] by Demod 3 with 471 at 3
% 0.12/0.38 Id : 503, {_}: multiply (inverse (divide ?439 ?440)) ?439 =>= ?440 [440, 439] by Demod 164 with 471 at 2
% 0.12/0.38 Id : 504, {_}: multiply (inverse (multiply (inverse ?440) ?439)) ?439 =>= ?440 [439, 440] by Demod 503 with 471 at 1,1,2
% 0.12/0.38 Id : 537, {_}: multiply (inverse (inverse ?439)) (inverse (multiply (inverse ?440) ?439)) =>= ?440 [440, 439] by Demod 504 with 511 at 2
% 0.12/0.38 Id : 276, {_}: divide ?771 (multiply ?771 ?772) =>= inverse ?772 [772, 771] by Super 159 with 35 at 1,2
% 0.12/0.38 Id : 284, {_}: divide (inverse ?801) ?802 =>= inverse (multiply ?802 ?801) [802, 801] by Super 276 with 35 at 2,2
% 0.12/0.38 Id : 527, {_}: multiply (inverse ?802) (inverse ?801) =>= inverse (multiply ?802 ?801) [801, 802] by Demod 284 with 471 at 2
% 0.12/0.38 Id : 538, {_}: inverse (multiply (inverse ?439) (multiply (inverse ?440) ?439)) =>= ?440 [440, 439] by Demod 537 with 527 at 2
% 0.12/0.38 Id : 539, {_}: inverse (inverse ?440) =>= ?440 [440] by Demod 538 with 35 at 1,2
% 0.12/0.38 Id : 540, {_}: multiply ?6 ?7 =?= multiply ?7 ?6 [7, 6] by Demod 511 with 539 at 1,3
% 0.12/0.38 Id : 550, {_}: multiply a b === multiply a b [] by Demod 1 with 540 at 3
% 0.12/0.38 Id : 1, {_}: multiply a b =<= multiply b a [] by prove_these_axioms_4
% 0.12/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.38 8758: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.043783 using lpo
%------------------------------------------------------------------------------