%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP167-5 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n020.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:19 EDT 2022
% Result : Unsatisfiable 1.35s 0.64s
% Output : CNFRefutation 1.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP167-5 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.11/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n020.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 : Tue Jun 14 13:58:35 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 11842: Facts:
% 0.12/0.34 11842: Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 0.12/0.34 11842: Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 0.12/0.34 11842: Id : 4, {_}:
% 0.12/0.34 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
% 0.12/0.34 [8, 7, 6] by associativity ?6 ?7 ?8
% 0.12/0.34 11842: Id : 5, {_}:
% 0.12/0.34 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
% 0.12/0.34 [11, 10] by symmetry_of_glb ?10 ?11
% 0.12/0.34 11842: Id : 6, {_}:
% 0.12/0.34 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
% 0.12/0.34 [14, 13] by symmetry_of_lub ?13 ?14
% 0.12/0.34 11842: Id : 7, {_}:
% 0.12/0.34 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
% 0.12/0.34 =?=
% 0.12/0.34 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
% 0.12/0.34 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
% 0.12/0.34 11842: Id : 8, {_}:
% 0.12/0.34 least_upper_bound ?20 (least_upper_bound ?21 ?22)
% 0.12/0.34 =?=
% 0.12/0.34 least_upper_bound (least_upper_bound ?20 ?21) ?22
% 0.12/0.34 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
% 0.12/0.34 11842: Id : 9, {_}: least_upper_bound ?24 ?24 =>= ?24 [24] by idempotence_of_lub ?24
% 0.12/0.34 11842: Id : 10, {_}:
% 0.12/0.34 greatest_lower_bound ?26 ?26 =>= ?26
% 0.12/0.34 [26] by idempotence_of_gld ?26
% 0.12/0.34 11842: Id : 11, {_}:
% 0.12/0.34 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
% 0.12/0.34 [29, 28] by lub_absorbtion ?28 ?29
% 0.12/0.34 11842: Id : 12, {_}:
% 0.12/0.34 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
% 0.12/0.34 [32, 31] by glb_absorbtion ?31 ?32
% 0.12/0.34 11842: Id : 13, {_}:
% 0.12/0.34 multiply ?34 (least_upper_bound ?35 ?36)
% 0.12/0.34 =<=
% 0.12/0.34 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
% 0.12/0.34 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
% 0.12/0.34 11842: Id : 14, {_}:
% 0.12/0.34 multiply ?38 (greatest_lower_bound ?39 ?40)
% 0.12/0.34 =<=
% 0.12/0.34 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
% 0.12/0.34 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
% 0.12/0.34 11842: Id : 15, {_}:
% 0.12/0.34 multiply (least_upper_bound ?42 ?43) ?44
% 0.12/0.34 =<=
% 0.12/0.34 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
% 0.12/0.34 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
% 0.12/0.34 11842: Id : 16, {_}:
% 0.12/0.34 multiply (greatest_lower_bound ?46 ?47) ?48
% 0.12/0.34 =<=
% 0.12/0.34 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
% 0.12/0.34 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
% 0.12/0.34 11842: Id : 17, {_}:
% 0.12/0.34 inverse (least_upper_bound ?50 ?51)
% 0.12/0.34 =<=
% 0.12/0.34 greatest_lower_bound (inverse ?50) (inverse ?51)
% 0.12/0.34 [51, 50] by p10 ?50 ?51
% 0.12/0.34 11842: Id : 18, {_}:
% 0.12/0.34 positive_part ?53 =<= least_upper_bound ?53 identity
% 0.12/0.34 [53] by lat4_1 ?53
% 0.12/0.34 11842: Id : 19, {_}:
% 0.12/0.34 negative_part ?55 =<= greatest_lower_bound ?55 identity
% 0.12/0.34 [55] by lat4_2 ?55
% 0.12/0.34 11842: Id : 20, {_}:
% 0.12/0.34 least_upper_bound ?57 (greatest_lower_bound ?58 ?59)
% 0.12/0.34 =<=
% 0.12/0.34 greatest_lower_bound (least_upper_bound ?57 ?58)
% 0.12/0.34 (least_upper_bound ?57 ?59)
% 0.12/0.34 [59, 58, 57] by lat4_3 ?57 ?58 ?59
% 0.12/0.34 11842: Id : 21, {_}:
% 0.12/0.34 greatest_lower_bound ?61 (least_upper_bound ?62 ?63)
% 0.12/0.34 =<=
% 0.12/0.34 least_upper_bound (greatest_lower_bound ?61 ?62)
% 0.12/0.34 (greatest_lower_bound ?61 ?63)
% 0.12/0.34 [63, 62, 61] by lat4_4 ?61 ?62 ?63
% 0.12/0.34 11842: Goal:
% 0.12/0.34 11842: Id : 1, {_}:
% 0.12/0.34 a =<= multiply (positive_part a) (negative_part a)
% 0.12/0.34 [] by prove_lat4
% 1.35/0.64 Statistics :
% 1.35/0.64 Max weight : 11
% 1.35/0.64 Found proof, 0.296260s
% 1.35/0.64 % SZS status Unsatisfiable for theBenchmark.p
% 1.35/0.64 % SZS output start CNFRefutation for theBenchmark.p
% 1.35/0.64 Id : 18, {_}: positive_part ?53 =<= least_upper_bound ?53 identity [53] by lat4_1 ?53
% 1.35/0.64 Id : 17, {_}: inverse (least_upper_bound ?50 ?51) =<= greatest_lower_bound (inverse ?50) (inverse ?51) [51, 50] by p10 ?50 ?51
% 1.35/0.64 Id : 19, {_}: negative_part ?55 =<= greatest_lower_bound ?55 identity [55] by lat4_2 ?55
% 1.35/0.64 Id : 5, {_}: greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10 [11, 10] by symmetry_of_glb ?10 ?11
% 1.35/0.64 Id : 222, {_}: multiply (greatest_lower_bound ?501 ?502) ?503 =<= greatest_lower_bound (multiply ?501 ?503) (multiply ?502 ?503) [503, 502, 501] by monotony_glb2 ?501 ?502 ?503
% 1.35/0.64 Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 1.35/0.64 Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 1.35/0.64 Id : 26, {_}: multiply (multiply ?72 ?73) ?74 =>= multiply ?72 (multiply ?73 ?74) [74, 73, 72] by associativity ?72 ?73 ?74
% 1.35/0.64 Id : 28, {_}: multiply identity ?79 =<= multiply (inverse ?80) (multiply ?80 ?79) [80, 79] by Super 26 with 3 at 1,2
% 1.35/0.64 Id : 32, {_}: ?79 =<= multiply (inverse ?80) (multiply ?80 ?79) [80, 79] by Demod 28 with 2 at 2
% 1.35/0.64 Id : 226, {_}: multiply (greatest_lower_bound identity ?516) ?517 =<= greatest_lower_bound ?517 (multiply ?516 ?517) [517, 516] by Super 222 with 2 at 1,3
% 1.35/0.64 Id : 281, {_}: greatest_lower_bound identity ?607 =>= negative_part ?607 [607] by Super 5 with 19 at 3
% 1.35/0.64 Id : 4502, {_}: multiply (negative_part ?6540) ?6541 =<= greatest_lower_bound ?6541 (multiply ?6540 ?6541) [6541, 6540] by Demod 226 with 281 at 1,2
% 1.35/0.64 Id : 4504, {_}: multiply (negative_part (inverse ?6545)) ?6545 =>= greatest_lower_bound ?6545 identity [6545] by Super 4502 with 3 at 2,3
% 1.35/0.64 Id : 4539, {_}: multiply (negative_part (inverse ?6545)) ?6545 =>= negative_part ?6545 [6545] by Demod 4504 with 19 at 3
% 1.35/0.64 Id : 4561, {_}: ?6582 =<= multiply (inverse (negative_part (inverse ?6582))) (negative_part ?6582) [6582] by Super 32 with 4539 at 2,3
% 1.35/0.64 Id : 447, {_}: ?923 =<= multiply (inverse ?924) (multiply ?924 ?923) [924, 923] by Demod 28 with 2 at 2
% 1.35/0.64 Id : 449, {_}: ?928 =<= multiply (inverse (inverse ?928)) identity [928] by Super 447 with 3 at 2,3
% 1.35/0.64 Id : 448, {_}: ?926 =<= multiply (inverse identity) ?926 [926] by Super 447 with 2 at 2,3
% 1.35/0.64 Id : 560, {_}: ?1047 =<= multiply (inverse (inverse identity)) ?1047 [1047] by Super 32 with 448 at 2,3
% 1.35/0.64 Id : 1182, {_}: inverse identity =>= identity [] by Super 3 with 560 at 2
% 1.35/0.64 Id : 1217, {_}: inverse (least_upper_bound ?2102 identity) =<= greatest_lower_bound (inverse ?2102) identity [2102] by Super 17 with 1182 at 2,3
% 1.35/0.64 Id : 1227, {_}: inverse (positive_part ?2102) =<= greatest_lower_bound (inverse ?2102) identity [2102] by Demod 1217 with 18 at 1,2
% 1.35/0.64 Id : 1228, {_}: inverse (positive_part ?2102) =<= greatest_lower_bound identity (inverse ?2102) [2102] by Demod 1227 with 5 at 3
% 1.35/0.64 Id : 1229, {_}: inverse (positive_part ?2102) =>= negative_part (inverse ?2102) [2102] by Demod 1228 with 281 at 3
% 1.35/0.64 Id : 1237, {_}: positive_part ?2112 =<= multiply (inverse (negative_part (inverse ?2112))) identity [2112] by Super 449 with 1229 at 1,1,3
% 1.35/0.64 Id : 451, {_}: multiply ?934 ?935 =<= multiply (inverse (inverse ?934)) ?935 [935, 934] by Super 447 with 32 at 2,3
% 1.35/0.64 Id : 1748, {_}: ?928 =<= multiply ?928 identity [928] by Demod 449 with 451 at 3
% 1.35/0.64 Id : 2307, {_}: positive_part ?3559 =<= inverse (negative_part (inverse ?3559)) [3559] by Demod 1237 with 1748 at 3
% 1.35/0.64 Id : 1749, {_}: inverse (inverse ?2821) =<= multiply ?2821 identity [2821] by Super 1748 with 451 at 3
% 1.35/0.64 Id : 1789, {_}: inverse (inverse ?2821) =>= ?2821 [2821] by Demod 1749 with 1748 at 3
% 1.35/0.64 Id : 2310, {_}: positive_part (inverse ?3564) =<= inverse (negative_part ?3564) [3564] by Super 2307 with 1789 at 1,1,3
% 1.35/0.64 Id : 4599, {_}: ?6582 =<= multiply (positive_part (inverse (inverse ?6582))) (negative_part ?6582) [6582] by Demod 4561 with 2310 at 1,3
% 1.35/0.64 Id : 4600, {_}: ?6582 =<= multiply (positive_part ?6582) (negative_part ?6582) [6582] by Demod 4599 with 1789 at 1,1,3
% 1.35/0.64 Id : 4775, {_}: a =?= a [] by Demod 1 with 4600 at 3
% 1.35/0.64 Id : 1, {_}: a =<= multiply (positive_part a) (negative_part a) [] by prove_lat4
% 1.35/0.64 % SZS output end CNFRefutation for theBenchmark.p
% 1.35/0.64 11843: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.298563 using kbo
%------------------------------------------------------------------------------