%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : COL001-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n026.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 1.12s 0.58s
% Output : CNFRefutation 1.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : COL001-1 : TPTP v8.1.0. Released v1.0.0.
% 0.12/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.34 % Computer : n026.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 16:07:26 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 30687: Facts:
% 0.13/0.35 30687: Id : 2, {_}:
% 0.13/0.35 apply (apply (apply s ?3) ?4) ?5
% 0.13/0.35 =?=
% 0.13/0.35 apply (apply ?3 ?5) (apply ?4 ?5)
% 0.13/0.35 [5, 4, 3] by s_definition ?3 ?4 ?5
% 0.13/0.35 30687: Id : 3, {_}: apply (apply k ?7) ?8 =>= ?7 [8, 7] by k_definition ?7 ?8
% 0.13/0.35 30687: Goal:
% 0.13/0.35 30687: Id : 1, {_}: ?1 =<= apply combinator ?1 [1] by prove_fixed_point ?1
% 1.12/0.58 Goal subsumed
% 1.12/0.58 Statistics :
% 1.12/0.58 Max weight : 74
% 1.12/0.58 Found proof, 0.233243s
% 1.12/0.58 % SZS status Unsatisfiable for theBenchmark.p
% 1.12/0.58 % SZS output start CNFRefutation for theBenchmark.p
% 1.12/0.58 Id : 3, {_}: apply (apply k ?7) ?8 =>= ?7 [8, 7] by k_definition ?7 ?8
% 1.12/0.58 Id : 2, {_}: apply (apply (apply s ?3) ?4) ?5 =?= apply (apply ?3 ?5) (apply ?4 ?5) [5, 4, 3] by s_definition ?3 ?4 ?5
% 1.12/0.58 Id : 4, {_}: apply (apply (apply s ?10) ?11) ?12 =?= apply (apply ?10 ?12) (apply ?11 ?12) [12, 11, 10] by s_definition ?10 ?11 ?12
% 1.12/0.58 Id : 116, {_}: apply (apply (apply s ?489) (apply ?490 ?491)) (apply ?492 ?491) =<= apply (apply ?489 (apply ?492 ?491)) (apply (apply (apply s ?490) ?492) ?491) [492, 491, 490, 489] by Super 4 with 2 at 2,3
% 1.12/0.58 Id : 135, {_}: apply (apply (apply s (apply k ?595)) (apply ?596 ?597)) (apply ?598 ?597) =>= apply ?595 (apply (apply (apply s ?596) ?598) ?597) [598, 597, 596, 595] by Super 116 with 3 at 1,3
% 1.12/0.58 Id : 13, {_}: apply (apply (apply s (apply k ?51)) ?52) ?53 =>= apply ?51 (apply ?52 ?53) [53, 52, 51] by Super 2 with 3 at 1,3
% 1.12/0.58 Id : 1263, {_}: apply ?595 (apply (apply ?596 ?597) (apply ?598 ?597)) =?= apply ?595 (apply (apply (apply s ?596) ?598) ?597) [598, 597, 596, 595] by Demod 135 with 13 at 2
% 1.12/0.58 Id : 14, {_}: apply (apply (apply s k) ?55) ?56 =>= ?56 [56, 55] by Super 2 with 3 at 3
% 1.12/0.58 Id : 60, {_}: apply (apply (apply s (apply s k)) ?285) ?286 =>= apply ?285 ?286 [286, 285] by Super 2 with 14 at 3
% 1.12/0.58 Id : 5, {_}: apply (apply (apply s ?14) (apply (apply s ?15) ?16)) ?17 =?= apply (apply ?14 ?17) (apply (apply ?15 ?17) (apply ?16 ?17)) [17, 16, 15, 14] by Super 4 with 2 at 2,3
% 1.12/0.58 Id : 1726, {_}: apply combinator (apply (apply (apply s (apply k combinator)) (apply (apply s (apply s (apply k combinator))) (apply (apply s k) ?6244))) (apply (apply s (apply s (apply k combinator))) (apply (apply s k) ?6244))) === apply combinator (apply (apply (apply s (apply k combinator)) (apply (apply s (apply s (apply k combinator))) (apply (apply s k) ?6244))) (apply (apply s (apply s (apply k combinator))) (apply (apply s k) ?6244))) [6244] by Super 1725 with 14 at 2,2,2
% 1.12/0.58 Id : 1725, {_}: apply combinator (apply (apply ?6240 ?6241) (apply ?6242 ?6241)) =?= apply combinator (apply (apply (apply s (apply k combinator)) (apply (apply s ?6240) ?6242)) ?6241) [6242, 6241, 6240] by Super 1703 with 3 at 1,2
% 1.12/0.58 Id : 1703, {_}: apply (apply ?6195 ?6196) (apply (apply ?6197 ?6196) (apply ?6198 ?6196)) =?= apply combinator (apply (apply (apply s ?6195) (apply (apply s ?6197) ?6198)) ?6196) [6198, 6197, 6196, 6195] by Super 1677 with 5 at 2,3
% 1.12/0.58 Id : 1677, {_}: apply ?6087 ?6088 =<= apply combinator (apply ?6087 ?6088) [6088, 6087] by Demod 1652 with 60 at 2
% 1.12/0.58 Id : 1652, {_}: apply (apply (apply s (apply s k)) ?6087) ?6088 =>= apply combinator (apply ?6087 ?6088) [6088, 6087] by Super 1594 with 14 at 2,3
% 1.12/0.58 Id : 1594, {_}: apply (apply (apply s ?5806) ?5807) ?5808 =<= apply combinator (apply (apply ?5806 ?5808) (apply ?5807 ?5808)) [5808, 5807, 5806] by Super 1 with 1263 at 3
% 1.12/0.58 Id : 1, {_}: ?1 =<= apply combinator ?1 [1] by prove_fixed_point ?1
% 1.12/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 1.12/0.58 30687: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.235658 using nrkbo
%------------------------------------------------------------------------------