%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET677+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 : 300s % DateTime : Mon Jun 24 14:22:12 EDT 2024 % Result : Theorem 0.63s 0.73s % Output : CNFRefutation 0.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET677+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n018.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 : 300 % 0.13/0.34 % DateTime : Sun Jun 23 12:43:24 EDT 2024 % 0.13/0.35 % CPUTime : % 0.60/0.61 start to proof:theBenchmark % 0.61/0.71 %------------------------------------------- % 0.61/0.71 % File :CSE---1.7 % 0.61/0.71 % Problem :theBenchmark % 0.61/0.71 % Transform :cnf % 0.61/0.71 % Format :tptp:raw % 0.61/0.71 % Command :java -jar mcs_scs.jar %d %s % 0.61/0.71 % 0.61/0.71 % Result :Theorem 0.040000s % 0.61/0.71 % Output :CNFRefutation 0.040000s % 0.61/0.71 %------------------------------------------- % 0.61/0.72 %-------------------------------------------------------------------------- % 0.61/0.72 % File : SET677+3 : TPTP v8.2.0. Released v2.2.0. % 0.61/0.72 % Domain : Set Theory (Relations) % 0.61/0.72 % Problem : Id on X a subset of R => X is domain of R & X is range of R % 0.61/0.72 % Version : [Wor90] axioms : Reduced > Incomplete. % 0.61/0.72 % English : If the identity relation on X is a subset of a relation R from % 0.61/0.72 % X to Y then X is the domain of R and X is the range of R. % 0.61/0.72 % 0.61/0.72 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 0.61/0.72 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 0.61/0.72 % Source : [ILF] % 0.61/0.72 % Names : RELSET_1 (44) [Wor90] % 0.61/0.72 % 0.61/0.72 % Status : Theorem % 0.61/0.72 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.10 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.16 v3.3.0, 0.07 v3.2.0, 0.09 v3.1.0, 0.00 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.25 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 0.61/0.72 % Syntax : Number of formulae : 35 ( 2 unt; 0 def) % 0.61/0.72 % Number of atoms : 135 ( 9 equ) % 0.61/0.72 % Maximal formula atoms : 7 ( 3 avg) % 0.61/0.72 % Number of connectives : 104 ( 4 ~; 0 |; 13 &) % 0.61/0.72 % ( 11 <=>; 76 =>; 0 <=; 0 <~>) % 0.61/0.72 % Maximal formula depth : 11 ( 6 avg) % 0.61/0.72 % Maximal term depth : 3 ( 1 avg) % 0.61/0.72 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 0.61/0.72 % Number of functors : 14 ( 14 usr; 2 con; 0-3 aty) % 0.61/0.72 % Number of variables : 77 ( 70 !; 7 ?) % 0.61/0.72 % SPC : FOF_THM_RFO_SEQ % 0.61/0.72 % 0.61/0.72 % Comments : % 0.61/0.72 %-------------------------------------------------------------------------- % 0.61/0.72 %---- line(relset_1 - th(31),1916588) % 0.61/0.72 fof(p1,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ! [D] : % 0.61/0.72 ( ilf_type(D,relation_type(C,B)) % 0.61/0.72 => ( subset(identity_relation_of(C),D) % 0.61/0.72 => ( C = domain(C,B,D) % 0.61/0.72 & subset(C,range(C,B,D)) ) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(relset_1 - th(32),1916604) % 0.61/0.72 fof(p2,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ! [D] : % 0.61/0.72 ( ilf_type(D,relation_type(B,C)) % 0.61/0.72 => ( subset(identity_relation_of(C),D) % 0.61/0.72 => ( subset(C,domain(B,C,D)) % 0.61/0.72 & C = range(B,C,D) ) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(relat_1 - df(10),1918876) % 0.61/0.72 fof(p3,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ! [D] : % 0.61/0.72 ( ilf_type(D,set_type) % 0.61/0.72 => ( member(ordered_pair(C,D),identity_relation_of(B)) % 0.61/0.72 <=> ( member(C,B) % 0.61/0.72 & C = D ) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- declaration(line(relat_1 - df(10),1918876)) % 0.61/0.72 fof(p4,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ilf_type(identity_relation_of(B),binary_relation_type) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(relset_1 - axiom517,1916837) % 0.61/0.72 fof(p5,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ( ilf_type(C,identity_relation_of_type(B)) % 0.61/0.72 <=> ilf_type(C,relation_type(B,B)) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- type_nonempty(line(relset_1 - axiom517,1916837)) % 0.61/0.72 fof(p6,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ? [C] : ilf_type(C,identity_relation_of_type(B)) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(relat_1 - df(3),1917829) % 0.61/0.72 fof(p7,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,binary_relation_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,binary_relation_type) % 0.61/0.72 => ( subset(B,C) % 0.61/0.72 <=> ! [D] : % 0.61/0.72 ( ilf_type(D,set_type) % 0.61/0.72 => ! [E] : % 0.61/0.72 ( ilf_type(E,set_type) % 0.61/0.72 => ( member(ordered_pair(D,E),B) % 0.61/0.72 => member(ordered_pair(D,E),C) ) ) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(boole - df(8),1909359) % 0.61/0.72 fof(p8,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ( B = C % 0.61/0.72 <=> ( subset(B,C) % 0.61/0.72 & subset(C,B) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- declaration(op(domain_of,1,function)) % 0.61/0.72 fof(p9,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,binary_relation_type) % 0.61/0.72 => ilf_type(domain_of(B),set_type) ) ). % 0.61/0.72 % 0.61/0.72 %---- declaration(op(range_of,1,function)) % 0.61/0.72 fof(p10,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,binary_relation_type) % 0.61/0.72 => ilf_type(range_of(B),set_type) ) ). % 0.61/0.72 % 0.61/0.72 %---- declaration(op(ordered_pair,2,function)) % 0.61/0.72 fof(p11,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(relat_1 - axiom518,1917641) % 0.61/0.72 fof(p12,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ( ilf_type(B,binary_relation_type) % 0.61/0.72 <=> ( relation_like(B) % 0.61/0.72 & ilf_type(B,set_type) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- type_nonempty(line(relat_1 - axiom518,1917641)) % 0.61/0.72 fof(p13,axiom, % 0.61/0.72 ? [B] : ilf_type(B,binary_relation_type) ). % 0.61/0.72 % 0.61/0.72 %---- line(relset_1 - df(1),1916080) % 0.61/0.72 fof(p14,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ( ! [D] : % 0.61/0.72 ( ilf_type(D,subset_type(cross_product(B,C))) % 0.61/0.72 => ilf_type(D,relation_type(B,C)) ) % 0.61/0.72 & ! [E] : % 0.61/0.72 ( ilf_type(E,relation_type(B,C)) % 0.61/0.72 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 0.61/0.72 fof(p15,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(hidden - axiom519,1832648) % 0.61/0.72 fof(p16,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ( ilf_type(C,subset_type(B)) % 0.61/0.72 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- type_nonempty(line(hidden - axiom519,1832648)) % 0.61/0.72 fof(p17,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(tarski - df(3),1832749) % 0.61/0.72 fof(p18,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ( subset(B,C) % 0.61/0.72 <=> ! [D] : % 0.61/0.72 ( ilf_type(D,set_type) % 0.61/0.72 => ( member(D,B) % 0.61/0.72 => member(D,C) ) ) ) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- property(reflexivity,op(subset,2,predicate)) % 0.61/0.72 fof(p19,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => subset(B,B) ) ). % 0.61/0.72 % 0.61/0.72 %---- property(reflexivity,op(subset,2,predicate)) % 0.61/0.72 fof(p20,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,binary_relation_type) % 0.61/0.72 => subset(B,B) ) ). % 0.61/0.72 % 0.61/0.72 %---- declaration(op(cross_product,2,function)) % 0.61/0.72 fof(p21,axiom, % 0.61/0.72 ! [B] : % 0.61/0.72 ( ilf_type(B,set_type) % 0.61/0.72 => ! [C] : % 0.61/0.72 ( ilf_type(C,set_type) % 0.61/0.72 => ilf_type(cross_product(B,C),set_type) ) ) ). % 0.61/0.72 % 0.61/0.72 %---- line(hidden - axiom521,1832644) % 0.61/0.72 fof(p22,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ! [C] : % 0.61/0.73 ( ilf_type(C,set_type) % 0.61/0.73 => ( member(B,power_set(C)) % 0.61/0.73 <=> ! [D] : % 0.61/0.73 ( ilf_type(D,set_type) % 0.61/0.73 => ( member(D,B) % 0.61/0.73 => member(D,C) ) ) ) ) ) ). % 0.61/0.73 % 0.61/0.73 %---- declaration(line(hidden - axiom521,1832644)) % 0.61/0.73 fof(p23,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ( ~ empty(power_set(B)) % 0.61/0.73 & ilf_type(power_set(B),set_type) ) ) ). % 0.61/0.73 % 0.61/0.73 %---- line(hidden - axiom522,1832640) % 0.61/0.73 fof(p24,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ! [C] : % 0.61/0.73 ( ( ~ empty(C) % 0.61/0.73 & ilf_type(C,set_type) ) % 0.61/0.73 => ( ilf_type(B,member_type(C)) % 0.61/0.73 <=> member(B,C) ) ) ) ). % 0.61/0.73 % 0.61/0.73 %---- type_nonempty(line(hidden - axiom522,1832640)) % 0.61/0.73 fof(p25,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ( ~ empty(B) % 0.61/0.73 & ilf_type(B,set_type) ) % 0.61/0.73 => ? [C] : ilf_type(C,member_type(B)) ) ). % 0.61/0.73 % 0.61/0.73 %---- line(relat_1 - df(1),1917627) % 0.61/0.73 fof(p26,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ( relation_like(B) % 0.61/0.73 <=> ! [C] : % 0.61/0.73 ( ilf_type(C,set_type) % 0.61/0.73 => ( member(C,B) % 0.61/0.73 => ? [D] : % 0.61/0.73 ( ilf_type(D,set_type) % 0.61/0.73 & ? [E] : % 0.61/0.73 ( ilf_type(E,set_type) % 0.61/0.73 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 0.61/0.73 % 0.61/0.73 %---- conditional_cluster(axiom524,relation_like) % 0.61/0.73 fof(p27,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ! [C] : % 0.61/0.73 ( ilf_type(C,set_type) % 0.61/0.73 => ! [D] : % 0.61/0.73 ( ilf_type(D,subset_type(cross_product(B,C))) % 0.61/0.73 => relation_like(D) ) ) ) ). % 0.61/0.73 % 0.61/0.73 %---- line(hidden - axiom525,1832628) % 0.61/0.73 fof(p28,axiom, % 0.61/0.73 ! [B] : % 0.61/0.73 ( ilf_type(B,set_type) % 0.61/0.73 => ( empty(B) % 0.61/0.73 <=> ! [C] : % 0.61/0.73 ( ilf_type(C,set_type) % 0.63/0.73 => ~ member(C,B) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %---- conditional_cluster(axiom526,empty) % 0.63/0.73 fof(p29,axiom, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ( empty(B) % 0.63/0.73 & ilf_type(B,set_type) ) % 0.63/0.73 => relation_like(B) ) ). % 0.63/0.73 % 0.63/0.73 %---- line(relset_1 - axiom530,1916330) % 0.63/0.73 fof(p30,axiom, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ilf_type(B,set_type) % 0.63/0.73 => ! [C] : % 0.63/0.73 ( ilf_type(C,set_type) % 0.63/0.73 => ! [D] : % 0.63/0.73 ( ilf_type(D,relation_type(B,C)) % 0.63/0.73 => domain(B,C,D) = domain_of(D) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %---- declaration(line(relset_1 - axiom530,1916330)) % 0.63/0.73 fof(p31,axiom, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ilf_type(B,set_type) % 0.63/0.73 => ! [C] : % 0.63/0.73 ( ilf_type(C,set_type) % 0.63/0.73 => ! [D] : % 0.63/0.73 ( ilf_type(D,relation_type(B,C)) % 0.63/0.73 => ilf_type(domain(B,C,D),subset_type(B)) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %---- line(relset_1 - axiom531,1916334) % 0.63/0.73 fof(p32,axiom, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ilf_type(B,set_type) % 0.63/0.73 => ! [C] : % 0.63/0.73 ( ilf_type(C,set_type) % 0.63/0.73 => ! [D] : % 0.63/0.73 ( ilf_type(D,relation_type(B,C)) % 0.63/0.73 => range(B,C,D) = range_of(D) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %---- declaration(line(relset_1 - axiom531,1916334)) % 0.63/0.73 fof(p33,axiom, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ilf_type(B,set_type) % 0.63/0.73 => ! [C] : % 0.63/0.73 ( ilf_type(C,set_type) % 0.63/0.73 => ! [D] : % 0.63/0.73 ( ilf_type(D,relation_type(B,C)) % 0.63/0.73 => ilf_type(range(B,C,D),subset_type(C)) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %---- declaration(set) % 0.63/0.73 fof(p34,axiom, % 0.63/0.73 ! [B] : ilf_type(B,set_type) ). % 0.63/0.73 % 0.63/0.73 %---- line(relset_1 - th(44),1916841) % 0.63/0.73 fof(prove_relset_1_44,conjecture, % 0.63/0.73 ! [B] : % 0.63/0.73 ( ilf_type(B,set_type) % 0.63/0.73 => ! [C] : % 0.63/0.73 ( ilf_type(C,identity_relation_of_type(B)) % 0.63/0.73 => ( subset(identity_relation_of(B),C) % 0.63/0.73 => ( B = domain(B,B,C) % 0.63/0.73 & B = range(B,B,C) ) ) ) ) ). % 0.63/0.73 % 0.63/0.73 %-------------------------------------------------------------------------- % 0.63/0.73 %------------------------------------------- % 0.63/0.73 % Proof found % 0.63/0.73 % SZS status Theorem for theBenchmark % 0.63/0.73 % SZS output start Proof % 0.63/0.73 %ClaNum:116(EqnAxiom:49) % 0.63/0.73 %VarNum:324(SingletonVarNum:102) % 0.63/0.73 %MaxLitNum:7 % 0.63/0.73 %MaxfuncDepth:2 % 0.63/0.73 %SharedTerms:15 % 0.63/0.73 %goalClause: 53 54 102 % 0.63/0.73 %singleGoalClaCount:2 % 0.63/0.73 [50]P1(a1,a2) % 0.63/0.73 [53]P1(a11,f16(a3)) % 0.63/0.73 [54]P3(f17(a3),a11) % 0.63/0.73 [52]P1(x521,a15) % 0.63/0.73 [102]~E(f6(a3,a3,a11),a3)+~E(f27(a3,a3,a11),a3) % 0.63/0.73 [56]P3(x561,x561)+~P1(x561,a15) % 0.63/0.73 [57]P3(x571,x571)+~P1(x571,a2) % 0.63/0.73 [58]~P1(x581,a15)+~P2(f23(x581)) % 0.63/0.73 [59]~P1(x591,a15)+P1(f17(x591),a2) % 0.63/0.73 [69]~P1(x691,a15)+P1(f12(x691),f16(x691)) % 0.63/0.73 [70]~P1(x701,a15)+P1(f18(x701),f29(x701)) % 0.63/0.73 [55]~P2(x551)+P4(x551)+~P1(x551,a15) % 0.63/0.73 [63]~P4(x631)+~P1(x631,a15)+P1(x631,a2) % 0.63/0.73 [66]P4(x661)+~P1(x661,a15)+~P1(x661,a2) % 0.63/0.73 [67]P4(x671)+P5(f7(x671),x671)+~P1(x671,a15) % 0.63/0.73 [68]P2(x681)+P5(f10(x681),x681)+~P1(x681,a15) % 0.63/0.73 [71]P2(x711)+P1(f20(x711),f24(x711))+~P1(x711,a15) % 0.63/0.73 [88]~P1(x882,a15)+~P1(x881,a15)+P1(f19(x881,x882),f28(x882,x881)) % 0.63/0.73 [73]~E(x731,x732)+P3(x731,x732)+~P1(x732,a15)+~P1(x731,a15) % 0.63/0.73 [74]~P2(x741)+~P5(x742,x741)+~P1(x742,a15)+~P1(x741,a15) % 0.63/0.73 [84]P3(x841,x842)+P5(f21(x841,x842),x841)+~P1(x842,a15)+~P1(x841,a15) % 0.63/0.73 [86]P5(f22(x861,x862),x861)+~P1(x862,a15)+~P1(x861,a15)+P5(x861,f23(x862)) % 0.63/0.73 [92]~P1(x922,a15)+~P1(x921,a15)+~P1(x921,f16(x922))+P1(x921,f28(x922,x922)) % 0.63/0.73 [93]P3(x931,x932)+~P1(x932,a15)+~P1(x931,a15)+~P5(f21(x931,x932),x932) % 0.63/0.73 [95]~P1(x952,a15)+~P1(x951,a15)+~P1(x951,f28(x952,x952))+P1(x951,f16(x952)) % 0.63/0.73 [96]~P1(x962,a15)+~P1(x961,a15)+~P5(f22(x961,x962),x962)+P5(x961,f23(x962)) % 0.63/0.73 [87]~P1(x872,a15)+~P1(x871,a15)+~P1(x871,f29(x872))+P1(x871,f24(f23(x872))) % 0.63/0.73 [91]~P1(x912,a15)+~P1(x911,a15)+P1(x911,f29(x912))+~P1(x911,f24(f23(x912))) % 0.63/0.73 [110]P3(x1101,x1102)+~P1(x1102,a2)+~P1(x1101,a2)+P5(f25(f13(x1101,x1102),f14(x1101,x1102)),x1101) % 0.63/0.73 [116]P3(x1161,x1162)+~P1(x1162,a2)+~P1(x1161,a2)+~P5(f25(f13(x1161,x1162),f14(x1161,x1162)),x1162) % 0.63/0.73 [104]~P1(x1042,a15)+~P1(x1041,a15)+~P1(x1043,f28(x1041,x1042))+E(f6(x1041,x1042,x1043),f4(x1043)) % 0.63/0.73 [105]~P1(x1052,a15)+~P1(x1051,a15)+~P1(x1053,f28(x1051,x1052))+E(f27(x1051,x1052,x1053),f26(x1053)) % 0.63/0.73 [112]~P1(x1122,a15)+~P1(x1121,a15)+~P1(x1123,f28(x1121,x1122))+P1(f6(x1121,x1122,x1123),f29(x1121)) % 0.63/0.73 [113]~P1(x1132,a15)+~P1(x1131,a15)+~P1(x1133,f28(x1131,x1132))+P1(f27(x1131,x1132,x1133),f29(x1132)) % 0.63/0.73 [103]P4(x1031)+~P1(x1032,a15)+~P1(x1033,a15)+~P1(x1031,f29(f5(x1033,x1032))) % 0.63/0.73 [106]~P1(x1063,a15)+~P1(x1062,a15)+~P1(x1061,f28(x1062,x1063))+P1(x1061,f29(f5(x1062,x1063))) % 0.63/0.73 [109]~P1(x1093,a15)+~P1(x1092,a15)+P1(x1091,f28(x1092,x1093))+~P1(x1091,f29(f5(x1092,x1093))) % 0.63/0.73 [77]~P3(x772,x771)+~P3(x771,x772)+E(x771,x772)+~P1(x772,a15)+~P1(x771,a15) % 0.63/0.73 [78]~P5(x782,x781)+P2(x781)+~P1(x781,a15)+~P1(x782,a15)+P1(x782,f24(x781)) % 0.63/0.73 [79]P2(x791)+P5(x792,x791)+~P1(x791,a15)+~P1(x792,a15)+~P1(x792,f24(x791)) % 0.63/0.73 [100]~P4(x1001)+~P5(x1002,x1001)+~P1(x1001,a15)+~P1(x1002,a15)+E(f25(f8(x1001,x1002),f9(x1001,x1002)),x1002) % 0.63/0.73 [83]P4(x831)+~P1(x831,a15)+~P1(x833,a15)+~P1(x832,a15)+~E(f7(x831),f25(x832,x833)) % 0.63/0.73 [99]E(x991,x992)+~P1(x992,a15)+~P1(x991,a15)+~P5(f25(x991,x992),f17(x993))+~P1(x993,a15) % 0.63/0.73 [101]P5(x1011,x1012)+~P1(x1012,a15)+~P1(x1011,a15)+~P5(f25(x1011,x1013),f17(x1012))+~P1(x1013,a15) % 0.63/0.73 [107]~P1(x1072,a15)+~P1(x1071,a15)+~P3(f17(x1071),x1073)+~P1(x1073,f28(x1071,x1072))+E(f6(x1071,x1072,x1073),x1071) % 0.63/0.73 [108]~P1(x1081,a15)+~P1(x1082,a15)+~P3(f17(x1082),x1083)+~P1(x1083,f28(x1081,x1082))+E(f27(x1081,x1082,x1083),x1082) % 0.63/0.73 [114]~P1(x1142,a15)+~P1(x1141,a15)+~P3(f17(x1141),x1143)+~P1(x1143,f28(x1142,x1141))+P3(x1141,f6(x1142,x1141,x1143)) % 0.63/0.73 [115]~P1(x1152,a15)+~P1(x1151,a15)+~P3(f17(x1151),x1153)+~P1(x1153,f28(x1151,x1152))+P3(x1151,f27(x1151,x1152,x1153)) % 0.63/0.73 [94]~P5(x941,x943)+P5(x941,x942)+~P3(x943,x942)+~P1(x941,a15)+~P1(x942,a15)+~P1(x943,a15) % 0.63/0.73 [97]P5(x971,x972)+~P5(x971,x973)+~P1(x971,a15)+~P1(x972,a15)+~P1(x973,a15)+~P5(x973,f23(x972)) % 0.63/0.73 [98]~E(x981,x982)+~P5(x981,x983)+~P1(x982,a15)+~P1(x983,a15)+~P1(x981,a15)+P5(f25(x981,x982),f17(x983)) % 0.63/0.73 [111]~P3(x1114,x1113)+~P1(x1112,a15)+~P1(x1111,a15)+~P1(x1113,a2)+~P1(x1114,a2)+~P5(f25(x1111,x1112),x1114)+P5(f25(x1111,x1112),x1113) % 0.63/0.73 %EqnAxiom % 0.63/0.73 [1]E(x11,x11) % 0.63/0.73 [2]E(x22,x21)+~E(x21,x22) % 0.63/0.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.63/0.73 [4]~E(x41,x42)+E(f16(x41),f16(x42)) % 0.63/0.73 [5]~E(x51,x52)+E(f17(x51),f17(x52)) % 0.63/0.73 [6]~E(x61,x62)+E(f23(x61),f23(x62)) % 0.63/0.73 [7]~E(x71,x72)+E(f28(x71,x73),f28(x72,x73)) % 0.63/0.73 [8]~E(x81,x82)+E(f28(x83,x81),f28(x83,x82)) % 0.63/0.73 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 0.63/0.73 [10]~E(x101,x102)+E(f26(x101),f26(x102)) % 0.63/0.73 [11]~E(x111,x112)+E(f27(x111,x113,x114),f27(x112,x113,x114)) % 0.63/0.73 [12]~E(x121,x122)+E(f27(x123,x121,x124),f27(x123,x122,x124)) % 0.63/0.73 [13]~E(x131,x132)+E(f27(x133,x134,x131),f27(x133,x134,x132)) % 0.63/0.73 [14]~E(x141,x142)+E(f7(x141),f7(x142)) % 0.63/0.73 [15]~E(x151,x152)+E(f10(x151),f10(x152)) % 0.63/0.73 [16]~E(x161,x162)+E(f29(x161),f29(x162)) % 0.63/0.73 [17]~E(x171,x172)+E(f5(x171,x173),f5(x172,x173)) % 0.63/0.73 [18]~E(x181,x182)+E(f5(x183,x181),f5(x183,x182)) % 0.63/0.73 [19]~E(x191,x192)+E(f12(x191),f12(x192)) % 0.63/0.73 [20]~E(x201,x202)+E(f25(x201,x203),f25(x202,x203)) % 0.63/0.73 [21]~E(x211,x212)+E(f25(x213,x211),f25(x213,x212)) % 0.63/0.73 [22]~E(x221,x222)+E(f18(x221),f18(x222)) % 0.63/0.73 [23]~E(x231,x232)+E(f8(x231,x233),f8(x232,x233)) % 0.63/0.74 [24]~E(x241,x242)+E(f8(x243,x241),f8(x243,x242)) % 0.63/0.74 [25]~E(x251,x252)+E(f20(x251),f20(x252)) % 0.63/0.74 [26]~E(x261,x262)+E(f24(x261),f24(x262)) % 0.63/0.74 [27]~E(x271,x272)+E(f6(x271,x273,x274),f6(x272,x273,x274)) % 0.63/0.74 [28]~E(x281,x282)+E(f6(x283,x281,x284),f6(x283,x282,x284)) % 0.63/0.74 [29]~E(x291,x292)+E(f6(x293,x294,x291),f6(x293,x294,x292)) % 0.63/0.74 [30]~E(x301,x302)+E(f9(x301,x303),f9(x302,x303)) % 0.63/0.74 [31]~E(x311,x312)+E(f9(x313,x311),f9(x313,x312)) % 0.63/0.74 [32]~E(x321,x322)+E(f21(x321,x323),f21(x322,x323)) % 0.63/0.74 [33]~E(x331,x332)+E(f21(x333,x331),f21(x333,x332)) % 0.63/0.74 [34]~E(x341,x342)+E(f13(x341,x343),f13(x342,x343)) % 0.63/0.74 [35]~E(x351,x352)+E(f13(x353,x351),f13(x353,x352)) % 0.63/0.74 [36]~E(x361,x362)+E(f22(x361,x363),f22(x362,x363)) % 0.63/0.74 [37]~E(x371,x372)+E(f22(x373,x371),f22(x373,x372)) % 0.63/0.74 [38]~E(x381,x382)+E(f14(x381,x383),f14(x382,x383)) % 0.63/0.74 [39]~E(x391,x392)+E(f14(x393,x391),f14(x393,x392)) % 0.63/0.74 [40]~E(x401,x402)+E(f19(x401,x403),f19(x402,x403)) % 0.63/0.74 [41]~E(x411,x412)+E(f19(x413,x411),f19(x413,x412)) % 0.63/0.74 [42]P1(x422,x423)+~E(x421,x422)+~P1(x421,x423) % 0.63/0.74 [43]P1(x433,x432)+~E(x431,x432)+~P1(x433,x431) % 0.63/0.74 [44]P5(x442,x443)+~E(x441,x442)+~P5(x441,x443) % 0.63/0.74 [45]P5(x453,x452)+~E(x451,x452)+~P5(x453,x451) % 0.63/0.74 [46]P3(x462,x463)+~E(x461,x462)+~P3(x461,x463) % 0.63/0.74 [47]P3(x473,x472)+~E(x471,x472)+~P3(x473,x471) % 0.63/0.74 [48]~P2(x481)+P2(x482)+~E(x481,x482) % 0.63/0.74 [49]~P4(x491)+P4(x492)+~E(x491,x492) % 0.63/0.74 % 0.63/0.74 %------------------------------------------- % 0.63/0.74 cnf(119,plain, % 0.63/0.74 (P3(x1191,x1191)), % 0.63/0.74 inference(scs_inference,[],[52,56])). % 0.63/0.74 cnf(163,plain, % 0.63/0.74 (P3(x1631,x1632)+~E(x1631,x1632)), % 0.63/0.74 inference(scs_inference,[],[119,46,47])). % 0.63/0.74 cnf(198,plain, % 0.63/0.74 (P1(a11,f28(a3,a3))+~P1(a11,a15)), % 0.63/0.74 inference(scs_inference,[],[53,52,74,92])). % 0.63/0.74 cnf(211,plain, % 0.63/0.74 (P1(x2111,a15)), % 0.63/0.74 inference(rename_variables,[],[52])). % 0.63/0.74 cnf(213,plain, % 0.63/0.74 (P1(x2131,a15)), % 0.63/0.74 inference(rename_variables,[],[52])). % 0.63/0.74 cnf(216,plain, % 0.63/0.74 (P1(x2161,a15)), % 0.63/0.74 inference(rename_variables,[],[52])). % 0.63/0.74 cnf(219,plain, % 0.63/0.74 (P1(x2191,a15)), % 0.63/0.74 inference(rename_variables,[],[52])). % 0.63/0.74 cnf(225,plain, % 0.63/0.74 ($false), % 0.63/0.74 inference(scs_inference,[],[54,52,211,213,216,219,198,114,108,107,115,163,102]), % 0.63/0.74 ['proof']). % 0.63/0.74 % SZS output end Proof % 0.63/0.74 % Total time :0.040000s %------------------------------------------------------------------------------