%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET654+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.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:09 EDT 2024 % Result : Theorem 59.80s 59.94s % Output : CNFRefutation 59.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SET654+3 : TPTP v8.2.0. Released v2.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 11:11:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 59.80/59.92 %------------------------------------------- % 59.80/59.92 % File :CSE---1.7 % 59.80/59.92 % Problem :theBenchmark % 59.80/59.92 % Transform :cnf % 59.80/59.92 % Format :tptp:raw % 59.80/59.92 % Command :java -jar mcs_scs.jar %d %s % 59.80/59.92 % 59.80/59.92 % Result :Theorem 59.230000s % 59.80/59.92 % Output :CNFRefutation 59.230000s % 59.80/59.92 %------------------------------------------- % 59.80/59.93 %-------------------------------------------------------------------------- % 59.80/59.93 % File : SET654+3 : TPTP v8.2.0. Released v2.2.0. % 59.80/59.93 % Domain : Set Theory (Relations) % 59.80/59.93 % Problem : Y a subset of Y1 => R (X to Y) is (X to Y1) % 59.80/59.93 % Version : [Wor90] axioms : Reduced > Incomplete. % 59.80/59.93 % English : If Y is a subset of Y1 then a relation R from X to Y is a % 59.80/59.93 % relation from X to Y1. % 59.80/59.93 % 59.80/59.93 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 59.80/59.93 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 59.80/59.93 % Source : [ILF] % 59.80/59.93 % Names : RELSET_1 (16) [Wor90] % 59.80/59.93 % 59.80/59.93 % Status : Theorem % 59.80/59.93 % Rating : 0.22 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.20 v7.3.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.24 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.18 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.11 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.80/59.93 % Syntax : Number of formulae : 23 ( 1 unt; 0 def) % 59.80/59.93 % Number of atoms : 92 ( 1 equ) % 59.80/59.93 % Maximal formula atoms : 7 ( 4 avg) % 59.80/59.93 % Number of connectives : 73 ( 4 ~; 0 |; 9 &) % 59.80/59.93 % ( 6 <=>; 54 =>; 0 <=; 0 <~>) % 59.80/59.93 % Maximal formula depth : 11 ( 6 avg) % 59.80/59.93 % Maximal term depth : 3 ( 1 avg) % 59.80/59.93 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 59.80/59.93 % Number of functors : 10 ( 10 usr; 2 con; 0-2 aty) % 59.80/59.93 % Number of variables : 54 ( 49 !; 5 ?) % 59.80/59.93 % SPC : FOF_THM_RFO_SEQ % 59.80/59.93 % 59.80/59.93 % Comments : % 59.80/59.93 %-------------------------------------------------------------------------- % 59.80/59.93 %---- line(boole - th(29),1909428) % 59.80/59.93 fof(p1,axiom, % 59.80/59.93 ! [B] : % 59.80/59.93 ( ilf_type(B,set_type) % 59.80/59.93 => ! [C] : % 59.80/59.93 ( ilf_type(C,set_type) % 59.80/59.93 => ! [D] : % 59.80/59.93 ( ilf_type(D,set_type) % 59.80/59.93 => ( ( subset(B,C) % 59.80/59.93 & subset(C,D) ) % 59.80/59.93 => subset(B,D) ) ) ) ) ). % 59.80/59.93 % 59.80/59.93 %---- line(relset_1 - th(12),1916203) % 59.80/59.93 fof(p2,axiom, % 59.80/59.93 ! [B] : % 59.80/59.93 ( ilf_type(B,set_type) % 59.80/59.93 => ! [C] : % 59.80/59.93 ( ilf_type(C,set_type) % 59.80/59.93 => ! [D] : % 59.80/59.93 ( ilf_type(D,relation_type(B,C)) % 59.80/59.93 => ( subset(domain_of(D),B) % 59.80/59.93 & subset(range_of(D),C) ) ) ) ) ). % 59.80/59.93 % 59.80/59.93 %---- line(relset_1 - th(14),1916237) % 59.80/59.93 fof(p3,axiom, % 59.80/59.93 ! [B] : % 59.80/59.93 ( ilf_type(B,set_type) % 59.80/59.93 => ! [C] : % 59.80/59.93 ( ilf_type(C,set_type) % 59.80/59.93 => ! [D] : % 59.80/59.93 ( ilf_type(D,set_type) % 59.80/59.93 => ! [E] : % 59.80/59.93 ( ilf_type(E,relation_type(D,B)) % 59.80/59.93 => ( subset(range_of(E),C) % 59.80/59.93 => ilf_type(E,relation_type(D,C)) ) ) ) ) ) ). % 59.80/59.93 % 59.80/59.93 %---- line(relset_1 - df(1),1916080) % 59.80/59.94 fof(p4,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ( ! [D] : % 59.80/59.94 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.80/59.94 => ilf_type(D,relation_type(B,C)) ) % 59.80/59.94 & ! [E] : % 59.80/59.94 ( ilf_type(E,relation_type(B,C)) % 59.80/59.94 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 59.80/59.94 fof(p5,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(tarski - df(3),1832749) % 59.80/59.94 fof(p6,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ( subset(B,C) % 59.80/59.94 <=> ! [D] : % 59.80/59.94 ( ilf_type(D,set_type) % 59.80/59.94 => ( member(D,B) % 59.80/59.94 => member(D,C) ) ) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(op(domain_of,1,function)) % 59.80/59.94 fof(p7,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,binary_relation_type) % 59.80/59.94 => ilf_type(domain_of(B),set_type) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(op(cross_product,2,function)) % 59.80/59.94 fof(p8,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ilf_type(cross_product(B,C),set_type) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(op(range_of,1,function)) % 59.80/59.94 fof(p9,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,binary_relation_type) % 59.80/59.94 => ilf_type(range_of(B),set_type) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(hidden - axiom123,1832648) % 59.80/59.94 fof(p10,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ( ilf_type(C,subset_type(B)) % 59.80/59.94 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- type_nonempty(line(hidden - axiom123,1832648)) % 59.80/59.94 fof(p11,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 59.80/59.94 % 59.80/59.94 %---- property(reflexivity,op(subset,2,predicate)) % 59.80/59.94 fof(p12,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => subset(B,B) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(hidden - axiom125,1832644) % 59.80/59.94 fof(p13,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ( member(B,power_set(C)) % 59.80/59.94 <=> ! [D] : % 59.80/59.94 ( ilf_type(D,set_type) % 59.80/59.94 => ( member(D,B) % 59.80/59.94 => member(D,C) ) ) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(line(hidden - axiom125,1832644)) % 59.80/59.94 fof(p14,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ( ~ empty(power_set(B)) % 59.80/59.94 & ilf_type(power_set(B),set_type) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(hidden - axiom126,1832640) % 59.80/59.94 fof(p15,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ( ~ empty(C) % 59.80/59.94 & ilf_type(C,set_type) ) % 59.80/59.94 => ( ilf_type(B,member_type(C)) % 59.80/59.94 <=> member(B,C) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- type_nonempty(line(hidden - axiom126,1832640)) % 59.80/59.94 fof(p16,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ( ~ empty(B) % 59.80/59.94 & ilf_type(B,set_type) ) % 59.80/59.94 => ? [C] : ilf_type(C,member_type(B)) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(hidden - axiom127,1832628) % 59.80/59.94 fof(p17,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ( empty(B) % 59.80/59.94 <=> ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ~ member(C,B) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- line(relat_1 - df(1),1917627) % 59.80/59.94 fof(p18,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ( relation_like(B) % 59.80/59.94 <=> ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ( member(C,B) % 59.80/59.94 => ? [D] : % 59.80/59.94 ( ilf_type(D,set_type) % 59.80/59.94 & ? [E] : % 59.80/59.94 ( ilf_type(E,set_type) % 59.80/59.94 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- conditional_cluster(axiom129,relation_like) % 59.80/59.94 fof(p19,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ( empty(B) % 59.80/59.94 & ilf_type(B,set_type) ) % 59.80/59.94 => relation_like(B) ) ). % 59.80/59.94 % 59.80/59.94 %---- conditional_cluster(axiom130,relation_like) % 59.80/59.94 fof(p20,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ! [D] : % 59.80/59.94 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.80/59.94 => relation_like(D) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(op(ordered_pair,2,function)) % 59.80/59.94 fof(p21,axiom, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 59.80/59.94 % 59.80/59.94 %---- declaration(set) % 59.80/59.94 fof(p22,axiom, % 59.80/59.94 ! [B] : ilf_type(B,set_type) ). % 59.80/59.94 % 59.80/59.94 %---- line(relset_1 - th(16),1916267) % 59.80/59.94 fof(prove_relset_1_16,conjecture, % 59.80/59.94 ! [B] : % 59.80/59.94 ( ilf_type(B,set_type) % 59.80/59.94 => ! [C] : % 59.80/59.94 ( ilf_type(C,set_type) % 59.80/59.94 => ! [D] : % 59.80/59.94 ( ilf_type(D,set_type) % 59.80/59.94 => ! [E] : % 59.80/59.94 ( ilf_type(E,relation_type(D,B)) % 59.80/59.94 => ( subset(B,C) % 59.80/59.94 => ilf_type(E,relation_type(D,C)) ) ) ) ) ) ). % 59.80/59.94 % 59.80/59.94 %-------------------------------------------------------------------------- % 59.80/59.94 %------------------------------------------- % 59.80/59.94 % Proof found % 59.80/59.94 % SZS status Theorem for theBenchmark % 59.80/59.94 % SZS output start Proof % 59.80/59.94 %ClaNum:82(EqnAxiom:36) % 59.80/59.94 %VarNum:180(SingletonVarNum:61) % 59.80/59.94 %MaxLitNum:6 % 59.80/59.94 %MaxfuncDepth:2 % 59.80/59.94 %SharedTerms:14 % 59.80/59.94 %goalClause: 40 42 43 % 59.80/59.94 %singleGoalClaCount:3 % 59.80/59.94 [40]P3(a1,a6) % 59.80/59.94 [42]P1(a8,f9(a7,a1)) % 59.80/59.94 [43]~P1(a8,f9(a7,a6)) % 59.80/59.94 [41]P1(x411,a5) % 59.80/59.94 [45]P3(x451,x451)+~P1(x451,a5) % 59.80/59.94 [46]~P1(x461,a5)+~P2(f10(x461)) % 59.80/59.94 [54]~P1(x541,a5)+P1(f12(x541),f23(x541)) % 59.80/59.94 [44]~P2(x441)+P4(x441)+~P1(x441,a5) % 59.80/59.94 [52]P2(x521)+P5(f11(x521),x521)+~P1(x521,a5) % 59.80/59.94 [53]P4(x531)+P5(f17(x531),x531)+~P1(x531,a5) % 59.80/59.94 [55]P2(x551)+P1(f15(x551),f20(x551))+~P1(x551,a5) % 59.80/59.94 [67]~P1(x672,a5)+~P1(x671,a5)+P1(f14(x671,x672),f9(x672,x671)) % 59.80/59.94 [56]~P2(x561)+~P5(x562,x561)+~P1(x562,a5)+~P1(x561,a5) % 59.80/59.94 [63]P3(x631,x632)+P5(f13(x631,x632),x631)+~P1(x632,a5)+~P1(x631,a5) % 59.80/59.94 [65]P5(f16(x651,x652),x651)+~P1(x652,a5)+~P1(x651,a5)+P5(x651,f10(x652)) % 59.80/59.94 [71]P3(x711,x712)+~P1(x712,a5)+~P1(x711,a5)+~P5(f13(x711,x712),x712) % 59.80/59.94 [74]~P1(x742,a5)+~P1(x741,a5)+~P5(f16(x741,x742),x742)+P5(x741,f10(x742)) % 59.80/59.94 [66]~P1(x662,a5)+~P1(x661,a5)+~P1(x661,f23(x662))+P1(x661,f20(f10(x662))) % 59.80/59.94 [70]~P1(x702,a5)+~P1(x701,a5)+P1(x701,f23(x702))+~P1(x701,f20(f10(x702))) % 59.80/59.94 [75]~P1(x752,a5)+~P1(x751,f9(x752,x753))+P3(f2(x751),x752)+~P1(x753,a5) % 59.80/59.94 [76]~P1(x762,a5)+~P1(x761,f9(x763,x762))+P3(f22(x761),x762)+~P1(x763,a5) % 59.80/59.94 [79]P4(x791)+~P1(x792,a5)+~P1(x793,a5)+~P1(x791,f23(f4(x793,x792))) % 59.80/59.94 [80]~P1(x803,a5)+~P1(x802,a5)+~P1(x801,f9(x802,x803))+P1(x801,f23(f4(x802,x803))) % 59.80/59.94 [81]~P1(x813,a5)+~P1(x812,a5)+P1(x811,f9(x812,x813))+~P1(x811,f23(f4(x812,x813))) % 59.80/59.94 [59]~P5(x592,x591)+P2(x591)+~P1(x591,a5)+~P1(x592,a5)+P1(x592,f20(x591)) % 59.80/59.94 [60]P2(x601)+P5(x602,x601)+~P1(x601,a5)+~P1(x602,a5)+~P1(x602,f20(x601)) % 59.80/59.94 [78]~P4(x781)+~P5(x782,x781)+~P1(x781,a5)+~P1(x782,a5)+E(f21(f18(x781,x782),f19(x781,x782)),x782) % 59.80/59.94 [62]P4(x621)+~P1(x621,a5)+~P1(x623,a5)+~P1(x622,a5)+~E(f17(x621),f21(x622,x623)) % 59.80/59.94 [72]~P3(x721,x723)+P3(x721,x722)+~P3(x723,x722)+~P1(x722,a5)+~P1(x723,a5)+~P1(x721,a5) % 59.80/59.94 [73]~P5(x731,x733)+P5(x731,x732)+~P3(x733,x732)+~P1(x731,a5)+~P1(x732,a5)+~P1(x733,a5) % 59.80/59.94 [77]P5(x771,x772)+~P5(x771,x773)+~P1(x771,a5)+~P1(x772,a5)+~P1(x773,a5)+~P5(x773,f10(x772)) % 59.80/59.94 [82]~P1(x822,a5)+~P1(x823,a5)+~P3(f22(x821),x823)+~P1(x821,f9(x822,x824))+P1(x821,f9(x822,x823))+~P1(x824,a5) % 59.80/59.94 %EqnAxiom % 59.80/59.94 [1]E(x11,x11) % 59.80/59.94 [2]E(x22,x21)+~E(x21,x22) % 59.80/59.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.80/59.94 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 59.80/59.94 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 59.80/59.94 [6]~E(x61,x62)+E(f22(x61),f22(x62)) % 59.80/59.94 [7]~E(x71,x72)+E(f10(x71),f10(x72)) % 59.80/59.94 [8]~E(x81,x82)+E(f2(x81),f2(x82)) % 59.80/59.94 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93)) % 59.80/59.94 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102)) % 59.80/59.94 [11]~E(x111,x112)+E(f16(x111,x113),f16(x112,x113)) % 59.80/59.94 [12]~E(x121,x122)+E(f16(x123,x121),f16(x123,x122)) % 59.80/59.94 [13]~E(x131,x132)+E(f11(x131),f11(x132)) % 59.80/59.94 [14]~E(x141,x142)+E(f17(x141),f17(x142)) % 59.80/59.94 [15]~E(x151,x152)+E(f23(x151),f23(x152)) % 59.80/59.94 [16]~E(x161,x162)+E(f18(x161,x163),f18(x162,x163)) % 59.80/59.94 [17]~E(x171,x172)+E(f18(x173,x171),f18(x173,x172)) % 59.80/59.94 [18]~E(x181,x182)+E(f12(x181),f12(x182)) % 59.80/59.94 [19]~E(x191,x192)+E(f14(x191,x193),f14(x192,x193)) % 59.80/59.94 [20]~E(x201,x202)+E(f14(x203,x201),f14(x203,x202)) % 59.80/59.94 [21]~E(x211,x212)+E(f15(x211),f15(x212)) % 59.80/59.94 [22]~E(x221,x222)+E(f20(x221),f20(x222)) % 59.80/59.94 [23]~E(x231,x232)+E(f19(x231,x233),f19(x232,x233)) % 59.80/59.94 [24]~E(x241,x242)+E(f19(x243,x241),f19(x243,x242)) % 59.80/59.94 [25]~E(x251,x252)+E(f21(x251,x253),f21(x252,x253)) % 59.80/59.94 [26]~E(x261,x262)+E(f21(x263,x261),f21(x263,x262)) % 59.80/59.94 [27]~E(x271,x272)+E(f13(x271,x273),f13(x272,x273)) % 59.80/59.94 [28]~E(x281,x282)+E(f13(x283,x281),f13(x283,x282)) % 59.80/59.94 [29]P1(x292,x293)+~E(x291,x292)+~P1(x291,x293) % 59.80/59.94 [30]P1(x303,x302)+~E(x301,x302)+~P1(x303,x301) % 59.80/59.94 [31]P3(x312,x313)+~E(x311,x312)+~P3(x311,x313) % 59.80/59.94 [32]P3(x323,x322)+~E(x321,x322)+~P3(x323,x321) % 59.80/59.94 [33]~P4(x331)+P4(x332)+~E(x331,x332) % 59.80/59.94 [34]P5(x342,x343)+~E(x341,x342)+~P5(x341,x343) % 59.80/59.94 [35]P5(x353,x352)+~E(x351,x352)+~P5(x353,x351) % 59.80/59.94 [36]~P2(x361)+P2(x362)+~E(x361,x362) % 59.80/59.94 % 59.80/59.94 %------------------------------------------- % 59.80/59.97 cnf(94,plain, % 59.80/59.97 (P5(x941,f10(x941))+P5(f16(x941,x941),x941)), % 59.80/59.97 inference(scs_inference,[],[40,42,43,41,45,30,5,29,31,32,44,56,65])). % 59.80/59.97 cnf(586,plain, % 59.80/59.97 (~E(x5861,x5862)+~P2(f10(x5862))), % 59.80/59.97 inference(scs_inference,[],[41,46,29])). % 59.80/59.97 cnf(587,plain, % 59.80/59.97 (~P2(f10(x5871))), % 59.80/59.97 inference(equality_inference,[],[586])). % 59.80/59.97 cnf(610,plain, % 59.80/59.97 (~P1(a8,f9(a7,a7))+~P3(f22(a8),a6)+~P1(a6,a5)), % 59.80/59.97 inference(scs_inference,[],[43,41,82])). % 59.80/59.97 cnf(611,plain, % 59.80/59.97 (~P1(a8,f9(a7,a7))+~P3(f22(a8),a6)), % 59.80/59.97 inference(scs_inference,[],[41,610])). % 59.80/59.97 cnf(1251,plain, % 59.80/59.97 (P1(x12511,f23(x12512))+~E(f12(x12512),x12511)), % 59.80/59.97 inference(scs_inference,[],[41,54,29])). % 59.80/59.97 cnf(1252,plain, % 59.80/59.97 (P1(f12(x12521),f23(x12521))), % 59.80/59.97 inference(equality_inference,[],[1251])). % 59.80/59.97 cnf(1253,plain, % 59.80/59.97 (P4(f12(f4(x12531,x12531)))), % 59.80/59.97 inference(scs_inference,[],[1252,41,79])). % 59.80/59.97 cnf(1254,plain, % 59.80/59.97 (P1(f12(x12541),f23(x12541))), % 59.80/59.97 inference(rename_variables,[],[1252])). % 59.80/59.97 cnf(1256,plain, % 59.80/59.97 (P1(f12(f4(x12561,x12561)),f9(x12561,x12561))), % 59.80/59.97 inference(scs_inference,[],[1252,1254,41,79,81])). % 59.80/59.97 cnf(1270,plain, % 59.80/59.97 (~E(f12(f4(a7,a7)),a8)+~P3(f22(a8),a6)), % 59.80/59.97 inference(scs_inference,[],[1256,29,611])). % 59.80/59.97 cnf(1410,plain, % 59.80/59.97 (P5(x14101,f10(x14101))), % 59.80/59.97 inference(scs_inference,[],[41,94,74])). % 59.80/59.97 cnf(7465,plain, % 59.80/59.97 (E(f23(x74651),f23(x74652))+~E(x74652,x74651)), % 59.80/59.97 inference(scs_inference,[],[2,15])). % 59.80/59.97 cnf(10705,plain, % 59.80/59.97 (~E(f12(f4(a7,a6)),a8)+~P1(a7,a5)), % 59.80/59.97 inference(scs_inference,[],[43,1252,41,29,81])). % 59.80/59.97 cnf(10712,plain, % 59.80/59.97 (~E(f12(f4(a7,a6)),a8)), % 59.80/59.97 inference(scs_inference,[],[41,10705])). % 59.80/59.97 cnf(10794,plain, % 59.80/59.97 (P3(f2(a8),a7)+~P1(a7,a5)), % 59.80/59.97 inference(scs_inference,[],[42,10712,41,1253,2,3,33,75])). % 59.80/59.97 cnf(10815,plain, % 59.80/59.97 (P3(f2(a8),a7)), % 59.80/59.97 inference(scs_inference,[],[41,10794])). % 59.80/59.97 cnf(32572,plain, % 59.80/59.97 (P1(f14(x325721,x325721),f9(x325721,x325721))), % 59.80/59.97 inference(scs_inference,[],[41,67])). % 59.80/59.97 cnf(32575,plain, % 59.80/59.97 (P1(f14(x325751,x325751),f23(f4(x325751,x325751)))), % 59.80/59.97 inference(scs_inference,[],[587,41,67,36,80])). % 59.80/59.97 cnf(32577,plain, % 59.80/59.97 (P3(f22(a8),a1)+~P1(a1,a5)), % 59.80/59.97 inference(scs_inference,[],[42,587,41,67,36,80,76])). % 59.80/59.97 cnf(32581,plain, % 59.80/59.97 (P3(f22(a8),a1)), % 59.80/59.97 inference(scs_inference,[],[41,32577])). % 59.80/59.97 cnf(32582,plain, % 59.80/59.97 (P1(x325821,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32584,plain, % 59.80/59.97 (P1(x325841,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32585,plain, % 59.80/59.97 (P1(x325851,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32587,plain, % 59.80/59.97 (~P1(a8,f23(f4(a7,a6)))), % 59.80/59.97 inference(scs_inference,[],[32572,41,32582,32585,32584,43,32577,76,81])). % 59.80/59.97 cnf(32588,plain, % 59.80/59.97 (P1(x325881,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32589,plain, % 59.80/59.97 (P1(x325891,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32591,plain, % 59.80/59.97 (P1(f14(x325911,x325912),f9(x325912,x325911))), % 59.80/59.97 inference(scs_inference,[],[32572,41,32582,32585,32588,32584,32589,43,32577,76,81,67])). % 59.80/59.97 cnf(32593,plain, % 59.80/59.97 (~E(f14(a6,a7),a8)), % 59.80/59.97 inference(scs_inference,[],[32572,41,32582,32585,32588,32584,32589,43,32577,76,81,67,29])). % 59.80/59.97 cnf(32619,plain, % 59.80/59.97 (~E(f9(a7,a1),f23(f4(a7,a6)))), % 59.80/59.97 inference(scs_inference,[],[32593,32587,42,2,30])). % 59.80/59.97 cnf(32621,plain, % 59.80/59.97 (P1(x326211,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32622,plain, % 59.80/59.97 (P1(x326221,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32627,plain, % 59.80/59.97 (P1(x326271,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32629,plain, % 59.80/59.97 (P1(f14(x326291,x326292),f23(f4(x326292,x326291)))), % 59.80/59.97 inference(scs_inference,[],[32591,32593,32587,32575,1252,42,41,32622,32627,32621,2,30,79,33,66,80])). % 59.80/59.97 cnf(32630,plain, % 59.80/59.97 (P1(x326301,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32631,plain, % 59.80/59.97 (P1(x326311,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32634,plain, % 59.80/59.97 (P1(x326341,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32637,plain, % 59.80/59.97 (P1(x326371,f20(f10(x326371)))), % 59.80/59.97 inference(scs_inference,[],[32591,32593,32587,32575,1252,42,587,1410,41,32622,32627,32631,32621,32630,32634,2,30,79,33,66,80,76,59])). % 59.80/59.97 cnf(32651,plain, % 59.80/59.97 (P1(x326511,f23(x326511))), % 59.80/59.97 inference(scs_inference,[],[32637,32619,41,2,70])). % 59.80/59.97 cnf(32857,plain, % 59.80/59.97 (P1(x328571,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32858,plain, % 59.80/59.97 (P1(x328581,a5)), % 59.80/59.97 inference(rename_variables,[],[41])). % 59.80/59.97 cnf(32859,plain, % 59.80/59.97 (P3(f22(a8),a6)+~P1(a6,a5)), % 59.80/59.97 inference(scs_inference,[],[10815,32581,40,41,32858,32857,73,72])). % 59.80/59.97 cnf(32863,plain, % 59.80/59.97 (~E(x328631,a6)+P3(f22(a8),a6)), % 59.80/59.97 inference(scs_inference,[],[41,32859,29])). % 59.80/59.97 cnf(32864,plain, % 59.80/59.97 (P3(f22(a8),a6)), % 59.80/59.97 inference(equality_inference,[],[32863])). % 59.80/59.97 cnf(32865,plain, % 59.80/59.97 (~P1(a8,f9(a7,a7))), % 59.80/59.97 inference(scs_inference,[],[32864,611])). % 59.80/59.97 cnf(32866,plain, % 59.80/59.97 (~E(f12(f4(a7,a7)),a8)), % 59.80/59.97 inference(scs_inference,[],[32864,1270])). % 59.80/59.97 cnf(32869,plain, % 59.80/59.97 (~E(a8,f12(f4(a7,a7)))), % 59.80/59.97 inference(scs_inference,[],[32866,2])). % 59.80/59.97 cnf(32872,plain, % 59.80/59.97 (~P1(a8,f23(f4(a7,a7)))), % 59.80/59.97 inference(scs_inference,[],[32865,32866,32637,41,2,30,81])). % 59.80/59.97 cnf(32897,plain, % 59.80/59.97 (~E(f14(a7,a7),a8)), % 59.80/59.97 inference(scs_inference,[],[32869,32872,32629,3,29])). % 59.80/59.97 cnf(32899,plain, % 59.80/59.97 (~E(f23(a8),f23(f4(a7,a7)))), % 59.80/59.97 inference(scs_inference,[],[32869,32872,32629,32651,3,29,30])). % 59.80/59.97 cnf(32908,plain, % 59.80/59.97 (~E(f4(a7,a7),a8)), % 59.80/59.97 inference(scs_inference,[],[32897,32899,2,7465])). % 59.80/59.97 cnf(32919,plain, % 59.80/59.97 (~P1(a7,a5)+~P1(a6,a5)), % 59.80/59.97 inference(scs_inference,[],[32908,32864,42,43,41,2,82])). % 59.80/59.97 cnf(32922,plain, % 59.80/59.97 (~P1(a6,a5)), % 59.80/59.97 inference(scs_inference,[],[41,32919])). % 59.80/59.97 cnf(32925,plain, % 59.80/59.97 ($false), % 59.80/59.97 inference(scs_inference,[],[32922,41]), % 59.80/59.97 ['proof']). % 59.92/60.00 % SZS output end Proof % 59.92/60.00 % Total time :59.230000s %------------------------------------------------------------------------------