%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : CAT010-10 : TPTP v8.1.0. Released v7.3.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:04:24 EDT 2022
% Result : Unsatisfiable 4.69s 1.49s
% Output : CNFRefutation 4.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : CAT010-10 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n022.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 : Sun May 29 22:19:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 16076: Facts:
% 0.12/0.33 16076: Id : 2, {_}: ifeq3 ?2 ?2 ?3 ?4 =>= ?3 [4, 3, 2] by ifeq_axiom ?2 ?3 ?4
% 0.12/0.33 16076: Id : 3, {_}: ifeq2 ?6 ?6 ?7 ?8 =>= ?7 [8, 7, 6] by ifeq_axiom_001 ?6 ?7 ?8
% 0.12/0.33 16076: Id : 4, {_}:
% 0.12/0.33 ifeq ?10 ?10 ?11 ?12 =>= ?11
% 0.12/0.33 [12, 11, 10] by ifeq_axiom_002 ?10 ?11 ?12
% 0.12/0.33 16076: Id : 5, {_}:
% 0.12/0.33 ifeq (equivalent ?14 ?15) true (there_exists ?14) true =>= true
% 0.12/0.33 [15, 14] by equivalence_implies_existence1 ?14 ?15
% 0.12/0.33 16076: Id : 6, {_}:
% 0.12/0.33 ifeq2 (equivalent ?17 ?18) true ?17 ?18 =>= ?18
% 0.12/0.33 [18, 17] by equivalence_implies_existence2 ?17 ?18
% 0.12/0.33 16076: Id : 7, {_}:
% 0.12/0.33 ifeq (there_exists ?20) true (equivalent ?20 ?20) true =>= true
% 0.12/0.33 [20] by existence_and_equality_implies_equivalence1 ?20
% 0.12/0.33 16076: Id : 8, {_}:
% 0.12/0.33 ifeq (there_exists (domain ?22)) true (there_exists ?22) true
% 0.12/0.33 =>=
% 0.12/0.33 true
% 0.12/0.33 [22] by domain_has_elements ?22
% 0.12/0.33 16076: Id : 9, {_}:
% 0.12/0.33 ifeq (there_exists (codomain ?24)) true (there_exists ?24) true
% 0.12/0.33 =>=
% 0.12/0.33 true
% 0.12/0.33 [24] by codomain_has_elements ?24
% 0.12/0.33 16076: Id : 10, {_}:
% 0.12/0.33 ifeq (there_exists (compose ?26 ?27)) true
% 0.12/0.33 (there_exists (domain ?26)) true
% 0.12/0.33 =>=
% 0.12/0.33 true
% 0.12/0.33 [27, 26] by composition_implies_domain ?26 ?27
% 0.12/0.33 16076: Id : 11, {_}:
% 0.12/0.33 ifeq2 (there_exists (compose ?29 ?30)) true (domain ?29)
% 0.12/0.33 (codomain ?30)
% 0.12/0.33 =>=
% 0.12/0.33 codomain ?30
% 0.12/0.33 [30, 29] by domain_codomain_composition1 ?29 ?30
% 0.12/0.33 16076: Id : 12, {_}:
% 0.12/0.33 ifeq (there_exists (domain ?32)) true
% 0.12/0.33 (ifeq3 (domain ?32) (codomain ?33) (there_exists (compose ?32 ?33))
% 0.12/0.33 true) true
% 0.12/0.33 =>=
% 0.12/0.33 true
% 0.12/0.33 [33, 32] by domain_codomain_composition2 ?32 ?33
% 0.12/0.33 16076: Id : 13, {_}:
% 0.12/0.33 compose ?35 (compose ?36 ?37) =?= compose (compose ?35 ?36) ?37
% 0.12/0.33 [37, 36, 35] by associativity_of_compose ?35 ?36 ?37
% 0.12/0.33 16076: Id : 14, {_}: compose ?39 (domain ?39) =>= ?39 [39] by compose_domain ?39
% 0.12/0.33 16076: Id : 15, {_}: compose (codomain ?41) ?41 =>= ?41 [41] by compose_codomain ?41
% 0.12/0.33 16076: Id : 16, {_}: there_exists (compose a b) =>= true [] by ab_exists
% 0.12/0.33 16076: Goal:
% 0.12/0.33 16076: Id : 1, {_}:
% 0.12/0.33 codomain (compose a b) =>= codomain a
% 0.12/0.33 [] by prove_codomain_of_ab_equals_codomain_of_a
% 4.69/1.49 Statistics :
% 4.69/1.49 Max weight : 14
% 4.69/1.49 Found proof, 1.160978s
% 4.69/1.49 % SZS status Unsatisfiable for theBenchmark.p
% 4.69/1.49 % SZS output start CNFRefutation for theBenchmark.p
% 4.69/1.49 Id : 13, {_}: compose ?35 (compose ?36 ?37) =<= compose (compose ?35 ?36) ?37 [37, 36, 35] by associativity_of_compose ?35 ?36 ?37
% 4.69/1.49 Id : 3, {_}: ifeq2 ?6 ?6 ?7 ?8 =>= ?7 [8, 7, 6] by ifeq_axiom_001 ?6 ?7 ?8
% 4.69/1.49 Id : 4, {_}: ifeq ?10 ?10 ?11 ?12 =>= ?11 [12, 11, 10] by ifeq_axiom_002 ?10 ?11 ?12
% 4.69/1.49 Id : 16, {_}: there_exists (compose a b) =>= true [] by ab_exists
% 4.69/1.49 Id : 10, {_}: ifeq (there_exists (compose ?26 ?27)) true (there_exists (domain ?26)) true =>= true [27, 26] by composition_implies_domain ?26 ?27
% 4.69/1.49 Id : 8, {_}: ifeq (there_exists (domain ?22)) true (there_exists ?22) true =>= true [22] by domain_has_elements ?22
% 4.69/1.49 Id : 15, {_}: compose (codomain ?41) ?41 =>= ?41 [41] by compose_codomain ?41
% 4.69/1.49 Id : 11, {_}: ifeq2 (there_exists (compose ?29 ?30)) true (domain ?29) (codomain ?30) =>= codomain ?30 [30, 29] by domain_codomain_composition1 ?29 ?30
% 4.69/1.49 Id : 2447, {_}: ifeq2 (there_exists ?2059) true (domain (codomain ?2059)) (codomain ?2059) =>= codomain ?2059 [2059] by Super 11 with 15 at 1,1,2
% 4.69/1.49 Id : 63, {_}: ifeq true true (there_exists (domain a)) true =>= true [] by Super 10 with 16 at 1,2
% 4.69/1.49 Id : 73, {_}: there_exists (domain a) =>= true [] by Demod 63 with 4 at 2
% 4.69/1.49 Id : 84, {_}: ifeq true true (there_exists a) true =>= true [] by Super 8 with 73 at 1,2
% 4.69/1.49 Id : 91, {_}: there_exists a =>= true [] by Demod 84 with 4 at 2
% 4.69/1.49 Id : 2458, {_}: ifeq2 true true (domain (codomain a)) (codomain a) =>= codomain a [] by Super 2447 with 91 at 1,2
% 4.69/1.49 Id : 2510, {_}: domain (codomain a) =>= codomain a [] by Demod 2458 with 3 at 2
% 4.69/1.49 Id : 7731, {_}: ifeq2 (there_exists (compose (codomain a) ?4978)) true (codomain a) (codomain ?4978) =>= codomain ?4978 [4978] by Super 11 with 2510 at 3,2
% 4.69/1.49 Id : 56, {_}: compose (codomain ?137) (compose ?137 ?138) =>= compose ?137 ?138 [138, 137] by Super 13 with 15 at 1,3
% 4.69/1.49 Id : 16185, {_}: ifeq2 (there_exists (compose a ?9789)) true (codomain a) (codomain (compose a ?9789)) =>= codomain (compose a ?9789) [9789] by Super 7731 with 56 at 1,1,2
% 4.69/1.49 Id : 16266, {_}: ifeq2 true true (codomain a) (codomain (compose a b)) =>= codomain (compose a b) [] by Super 16185 with 16 at 1,2
% 4.69/1.49 Id : 16558, {_}: codomain a =<= codomain (compose a b) [] by Demod 16266 with 3 at 2
% 4.69/1.49 Id : 16834, {_}: codomain a === codomain a [] by Demod 1 with 16558 at 2
% 4.69/1.49 Id : 1, {_}: codomain (compose a b) =>= codomain a [] by prove_codomain_of_ab_equals_codomain_of_a
% 4.69/1.49 % SZS output end CNFRefutation for theBenchmark.p
% 4.69/1.49 16078: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 1.16279 using lpo
%------------------------------------------------------------------------------