%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP195-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n019.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:29:35 EDT 2022
% Result : Unsatisfiable 0.21s 0.47s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP195-1 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.14 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Mon Jun 13 10:12:54 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.36 25340: Facts:
% 0.13/0.36 25340: Id : 2, {_}:
% 0.13/0.36 multiply (multiply ?2 ?3) ?4 =?= multiply ?2 (multiply ?3 ?4)
% 0.13/0.36 [4, 3, 2] by associativity_of_multiply ?2 ?3 ?4
% 0.13/0.36 25340: Id : 3, {_}:
% 0.13/0.36 multiply ?6 (multiply ?7 ?7) =?= multiply ?7 (multiply ?7 ?6)
% 0.13/0.36 [7, 6] by condition ?6 ?7
% 0.13/0.36 25340: Goal:
% 0.13/0.36 25340: Id : 1, {_}:
% 0.13/0.36 multiply a
% 0.13/0.36 (multiply b
% 0.13/0.36 (multiply a
% 0.13/0.36 (multiply b (multiply a (multiply b (multiply a b))))))
% 0.13/0.36 =>=
% 0.13/0.36 multiply a
% 0.13/0.36 (multiply a
% 0.13/0.36 (multiply a
% 0.13/0.36 (multiply a (multiply b (multiply b (multiply b b))))))
% 0.13/0.36 [] by prove_this
% 0.21/0.47 Statistics :
% 0.21/0.47 Max weight : 30
% 0.21/0.47 Found proof, 0.110849s
% 0.21/0.47 % SZS status Unsatisfiable for theBenchmark.p
% 0.21/0.47 % SZS output start CNFRefutation for theBenchmark.p
% 0.21/0.47 Id : 3, {_}: multiply ?6 (multiply ?7 ?7) =?= multiply ?7 (multiply ?7 ?6) [7, 6] by condition ?6 ?7
% 0.21/0.47 Id : 2, {_}: multiply (multiply ?2 ?3) ?4 =>= multiply ?2 (multiply ?3 ?4) [4, 3, 2] by associativity_of_multiply ?2 ?3 ?4
% 0.21/0.47 Id : 13, {_}: multiply ?34 (multiply (multiply ?35 ?36) (multiply ?35 ?36)) =?= multiply ?35 (multiply ?36 (multiply (multiply ?35 ?36) ?34)) [36, 35, 34] by Super 2 with 3 at 2
% 0.21/0.47 Id : 30, {_}: multiply ?34 (multiply ?35 (multiply ?36 (multiply ?35 ?36))) =?= multiply ?35 (multiply ?36 (multiply (multiply ?35 ?36) ?34)) [36, 35, 34] by Demod 13 with 2 at 2,2
% 0.21/0.47 Id : 31, {_}: multiply ?34 (multiply ?35 (multiply ?36 (multiply ?35 ?36))) =?= multiply ?35 (multiply ?36 (multiply ?35 (multiply ?36 ?34))) [36, 35, 34] by Demod 30 with 2 at 2,2,3
% 0.21/0.47 Id : 10, {_}: multiply (multiply ?22 (multiply ?22 ?23)) ?24 =>= multiply ?23 (multiply (multiply ?22 ?22) ?24) [24, 23, 22] by Super 2 with 3 at 1,2
% 0.21/0.47 Id : 24, {_}: multiply ?22 (multiply (multiply ?22 ?23) ?24) =?= multiply ?23 (multiply (multiply ?22 ?22) ?24) [24, 23, 22] by Demod 10 with 2 at 2
% 0.21/0.47 Id : 25, {_}: multiply ?22 (multiply (multiply ?22 ?23) ?24) =?= multiply ?23 (multiply ?22 (multiply ?22 ?24)) [24, 23, 22] by Demod 24 with 2 at 2,3
% 0.21/0.47 Id : 26, {_}: multiply ?22 (multiply ?22 (multiply ?23 ?24)) =?= multiply ?23 (multiply ?22 (multiply ?22 ?24)) [24, 23, 22] by Demod 25 with 2 at 2,2
% 0.21/0.47 Id : 12, {_}: multiply ?30 (multiply ?30 (multiply ?31 ?32)) =?= multiply ?31 (multiply ?32 (multiply ?30 ?30)) [32, 31, 30] by Super 2 with 3 at 2
% 0.21/0.47 Id : 669, {_}: multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) =?= multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) [] by Demod 668 with 2 at 2,2,2,2,2
% 0.21/0.47 Id : 668, {_}: multiply a (multiply a (multiply a (multiply a (multiply (multiply b b) (multiply b b))))) =?= multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) [] by Demod 667 with 12 at 2,2,2,2
% 0.21/0.47 Id : 667, {_}: multiply a (multiply a (multiply a (multiply b (multiply b (multiply a (multiply b b)))))) =?= multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) [] by Demod 666 with 26 at 2,2
% 0.21/0.47 Id : 666, {_}: multiply a (multiply b (multiply a (multiply a (multiply b (multiply a (multiply b b)))))) =?= multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) [] by Demod 1 with 31 at 2,2,2,2
% 0.21/0.47 Id : 1, {_}: multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b)))))) =?= multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))) [] by prove_this
% 0.21/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.47 25341: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.112651 using kbo
%------------------------------------------------------------------------------