%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET664+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 : 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 : 300s % DateTime : Mon Jun 24 14:22:10 EDT 2024 % Result : Theorem 59.06s 59.16s % Output : CNFRefutation 59.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET664+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %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 : 300 % 0.12/0.33 % DateTime : Sun Jun 23 14:16:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 59.06/59.13 %------------------------------------------- % 59.06/59.13 % File :CSE---1.7 % 59.06/59.13 % Problem :theBenchmark % 59.06/59.13 % Transform :cnf % 59.06/59.13 % Format :tptp:raw % 59.06/59.14 % Command :java -jar mcs_scs.jar %d %s % 59.06/59.14 % 59.06/59.14 % Result :Theorem 58.530000s % 59.06/59.14 % Output :CNFRefutation 58.530000s % 59.06/59.14 %------------------------------------------- % 59.06/59.14 %-------------------------------------------------------------------------- % 59.06/59.14 % File : SET664+3 : TPTP v8.2.0. Released v2.2.0. % 59.06/59.14 % Domain : Set Theory (Relations) % 59.06/59.14 % Problem : R (X to Y) is (X to empty set) => R is empty set % 59.06/59.14 % Version : [Wor90] axioms : Reduced > Incomplete. % 59.06/59.14 % English : If a relation R from X to Y is a relation from X to the empty % 59.06/59.14 % set then R is the empty set. % 59.06/59.14 % 59.06/59.14 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 59.06/59.14 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 59.06/59.14 % Source : [ILF] % 59.06/59.14 % Names : RELSET_1 (27) [Wor90] % 59.06/59.14 % 59.06/59.14 % Status : Theorem % 59.06/59.14 % Rating : 0.33 v8.2.0, 0.31 v7.5.0, 0.34 v7.4.0, 0.20 v7.3.0, 0.28 v7.1.0, 0.30 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.33 v6.2.0, 0.28 v6.1.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.39 v4.0.0, 0.38 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.26 v3.3.0, 0.29 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 59.06/59.14 % Syntax : Number of formulae : 35 ( 4 unt; 0 def) % 59.06/59.15 % Number of atoms : 124 ( 12 equ) % 59.06/59.15 % Maximal formula atoms : 7 ( 3 avg) % 59.06/59.15 % Number of connectives : 94 ( 5 ~; 1 |; 9 &) % 59.06/59.15 % ( 9 <=>; 70 =>; 0 <=; 0 <~>) % 59.06/59.15 % Maximal formula depth : 11 ( 6 avg) % 59.06/59.15 % Maximal term depth : 3 ( 1 avg) % 59.06/59.15 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 59.06/59.15 % Number of functors : 13 ( 13 usr; 3 con; 0-3 aty) % 59.06/59.15 % Number of variables : 70 ( 64 !; 6 ?) % 59.06/59.15 % SPC : FOF_THM_RFO_SEQ % 59.06/59.15 % 59.06/59.15 % Comments : % 59.06/59.15 %-------------------------------------------------------------------------- % 59.06/59.15 %---- line(boole - th(30),1909435) % 59.06/59.15 fof(p1,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ( subset(B,empty_set) % 59.06/59.15 => B = empty_set ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(relat_1 - th(64),1918818) % 59.06/59.15 fof(p2,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => ( ( domain_of(B) = empty_set % 59.06/59.15 | range_of(B) = empty_set ) % 59.06/59.15 => B = empty_set ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(relset_1 - th(12),1916203) % 59.06/59.15 fof(p3,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ! [D] : % 59.06/59.15 ( ilf_type(D,relation_type(B,C)) % 59.06/59.15 => ( subset(domain_of(D),B) % 59.06/59.15 & subset(range_of(D),C) ) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(hidden - axiom266,1832636) % 59.06/59.15 fof(p4,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ~ member(B,empty_set) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(line(hidden - axiom266,1832636)) Part 1 % 59.06/59.15 fof(p5a,axiom, % 59.06/59.15 empty(empty_set) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(line(hidden - axiom266,1832636)) Part 2 % 59.06/59.15 fof(p5b,axiom, % 59.06/59.15 type(empty_set,set_type) ). % 59.06/59.15 % 59.06/59.15 %---- line(relset_1 - df(1),1916080) % 59.06/59.15 fof(p6,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ( ! [D] : % 59.06/59.15 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.06/59.15 => ilf_type(D,relation_type(B,C)) ) % 59.06/59.15 & ! [E] : % 59.06/59.15 ( ilf_type(E,relation_type(B,C)) % 59.06/59.15 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 59.06/59.15 fof(p7,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(relat_1 - df(2),1917780) % 59.06/59.15 fof(p8,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,binary_relation_type) % 59.06/59.15 => ( B = C % 59.06/59.15 <=> ! [D] : % 59.06/59.15 ( ilf_type(D,set_type) % 59.06/59.15 => ! [E] : % 59.06/59.15 ( ilf_type(E,set_type) % 59.06/59.15 => ( member(ordered_pair(D,E),B) % 59.06/59.15 <=> member(ordered_pair(D,E),C) ) ) ) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(op(domain_of,1,function)) % 59.06/59.15 fof(p9,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => ilf_type(domain_of(B),set_type) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(op(cross_product,2,function)) % 59.06/59.15 fof(p10,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ilf_type(cross_product(B,C),set_type) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(op(range_of,1,function)) % 59.06/59.15 fof(p11,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => ilf_type(range_of(B),set_type) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(op(ordered_pair,2,function)) % 59.06/59.15 fof(p12,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(relat_1 - axiom267,1917641) % 59.06/59.15 fof(p13,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ( ilf_type(B,binary_relation_type) % 59.06/59.15 <=> ( relation_like(B) % 59.06/59.15 & ilf_type(B,set_type) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- type_nonempty(line(relat_1 - axiom267,1917641)) % 59.06/59.15 fof(p14,axiom, % 59.06/59.15 ? [B] : ilf_type(B,binary_relation_type) ). % 59.06/59.15 % 59.06/59.15 %---- line(hidden - axiom268,1832648) % 59.06/59.15 fof(p15,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ( ilf_type(C,subset_type(B)) % 59.06/59.15 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- type_nonempty(line(hidden - axiom268,1832648)) % 59.06/59.15 fof(p16,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 59.06/59.15 % 59.06/59.15 %---- property(symmetry,op(=,2,predicate)) % 59.06/59.15 fof(p17,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,binary_relation_type) % 59.06/59.15 => ( B = C % 59.06/59.15 => C = B ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- property(reflexivity,op(=,2,predicate)) % 59.06/59.15 fof(p18,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,binary_relation_type) % 59.06/59.15 => B = B ) ). % 59.06/59.15 % 59.06/59.15 %---- line(tarski - df(3),1832749) % 59.06/59.15 fof(p19,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ( subset(B,C) % 59.06/59.15 <=> ! [D] : % 59.06/59.15 ( ilf_type(D,set_type) % 59.06/59.15 => ( member(D,B) % 59.06/59.15 => member(D,C) ) ) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- property(reflexivity,op(subset,2,predicate)) % 59.06/59.15 fof(p20,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => subset(B,B) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(hidden - axiom270,1832628) % 59.06/59.15 fof(p21,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ( empty(B) % 59.06/59.15 <=> ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ~ member(C,B) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(hidden - axiom272,1832644) % 59.06/59.15 fof(p22,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ( member(B,power_set(C)) % 59.06/59.15 <=> ! [D] : % 59.06/59.15 ( ilf_type(D,set_type) % 59.06/59.15 => ( member(D,B) % 59.06/59.15 => member(D,C) ) ) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- declaration(line(hidden - axiom272,1832644)) % 59.06/59.15 fof(p23,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ( ~ empty(power_set(B)) % 59.06/59.15 & ilf_type(power_set(B),set_type) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(hidden - axiom273,1832640) % 59.06/59.15 fof(p24,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ! [C] : % 59.06/59.15 ( ( ~ empty(C) % 59.06/59.15 & ilf_type(C,set_type) ) % 59.06/59.15 => ( ilf_type(B,member_type(C)) % 59.06/59.15 <=> member(B,C) ) ) ) ). % 59.06/59.15 % 59.06/59.15 %---- type_nonempty(line(hidden - axiom273,1832640)) % 59.06/59.15 fof(p25,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ( ~ empty(B) % 59.06/59.15 & ilf_type(B,set_type) ) % 59.06/59.15 => ? [C] : ilf_type(C,member_type(B)) ) ). % 59.06/59.15 % 59.06/59.15 %---- line(relat_1 - df(1),1917627) % 59.06/59.15 fof(p26,axiom, % 59.06/59.15 ! [B] : % 59.06/59.15 ( ilf_type(B,set_type) % 59.06/59.15 => ( relation_like(B) % 59.06/59.15 <=> ! [C] : % 59.06/59.15 ( ilf_type(C,set_type) % 59.06/59.15 => ( member(C,B) % 59.06/59.15 => ? [D] : % 59.06/59.15 ( ilf_type(D,set_type) % 59.06/59.16 & ? [E] : % 59.06/59.16 ( ilf_type(E,set_type) % 59.06/59.16 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- conditional_cluster(axiom274,relation_like) % 59.06/59.16 fof(p27,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ( empty(B) % 59.06/59.16 & ilf_type(B,set_type) ) % 59.06/59.16 => relation_like(B) ) ). % 59.06/59.16 % 59.06/59.16 %---- conditional_cluster(axiom275,relation_like) % 59.06/59.16 fof(p28,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.06/59.16 => relation_like(D) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- line(relset_1 - axiom279,1916330) % 59.06/59.16 fof(p29,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,relation_type(B,C)) % 59.06/59.16 => domain(B,C,D) = domain_of(D) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- declaration(line(relset_1 - axiom279,1916330)) % 59.06/59.16 fof(p30,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,relation_type(B,C)) % 59.06/59.16 => ilf_type(domain(B,C,D),subset_type(B)) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- line(relset_1 - axiom280,1916334) % 59.06/59.16 fof(p31,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,relation_type(B,C)) % 59.06/59.16 => range(B,C,D) = range_of(D) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- declaration(line(relset_1 - axiom280,1916334)) % 59.06/59.16 fof(p32,axiom, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,relation_type(B,C)) % 59.06/59.16 => ilf_type(range(B,C,D),subset_type(C)) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %---- declaration(set) % 59.06/59.16 fof(p33,axiom, % 59.06/59.16 ! [B] : ilf_type(B,set_type) ). % 59.06/59.16 % 59.06/59.16 %---- line(relset_1 - th(27),1916521) % 59.06/59.16 fof(prove_relset_1_27,conjecture, % 59.06/59.16 ! [B] : % 59.06/59.16 ( ilf_type(B,set_type) % 59.06/59.16 => ! [C] : % 59.06/59.16 ( ilf_type(C,set_type) % 59.06/59.16 => ! [D] : % 59.06/59.16 ( ilf_type(D,relation_type(C,B)) % 59.06/59.16 => ( ilf_type(D,relation_type(C,empty_set)) % 59.06/59.16 => D = empty_set ) ) ) ) ). % 59.06/59.16 % 59.06/59.16 %-------------------------------------------------------------------------- % 59.06/59.16 %------------------------------------------- % 59.06/59.16 % Proof found % 59.06/59.16 % SZS status Theorem for theBenchmark % 59.06/59.16 % SZS output start Proof % 59.06/59.16 %ClaNum:108(EqnAxiom:48) % 59.06/59.16 %VarNum:241(SingletonVarNum:76) % 59.06/59.16 %MaxLitNum:6 % 59.06/59.16 %MaxfuncDepth:2 % 59.06/59.16 %SharedTerms:17 % 59.06/59.16 %goalClause: 55 56 57 % 59.06/59.16 %singleGoalClaCount:3 % 59.06/59.16 [49]P1(a1) % 59.06/59.16 [50]P2(a6,a2) % 59.06/59.16 [53]P3(a1,a16) % 59.06/59.16 [57]~E(a12,a1) % 59.06/59.16 [55]P2(a12,f17(a11,a1)) % 59.06/59.16 [56]P2(a12,f17(a11,a7)) % 59.06/59.16 [54]P2(x541,a16) % 59.06/59.16 [61]P6(x611,x611)+~P2(x611,a16) % 59.06/59.16 [67]~P5(x671,a1)+~P2(x671,a16) % 59.06/59.16 [62]~P2(x621,a16)+~P1(f19(x621)) % 59.06/59.16 [74]~P2(x741,a16)+P2(f21(x741),f28(x741)) % 59.06/59.16 [60]~P1(x601)+P4(x601)+~P2(x601,a16) % 59.06/59.16 [66]~P4(x661)+~P2(x661,a16)+P2(x661,a2) % 59.06/59.16 [68]~P2(x681,a16)+~P6(x681,a1)+E(x681,a1) % 59.06/59.16 [71]P4(x711)+~P2(x711,a16)+~P2(x711,a2) % 59.06/59.16 [58]~P2(x581,a2)+E(x581,a1)+~E(f3(x581),a1) % 59.06/59.16 [59]~P2(x591,a2)+E(x591,a1)+~E(f18(x591),a1) % 59.06/59.16 [72]P1(x721)+P5(f20(x721),x721)+~P2(x721,a16) % 59.06/59.16 [73]P4(x731)+P5(f8(x731),x731)+~P2(x731,a16) % 59.06/59.16 [75]P1(x751)+P2(f23(x751),f25(x751))+~P2(x751,a16) % 59.06/59.16 [89]~P2(x892,a16)+~P2(x891,a16)+P2(f14(x891,x892),f17(x892,x891)) % 59.06/59.16 [76]~P1(x761)+~P5(x762,x761)+~P2(x762,a16)+~P2(x761,a16) % 59.06/59.16 [85]P6(x851,x852)+P5(f22(x851,x852),x851)+~P2(x852,a16)+~P2(x851,a16) % 59.06/59.16 [87]P5(f24(x871,x872),x871)+~P2(x872,a16)+~P2(x871,a16)+P5(x871,f19(x872)) % 59.06/59.16 [93]P6(x931,x932)+~P2(x932,a16)+~P2(x931,a16)+~P5(f22(x931,x932),x932) % 59.06/59.16 [95]~P2(x952,a16)+~P2(x951,a16)+~P5(f24(x951,x952),x952)+P5(x951,f19(x952)) % 59.06/59.16 [88]~P2(x882,a16)+~P2(x881,a16)+~P2(x881,f28(x882))+P2(x881,f25(f19(x882))) % 59.06/59.16 [92]~P2(x922,a16)+~P2(x921,a16)+P2(x921,f28(x922))+~P2(x921,f25(f19(x922))) % 59.06/59.16 [96]~P2(x962,a16)+~P2(x961,f17(x962,x963))+P6(f3(x961),x962)+~P2(x963,a16) % 59.06/59.16 [97]~P2(x972,a16)+~P2(x971,f17(x973,x972))+P6(f18(x971),x972)+~P2(x973,a16) % 59.06/59.16 [101]~P2(x1012,a16)+~P2(x1011,a16)+~P2(x1013,f17(x1011,x1012))+E(f5(x1011,x1012,x1013),f3(x1013)) % 59.06/59.16 [102]~P2(x1022,a16)+~P2(x1021,a16)+~P2(x1023,f17(x1021,x1022))+E(f27(x1021,x1022,x1023),f18(x1023)) % 59.06/59.16 [105]~P2(x1052,a16)+~P2(x1051,a16)+~P2(x1053,f17(x1051,x1052))+P2(f5(x1051,x1052,x1053),f28(x1051)) % 59.06/59.16 [106]~P2(x1062,a16)+~P2(x1061,a16)+~P2(x1063,f17(x1061,x1062))+P2(f27(x1061,x1062,x1063),f28(x1062)) % 59.06/59.16 [100]P4(x1001)+~P2(x1002,a16)+~P2(x1003,a16)+~P2(x1001,f28(f4(x1003,x1002))) % 59.06/59.16 [103]~P2(x1033,a16)+~P2(x1032,a16)+~P2(x1031,f17(x1032,x1033))+P2(x1031,f28(f4(x1032,x1033))) % 59.06/59.16 [104]~P2(x1043,a16)+~P2(x1042,a16)+P2(x1041,f17(x1042,x1043))+~P2(x1041,f28(f4(x1042,x1043))) % 59.06/59.16 [81]~P5(x812,x811)+P1(x811)+~P2(x811,a16)+~P2(x812,a16)+P2(x812,f25(x811)) % 59.06/59.16 [82]P1(x821)+P5(x822,x821)+~P2(x821,a16)+~P2(x822,a16)+~P2(x822,f25(x821)) % 59.06/59.16 [99]~P4(x991)+~P5(x992,x991)+~P2(x991,a16)+~P2(x992,a16)+E(f26(f9(x991,x992),f10(x991,x992)),x992) % 59.06/59.16 [107]E(x1071,x1072)+~P2(x1072,a2)+~P2(x1071,a2)+P5(f26(f13(x1071,x1072),f15(x1071,x1072)),x1072)+P5(f26(f13(x1071,x1072),f15(x1071,x1072)),x1071) % 59.06/59.16 [108]E(x1081,x1082)+~P2(x1082,a2)+~P2(x1081,a2)+~P5(f26(f13(x1081,x1082),f15(x1081,x1082)),x1082)+~P5(f26(f13(x1081,x1082),f15(x1081,x1082)),x1081) % 59.06/59.16 [84]P4(x841)+~P2(x841,a16)+~P2(x843,a16)+~P2(x842,a16)+~E(f8(x841),f26(x842,x843)) % 59.06/59.16 [94]~P5(x941,x943)+P5(x941,x942)+~P6(x943,x942)+~P2(x941,a16)+~P2(x942,a16)+~P2(x943,a16) % 59.06/59.16 [98]P5(x981,x982)+~P5(x981,x983)+~P2(x981,a16)+~P2(x982,a16)+~P2(x983,a16)+~P5(x983,f19(x982)) % 59.06/59.16 %EqnAxiom % 59.06/59.16 [1]E(x11,x11) % 59.06/59.16 [2]E(x22,x21)+~E(x21,x22) % 59.06/59.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.06/59.16 [4]~E(x41,x42)+E(f17(x41,x43),f17(x42,x43)) % 59.06/59.16 [5]~E(x51,x52)+E(f17(x53,x51),f17(x53,x52)) % 59.06/59.16 [6]~E(x61,x62)+E(f26(x61,x63),f26(x62,x63)) % 59.06/59.16 [7]~E(x71,x72)+E(f26(x73,x71),f26(x73,x72)) % 59.06/59.16 [8]~E(x81,x82)+E(f3(x81),f3(x82)) % 59.06/59.16 [9]~E(x91,x92)+E(f18(x91),f18(x92)) % 59.06/59.16 [10]~E(x101,x102)+E(f19(x101),f19(x102)) % 59.06/59.16 [11]~E(x111,x112)+E(f28(x111),f28(x112)) % 59.06/59.16 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 59.06/59.16 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 59.06/59.16 [14]~E(x141,x142)+E(f5(x141,x143,x144),f5(x142,x143,x144)) % 59.06/59.16 [15]~E(x151,x152)+E(f5(x153,x151,x154),f5(x153,x152,x154)) % 59.06/59.16 [16]~E(x161,x162)+E(f5(x163,x164,x161),f5(x163,x164,x162)) % 59.06/59.16 [17]~E(x171,x172)+E(f20(x171),f20(x172)) % 59.06/59.16 [18]~E(x181,x182)+E(f8(x181),f8(x182)) % 59.06/59.16 [19]~E(x191,x192)+E(f24(x191,x193),f24(x192,x193)) % 59.06/59.16 [20]~E(x201,x202)+E(f24(x203,x201),f24(x203,x202)) % 59.06/59.16 [21]~E(x211,x212)+E(f15(x211,x213),f15(x212,x213)) % 59.06/59.16 [22]~E(x221,x222)+E(f15(x223,x221),f15(x223,x222)) % 59.06/59.16 [23]~E(x231,x232)+E(f21(x231),f21(x232)) % 59.06/59.16 [24]~E(x241,x242)+E(f9(x241,x243),f9(x242,x243)) % 59.06/59.16 [25]~E(x251,x252)+E(f9(x253,x251),f9(x253,x252)) % 59.06/59.16 [26]~E(x261,x262)+E(f23(x261),f23(x262)) % 59.06/59.16 [27]~E(x271,x272)+E(f25(x271),f25(x272)) % 59.06/59.16 [28]~E(x281,x282)+E(f10(x281,x283),f10(x282,x283)) % 59.06/59.16 [29]~E(x291,x292)+E(f10(x293,x291),f10(x293,x292)) % 59.06/59.16 [30]~E(x301,x302)+E(f13(x301,x303),f13(x302,x303)) % 59.06/59.16 [31]~E(x311,x312)+E(f13(x313,x311),f13(x313,x312)) % 59.06/59.16 [32]~E(x321,x322)+E(f27(x321,x323,x324),f27(x322,x323,x324)) % 59.06/59.16 [33]~E(x331,x332)+E(f27(x333,x331,x334),f27(x333,x332,x334)) % 59.06/59.16 [34]~E(x341,x342)+E(f27(x343,x344,x341),f27(x343,x344,x342)) % 59.06/59.16 [35]~E(x351,x352)+E(f14(x351,x353),f14(x352,x353)) % 59.06/59.16 [36]~E(x361,x362)+E(f14(x363,x361),f14(x363,x362)) % 59.06/59.16 [37]~E(x371,x372)+E(f22(x371,x373),f22(x372,x373)) % 59.06/59.16 [38]~E(x381,x382)+E(f22(x383,x381),f22(x383,x382)) % 59.06/59.16 [39]~P1(x391)+P1(x392)+~E(x391,x392) % 59.06/59.16 [40]P2(x402,x403)+~E(x401,x402)+~P2(x401,x403) % 59.06/59.16 [41]P2(x413,x412)+~E(x411,x412)+~P2(x413,x411) % 59.06/59.16 [42]~P4(x421)+P4(x422)+~E(x421,x422) % 59.06/59.16 [43]P5(x432,x433)+~E(x431,x432)+~P5(x431,x433) % 59.06/59.16 [44]P5(x443,x442)+~E(x441,x442)+~P5(x443,x441) % 59.06/59.16 [45]P3(x452,x453)+~E(x451,x452)+~P3(x451,x453) % 59.06/59.16 [46]P3(x463,x462)+~E(x461,x462)+~P3(x463,x461) % 59.06/59.16 [47]P6(x472,x473)+~E(x471,x472)+~P6(x471,x473) % 59.06/59.16 [48]P6(x483,x482)+~E(x481,x482)+~P6(x483,x481) % 59.06/59.16 % 59.06/59.16 %------------------------------------------- % 59.06/59.16 cnf(109,plain, % 59.06/59.16 (P6(x1091,x1091)), % 59.06/59.16 inference(scs_inference,[],[54,61])). % 59.06/59.16 cnf(111,plain, % 59.06/59.16 (~P5(x1111,a1)), % 59.06/59.16 inference(scs_inference,[],[54,61,67])). % 59.06/59.16 cnf(114,plain, % 59.06/59.16 (P2(x1141,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(116,plain, % 59.06/59.16 (P2(a1,a2)), % 59.06/59.16 inference(scs_inference,[],[54,114,49,61,67,60,66])). % 59.06/59.16 cnf(147,plain, % 59.06/59.16 (P6(x1471,x1472)+~E(x1472,x1471)), % 59.06/59.16 inference(scs_inference,[],[109,47])). % 59.06/59.16 cnf(212,plain, % 59.06/59.16 (E(f3(a12),f5(a11,a1,a12))+~P2(a11,a16)), % 59.06/59.16 inference(scs_inference,[],[54,55,2,101])). % 59.06/59.16 cnf(213,plain, % 59.06/59.16 (E(f3(a12),f5(a11,a1,a12))), % 59.06/59.16 inference(scs_inference,[],[54,212])). % 59.06/59.16 cnf(273,plain, % 59.06/59.16 (P2(f21(x2731),x2732)+~E(f28(x2731),x2732)), % 59.06/59.16 inference(scs_inference,[],[54,74,41])). % 59.06/59.16 cnf(274,plain, % 59.06/59.16 (P2(f21(x2741),f28(x2741))), % 59.06/59.16 inference(equality_inference,[],[273])). % 59.06/59.16 cnf(380,plain, % 59.06/59.16 (P4(x3801)+~E(x3801,a1)), % 59.06/59.16 inference(scs_inference,[],[54,111,73,44])). % 59.06/59.16 cnf(391,plain, % 59.06/59.16 (P6(f18(f14(x3911,x3911)),x3911)), % 59.06/59.16 inference(scs_inference,[],[54,89,97])). % 59.06/59.16 cnf(392,plain, % 59.06/59.16 (E(f18(f14(a1,a1)),a1)), % 59.06/59.16 inference(scs_inference,[],[54,391,68])). % 59.06/59.16 cnf(402,plain, % 59.06/59.16 (~E(a12,f18(f14(a1,a1)))), % 59.06/59.16 inference(scs_inference,[],[57,54,391,68,380,147,2,59,3])). % 59.06/59.16 cnf(403,plain, % 59.06/59.16 (P1(f18(f14(a1,a1)))), % 59.06/59.16 inference(scs_inference,[],[57,54,391,49,68,380,147,2,59,3,39])). % 59.06/59.16 cnf(439,plain, % 59.06/59.16 (P2(x4391,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(440,plain, % 59.06/59.16 (P2(x4401,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(442,plain, % 59.06/59.16 (P5(a1,f19(x4421))), % 59.06/59.16 inference(scs_inference,[],[54,440,439,403,111,76,87])). % 59.06/59.16 cnf(444,plain, % 59.06/59.16 (~P5(x4441,a1)), % 59.06/59.16 inference(rename_variables,[],[111])). % 59.06/59.16 cnf(446,plain, % 59.06/59.16 (~E(f19(x4461),a1)), % 59.06/59.16 inference(scs_inference,[],[54,440,439,403,111,444,76,87,44])). % 59.06/59.16 cnf(3866,plain, % 59.06/59.16 (~P1(f19(x38661))), % 59.06/59.16 inference(scs_inference,[],[54,62])). % 59.06/59.16 cnf(3869,plain, % 59.06/59.16 (P2(f14(x38691,x38691),f17(x38691,x38691))), % 59.06/59.16 inference(scs_inference,[],[446,54,62,2,89])). % 59.06/59.16 cnf(3871,plain, % 59.06/59.16 (~P6(f19(x38711),a1)), % 59.06/59.16 inference(scs_inference,[],[446,54,62,2,89,68])). % 59.06/59.16 cnf(3921,plain, % 59.06/59.16 (P2(x39211,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3923,plain, % 59.06/59.16 (P6(f3(f14(x39231,x39231)),x39231)), % 59.06/59.16 inference(scs_inference,[],[3869,3866,402,54,3921,2,72,96])). % 59.06/59.16 cnf(3924,plain, % 59.06/59.16 (P2(x39241,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3925,plain, % 59.06/59.16 (P2(x39251,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3928,plain, % 59.06/59.16 (P2(x39281,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3929,plain, % 59.06/59.16 (P2(x39291,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3931,plain, % 59.06/59.16 (P2(f21(x39311),f25(f19(x39311)))), % 59.06/59.16 inference(scs_inference,[],[56,3869,3866,402,274,54,3921,3925,3929,3924,3928,2,72,96,97,88])). % 59.06/59.16 cnf(3932,plain, % 59.06/59.16 (P2(x39321,a16)), % 59.06/59.16 inference(rename_variables,[],[54])). % 59.06/59.16 cnf(3933,plain, % 59.06/59.17 (P2(f21(x39331),f28(x39331))), % 59.06/59.17 inference(rename_variables,[],[274])). % 59.06/59.17 cnf(3935,plain, % 59.06/59.17 (P2(a12,f28(f4(a11,a7)))), % 59.06/59.17 inference(scs_inference,[],[56,3869,3866,402,274,54,3921,3925,3929,3932,3924,3928,2,72,96,97,88,103])). % 59.06/59.17 cnf(3936,plain, % 59.06/59.17 (P2(x39361,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3937,plain, % 59.06/59.17 (P2(x39371,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3939,plain, % 59.06/59.17 (E(f5(a11,a7,a12),f3(a12))), % 59.06/59.17 inference(scs_inference,[],[56,3869,3866,402,274,54,3921,3925,3929,3932,3936,3924,3928,3937,2,72,96,97,88,103,101])). % 59.06/59.17 cnf(3940,plain, % 59.06/59.17 (P2(x39401,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3941,plain, % 59.06/59.17 (P2(x39411,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3944,plain, % 59.06/59.17 (P2(x39441,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3945,plain, % 59.06/59.17 (P2(x39451,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3947,plain, % 59.06/59.17 (P2(f5(a11,a7,a12),f28(a11))), % 59.06/59.17 inference(scs_inference,[],[56,3869,3866,402,274,54,3921,3925,3929,3932,3936,3940,3944,3924,3928,3937,3941,3945,2,72,96,97,88,103,101,102,105])). % 59.06/59.17 cnf(3948,plain, % 59.06/59.17 (P2(x39481,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3949,plain, % 59.06/59.17 (P2(x39491,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3952,plain, % 59.06/59.17 (P2(x39521,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3953,plain, % 59.06/59.17 (P2(x39531,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3956,plain, % 59.06/59.17 (P2(x39561,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3957,plain, % 59.06/59.17 (P2(x39571,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3963,plain, % 59.06/59.17 (~P1(f19(x39631))), % 59.06/59.17 inference(rename_variables,[],[3866])). % 59.06/59.17 cnf(3964,plain, % 59.06/59.17 (P2(x39641,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3965,plain, % 59.06/59.17 (P2(x39651,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3967,plain, % 59.06/59.17 (P2(a1,f25(f19(x39671)))), % 59.06/59.17 inference(scs_inference,[],[56,3869,3866,3963,3871,402,442,274,3933,54,3921,3925,3929,3932,3936,3940,3944,3948,3952,3957,3964,3924,3928,3937,3941,3945,3949,3953,3956,3965,2,72,96,97,88,103,101,102,105,106,85,104,82,81])). % 59.06/59.17 cnf(3969,plain, % 59.06/59.17 (P2(x39691,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3970,plain, % 59.06/59.17 (P2(x39701,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(3974,plain, % 59.06/59.17 (P2(f14(x39741,x39742),f17(x39742,x39741))), % 59.06/59.17 inference(scs_inference,[],[56,3869,3866,3963,3871,402,442,446,274,3933,54,3921,3925,3929,3932,3936,3940,3944,3948,3952,3957,3964,3969,3924,3928,3937,3941,3945,3949,3953,3956,3965,3970,2,72,96,97,88,103,101,102,105,106,85,104,82,81,58,89])). % 59.06/59.17 cnf(3992,plain, % 59.06/59.17 (~E(a1,a12)), % 59.06/59.17 inference(scs_inference,[],[57,2])). % 59.06/59.17 cnf(3994,plain, % 59.06/59.17 (P2(x39941,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4002,plain, % 59.06/59.17 (P2(f14(x40021,x40022),f17(x40022,x40021))), % 59.06/59.17 inference(rename_variables,[],[3974])). % 59.06/59.17 cnf(4005,plain, % 59.06/59.17 (P2(f14(x40051,x40052),f17(x40052,x40051))), % 59.06/59.17 inference(rename_variables,[],[3974])). % 59.06/59.17 cnf(4011,plain, % 59.06/59.17 (P2(x40111,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4012,plain, % 59.06/59.17 (P2(x40121,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4015,plain, % 59.06/59.17 (P4(a12)), % 59.06/59.17 inference(scs_inference,[],[3974,4002,4005,3947,3939,3923,3967,3935,3871,57,392,213,54,3994,4012,4011,2,68,3,47,48,40,105,103,106,92,100])). % 59.06/59.17 cnf(4016,plain, % 59.06/59.17 (P2(x40161,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4017,plain, % 59.06/59.17 (P2(x40171,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4021,plain, % 59.06/59.17 (P2(x40211,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4022,plain, % 59.06/59.17 (P2(x40221,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4026,plain, % 59.06/59.17 (P2(x40261,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4027,plain, % 59.06/59.17 (P2(x40271,a16)), % 59.06/59.17 inference(rename_variables,[],[54])). % 59.06/59.17 cnf(4029,plain, % 59.06/59.17 (P6(f18(a12),a1)), % 59.06/59.17 inference(scs_inference,[],[56,3974,4002,4005,3947,3939,3923,3931,3967,3935,3871,3866,57,392,213,55,54,3994,4012,4017,4021,4026,4011,4016,4022,4027,2,68,3,47,48,40,105,103,106,92,100,82,44,96,97])). % 59.06/59.17 cnf(4231,plain, % 59.06/59.17 (P2(a12,a2)), % 59.06/59.17 inference(scs_inference,[],[4015,3939,54,45,66])). % 59.06/59.17 cnf(4234,plain, % 59.06/59.17 (~E(f18(a12),a1)), % 59.06/59.17 inference(scs_inference,[],[57,4015,3939,54,45,66,59])). % 59.06/59.17 cnf(4248,plain, % 59.06/59.17 ($false), % 59.06/59.17 inference(scs_inference,[],[4231,4234,3992,4029,116,54,111,2,107,68]), % 59.06/59.17 ['proof']). % 59.06/59.17 % SZS output end Proof % 59.06/59.17 % Total time :58.530000s %------------------------------------------------------------------------------