%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET653+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 : n021.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:08 EDT 2024 % Result : Theorem 59.15s 59.31s % Output : CNFRefutation 59.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SET653+3 : TPTP v8.2.0. Released v2.2.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n021.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sun Jun 23 16:14:23 EDT 2024 % 0.12/0.32 % CPUTime : % 0.49/0.60 start to proof:theBenchmark % 59.15/59.29 %------------------------------------------- % 59.15/59.29 % File :CSE---1.7 % 59.15/59.29 % Problem :theBenchmark % 59.15/59.29 % Transform :cnf % 59.15/59.29 % Format :tptp:raw % 59.15/59.29 % Command :java -jar mcs_scs.jar %d %s % 59.15/59.29 % 59.15/59.29 % Result :Theorem 58.540000s % 59.15/59.29 % Output :CNFRefutation 58.540000s % 59.15/59.29 %------------------------------------------- % 59.15/59.30 %-------------------------------------------------------------------------- % 59.15/59.30 % File : SET653+3 : TPTP v8.2.0. Released v2.2.0. % 59.15/59.30 % Domain : Set Theory (Relations) % 59.15/59.30 % Problem : X a subset of X1 => R (X to Y) is (X1 to Y) % 59.15/59.30 % Version : [Wor90] axioms : Reduced > Incomplete. % 59.15/59.30 % English : If X is a subset of X1 then a relation R from X to Y is a % 59.15/59.30 % relation from X1 to Y. % 59.15/59.30 % 59.15/59.30 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 59.15/59.30 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 59.15/59.30 % Source : [ILF] % 59.15/59.30 % Names : RELSET_1 (15) [Wor90] % 59.15/59.30 % 59.15/59.30 % Status : Theorem % 59.15/59.30 % Rating : 0.28 v8.2.0, 0.25 v7.5.0, 0.31 v7.4.0, 0.23 v7.3.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.29 v6.2.0, 0.28 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.19 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.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.15/59.30 % Syntax : Number of formulae : 23 ( 1 unt; 0 def) % 59.15/59.30 % Number of atoms : 92 ( 1 equ) % 59.15/59.30 % Maximal formula atoms : 7 ( 4 avg) % 59.15/59.30 % Number of connectives : 73 ( 4 ~; 0 |; 9 &) % 59.15/59.30 % ( 6 <=>; 54 =>; 0 <=; 0 <~>) % 59.15/59.30 % Maximal formula depth : 11 ( 6 avg) % 59.15/59.30 % Maximal term depth : 3 ( 1 avg) % 59.15/59.30 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 59.15/59.30 % Number of functors : 10 ( 10 usr; 2 con; 0-2 aty) % 59.15/59.30 % Number of variables : 54 ( 49 !; 5 ?) % 59.15/59.30 % SPC : FOF_THM_RFO_SEQ % 59.15/59.30 % 59.15/59.30 % Comments : % 59.15/59.30 %-------------------------------------------------------------------------- % 59.15/59.30 %---- line(boole - th(29),1909428) % 59.15/59.30 fof(p1,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ! [D] : % 59.15/59.30 ( ilf_type(D,set_type) % 59.15/59.30 => ( ( subset(B,C) % 59.15/59.30 & subset(C,D) ) % 59.15/59.30 => subset(B,D) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(relset_1 - th(12),1916203) % 59.15/59.30 fof(p2,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ! [D] : % 59.15/59.30 ( ilf_type(D,relation_type(B,C)) % 59.15/59.30 => ( subset(domain_of(D),B) % 59.15/59.30 & subset(range_of(D),C) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(relset_1 - th(13),1916220) % 59.15/59.30 fof(p3,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ! [D] : % 59.15/59.30 ( ilf_type(D,set_type) % 59.15/59.30 => ! [E] : % 59.15/59.30 ( ilf_type(E,relation_type(B,D)) % 59.15/59.30 => ( subset(domain_of(E),C) % 59.15/59.30 => ilf_type(E,relation_type(C,D)) ) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(relset_1 - df(1),1916080) % 59.15/59.30 fof(p4,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ( ! [D] : % 59.15/59.30 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.15/59.30 => ilf_type(D,relation_type(B,C)) ) % 59.15/59.30 & ! [E] : % 59.15/59.30 ( ilf_type(E,relation_type(B,C)) % 59.15/59.30 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 59.15/59.30 fof(p5,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(tarski - df(3),1832749) % 59.15/59.30 fof(p6,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ( subset(B,C) % 59.15/59.30 <=> ! [D] : % 59.15/59.30 ( ilf_type(D,set_type) % 59.15/59.30 => ( member(D,B) % 59.15/59.30 => member(D,C) ) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- declaration(op(domain_of,1,function)) % 59.15/59.30 fof(p7,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,binary_relation_type) % 59.15/59.30 => ilf_type(domain_of(B),set_type) ) ). % 59.15/59.30 % 59.15/59.30 %---- declaration(op(cross_product,2,function)) % 59.15/59.30 fof(p8,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ilf_type(cross_product(B,C),set_type) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- declaration(op(range_of,1,function)) % 59.15/59.30 fof(p9,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,binary_relation_type) % 59.15/59.30 => ilf_type(range_of(B),set_type) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(hidden - axiom115,1832648) % 59.15/59.30 fof(p10,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ( ilf_type(C,subset_type(B)) % 59.15/59.30 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- type_nonempty(line(hidden - axiom115,1832648)) % 59.15/59.30 fof(p11,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 59.15/59.30 % 59.15/59.30 %---- property(reflexivity,op(subset,2,predicate)) % 59.15/59.30 fof(p12,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => subset(B,B) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(hidden - axiom117,1832644) % 59.15/59.30 fof(p13,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ( member(B,power_set(C)) % 59.15/59.30 <=> ! [D] : % 59.15/59.30 ( ilf_type(D,set_type) % 59.15/59.30 => ( member(D,B) % 59.15/59.30 => member(D,C) ) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- declaration(line(hidden - axiom117,1832644)) % 59.15/59.30 fof(p14,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ( ~ empty(power_set(B)) % 59.15/59.30 & ilf_type(power_set(B),set_type) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(hidden - axiom118,1832640) % 59.15/59.30 fof(p15,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ( ~ empty(C) % 59.15/59.30 & ilf_type(C,set_type) ) % 59.15/59.30 => ( ilf_type(B,member_type(C)) % 59.15/59.30 <=> member(B,C) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- type_nonempty(line(hidden - axiom118,1832640)) % 59.15/59.30 fof(p16,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ( ~ empty(B) % 59.15/59.30 & ilf_type(B,set_type) ) % 59.15/59.30 => ? [C] : ilf_type(C,member_type(B)) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(hidden - axiom119,1832628) % 59.15/59.30 fof(p17,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ( empty(B) % 59.15/59.30 <=> ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ~ member(C,B) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- line(relat_1 - df(1),1917627) % 59.15/59.30 fof(p18,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ( relation_like(B) % 59.15/59.30 <=> ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ( member(C,B) % 59.15/59.30 => ? [D] : % 59.15/59.30 ( ilf_type(D,set_type) % 59.15/59.30 & ? [E] : % 59.15/59.30 ( ilf_type(E,set_type) % 59.15/59.30 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 59.15/59.30 % 59.15/59.30 %---- conditional_cluster(axiom121,relation_like) % 59.15/59.30 fof(p19,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ( empty(B) % 59.15/59.30 & ilf_type(B,set_type) ) % 59.15/59.30 => relation_like(B) ) ). % 59.15/59.30 % 59.15/59.30 %---- conditional_cluster(axiom122,relation_like) % 59.15/59.30 fof(p20,axiom, % 59.15/59.30 ! [B] : % 59.15/59.30 ( ilf_type(B,set_type) % 59.15/59.30 => ! [C] : % 59.15/59.30 ( ilf_type(C,set_type) % 59.15/59.30 => ! [D] : % 59.15/59.31 ( ilf_type(D,subset_type(cross_product(B,C))) % 59.15/59.31 => relation_like(D) ) ) ) ). % 59.15/59.31 % 59.15/59.31 %---- declaration(op(ordered_pair,2,function)) % 59.15/59.31 fof(p21,axiom, % 59.15/59.31 ! [B] : % 59.15/59.31 ( ilf_type(B,set_type) % 59.15/59.31 => ! [C] : % 59.15/59.31 ( ilf_type(C,set_type) % 59.15/59.31 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 59.15/59.31 % 59.15/59.31 %---- declaration(set) % 59.15/59.31 fof(p22,axiom, % 59.15/59.31 ! [B] : ilf_type(B,set_type) ). % 59.15/59.31 % 59.15/59.31 %---- line(relset_1 - th(15),1916252) % 59.15/59.31 fof(prove_relset_1_15,conjecture, % 59.15/59.31 ! [B] : % 59.15/59.31 ( ilf_type(B,set_type) % 59.15/59.31 => ! [C] : % 59.15/59.31 ( ilf_type(C,set_type) % 59.15/59.31 => ! [D] : % 59.15/59.31 ( ilf_type(D,set_type) % 59.15/59.31 => ! [E] : % 59.15/59.31 ( ilf_type(E,relation_type(B,D)) % 59.15/59.31 => ( subset(B,C) % 59.15/59.31 => ilf_type(E,relation_type(C,D)) ) ) ) ) ) ). % 59.15/59.31 % 59.15/59.31 %-------------------------------------------------------------------------- % 59.15/59.31 %------------------------------------------- % 59.15/59.31 % Proof found % 59.15/59.31 % SZS status Theorem for theBenchmark % 59.15/59.31 % SZS output start Proof % 59.15/59.31 %ClaNum:82(EqnAxiom:36) % 59.15/59.31 %VarNum:180(SingletonVarNum:61) % 59.15/59.31 %MaxLitNum:6 % 59.15/59.31 %MaxfuncDepth:2 % 59.15/59.31 %SharedTerms:14 % 59.15/59.31 %goalClause: 40 42 43 % 59.15/59.31 %singleGoalClaCount:3 % 59.15/59.31 [40]P3(a1,a6) % 59.15/59.31 [42]P1(a8,f9(a1,a7)) % 59.15/59.31 [43]~P1(a8,f9(a6,a7)) % 59.15/59.31 [41]P1(x411,a5) % 59.15/59.31 [45]P3(x451,x451)+~P1(x451,a5) % 59.15/59.31 [46]~P1(x461,a5)+~P2(f10(x461)) % 59.15/59.31 [54]~P1(x541,a5)+P1(f12(x541),f23(x541)) % 59.15/59.31 [44]~P2(x441)+P4(x441)+~P1(x441,a5) % 59.15/59.31 [52]P2(x521)+P5(f11(x521),x521)+~P1(x521,a5) % 59.15/59.31 [53]P4(x531)+P5(f17(x531),x531)+~P1(x531,a5) % 59.15/59.31 [55]P2(x551)+P1(f15(x551),f20(x551))+~P1(x551,a5) % 59.15/59.31 [67]~P1(x672,a5)+~P1(x671,a5)+P1(f14(x671,x672),f9(x672,x671)) % 59.15/59.31 [56]~P2(x561)+~P5(x562,x561)+~P1(x562,a5)+~P1(x561,a5) % 59.15/59.31 [63]P3(x631,x632)+P5(f13(x631,x632),x631)+~P1(x632,a5)+~P1(x631,a5) % 59.15/59.31 [65]P5(f16(x651,x652),x651)+~P1(x652,a5)+~P1(x651,a5)+P5(x651,f10(x652)) % 59.15/59.31 [71]P3(x711,x712)+~P1(x712,a5)+~P1(x711,a5)+~P5(f13(x711,x712),x712) % 59.15/59.31 [74]~P1(x742,a5)+~P1(x741,a5)+~P5(f16(x741,x742),x742)+P5(x741,f10(x742)) % 59.15/59.31 [66]~P1(x662,a5)+~P1(x661,a5)+~P1(x661,f23(x662))+P1(x661,f20(f10(x662))) % 59.15/59.31 [70]~P1(x702,a5)+~P1(x701,a5)+P1(x701,f23(x702))+~P1(x701,f20(f10(x702))) % 59.15/59.31 [75]~P1(x752,a5)+~P1(x751,f9(x752,x753))+P3(f2(x751),x752)+~P1(x753,a5) % 59.15/59.31 [76]~P1(x762,a5)+~P1(x761,f9(x763,x762))+P3(f22(x761),x762)+~P1(x763,a5) % 59.15/59.31 [79]P4(x791)+~P1(x792,a5)+~P1(x793,a5)+~P1(x791,f23(f4(x793,x792))) % 59.15/59.31 [80]~P1(x803,a5)+~P1(x802,a5)+~P1(x801,f9(x802,x803))+P1(x801,f23(f4(x802,x803))) % 59.15/59.31 [81]~P1(x813,a5)+~P1(x812,a5)+P1(x811,f9(x812,x813))+~P1(x811,f23(f4(x812,x813))) % 59.15/59.31 [59]~P5(x592,x591)+P2(x591)+~P1(x591,a5)+~P1(x592,a5)+P1(x592,f20(x591)) % 59.15/59.31 [60]P2(x601)+P5(x602,x601)+~P1(x601,a5)+~P1(x602,a5)+~P1(x602,f20(x601)) % 59.15/59.31 [78]~P4(x781)+~P5(x782,x781)+~P1(x781,a5)+~P1(x782,a5)+E(f21(f18(x781,x782),f19(x781,x782)),x782) % 59.15/59.31 [62]P4(x621)+~P1(x621,a5)+~P1(x623,a5)+~P1(x622,a5)+~E(f17(x621),f21(x622,x623)) % 59.15/59.31 [72]~P3(x721,x723)+P3(x721,x722)+~P3(x723,x722)+~P1(x722,a5)+~P1(x723,a5)+~P1(x721,a5) % 59.15/59.31 [73]~P5(x731,x733)+P5(x731,x732)+~P3(x733,x732)+~P1(x731,a5)+~P1(x732,a5)+~P1(x733,a5) % 59.15/59.31 [77]P5(x771,x772)+~P5(x771,x773)+~P1(x771,a5)+~P1(x772,a5)+~P1(x773,a5)+~P5(x773,f10(x772)) % 59.15/59.31 [82]~P1(x823,a5)+~P1(x822,a5)+~P3(f2(x821),x822)+~P1(x821,f9(x824,x823))+P1(x821,f9(x822,x823))+~P1(x824,a5) % 59.15/59.31 %EqnAxiom % 59.15/59.31 [1]E(x11,x11) % 59.15/59.31 [2]E(x22,x21)+~E(x21,x22) % 59.15/59.31 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.15/59.31 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 59.15/59.31 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 59.15/59.31 [6]~E(x61,x62)+E(f2(x61),f2(x62)) % 59.15/59.31 [7]~E(x71,x72)+E(f10(x71),f10(x72)) % 59.15/59.31 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 59.15/59.31 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 59.15/59.31 [10]~E(x101,x102)+E(f22(x101),f22(x102)) % 59.15/59.31 [11]~E(x111,x112)+E(f23(x111),f23(x112)) % 59.15/59.31 [12]~E(x121,x122)+E(f11(x121),f11(x122)) % 59.15/59.31 [13]~E(x131,x132)+E(f17(x131),f17(x132)) % 59.15/59.31 [14]~E(x141,x142)+E(f18(x141,x143),f18(x142,x143)) % 59.15/59.31 [15]~E(x151,x152)+E(f18(x153,x151),f18(x153,x152)) % 59.15/59.31 [16]~E(x161,x162)+E(f19(x161,x163),f19(x162,x163)) % 59.15/59.31 [17]~E(x171,x172)+E(f19(x173,x171),f19(x173,x172)) % 59.15/59.31 [18]~E(x181,x182)+E(f12(x181),f12(x182)) % 59.15/59.31 [19]~E(x191,x192)+E(f13(x191,x193),f13(x192,x193)) % 59.15/59.31 [20]~E(x201,x202)+E(f13(x203,x201),f13(x203,x202)) % 59.15/59.31 [21]~E(x211,x212)+E(f15(x211),f15(x212)) % 59.15/59.31 [22]~E(x221,x222)+E(f20(x221),f20(x222)) % 59.15/59.31 [23]~E(x231,x232)+E(f16(x231,x233),f16(x232,x233)) % 59.15/59.31 [24]~E(x241,x242)+E(f16(x243,x241),f16(x243,x242)) % 59.15/59.31 [25]~E(x251,x252)+E(f21(x251,x253),f21(x252,x253)) % 59.15/59.31 [26]~E(x261,x262)+E(f21(x263,x261),f21(x263,x262)) % 59.15/59.31 [27]~E(x271,x272)+E(f14(x271,x273),f14(x272,x273)) % 59.15/59.31 [28]~E(x281,x282)+E(f14(x283,x281),f14(x283,x282)) % 59.15/59.31 [29]P1(x292,x293)+~E(x291,x292)+~P1(x291,x293) % 59.15/59.31 [30]P1(x303,x302)+~E(x301,x302)+~P1(x303,x301) % 59.15/59.31 [31]P3(x312,x313)+~E(x311,x312)+~P3(x311,x313) % 59.15/59.31 [32]P3(x323,x322)+~E(x321,x322)+~P3(x323,x321) % 59.15/59.31 [33]~P4(x331)+P4(x332)+~E(x331,x332) % 59.15/59.31 [34]P5(x342,x343)+~E(x341,x342)+~P5(x341,x343) % 59.15/59.31 [35]P5(x353,x352)+~E(x351,x352)+~P5(x353,x351) % 59.15/59.31 [36]~P2(x361)+P2(x362)+~E(x361,x362) % 59.15/59.31 % 59.15/59.31 %------------------------------------------- % 59.22/59.33 cnf(94,plain, % 59.22/59.33 (P5(x941,f10(x941))+P5(f16(x941,x941),x941)), % 59.22/59.33 inference(scs_inference,[],[40,42,43,41,45,30,4,29,31,32,44,56,65])). % 59.22/59.33 cnf(824,plain, % 59.22/59.33 (~E(x8241,x8242)+~P2(f10(x8242))), % 59.22/59.33 inference(scs_inference,[],[41,46,29])). % 59.22/59.33 cnf(825,plain, % 59.22/59.33 (~P2(f10(x8251))), % 59.22/59.33 inference(equality_inference,[],[824])). % 59.22/59.33 cnf(1513,plain, % 59.22/59.33 (P1(x15131,f23(x15132))+~E(f12(x15132),x15131)), % 59.22/59.33 inference(scs_inference,[],[41,54,29])). % 59.22/59.33 cnf(1514,plain, % 59.22/59.33 (P1(f12(x15141),f23(x15141))), % 59.22/59.33 inference(equality_inference,[],[1513])). % 59.22/59.33 cnf(1756,plain, % 59.22/59.33 (P5(x17561,f10(x17561))), % 59.22/59.33 inference(scs_inference,[],[41,94,74])). % 59.22/59.33 cnf(11123,plain, % 59.22/59.33 (P3(f2(a8),a1)+~P1(a1,a5)), % 59.22/59.33 inference(scs_inference,[],[42,41,75])). % 59.22/59.33 cnf(11129,plain, % 59.22/59.33 (P3(f2(a8),a1)), % 59.22/59.33 inference(scs_inference,[],[41,11123])). % 59.22/59.33 cnf(47311,plain, % 59.22/59.33 (P1(f14(x473111,x473111),f9(x473111,x473111))), % 59.22/59.33 inference(scs_inference,[],[41,67])). % 59.22/59.33 cnf(47314,plain, % 59.22/59.33 (P1(f14(x473141,x473141),f23(f4(x473141,x473141)))), % 59.22/59.33 inference(scs_inference,[],[825,41,67,36,80])). % 59.22/59.33 cnf(47316,plain, % 59.22/59.33 (P1(x473161,f23(x473161))+~P1(x473161,f20(f10(x473161)))), % 59.22/59.33 inference(scs_inference,[],[825,41,67,36,80,70])). % 59.22/59.33 cnf(47320,plain, % 59.22/59.33 (P1(x473201,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47321,plain, % 59.22/59.33 (P1(x473211,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47323,plain, % 59.22/59.33 (P1(f14(x473231,x473232),f9(x473232,x473231))), % 59.22/59.33 inference(scs_inference,[],[47311,41,47321,47320,75,67])). % 59.22/59.33 cnf(47325,plain, % 59.22/59.33 (~E(f14(a7,a6),a8)), % 59.22/59.33 inference(scs_inference,[],[47311,43,41,47321,47320,75,67,29])). % 59.22/59.33 cnf(47347,plain, % 59.22/59.33 (P1(x473471,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47348,plain, % 59.22/59.33 (P1(x473481,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47350,plain, % 59.22/59.33 (P3(f2(f14(x473501,x473502)),x473502)), % 59.22/59.33 inference(scs_inference,[],[47323,47325,47314,41,47348,47347,2,79,75])). % 59.22/59.33 cnf(47351,plain, % 59.22/59.33 (P1(x473511,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47352,plain, % 59.22/59.33 (P1(x473521,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47358,plain, % 59.22/59.33 (P1(x473581,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47361,plain, % 59.22/59.33 (P1(x473611,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47362,plain, % 59.22/59.33 (P1(x473621,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47365,plain, % 59.22/59.33 (P1(x473651,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47366,plain, % 59.22/59.33 (P1(x473661,a5)), % 59.22/59.33 inference(rename_variables,[],[41])). % 59.22/59.33 cnf(47368,plain, % 59.22/59.33 (P1(x473681,f20(f10(x473681)))), % 59.22/59.33 inference(scs_inference,[],[47323,47325,47314,1514,825,1756,43,41,47348,47352,47358,47362,47366,47347,47351,47361,47365,2,79,75,63,66,80,81,59])). % 59.22/59.33 cnf(47373,plain, % 59.22/59.33 (~E(f9(a1,a7),f23(f4(a6,a7)))), % 59.22/59.33 inference(scs_inference,[],[47323,47325,47314,1514,825,1756,42,43,41,47348,47352,47358,47362,47366,47347,47351,47361,47365,2,79,75,63,66,80,81,59,30])). % 59.22/59.33 cnf(47382,plain, % 59.22/59.33 (P3(f2(f14(x473821,a1)),a6)+~P1(f2(f14(x473821,a1)),a5)+~P1(a6,a5)), % 59.22/59.33 inference(scs_inference,[],[40,47368,47350,47373,41,47316,2,72])). % 59.22/59.33 cnf(47383,plain, % 59.22/59.33 (~P1(a6,a5)+P3(f2(f14(x473831,a1)),a6)), % 59.22/59.33 inference(scs_inference,[],[41,47382])). % 59.22/59.33 cnf(47385,plain, % 59.22/59.33 (P3(f2(f14(x473851,a1)),a6)), % 59.22/59.33 inference(scs_inference,[],[41,47383])). % 59.22/59.33 cnf(47581,plain, % 59.22/59.33 (P3(f2(a8),a6)+~P1(a1,a5)+~P1(a6,a5)), % 59.22/59.33 inference(scs_inference,[],[11129,47385,40,41,72])). % 59.22/59.33 cnf(47584,plain, % 59.22/59.33 (~P1(a6,a5)+P3(f2(a8),a6)), % 59.22/59.33 inference(scs_inference,[],[41,47581])). % 59.22/59.33 cnf(47585,plain, % 59.22/59.33 (P3(f2(a8),a6)), % 59.22/59.33 inference(scs_inference,[],[41,47584])). % 59.22/59.33 cnf(47747,plain, % 59.22/59.33 (~P1(a1,a5)+~P1(a7,a5)), % 59.22/59.33 inference(scs_inference,[],[47585,42,43,41,82])). % 59.22/59.33 cnf(47757,plain, % 59.22/59.33 (~P1(a7,a5)), % 59.22/59.33 inference(scs_inference,[],[41,47747])). % 59.22/59.33 cnf(47766,plain, % 59.22/59.33 ($false), % 59.22/59.33 inference(scs_inference,[],[47757,41]), % 59.22/59.33 ['proof']). % 59.26/59.36 % SZS output end Proof % 59.26/59.36 % Total time :58.540000s %------------------------------------------------------------------------------