%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : RNG128-1 : TPTP v8.1.0. Released v5.4.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 : Mon Jul 18 20:35:41 EDT 2022
% Result : Unsatisfiable 0.19s 0.42s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG128-1 : TPTP v8.1.0. Released v5.4.0.
% 0.11/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n019.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 May 30 10:07:25 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.34 30936: Facts:
% 0.19/0.34 30936: Id : 2, {_}:
% 0.19/0.34 add ?2 (add ?3 ?4) =?= add (add ?2 ?3) ?4
% 0.19/0.34 [4, 3, 2] by sos ?2 ?3 ?4
% 0.19/0.34 30936: Id : 3, {_}: add ?6 ?7 =?= add ?7 ?6 [7, 6] by sos_001 ?6 ?7
% 0.19/0.34 30936: Id : 4, {_}: mult ?9 ?10 =?= mult ?10 ?9 [10, 9] by sos_002 ?9 ?10
% 0.19/0.34 30936: Id : 5, {_}:
% 0.19/0.34 mult ?12 (add ?13 ?14) =<= add (mult ?12 ?13) (mult ?12 ?14)
% 0.19/0.34 [14, 13, 12] by sos_003 ?12 ?13 ?14
% 0.19/0.34 30936: Id : 6, {_}: add zero ?16 =>= ?16 [16] by sos_004 ?16
% 0.19/0.34 30936: Id : 7, {_}: mult ?18 unit =>= ?18 [18] by sos_005 ?18
% 0.19/0.34 30936: Id : 8, {_}: add unit (add ?20 (mult ?20 ?20)) =>= ?20 [20] by sos_006 ?20
% 0.19/0.34 30936: Goal:
% 0.19/0.34 30936: Id : 1, {_}: add x0 x1 =>= mult x0 x1 [] by goals
% 0.19/0.42 Statistics :
% 0.19/0.42 Max weight : 16
% 0.19/0.42 Found proof, 0.082901s
% 0.19/0.42 % SZS status Unsatisfiable for theBenchmark.p
% 0.19/0.42 % SZS output start CNFRefutation for theBenchmark.p
% 0.19/0.42 Id : 6, {_}: add zero ?16 =>= ?16 [16] by sos_004 ?16
% 0.19/0.42 Id : 3, {_}: add ?6 ?7 =?= add ?7 ?6 [7, 6] by sos_001 ?6 ?7
% 0.19/0.42 Id : 8, {_}: add unit (add ?20 (mult ?20 ?20)) =>= ?20 [20] by sos_006 ?20
% 0.19/0.42 Id : 73, {_}: add unit (add ?225 (mult ?225 ?225)) =>= ?225 [225] by sos_006 ?225
% 0.19/0.42 Id : 2, {_}: add ?2 (add ?3 ?4) =?= add (add ?2 ?3) ?4 [4, 3, 2] by sos ?2 ?3 ?4
% 0.19/0.42 Id : 4, {_}: mult ?9 ?10 =?= mult ?10 ?9 [10, 9] by sos_002 ?9 ?10
% 0.19/0.42 Id : 7, {_}: mult ?18 unit =>= ?18 [18] by sos_005 ?18
% 0.19/0.42 Id : 5, {_}: mult ?12 (add ?13 ?14) =<= add (mult ?12 ?13) (mult ?12 ?14) [14, 13, 12] by sos_003 ?12 ?13 ?14
% 0.19/0.42 Id : 272, {_}: mult ?420 (add unit ?421) =<= add ?420 (mult ?420 ?421) [421, 420] by Super 5 with 7 at 1,3
% 0.19/0.42 Id : 273, {_}: mult ?423 (add unit ?424) =<= add ?423 (mult ?424 ?423) [424, 423] by Super 272 with 4 at 2,3
% 0.19/0.42 Id : 74, {_}: add unit (add unit unit) =>= unit [] by Super 73 with 7 at 2,2,2
% 0.19/0.42 Id : 130, {_}: add unit (add (add unit unit) ?289) =>= add unit ?289 [289] by Super 2 with 74 at 1,3
% 0.19/0.42 Id : 317, {_}: add unit (add unit (add unit ?463)) =>= add unit ?463 [463] by Demod 130 with 2 at 2,2
% 0.19/0.42 Id : 64, {_}: mult ?205 (add unit ?206) =<= add ?205 (mult ?205 ?206) [206, 205] by Super 5 with 7 at 1,3
% 0.19/0.42 Id : 261, {_}: add unit (mult ?20 (add unit ?20)) =>= ?20 [20] by Demod 8 with 64 at 2,2
% 0.19/0.42 Id : 323, {_}: add unit (add unit ?472) =<= add unit (mult ?472 (add unit ?472)) [472] by Super 317 with 261 at 2,2,2
% 0.19/0.42 Id : 427, {_}: add unit (add unit ?500) =>= ?500 [500] by Demod 323 with 261 at 3
% 0.19/0.42 Id : 512, {_}: add unit ?561 =<= mult ?561 (add unit ?561) [561] by Super 427 with 261 at 2,2
% 0.19/0.42 Id : 56, {_}: add ?190 zero =>= ?190 [190] by Super 3 with 6 at 3
% 0.19/0.42 Id : 514, {_}: add unit zero =>= mult zero unit [] by Super 512 with 56 at 2,3
% 0.19/0.42 Id : 534, {_}: add zero unit =>= mult zero unit [] by Demod 514 with 3 at 2
% 0.19/0.42 Id : 535, {_}: add zero unit =>= zero [] by Demod 534 with 7 at 3
% 0.19/0.42 Id : 536, {_}: unit =>= zero [] by Demod 535 with 6 at 2
% 0.19/0.42 Id : 703, {_}: mult ?423 (add zero ?424) =<= add ?423 (mult ?424 ?423) [424, 423] by Demod 273 with 536 at 1,2,2
% 0.19/0.42 Id : 704, {_}: mult ?423 ?424 =<= add ?423 (mult ?424 ?423) [424, 423] by Demod 703 with 6 at 2,2
% 0.19/0.42 Id : 431, {_}: add unit ?506 =<= mult ?506 (add unit ?506) [506] by Super 427 with 261 at 2,2
% 0.19/0.42 Id : 506, {_}: mult ?548 (add ?549 (add unit ?548)) =<= add (mult ?548 ?549) (add unit ?548) [549, 548] by Super 5 with 431 at 2,3
% 0.19/0.42 Id : 1055, {_}: mult ?548 (add ?549 (add zero ?548)) =<= add (mult ?548 ?549) (add unit ?548) [549, 548] by Demod 506 with 536 at 1,2,2,2
% 0.19/0.42 Id : 1056, {_}: mult ?548 (add ?549 (add zero ?548)) =<= add (mult ?548 ?549) (add zero ?548) [549, 548] by Demod 1055 with 536 at 1,2,3
% 0.19/0.42 Id : 1057, {_}: mult ?548 (add ?549 ?548) =<= add (mult ?548 ?549) (add zero ?548) [549, 548] by Demod 1056 with 6 at 2,2,2
% 0.19/0.42 Id : 1058, {_}: mult ?548 (add ?549 ?548) =<= add (mult ?548 ?549) ?548 [549, 548] by Demod 1057 with 6 at 2,3
% 0.19/0.42 Id : 63, {_}: mult ?202 (add ?203 unit) =<= add (mult ?202 ?203) ?202 [203, 202] by Super 5 with 7 at 2,3
% 0.19/0.42 Id : 557, {_}: mult ?202 (add ?203 zero) =<= add (mult ?202 ?203) ?202 [203, 202] by Demod 63 with 536 at 2,2,2
% 0.19/0.42 Id : 577, {_}: mult ?202 ?203 =<= add (mult ?202 ?203) ?202 [203, 202] by Demod 557 with 56 at 2,2
% 0.19/0.42 Id : 1069, {_}: mult ?1134 (add ?1135 ?1134) =>= mult ?1134 ?1135 [1135, 1134] by Demod 1058 with 577 at 3
% 0.19/0.42 Id : 511, {_}: mult ?559 (add unit (add unit ?559)) =>= add ?559 (add unit ?559) [559] by Super 64 with 431 at 2,3
% 0.19/0.42 Id : 344, {_}: add unit (add unit ?472) =>= ?472 [472] by Demod 323 with 261 at 3
% 0.19/0.42 Id : 526, {_}: mult ?559 ?559 =<= add ?559 (add unit ?559) [559] by Demod 511 with 344 at 2,2
% 0.19/0.42 Id : 552, {_}: add zero ?506 =<= mult ?506 (add unit ?506) [506] by Demod 431 with 536 at 1,2
% 0.19/0.42 Id : 553, {_}: add zero ?506 =<= mult ?506 (add zero ?506) [506] by Demod 552 with 536 at 1,2,3
% 0.19/0.42 Id : 583, {_}: ?506 =<= mult ?506 (add zero ?506) [506] by Demod 553 with 6 at 2
% 0.19/0.42 Id : 584, {_}: ?506 =<= mult ?506 ?506 [506] by Demod 583 with 6 at 2,3
% 0.19/0.42 Id : 621, {_}: ?559 =<= add ?559 (add unit ?559) [559] by Demod 526 with 584 at 2
% 0.19/0.42 Id : 622, {_}: ?559 =<= add ?559 (add zero ?559) [559] by Demod 621 with 536 at 1,2,3
% 0.19/0.42 Id : 623, {_}: ?559 =<= add ?559 ?559 [559] by Demod 622 with 6 at 2,3
% 0.19/0.42 Id : 625, {_}: add ?587 (add ?587 ?588) =>= add ?587 ?588 [588, 587] by Super 2 with 623 at 1,3
% 0.19/0.42 Id : 1074, {_}: mult (add ?1148 ?1149) (add ?1148 ?1149) =>= mult (add ?1148 ?1149) ?1148 [1149, 1148] by Super 1069 with 625 at 2,2
% 0.19/0.42 Id : 1101, {_}: add ?1148 ?1149 =<= mult (add ?1148 ?1149) ?1148 [1149, 1148] by Demod 1074 with 584 at 2
% 0.19/0.42 Id : 1224, {_}: mult ?1407 (add ?1407 ?1408) =<= add ?1407 (add ?1407 ?1408) [1408, 1407] by Super 704 with 1101 at 2,3
% 0.19/0.42 Id : 1071, {_}: mult ?1141 (add ?1141 ?1142) =>= mult ?1141 ?1142 [1142, 1141] by Super 1069 with 3 at 2,2
% 0.19/0.42 Id : 1247, {_}: mult ?1407 ?1408 =<= add ?1407 (add ?1407 ?1408) [1408, 1407] by Demod 1224 with 1071 at 2
% 0.19/0.42 Id : 1248, {_}: mult ?1407 ?1408 =<= add ?1407 ?1408 [1408, 1407] by Demod 1247 with 625 at 3
% 0.19/0.42 Id : 1332, {_}: mult x0 x1 === mult x0 x1 [] by Demod 1 with 1248 at 2
% 0.19/0.42 Id : 1, {_}: add x0 x1 =>= mult x0 x1 [] by goals
% 0.19/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.42 30939: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.08574 using nrkbo
%------------------------------------------------------------------------------