%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : COL003-15 : TPTP v8.1.0. Released v2.1.0.
% 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 : Fri Jul 15 00:35:51 EDT 2022
% Result : Unsatisfiable 180.52s 45.53s
% Output : CNFRefutation 180.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : COL003-15 : TPTP v8.1.0. Released v2.1.0.
% 0.10/0.13 % 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 May 31 05:57:08 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 6783: Facts:
% 0.12/0.34 6783: Id : 2, {_}:
% 0.12/0.34 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
% 0.12/0.34 [4, 3, 2] by b_definition ?2 ?3 ?4
% 0.12/0.34 6783: Id : 3, {_}:
% 0.12/0.34 apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
% 0.12/0.34 [7, 6] by w_definition ?6 ?7
% 0.12/0.34 6783: Id : 4, {_}:
% 0.12/0.34 strong_fixed_point
% 0.12/0.34 =<=
% 0.12/0.34 apply (apply b (apply (apply b (apply w w)) w)) (apply (apply b b) b)
% 0.12/0.34 [] by strong_fixed_point
% 0.12/0.34 6783: Goal:
% 0.12/0.34 6783: Id : 1, {_}:
% 0.12/0.34 apply strong_fixed_point fixed_pt
% 0.12/0.34 =<=
% 0.12/0.34 apply fixed_pt (apply strong_fixed_point fixed_pt)
% 0.12/0.34 [] by prove_strong_fixed_point
% 180.52/45.53 Statistics :
% 180.52/45.53 Max weight : 33
% 180.52/45.53 Found proof, 45.192429s
% 180.52/45.53 % SZS status Unsatisfiable for theBenchmark.p
% 180.52/45.53 % SZS output start CNFRefutation for theBenchmark.p
% 180.52/45.53 Id : 4, {_}: strong_fixed_point =<= apply (apply b (apply (apply b (apply w w)) w)) (apply (apply b b) b) [] by strong_fixed_point
% 180.52/45.53 Id : 9, {_}: apply (apply w ?24) ?25 =?= apply (apply ?24 ?25) ?25 [25, 24] by w_definition ?24 ?25
% 180.52/45.53 Id : 2, {_}: apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4) [4, 3, 2] by b_definition ?2 ?3 ?4
% 180.52/45.54 Id : 3, {_}: apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7 [7, 6] by w_definition ?6 ?7
% 180.52/45.54 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
% 180.52/45.54 Id : 431, {_}: apply (apply w (apply (apply b ?796) (apply ?797 ?798))) ?798 =>= apply (apply ?796 (apply (apply w ?797) ?798)) ?798 [798, 797, 796] by Super 382 with 3 at 2,1,2
% 180.52/45.54 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
% 180.52/45.54 Id : 12542, {_}: apply (apply ?12131 (apply (apply w ?12132) ?12133)) ?12133 =?= apply (apply ?12131 (apply (apply w ?12132) ?12133)) ?12133 [12133, 12132, 12131] by Demod 431 with 392 at 2
% 180.52/45.54 Id : 8, {_}: apply (apply w (apply b ?21)) ?22 =?= apply ?21 (apply ?22 ?22) [22, 21] by Super 2 with 3 at 2
% 180.52/45.54 Id : 12655, {_}: apply (apply ?12477 (apply (apply w ?12478) (apply w ?12478))) (apply w ?12478) =?= apply (apply (apply w (apply b ?12477)) (apply w ?12478)) (apply w ?12478) [12478, 12477] by Super 12542 with 8 at 1,3
% 180.52/45.54 Id : 13033, {_}: apply (apply ?12477 (apply (apply w ?12478) (apply w ?12478))) (apply w ?12478) =>= apply (apply w (apply w (apply b ?12477))) (apply w ?12478) [12478, 12477] by Demod 12655 with 3 at 3
% 180.52/45.54 Id : 85563, {_}: apply (apply w (apply w (apply b (apply b ?70254)))) (apply w ?70255) =?= apply ?70254 (apply (apply (apply w ?70255) (apply w ?70255)) (apply w ?70255)) [70255, 70254] by Super 2 with 13033 at 2
% 180.52/45.54 Id : 85885, {_}: apply (apply w (apply w (apply b (apply b ?70254)))) (apply w ?70255) =?= apply ?70254 (apply (apply w (apply w ?70255)) (apply w ?70255)) [70255, 70254] by Demod 85563 with 3 at 2,3
% 180.52/45.54 Id : 85886, {_}: apply (apply w (apply w (apply b (apply b ?70254)))) (apply w ?70255) =>= apply ?70254 (apply (apply w w) (apply w ?70255)) [70255, 70254] by Demod 85885 with 3 at 2,3
% 180.52/45.54 Id : 124536, {_}: apply (apply w w) (apply w (apply b (apply b ?94042))) =<= apply ?94042 (apply (apply w w) (apply w (apply b (apply b ?94042)))) [94042] by Super 3 with 85886 at 3
% 180.52/45.54 Id : 20, {_}: apply strong_fixed_point ?50 =<= apply (apply (apply b (apply w w)) w) (apply (apply (apply b b) b) ?50) [50] by Super 2 with 4 at 1,2
% 180.52/45.54 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 3
% 180.52/45.54 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
% 180.52/45.54 Id : 124698, {_}: apply strong_fixed_point ?94042 =<= apply ?94042 (apply (apply w w) (apply w (apply b (apply b ?94042)))) [94042] by Demod 124536 with 25 at 2
% 180.52/45.54 Id : 124699, {_}: apply strong_fixed_point ?94042 =<= apply ?94042 (apply strong_fixed_point ?94042) [94042] by Demod 124698 with 25 at 2,3
% 180.52/45.54 Id : 125854, {_}: apply strong_fixed_point fixed_pt =?= apply strong_fixed_point fixed_pt [] by Demod 1 with 124699 at 3
% 180.52/45.54 Id : 1, {_}: apply strong_fixed_point fixed_pt =<= apply fixed_pt (apply strong_fixed_point fixed_pt) [] by prove_strong_fixed_point
% 180.52/45.54 % SZS output end CNFRefutation for theBenchmark.p
% 180.52/45.54 6784: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 45.071885 using kbo
%------------------------------------------------------------------------------