%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : COL058-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n022.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:59 EDT 2022
% Result : Unsatisfiable 0.13s 0.35s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COL058-2 : TPTP v8.1.0. Released v1.0.0.
% 0.07/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.13/0.34 % Computer : n022.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 13:31:22 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 26255: Facts:
% 0.13/0.34 26255: Id : 2, {_}:
% 0.13/0.34 response (response lark ?2) ?3 =?= response ?2 (response ?3 ?3)
% 0.13/0.34 [3, 2] by lark_exists ?2 ?3
% 0.13/0.34 26255: Goal:
% 0.13/0.34 26255: Id : 1, {_}:
% 0.13/0.34 response
% 0.13/0.34 (response
% 0.13/0.34 (response lark
% 0.13/0.34 (response (response lark (response lark lark))
% 0.13/0.34 (response lark (response lark lark))))
% 0.13/0.34 (response lark (response lark lark)))
% 0.13/0.34 (response
% 0.13/0.34 (response lark
% 0.13/0.34 (response (response lark (response lark lark))
% 0.13/0.34 (response lark (response lark lark))))
% 0.13/0.34 (response lark (response lark lark)))
% 0.13/0.34 =>=
% 0.13/0.34 response
% 0.13/0.34 (response lark
% 0.13/0.34 (response (response lark (response lark lark))
% 0.13/0.34 (response lark (response lark lark))))
% 0.13/0.34 (response lark (response lark lark))
% 0.13/0.34 [] by prove_the_bird_exists
% 0.13/0.35 Statistics :
% 0.13/0.35 Max weight : 39
% 0.13/0.35 Found proof, 0.006415s
% 0.13/0.35 % SZS status Unsatisfiable for theBenchmark.p
% 0.13/0.35 % SZS output start CNFRefutation for theBenchmark.p
% 0.13/0.35 Id : 3, {_}: response (response lark ?5) ?6 =?= response ?5 (response ?6 ?6) [6, 5] by lark_exists ?5 ?6
% 0.13/0.35 Statistics :
% 0.13/0.35 Max weight : 39
% 0.13/0.35 Found proof, 0.007248s
% 0.13/0.35 % SZS status Unsatisfiable for theBenchmark.p
% 0.13/0.35 % SZS output start CNFRefutation for theBenchmark.p
% 0.13/0.35 Id : 3, {_}: response (response lark ?5) ?6 =?= response ?5 (response ?6 ?6) [6, 5] by lark_exists ?5 ?6
% 0.13/0.35 Id : 2, {_}: response (response lark ?2) ?3 =?= response ?2 (response ?3 ?3) [3, 2] by lark_exists ?2 ?3
% 0.13/0.35 Id : 2, {_}: response (response lark ?2) ?3 =?= response ?2 (response ?3 ?3) [3, 2] by lark_exists ?2 ?3
% 0.13/0.35 Id : 11, {_}: response (response lark ?20) (response ?21 ?21) =<= response ?20 (response (response lark (response ?21 ?21)) ?21) [21, 20] by Super 3 with 2 at 2,3
% 0.13/0.35 Id : 14, {_}: response (response lark ?29) (response ?30 ?30) =<= response ?29 (response (response (response lark lark) ?30) ?30) [30, 29] by Super 11 with 2 at 1,2,3
% 0.13/0.35 Id : 11, {_}: response (response lark ?20) (response ?21 ?21) =<= response ?20 (response (response lark (response ?21 ?21)) ?21) [21, 20] by Super 3 with 2 at 2,3
% 0.13/0.35 Id : 14, {_}: response (response lark ?29) (response ?30 ?30) =<= response ?29 (response (response (response lark lark) ?30) ?30) [30, 29] by Super 11 with 2 at 1,2,3
% 0.13/0.35 Id : 89, {_}: response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) === response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 88 with 2 at 1,2
% 0.13/0.35 Id : 89, {_}: response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) === response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 88 with 2 at 1,2
% 0.13/0.35 Id : 88, {_}: response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 87 with 2 at 2,1,2
% 0.13/0.35 Id : 88, {_}: response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 87 with 2 at 2,1,2
% 0.13/0.35 Id : 87, {_}: response (response lark (response (response lark lark) (response (response lark (response lark lark)) (response lark (response lark lark))))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 86 with 14 at 2,1,2
% 0.13/0.35 Id : 87, {_}: response (response lark (response (response lark lark) (response (response lark (response lark lark)) (response lark (response lark lark))))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 86 with 14 at 2,1,2
% 0.13/0.35 Id : 86, {_}: response (response lark (response lark (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 85 with 2 at 2
% 0.13/0.35 Id : 85, {_}: response (response lark (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response lark (response lark lark)) (response lark (response lark lark))) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 9 with 14 at 2
% 0.13/0.35 Id : 86, {_}: response (response lark (response lark (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))))) (response lark (response lark lark)) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 85 with 2 at 2
% 0.13/0.35 Id : 85, {_}: response (response lark (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response lark (response lark lark)) (response lark (response lark lark))) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 9 with 14 at 2
% 0.13/0.35 Id : 9, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 8 with 2 at 1,3
% 0.13/0.35 Id : 8, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by Demod 7 with 2 at 1,2,2
% 0.13/0.35 Id : 9, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) =>= response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)) [] by Demod 8 with 2 at 1,3
% 0.13/0.35 Id : 7, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by Demod 1 with 2 at 1,1,2
% 0.13/0.35 Id : 8, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by Demod 7 with 2 at 1,2,2
% 0.13/0.35 Id : 7, {_}: response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by Demod 1 with 2 at 1,1,2
% 0.13/0.35 Id : 1, {_}: response (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by prove_the_bird_exists
% 0.13/0.35 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.35 26255: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.009848 using nrkbo
% 0.13/0.35 Id : 1, {_}: response (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) =>= response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)) [] by prove_the_bird_exists
% 0.13/0.35 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.35 26258: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 0.009784 using nrkbo
%------------------------------------------------------------------------------