%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP715-10 : TPTP v8.1.0. Released v8.1.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:31:45 EDT 2022
% Result : Unsatisfiable 4.04s 1.34s
% Output : CNFRefutation 4.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP715-10 : TPTP v8.1.0. Released v8.1.0.
% 0.07/0.13 % 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 : Tue Jun 14 08:21:24 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 3312: Facts:
% 0.13/0.35 3312: Id : 2, {_}:
% 0.13/0.35 plus (plus ?2 ?3) ?4 =?= plus ?2 (plus ?3 ?4)
% 0.13/0.35 [4, 3, 2] by f01 ?2 ?3 ?4
% 0.13/0.35 3312: Id : 3, {_}: plus ?6 ?7 =?= plus ?7 ?6 [7, 6] by f02 ?6 ?7
% 0.13/0.35 3312: Id : 4, {_}: plus ?9 op_0 =>= ?9 [9] by f03 ?9
% 0.13/0.35 3312: Id : 5, {_}: plus ?11 (minus ?11) =>= op_0 [11] by f04 ?11
% 0.13/0.35 3312: Id : 6, {_}:
% 0.13/0.35 mult ?13 (plus ?14 ?15) =<= plus (mult ?13 ?14) (mult ?13 ?15)
% 0.13/0.35 [15, 14, 13] by f05 ?13 ?14 ?15
% 0.13/0.35 3312: Id : 7, {_}:
% 0.13/0.35 mult (mult (mult ?17 ?18) ?19) ?18
% 0.13/0.35 =?=
% 0.13/0.35 mult ?17 (mult (mult ?18 ?19) ?18)
% 0.13/0.35 [19, 18, 17] by f06 ?17 ?18 ?19
% 0.13/0.35 3312: Id : 8, {_}:
% 0.13/0.35 mult ?21 (mult ?22 ?22) =?= mult (mult ?21 ?22) ?22
% 0.13/0.35 [22, 21] by f07 ?21 ?22
% 0.13/0.35 3312: Id : 9, {_}: mult ?24 unit =>= ?24 [24] by f08 ?24
% 0.13/0.35 3312: Id : 10, {_}: mult unit ?26 =>= ?26 [26] by f09 ?26
% 0.13/0.35 3312: Id : 11, {_}: mult op_a op_b =>= unit [] by f10
% 0.13/0.35 3312: Id : 12, {_}: mult op_b op_a =>= unit [] by f11
% 0.13/0.35 3312: Goal:
% 0.13/0.35 3312: Id : 1, {_}: mult (mult x0 op_a) op_b =>= x0 [] by goal
% 4.04/1.34 Statistics :
% 4.04/1.34 Max weight : 20
% 4.04/1.34 Found proof, 0.989889s
% 4.04/1.34 % SZS status Unsatisfiable for theBenchmark.p
% 4.04/1.34 % SZS output start CNFRefutation for theBenchmark.p
% 4.04/1.34 Id : 9, {_}: mult ?24 unit =>= ?24 [24] by f08 ?24
% 4.04/1.34 Id : 12, {_}: mult op_b op_a =>= unit [] by f11
% 4.04/1.34 Id : 8, {_}: mult ?21 (mult ?22 ?22) =<= mult (mult ?21 ?22) ?22 [22, 21] by f07 ?21 ?22
% 4.04/1.34 Id : 10, {_}: mult unit ?26 =>= ?26 [26] by f09 ?26
% 4.04/1.34 Id : 11, {_}: mult op_a op_b =>= unit [] by f10
% 4.04/1.34 Id : 65, {_}: mult (mult (mult ?149 ?150) ?151) ?150 =>= mult ?149 (mult (mult ?150 ?151) ?150) [151, 150, 149] by f06 ?149 ?150 ?151
% 4.04/1.34 Id : 7, {_}: mult (mult (mult ?17 ?18) ?19) ?18 =>= mult ?17 (mult (mult ?18 ?19) ?18) [19, 18, 17] by f06 ?17 ?18 ?19
% 4.04/1.34 Id : 1533, {_}: mult (mult (mult ?1735 (mult (mult ?1736 ?1737) ?1736)) ?1738) ?1736 =>= mult (mult (mult ?1735 ?1736) ?1737) (mult (mult ?1736 ?1738) ?1736) [1738, 1737, 1736, 1735] by Super 65 with 7 at 1,1,2
% 4.04/1.34 Id : 149, {_}: mult (mult unit ?258) op_b =>= mult op_a (mult (mult op_b ?258) op_b) [258] by Super 7 with 11 at 1,1,2
% 4.04/1.34 Id : 280, {_}: mult ?476 op_b =<= mult op_a (mult (mult op_b ?476) op_b) [476] by Demod 149 with 10 at 1,2
% 4.04/1.34 Id : 285, {_}: mult op_b op_b =<= mult op_a (mult op_b (mult op_b op_b)) [] by Super 280 with 8 at 2,3
% 4.04/1.34 Id : 1563, {_}: mult (mult (mult ?1848 (mult (mult op_b op_b) op_a)) ?1849) op_a =>= mult (mult (mult ?1848 op_a) (mult op_b (mult op_b op_b))) (mult (mult op_a ?1849) op_a) [1849, 1848] by Super 1533 with 285 at 1,2,1,1,2
% 4.04/1.34 Id : 156, {_}: mult (mult unit ?264) op_a =>= mult op_b (mult (mult op_a ?264) op_a) [264] by Super 7 with 12 at 1,1,2
% 4.04/1.34 Id : 417, {_}: mult ?751 op_a =<= mult op_b (mult (mult op_a ?751) op_a) [751] by Demod 156 with 10 at 1,2
% 4.04/1.34 Id : 150, {_}: mult op_a (mult op_b op_b) =<= mult unit op_b [] by Super 8 with 11 at 1,3
% 4.04/1.34 Id : 153, {_}: mult op_a (mult op_b op_b) =>= op_b [] by Demod 150 with 10 at 3
% 4.04/1.34 Id : 421, {_}: mult (mult op_b op_b) op_a =>= mult op_b (mult op_b op_a) [] by Super 417 with 153 at 1,2,3
% 4.04/1.34 Id : 431, {_}: mult (mult op_b op_b) op_a =>= mult op_b unit [] by Demod 421 with 12 at 2,3
% 4.04/1.34 Id : 432, {_}: mult (mult op_b op_b) op_a =>= op_b [] by Demod 431 with 9 at 3
% 4.04/1.34 Id : 2523, {_}: mult (mult (mult ?2817 op_b) ?2818) op_a =>= mult (mult (mult ?2817 op_a) (mult op_b (mult op_b op_b))) (mult (mult op_a ?2818) op_a) [2818, 2817] by Demod 1563 with 432 at 2,1,1,2
% 4.04/1.34 Id : 2552, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =<= mult (mult (mult ?2888 op_a) (mult op_b (mult op_b op_b))) (mult (mult op_a op_b) op_a) [2888] by Super 2523 with 8 at 1,2
% 4.04/1.34 Id : 2615, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =<= mult (mult (mult ?2888 op_a) (mult op_b (mult op_b op_b))) (mult unit op_a) [2888] by Demod 2552 with 11 at 1,2,3
% 4.04/1.34 Id : 2616, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =<= mult (mult (mult ?2888 op_a) (mult op_b (mult op_b op_b))) op_a [2888] by Demod 2615 with 10 at 2,3
% 4.04/1.34 Id : 2617, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =?= mult ?2888 (mult (mult op_a (mult op_b (mult op_b op_b))) op_a) [2888] by Demod 2616 with 7 at 3
% 4.04/1.34 Id : 2618, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =>= mult ?2888 (mult (mult op_b op_b) op_a) [2888] by Demod 2617 with 285 at 1,2,3
% 4.04/1.34 Id : 2619, {_}: mult (mult ?2888 (mult op_b op_b)) op_a =>= mult ?2888 op_b [2888] by Demod 2618 with 432 at 2,3
% 4.04/1.34 Id : 2645, {_}: mult (mult ?2929 op_a) op_b =?= mult ?2929 (mult (mult op_a (mult op_b op_b)) op_a) [2929] by Super 7 with 2619 at 2
% 4.04/1.34 Id : 2674, {_}: mult (mult ?2929 op_a) op_b =>= mult ?2929 (mult op_a op_b) [2929] by Demod 2645 with 2619 at 2,3
% 4.04/1.34 Id : 2675, {_}: mult (mult ?2929 op_a) op_b =>= mult ?2929 unit [2929] by Demod 2674 with 11 at 2,3
% 4.04/1.34 Id : 2676, {_}: mult (mult ?2929 op_a) op_b =>= ?2929 [2929] by Demod 2675 with 9 at 3
% 4.04/1.34 Id : 2781, {_}: x0 === x0 [] by Demod 1 with 2676 at 2
% 4.04/1.34 Id : 1, {_}: mult (mult x0 op_a) op_b =>= x0 [] by goal
% 4.04/1.34 % SZS output end CNFRefutation for theBenchmark.p
% 4.04/1.34 3314: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.992056 using lpo
%------------------------------------------------------------------------------