%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : COL003-16 : 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:51 EDT 2022
% Result : Unsatisfiable 149.96s 37.86s
% Output : CNFRefutation 149.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COL003-16 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox/benchmark %s
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue May 31 14:49:15 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 10372: Facts:
% 0.13/0.34 10372: Id : 2, {_}:
% 0.13/0.34 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
% 0.13/0.34 [4, 3, 2] by b_definition ?2 ?3 ?4
% 0.13/0.34 10372: Id : 3, {_}:
% 0.13/0.34 apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
% 0.13/0.34 [7, 6] by w_definition ?6 ?7
% 0.13/0.34 10372: Id : 4, {_}:
% 0.13/0.34 strong_fixed_point
% 0.13/0.34 =<=
% 0.13/0.34 apply (apply b (apply (apply b (apply (apply b (apply w w)) w)) b)) b
% 0.13/0.34 [] by strong_fixed_point
% 0.13/0.34 10372: Goal:
% 0.13/0.34 10372: Id : 1, {_}:
% 0.13/0.34 apply strong_fixed_point fixed_pt
% 0.13/0.34 =<=
% 0.13/0.34 apply fixed_pt (apply strong_fixed_point fixed_pt)
% 0.13/0.34 [] by prove_strong_fixed_point
% 149.96/37.86 Statistics :
% 149.96/37.86 Max weight : 33
% 149.96/37.86 Found proof, 37.517635s
% 149.96/37.86 % SZS status Unsatisfiable for theBenchmark.p
% 149.96/37.86 % SZS output start CNFRefutation for theBenchmark.p
% 149.96/37.86 Id : 4, {_}: strong_fixed_point =<= apply (apply b (apply (apply b (apply (apply b (apply w w)) w)) b)) b [] by strong_fixed_point
% 149.96/37.86 Id : 9, {_}: apply (apply w ?24) ?25 =?= apply (apply ?24 ?25) ?25 [25, 24] by w_definition ?24 ?25
% 149.96/37.86 Id : 2, {_}: apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4) [4, 3, 2] by b_definition ?2 ?3 ?4
% 149.96/37.86 Id : 3, {_}: apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7 [7, 6] by w_definition ?6 ?7
% 149.96/37.86 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
% 149.96/37.86 Id : 430, {_}: apply (apply w (apply (apply b ?794) (apply ?795 ?796))) ?796 =>= apply (apply ?794 (apply (apply w ?795) ?796)) ?796 [796, 795, 794] by Super 382 with 3 at 2,1,2
% 149.96/37.86 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
% 149.96/37.86 Id : 13631, {_}: apply (apply ?13138 (apply (apply w ?13139) ?13140)) ?13140 =?= apply (apply ?13138 (apply (apply w ?13139) ?13140)) ?13140 [13140, 13139, 13138] by Demod 430 with 392 at 2
% 149.96/37.86 Id : 8, {_}: apply (apply w (apply b ?21)) ?22 =?= apply ?21 (apply ?22 ?22) [22, 21] by Super 2 with 3 at 2
% 149.96/37.86 Id : 13748, {_}: apply (apply ?13497 (apply (apply w ?13498) (apply w ?13498))) (apply w ?13498) =?= apply (apply (apply w (apply b ?13497)) (apply w ?13498)) (apply w ?13498) [13498, 13497] by Super 13631 with 8 at 1,3
% 149.96/37.86 Id : 14134, {_}: apply (apply ?13497 (apply (apply w ?13498) (apply w ?13498))) (apply w ?13498) =>= apply (apply w (apply w (apply b ?13497))) (apply w ?13498) [13498, 13497] by Demod 13748 with 3 at 3
% 149.96/37.86 Id : 106405, {_}: apply (apply w (apply w (apply b (apply b ?83652)))) (apply w ?83653) =?= apply ?83652 (apply (apply (apply w ?83653) (apply w ?83653)) (apply w ?83653)) [83653, 83652] by Super 2 with 14134 at 2
% 149.96/37.86 Id : 106771, {_}: apply (apply w (apply w (apply b (apply b ?83652)))) (apply w ?83653) =?= apply ?83652 (apply (apply w (apply w ?83653)) (apply w ?83653)) [83653, 83652] by Demod 106405 with 3 at 2,3
% 149.96/37.86 Id : 106772, {_}: apply (apply w (apply w (apply b (apply b ?83652)))) (apply w ?83653) =>= apply ?83652 (apply (apply w w) (apply w ?83653)) [83653, 83652] by Demod 106771 with 3 at 2,3
% 149.96/37.86 Id : 144278, {_}: apply (apply w w) (apply w (apply b (apply b ?106331))) =<= apply ?106331 (apply (apply w w) (apply w (apply b (apply b ?106331)))) [106331] by Super 3 with 106772 at 3
% 149.96/37.86 Id : 20, {_}: apply strong_fixed_point ?50 =<= apply (apply (apply b (apply (apply b (apply w w)) w)) b) (apply b ?50) [50] by Super 2 with 4 at 1,2
% 149.96/37.86 Id : 24, {_}: apply strong_fixed_point ?50 =<= apply (apply (apply b (apply w w)) w) (apply b (apply b ?50)) [50] by Demod 20 with 2 at 3
% 149.96/37.86 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 3
% 149.96/37.86 Id : 144454, {_}: apply strong_fixed_point ?106331 =<= apply ?106331 (apply (apply w w) (apply w (apply b (apply b ?106331)))) [106331] by Demod 144278 with 25 at 2
% 149.96/37.86 Id : 144455, {_}: apply strong_fixed_point ?106331 =<= apply ?106331 (apply strong_fixed_point ?106331) [106331] by Demod 144454 with 25 at 2,3
% 149.96/37.86 Id : 145727, {_}: apply strong_fixed_point fixed_pt =?= apply strong_fixed_point fixed_pt [] by Demod 1 with 144455 at 3
% 149.96/37.86 Id : 1, {_}: apply strong_fixed_point fixed_pt =<= apply fixed_pt (apply strong_fixed_point fixed_pt) [] by prove_strong_fixed_point
% 149.96/37.86 % SZS output end CNFRefutation for theBenchmark.p
% 149.96/37.86 10373: solved /export/starexec/sandbox/benchmark/theBenchmark.p in 37.512027 using kbo
%------------------------------------------------------------------------------