%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : BOO008-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n021.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 : Thu Jul 14 23:44:11 EDT 2022
% Result : Unsatisfiable 11.20s 3.13s
% Output : CNFRefutation 11.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : BOO008-2 : TPTP v8.1.0. Released v1.0.0.
% 0.11/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n021.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 : Wed Jun 1 17:01:46 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 14429: Facts:
% 0.12/0.34 14429: Id : 2, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
% 0.12/0.34 14429: Id : 3, {_}:
% 0.12/0.34 multiply ?5 ?6 =?= multiply ?6 ?5
% 0.12/0.34 [6, 5] by commutativity_of_multiply ?5 ?6
% 0.12/0.34 14429: Id : 4, {_}:
% 0.12/0.34 add (multiply ?8 ?9) ?10 =<= multiply (add ?8 ?10) (add ?9 ?10)
% 0.12/0.34 [10, 9, 8] by distributivity1 ?8 ?9 ?10
% 0.12/0.34 14429: Id : 5, {_}:
% 0.12/0.34 add ?12 (multiply ?13 ?14) =<= multiply (add ?12 ?13) (add ?12 ?14)
% 0.12/0.34 [14, 13, 12] by distributivity2 ?12 ?13 ?14
% 0.12/0.34 14429: Id : 6, {_}:
% 0.12/0.34 multiply (add ?16 ?17) ?18
% 0.12/0.34 =<=
% 0.12/0.34 add (multiply ?16 ?18) (multiply ?17 ?18)
% 0.12/0.34 [18, 17, 16] by distributivity3 ?16 ?17 ?18
% 0.12/0.34 14429: Id : 7, {_}:
% 0.12/0.34 multiply ?20 (add ?21 ?22)
% 0.12/0.34 =<=
% 0.12/0.34 add (multiply ?20 ?21) (multiply ?20 ?22)
% 0.12/0.34 [22, 21, 20] by distributivity4 ?20 ?21 ?22
% 0.12/0.34 14429: Id : 8, {_}:
% 0.12/0.34 add ?24 (inverse ?24) =>= multiplicative_identity
% 0.12/0.34 [24] by additive_inverse1 ?24
% 0.12/0.34 14429: Id : 9, {_}:
% 0.12/0.34 add (inverse ?26) ?26 =>= multiplicative_identity
% 0.12/0.34 [26] by additive_inverse2 ?26
% 0.12/0.34 14429: Id : 10, {_}:
% 0.12/0.34 multiply ?28 (inverse ?28) =>= additive_identity
% 0.12/0.34 [28] by multiplicative_inverse1 ?28
% 0.12/0.34 14429: Id : 11, {_}:
% 0.12/0.34 multiply (inverse ?30) ?30 =>= additive_identity
% 0.12/0.34 [30] by multiplicative_inverse2 ?30
% 0.12/0.34 14429: Id : 12, {_}:
% 0.12/0.34 multiply ?32 multiplicative_identity =>= ?32
% 0.12/0.34 [32] by multiplicative_id1 ?32
% 0.12/0.34 14429: Id : 13, {_}:
% 0.12/0.34 multiply multiplicative_identity ?34 =>= ?34
% 0.12/0.34 [34] by multiplicative_id2 ?34
% 0.12/0.34 14429: Id : 14, {_}: add ?36 additive_identity =>= ?36 [36] by additive_id1 ?36
% 0.12/0.34 14429: Id : 15, {_}: add additive_identity ?38 =>= ?38 [38] by additive_id2 ?38
% 0.12/0.34 14429: Goal:
% 0.12/0.34 14429: Id : 1, {_}: add a (add b c) =<= add (add a b) c [] by prove_associativity
% 11.20/3.13 Statistics :
% 11.20/3.13 Max weight : 22
% 11.20/3.13 Found proof, 2.790315s
% 11.20/3.13 % SZS status Unsatisfiable for theBenchmark.p
% 11.20/3.13 % SZS output start CNFRefutation for theBenchmark.p
% 11.20/3.13 Id : 29, {_}: add (multiply ?78 ?79) ?80 =<= multiply (add ?78 ?80) (add ?79 ?80) [80, 79, 78] by distributivity1 ?78 ?79 ?80
% 11.20/3.13 Id : 3, {_}: multiply ?5 ?6 =?= multiply ?6 ?5 [6, 5] by commutativity_of_multiply ?5 ?6
% 11.20/3.13 Id : 13, {_}: multiply multiplicative_identity ?34 =>= ?34 [34] by multiplicative_id2 ?34
% 11.20/3.13 Id : 8, {_}: add ?24 (inverse ?24) =>= multiplicative_identity [24] by additive_inverse1 ?24
% 11.20/3.13 Id : 12, {_}: multiply ?32 multiplicative_identity =>= ?32 [32] by multiplicative_id1 ?32
% 11.20/3.13 Id : 15, {_}: add additive_identity ?38 =>= ?38 [38] by additive_id2 ?38
% 11.20/3.13 Id : 5, {_}: add ?12 (multiply ?13 ?14) =<= multiply (add ?12 ?13) (add ?12 ?14) [14, 13, 12] by distributivity2 ?12 ?13 ?14
% 11.20/3.13 Id : 4, {_}: add (multiply ?8 ?9) ?10 =<= multiply (add ?8 ?10) (add ?9 ?10) [10, 9, 8] by distributivity1 ?8 ?9 ?10
% 11.20/3.13 Id : 14, {_}: add ?36 additive_identity =>= ?36 [36] by additive_id1 ?36
% 11.20/3.13 Id : 7, {_}: multiply ?20 (add ?21 ?22) =<= add (multiply ?20 ?21) (multiply ?20 ?22) [22, 21, 20] by distributivity4 ?20 ?21 ?22
% 11.20/3.13 Id : 6, {_}: multiply (add ?16 ?17) ?18 =<= add (multiply ?16 ?18) (multiply ?17 ?18) [18, 17, 16] by distributivity3 ?16 ?17 ?18
% 11.20/3.13 Id : 2, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
% 11.20/3.13 Id : 43, {_}: add (multiply ?118 ?118) ?119 =?= add ?118 (multiply ?119 ?119) [119, 118] by Super 4 with 5 at 3
% 11.20/3.13 Id : 2193, {_}: add ?2661 (multiply additive_identity additive_identity) =?= multiply ?2661 ?2661 [2661] by Super 14 with 43 at 2
% 11.20/3.13 Id : 148, {_}: multiply ?379 (add multiplicative_identity ?380) =<= add ?379 (multiply ?379 ?380) [380, 379] by Super 7 with 12 at 1,3
% 11.20/3.13 Id : 277, {_}: multiply additive_identity (add multiplicative_identity ?520) =>= multiply additive_identity ?520 [520] by Super 15 with 148 at 2
% 11.20/3.13 Id : 147, {_}: multiply ?376 (add ?377 multiplicative_identity) =<= add (multiply ?376 ?377) ?376 [377, 376] by Super 7 with 12 at 2,3
% 11.20/3.13 Id : 155, {_}: multiply ?376 (add ?377 multiplicative_identity) =<= add ?376 (multiply ?376 ?377) [377, 376] by Demod 147 with 2 at 3
% 11.20/3.13 Id : 569, {_}: multiply ?376 (add ?377 multiplicative_identity) =?= multiply ?376 (add multiplicative_identity ?377) [377, 376] by Demod 155 with 148 at 3
% 11.20/3.13 Id : 107, {_}: add ?333 (multiply (inverse ?333) ?334) =>= multiply multiplicative_identity (add ?333 ?334) [334, 333] by Super 5 with 8 at 1,3
% 11.20/3.13 Id : 1937, {_}: add ?2405 (multiply (inverse ?2405) ?2406) =>= add ?2405 ?2406 [2406, 2405] by Demod 107 with 13 at 3
% 11.20/3.13 Id : 1942, {_}: add ?2417 (inverse ?2417) =>= add ?2417 multiplicative_identity [2417] by Super 1937 with 12 at 2,2
% 11.20/3.13 Id : 1992, {_}: multiplicative_identity =<= add ?2417 multiplicative_identity [2417] by Demod 1942 with 8 at 2
% 11.20/3.13 Id : 2012, {_}: multiply ?376 multiplicative_identity =<= multiply ?376 (add multiplicative_identity ?377) [377, 376] by Demod 569 with 1992 at 2,2
% 11.20/3.13 Id : 2017, {_}: ?376 =<= multiply ?376 (add multiplicative_identity ?377) [377, 376] by Demod 2012 with 12 at 2
% 11.20/3.13 Id : 2018, {_}: additive_identity =<= multiply additive_identity ?520 [520] by Demod 277 with 2017 at 2
% 11.20/3.13 Id : 2230, {_}: add ?2661 additive_identity =?= multiply ?2661 ?2661 [2661] by Demod 2193 with 2018 at 2,2
% 11.20/3.13 Id : 2231, {_}: ?2661 =<= multiply ?2661 ?2661 [2661] by Demod 2230 with 14 at 2
% 11.20/3.13 Id : 2289, {_}: multiply ?2779 (add ?2780 ?2779) =<= add (multiply ?2779 ?2780) ?2779 [2780, 2779] by Super 7 with 2231 at 2,3
% 11.20/3.13 Id : 2309, {_}: multiply ?2779 (add ?2780 ?2779) =<= add ?2779 (multiply ?2779 ?2780) [2780, 2779] by Demod 2289 with 2 at 3
% 11.20/3.13 Id : 2019, {_}: ?379 =<= add ?379 (multiply ?379 ?380) [380, 379] by Demod 148 with 2017 at 2
% 11.20/3.13 Id : 2310, {_}: multiply ?2779 (add ?2780 ?2779) =>= ?2779 [2780, 2779] by Demod 2309 with 2019 at 3
% 11.20/3.13 Id : 2442, {_}: multiply (add ?2945 ?2946) (add ?2947 ?2946) =<= add (multiply ?2945 (add ?2947 ?2946)) ?2946 [2947, 2946, 2945] by Super 6 with 2310 at 2,3
% 11.20/3.13 Id : 2470, {_}: add (multiply ?2945 ?2947) ?2946 =<= add (multiply ?2945 (add ?2947 ?2946)) ?2946 [2946, 2947, 2945] by Demod 2442 with 4 at 2
% 11.20/3.13 Id : 11497, {_}: add (multiply ?14946 ?14947) ?14948 =<= add ?14948 (multiply ?14946 (add ?14947 ?14948)) [14948, 14947, 14946] by Demod 2470 with 2 at 3
% 11.20/3.13 Id : 11547, {_}: add (multiply (add ?15142 ?15143) ?15142) ?15144 =?= add ?15144 (add ?15142 (multiply ?15143 ?15144)) [15144, 15143, 15142] by Super 11497 with 5 at 2,3
% 11.20/3.13 Id : 27, {_}: multiply (add ?70 ?71) (add ?72 ?71) =>= add (multiply ?72 ?70) ?71 [72, 71, 70] by Super 3 with 4 at 3
% 11.20/3.13 Id : 37, {_}: add (multiply ?70 ?72) ?71 =?= add (multiply ?72 ?70) ?71 [71, 72, 70] by Demod 27 with 4 at 2
% 11.20/3.13 Id : 11672, {_}: add (multiply ?15142 (add ?15142 ?15143)) ?15144 =?= add ?15144 (add ?15142 (multiply ?15143 ?15144)) [15144, 15143, 15142] by Demod 11547 with 37 at 2
% 11.20/3.13 Id : 2290, {_}: multiply ?2782 (add ?2782 ?2783) =<= add ?2782 (multiply ?2782 ?2783) [2783, 2782] by Super 7 with 2231 at 1,3
% 11.20/3.13 Id : 2311, {_}: multiply ?2782 (add ?2782 ?2783) =>= ?2782 [2783, 2782] by Demod 2290 with 2019 at 3
% 11.20/3.13 Id : 20276, {_}: add ?32243 ?32244 =<= add ?32244 (add ?32243 (multiply ?32245 ?32244)) [32245, 32244, 32243] by Demod 11672 with 2311 at 1,2
% 11.20/3.13 Id : 20282, {_}: add ?32264 (add ?32265 ?32266) =<= add (add ?32265 ?32266) (add ?32264 ?32265) [32266, 32265, 32264] by Super 20276 with 2311 at 2,2,3
% 11.20/3.13 Id : 34107, {_}: add (add ?59024 ?59025) (add ?59025 ?59026) =>= add ?59024 (add ?59025 ?59026) [59026, 59025, 59024] by Super 2 with 20282 at 3
% 11.20/3.13 Id : 30, {_}: add (multiply ?82 ?83) ?84 =<= multiply (add ?82 ?84) (add ?84 ?83) [84, 83, 82] by Super 29 with 2 at 2,3
% 11.20/3.13 Id : 11548, {_}: add (multiply (add ?15146 ?15147) ?15147) ?15148 =?= add ?15148 (add (multiply ?15146 ?15148) ?15147) [15148, 15147, 15146] by Super 11497 with 30 at 2,3
% 11.20/3.13 Id : 11674, {_}: add (multiply ?15147 (add ?15146 ?15147)) ?15148 =?= add ?15148 (add (multiply ?15146 ?15148) ?15147) [15148, 15146, 15147] by Demod 11548 with 37 at 2
% 11.20/3.13 Id : 20578, {_}: add ?32901 ?32902 =<= add ?32902 (add (multiply ?32903 ?32902) ?32901) [32903, 32902, 32901] by Demod 11674 with 2310 at 1,2
% 11.20/3.13 Id : 20583, {_}: add ?32918 (add ?32919 ?32920) =<= add (add ?32919 ?32920) (add ?32920 ?32918) [32920, 32919, 32918] by Super 20578 with 2310 at 1,2,3
% 11.20/3.13 Id : 39666, {_}: add ?59026 (add ?59024 ?59025) =?= add ?59024 (add ?59025 ?59026) [59025, 59024, 59026] by Demod 34107 with 20583 at 2
% 11.20/3.13 Id : 40262, {_}: add a (add b c) =?= add a (add b c) [] by Demod 21 with 39666 at 3
% 11.20/3.13 Id : 21, {_}: add a (add b c) =<= add c (add a b) [] by Demod 1 with 2 at 3
% 11.20/3.13 Id : 1, {_}: add a (add b c) =<= add (add a b) c [] by prove_associativity
% 11.20/3.13 % SZS output end CNFRefutation for theBenchmark.p
% 11.20/3.13 14430: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 2.789993 using kbo
%------------------------------------------------------------------------------