%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : COL003-12 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% Computer : n029.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 : Fri Jul 15 00:35:50 EDT 2022
% Result : Unsatisfiable 117.86s 29.80s
% Output : CNFRefutation 117.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : COL003-12 : TPTP v8.1.0. Released v2.1.0.
% 0.06/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.11/0.33 % Computer : n029.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Tue May 31 06:40:29 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.11/0.33 24772: Facts:
% 0.11/0.33 24772: Id : 2, {_}:
% 0.11/0.33 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
% 0.11/0.33 [4, 3, 2] by b_definition ?2 ?3 ?4
% 0.11/0.33 24772: Id : 3, {_}:
% 0.11/0.33 apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
% 0.11/0.33 [7, 6] by w_definition ?6 ?7
% 0.11/0.33 24772: Id : 4, {_}:
% 0.11/0.33 strong_fixed_point
% 0.11/0.33 =<=
% 0.11/0.33 apply (apply b (apply w w)) (apply (apply b w) (apply (apply b b) b))
% 0.11/0.33 [] by strong_fixed_point
% 0.11/0.33 24772: Goal:
% 0.11/0.33 24772: Id : 1, {_}:
% 0.11/0.33 apply strong_fixed_point fixed_pt
% 0.11/0.33 =<=
% 0.11/0.33 apply fixed_pt (apply strong_fixed_point fixed_pt)
% 0.11/0.33 [] by prove_strong_fixed_point
% 117.86/29.80 Statistics :
% 117.86/29.80 Max weight : 33
% 117.86/29.80 Found proof, 29.465442s
% 117.86/29.80 % SZS status Unsatisfiable for theBenchmark.p
% 117.86/29.80 % SZS output start CNFRefutation for theBenchmark.p
% 117.86/29.80 Id : 4, {_}: strong_fixed_point =<= apply (apply b (apply w w)) (apply (apply b w) (apply (apply b b) b)) [] by strong_fixed_point
% 117.86/29.80 Id : 9, {_}: apply (apply w ?24) ?25 =?= apply (apply ?24 ?25) ?25 [25, 24] by w_definition ?24 ?25
% 117.86/29.80 Id : 2, {_}: apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4) [4, 3, 2] by b_definition ?2 ?3 ?4
% 117.86/29.80 Id : 3, {_}: apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7 [7, 6] by w_definition ?6 ?7
% 117.86/29.80 Id : 382, {_}: apply (apply w (apply (apply b ?618) ?619)) ?620 =?= apply (apply ?618 (apply ?619 ?620)) ?620 [620, 619, 618] by Super 9 with 2 at 1,3
% 117.86/29.80 Id : 432, {_}: apply (apply w (apply (apply b ?797) (apply ?798 ?799))) ?799 =>= apply (apply ?797 (apply (apply w ?798) ?799)) ?799 [799, 798, 797] by Super 382 with 3 at 2,1,2
% 117.86/29.80 Id : 392, {_}: apply (apply w (apply (apply b ?658) (apply ?659 ?660))) ?660 =>= apply (apply ?658 (apply (apply w ?659) ?660)) ?660 [660, 659, 658] by Super 382 with 3 at 2,1,3
% 117.86/29.80 Id : 12464, {_}: apply (apply ?12082 (apply (apply w ?12083) ?12084)) ?12084 =?= apply (apply ?12082 (apply (apply w ?12083) ?12084)) ?12084 [12084, 12083, 12082] by Demod 432 with 392 at 2
% 117.86/29.80 Id : 8, {_}: apply (apply w (apply b ?21)) ?22 =?= apply ?21 (apply ?22 ?22) [22, 21] by Super 2 with 3 at 2
% 117.86/29.80 Id : 12577, {_}: apply (apply ?12428 (apply (apply w ?12429) (apply w ?12429))) (apply w ?12429) =?= apply (apply (apply w (apply b ?12428)) (apply w ?12429)) (apply w ?12429) [12429, 12428] by Super 12464 with 8 at 1,3
% 117.86/29.80 Id : 12955, {_}: apply (apply ?12428 (apply (apply w ?12429) (apply w ?12429))) (apply w ?12429) =>= apply (apply w (apply w (apply b ?12428))) (apply w ?12429) [12429, 12428] by Demod 12577 with 3 at 3
% 117.86/29.80 Id : 86040, {_}: apply (apply w (apply w (apply b (apply b ?70517)))) (apply w ?70518) =?= apply ?70517 (apply (apply (apply w ?70518) (apply w ?70518)) (apply w ?70518)) [70518, 70517] by Super 2 with 12955 at 2
% 117.86/29.80 Id : 86357, {_}: apply (apply w (apply w (apply b (apply b ?70517)))) (apply w ?70518) =?= apply ?70517 (apply (apply w (apply w ?70518)) (apply w ?70518)) [70518, 70517] by Demod 86040 with 3 at 2,3
% 117.86/29.80 Id : 86358, {_}: apply (apply w (apply w (apply b (apply b ?70517)))) (apply w ?70518) =>= apply ?70517 (apply (apply w w) (apply w ?70518)) [70518, 70517] by Demod 86357 with 3 at 2,3
% 117.86/29.80 Id : 128576, {_}: apply (apply w w) (apply w (apply b (apply b ?96072))) =<= apply ?96072 (apply (apply w w) (apply w (apply b (apply b ?96072)))) [96072] by Super 3 with 86358 at 3
% 117.86/29.80 Id : 20, {_}: apply strong_fixed_point ?50 =<= apply (apply w w) (apply (apply (apply b w) (apply (apply b b) b)) ?50) [50] by Super 2 with 4 at 1,2
% 117.86/29.80 Id : 24, {_}: apply strong_fixed_point ?50 =<= apply (apply w w) (apply w (apply (apply (apply b b) b) ?50)) [50] by Demod 20 with 2 at 2,3
% 117.86/29.80 Id : 25, {_}: apply strong_fixed_point ?50 =<= apply (apply w w) (apply w (apply b (apply b ?50))) [50] by Demod 24 with 2 at 2,2,3
% 117.86/29.80 Id : 128766, {_}: apply strong_fixed_point ?96072 =<= apply ?96072 (apply (apply w w) (apply w (apply b (apply b ?96072)))) [96072] by Demod 128576 with 25 at 2
% 117.86/29.80 Id : 128767, {_}: apply strong_fixed_point ?96072 =<= apply ?96072 (apply strong_fixed_point ?96072) [96072] by Demod 128766 with 25 at 2,3
% 117.86/29.80 Id : 129906, {_}: apply strong_fixed_point fixed_pt =?= apply strong_fixed_point fixed_pt [] by Demod 1 with 128767 at 3
% 117.86/29.80 Id : 1, {_}: apply strong_fixed_point fixed_pt =<= apply fixed_pt (apply strong_fixed_point fixed_pt) [] by prove_strong_fixed_point
% 117.86/29.80 % SZS output end CNFRefutation for theBenchmark.p
% 117.86/29.80 24773: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 29.452242 using kbo
%------------------------------------------------------------------------------