%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET679+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 : n017.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:13 EDT 2024 % Result : Theorem 1.04s 1.11s % Output : CNFRefutation 1.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET679+3 : TPTP v8.2.0. Released v2.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.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 15:07:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.54/0.58 start to proof:theBenchmark % 1.04/1.10 %------------------------------------------- % 1.04/1.10 % File :CSE---1.7 % 1.04/1.10 % Problem :theBenchmark % 1.04/1.10 % Transform :cnf % 1.04/1.10 % Format :tptp:raw % 1.04/1.10 % Command :java -jar mcs_scs.jar %d %s % 1.04/1.10 % 1.04/1.10 % Result :Theorem 0.470000s % 1.04/1.10 % Output :CNFRefutation 0.470000s % 1.04/1.10 %------------------------------------------- % 1.04/1.11 %-------------------------------------------------------------------------- % 1.04/1.11 % File : SET679+3 : TPTP v8.2.0. Released v2.2.0. % 1.04/1.11 % Domain : Set Theory (Relations) % 1.04/1.11 % Problem : The identity relation on D is not the empty set % 1.04/1.11 % Version : [Wor90] axioms : Reduced > Incomplete. % 1.04/1.11 % English : % 1.04/1.11 % 1.04/1.11 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 1.04/1.11 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 1.04/1.11 % Source : [ILF] % 1.04/1.11 % Names : RELSET_1 (46) [Wor90] % 1.04/1.11 % 1.04/1.11 % Status : Theorem % 1.04/1.11 % Rating : 0.31 v7.4.0, 0.23 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.17 v6.4.0, 0.15 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.30 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.26 v4.0.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.16 v3.3.0, 0.21 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 % 1.04/1.11 % Syntax : Number of formulae : 24 ( 4 unt; 0 def) % 1.04/1.11 % Number of atoms : 82 ( 4 equ) % 1.04/1.11 % Maximal formula atoms : 7 ( 3 avg) % 1.04/1.11 % Number of connectives : 65 ( 7 ~; 0 |; 9 &) % 1.04/1.11 % ( 11 <=>; 38 =>; 0 <=; 0 <~>) % 1.04/1.11 % Maximal formula depth : 11 ( 5 avg) % 1.04/1.11 % Maximal term depth : 3 ( 1 avg) % 1.04/1.11 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 1.04/1.11 % Number of functors : 9 ( 9 usr; 3 con; 0-2 aty) % 1.04/1.11 % Number of variables : 42 ( 37 !; 5 ?) % 1.04/1.11 % SPC : FOF_THM_RFO_SEQ % 1.04/1.11 % 1.04/1.11 % Comments : % 1.04/1.11 %-------------------------------------------------------------------------- % 1.04/1.11 %---- line(relat_1 - th(70),1918880) % 1.04/1.11 fof(p1,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( member(C,B) % 1.04/1.11 <=> member(ordered_pair(C,C),identity_relation_of(B)) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom559,1832636) % 1.04/1.11 fof(p2,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ~ member(B,empty_set) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(line(hidden - axiom559,1832636)) Part 1 % 1.04/1.11 fof(p3a,axiom, % 1.04/1.11 empty(empty_set) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(line(hidden - axiom559,1832636)) Part 2 % 1.04/1.11 fof(p3b,axiom, % 1.04/1.11 type(empty_set,set_type) ). % 1.04/1.11 % 1.04/1.11 %---- line(relat_1 - df(10),1918876) % 1.04/1.11 fof(p4,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ! [D] : % 1.04/1.11 ( ilf_type(D,set_type) % 1.04/1.11 => ( member(ordered_pair(C,D),identity_relation_of(B)) % 1.04/1.11 <=> ( member(C,B) % 1.04/1.11 & C = D ) ) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(line(relat_1 - df(10),1918876)) % 1.04/1.11 fof(p5,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ilf_type(identity_relation_of(B),binary_relation_type) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom560,1832615) % 1.04/1.11 fof(p6,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( B = C % 1.04/1.11 <=> ! [D] : % 1.04/1.11 ( ilf_type(D,set_type) % 1.04/1.11 => ( member(D,B) % 1.04/1.11 <=> member(D,C) ) ) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom561,1832619) % 1.04/1.11 fof(p7,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( not_equal(B,C) % 1.04/1.11 <=> B != C ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom562,1832628) % 1.04/1.11 fof(p8,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ( empty(B) % 1.04/1.11 <=> ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ~ member(C,B) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(op(ordered_pair,2,function)) % 1.04/1.11 fof(p9,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(relat_1 - axiom563,1917641) % 1.04/1.11 fof(p10,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ( ilf_type(B,binary_relation_type) % 1.04/1.11 <=> ( relation_like(B) % 1.04/1.11 & ilf_type(B,set_type) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- type_nonempty(line(relat_1 - axiom563,1917641)) % 1.04/1.11 fof(p11,axiom, % 1.04/1.11 ? [B] : ilf_type(B,binary_relation_type) ). % 1.04/1.11 % 1.04/1.11 %---- line(relat_1 - df(1),1917627) % 1.04/1.11 fof(p12,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ( relation_like(B) % 1.04/1.11 <=> ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( member(C,B) % 1.04/1.11 => ? [D] : % 1.04/1.11 ( ilf_type(D,set_type) % 1.04/1.11 & ? [E] : % 1.04/1.11 ( ilf_type(E,set_type) % 1.04/1.11 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- conditional_cluster(axiom566,relation_like) % 1.04/1.11 fof(p13,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ( empty(B) % 1.04/1.11 & ilf_type(B,set_type) ) % 1.04/1.11 => relation_like(B) ) ). % 1.04/1.11 % 1.04/1.11 %---- conditional_cluster(axiom567,relation_like) % 1.04/1.11 fof(p14,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ! [D] : % 1.04/1.11 ( ilf_type(D,subset_type(cross_product(B,C))) % 1.04/1.11 => relation_like(D) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(op(cross_product,2,function)) % 1.04/1.11 fof(p15,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ilf_type(cross_product(B,C),set_type) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom568,1832648) % 1.04/1.11 fof(p16,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( ilf_type(C,subset_type(B)) % 1.04/1.11 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- type_nonempty(line(hidden - axiom568,1832648)) % 1.04/1.11 fof(p17,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom569,1832644) % 1.04/1.11 fof(p18,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ilf_type(C,set_type) % 1.04/1.11 => ( member(B,power_set(C)) % 1.04/1.11 <=> ! [D] : % 1.04/1.11 ( ilf_type(D,set_type) % 1.04/1.11 => ( member(D,B) % 1.04/1.11 => member(D,C) ) ) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(line(hidden - axiom569,1832644)) % 1.04/1.11 fof(p19,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ( ~ empty(power_set(B)) % 1.04/1.11 & ilf_type(power_set(B),set_type) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- line(hidden - axiom570,1832640) % 1.04/1.11 fof(p20,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ilf_type(B,set_type) % 1.04/1.11 => ! [C] : % 1.04/1.11 ( ( ~ empty(C) % 1.04/1.11 & ilf_type(C,set_type) ) % 1.04/1.11 => ( ilf_type(B,member_type(C)) % 1.04/1.11 <=> member(B,C) ) ) ) ). % 1.04/1.11 % 1.04/1.11 %---- type_nonempty(line(hidden - axiom570,1832640)) % 1.04/1.11 fof(p21,axiom, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ( ~ empty(B) % 1.04/1.11 & ilf_type(B,set_type) ) % 1.04/1.11 => ? [C] : ilf_type(C,member_type(B)) ) ). % 1.04/1.11 % 1.04/1.11 %---- declaration(set) % 1.04/1.11 fof(p22,axiom, % 1.04/1.11 ! [B] : ilf_type(B,set_type) ). % 1.04/1.11 % 1.04/1.11 %---- line(relset_1 - th(46),1916859) % 1.04/1.11 fof(prove_relset_1_46,conjecture, % 1.04/1.11 ! [B] : % 1.04/1.11 ( ( ~ empty(B) % 1.04/1.11 & ilf_type(B,set_type) ) % 1.04/1.11 => not_equal(identity_relation_of(B),empty_set) ) ). % 1.04/1.11 % 1.04/1.11 %-------------------------------------------------------------------------- % 1.04/1.11 %------------------------------------------- % 1.04/1.11 % Proof found % 1.04/1.11 % SZS status Theorem for theBenchmark % 1.04/1.11 % SZS output start Proof % 1.04/1.11 %ClaNum:79(EqnAxiom:33) % 1.04/1.11 %VarNum:180(SingletonVarNum:57) % 1.04/1.11 %MaxLitNum:6 % 1.04/1.11 %MaxfuncDepth:2 % 1.04/1.11 %SharedTerms:12 % 1.04/1.11 %goalClause: 39 40 % 1.04/1.11 %singleGoalClaCount:2 % 1.04/1.11 [34]P1(a1) % 1.04/1.11 [35]P2(a4,a2) % 1.04/1.11 [37]P3(a1,a8) % 1.04/1.11 [39]~P1(a5) % 1.04/1.11 [40]~P4(f9(a5),a1) % 1.04/1.11 [38]P2(x381,a8) % 1.04/1.11 [46]~P5(x461,a1)+~P2(x461,a8) % 1.04/1.11 [42]~P2(x421,a8)+~P1(f16(x421)) % 1.04/1.11 [43]~P2(x431,a8)+P2(f9(x431),a2) % 1.04/1.11 [52]~P2(x521,a8)+P2(f13(x521),f19(x521)) % 1.04/1.11 [41]~P1(x411)+P6(x411)+~P2(x411,a8) % 1.04/1.11 [45]~P6(x451)+~P2(x451,a8)+P2(x451,a2) % 1.04/1.11 [49]P6(x491)+~P2(x491,a8)+~P2(x491,a2) % 1.04/1.11 [50]P1(x501)+P5(f6(x501),x501)+~P2(x501,a8) % 1.04/1.11 [51]P6(x511)+P5(f10(x511),x511)+~P2(x511,a8) % 1.04/1.11 [53]P1(x531)+P2(f14(x531),f17(x531))+~P2(x531,a8) % 1.04/1.11 [54]P4(x541,x542)+E(x541,x542)+~P2(x542,a8)+~P2(x541,a8) % 1.04/1.11 [55]~P4(x551,x552)+~E(x551,x552)+~P2(x552,a8)+~P2(x551,a8) % 1.04/1.11 [56]~P1(x561)+~P5(x562,x561)+~P2(x562,a8)+~P2(x561,a8) % 1.04/1.11 [64]P5(f15(x641,x642),x641)+~P2(x642,a8)+~P2(x641,a8)+P5(x641,f16(x642)) % 1.04/1.11 [68]~P5(x681,x682)+~P2(x682,a8)+~P2(x681,a8)+P5(f18(x681,x681),f9(x682)) % 1.04/1.11 [71]~P2(x712,a8)+~P2(x711,a8)+~P5(f15(x711,x712),x712)+P5(x711,f16(x712)) % 1.04/1.11 [72]P5(x721,x722)+~P2(x722,a8)+~P2(x721,a8)+~P5(f18(x721,x721),f9(x722)) % 1.04/1.11 [65]~P2(x652,a8)+~P2(x651,a8)+~P2(x651,f19(x652))+P2(x651,f17(f16(x652))) % 1.04/1.11 [69]~P2(x692,a8)+~P2(x691,a8)+P2(x691,f19(x692))+~P2(x691,f17(f16(x692))) % 1.04/1.11 [78]P6(x781)+~P2(x782,a8)+~P2(x783,a8)+~P2(x781,f19(f3(x783,x782))) % 1.04/1.11 [60]~P5(x602,x601)+P1(x601)+~P2(x601,a8)+~P2(x602,a8)+P2(x602,f17(x601)) % 1.04/1.11 [61]P1(x611)+P5(x612,x611)+~P2(x611,a8)+~P2(x612,a8)+~P2(x612,f17(x611)) % 1.04/1.11 [70]E(x701,x702)+P5(f7(x701,x702),x702)+P5(f7(x701,x702),x701)+~P2(x702,a8)+~P2(x701,a8) % 1.04/1.11 [79]E(x791,x792)+~P2(x792,a8)+~P2(x791,a8)+~P5(f7(x791,x792),x792)+~P5(f7(x791,x792),x791) % 1.04/1.11 [76]~P6(x761)+~P5(x762,x761)+~P2(x761,a8)+~P2(x762,a8)+E(f18(f11(x761,x762),f12(x761,x762)),x762) % 1.04/1.11 [62]P6(x621)+~P2(x621,a8)+~P2(x623,a8)+~P2(x622,a8)+~E(f10(x621),f18(x622,x623)) % 1.04/1.11 [75]E(x751,x752)+~P2(x752,a8)+~P2(x751,a8)+~P5(f18(x751,x752),f9(x753))+~P2(x753,a8) % 1.04/1.11 [77]P5(x771,x772)+~P2(x772,a8)+~P2(x771,a8)+~P5(f18(x771,x773),f9(x772))+~P2(x773,a8) % 1.04/1.11 [73]P5(x731,x732)+~P5(x731,x733)+~P2(x731,a8)+~P2(x732,a8)+~P2(x733,a8)+~P5(x733,f16(x732)) % 1.04/1.11 [74]~E(x741,x742)+~P5(x741,x743)+~P2(x742,a8)+~P2(x743,a8)+~P2(x741,a8)+P5(f18(x741,x742),f9(x743)) % 1.04/1.11 %EqnAxiom % 1.04/1.11 [1]E(x11,x11) % 1.04/1.11 [2]E(x22,x21)+~E(x21,x22) % 1.04/1.11 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.04/1.11 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 1.04/1.11 [5]~E(x51,x52)+E(f16(x51),f16(x52)) % 1.04/1.11 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63)) % 1.04/1.11 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72)) % 1.04/1.11 [8]~E(x81,x82)+E(f18(x81,x83),f18(x82,x83)) % 1.04/1.11 [9]~E(x91,x92)+E(f18(x93,x91),f18(x93,x92)) % 1.04/1.11 [10]~E(x101,x102)+E(f6(x101),f6(x102)) % 1.04/1.11 [11]~E(x111,x112)+E(f10(x111),f10(x112)) % 1.04/1.11 [12]~E(x121,x122)+E(f19(x121),f19(x122)) % 1.04/1.11 [13]~E(x131,x132)+E(f12(x131,x133),f12(x132,x133)) % 1.04/1.11 [14]~E(x141,x142)+E(f12(x143,x141),f12(x143,x142)) % 1.04/1.11 [15]~E(x151,x152)+E(f13(x151),f13(x152)) % 1.04/1.11 [16]~E(x161,x162)+E(f17(x161),f17(x162)) % 1.04/1.11 [17]~E(x171,x172)+E(f14(x171),f14(x172)) % 1.04/1.11 [18]~E(x181,x182)+E(f11(x181,x183),f11(x182,x183)) % 1.04/1.11 [19]~E(x191,x192)+E(f11(x193,x191),f11(x193,x192)) % 1.04/1.11 [20]~E(x201,x202)+E(f3(x201,x203),f3(x202,x203)) % 1.04/1.11 [21]~E(x211,x212)+E(f3(x213,x211),f3(x213,x212)) % 1.04/1.11 [22]~E(x221,x222)+E(f15(x221,x223),f15(x222,x223)) % 1.04/1.11 [23]~E(x231,x232)+E(f15(x233,x231),f15(x233,x232)) % 1.04/1.11 [24]~P1(x241)+P1(x242)+~E(x241,x242) % 1.04/1.11 [25]P2(x252,x253)+~E(x251,x252)+~P2(x251,x253) % 1.04/1.11 [26]P2(x263,x262)+~E(x261,x262)+~P2(x263,x261) % 1.04/1.11 [27]P5(x272,x273)+~E(x271,x272)+~P5(x271,x273) % 1.04/1.11 [28]P5(x283,x282)+~E(x281,x282)+~P5(x283,x281) % 1.04/1.11 [29]P3(x292,x293)+~E(x291,x292)+~P3(x291,x293) % 1.04/1.11 [30]P3(x303,x302)+~E(x301,x302)+~P3(x303,x301) % 1.04/1.11 [31]P4(x312,x313)+~E(x311,x312)+~P4(x311,x313) % 1.04/1.11 [32]P4(x323,x322)+~E(x321,x322)+~P4(x323,x321) % 1.04/1.11 [33]~P6(x331)+P6(x332)+~E(x331,x332) % 1.04/1.11 % 1.04/1.11 %------------------------------------------- % 1.04/1.11 cnf(80,plain, % 1.04/1.11 (~P4(x801,x801)+~P2(x801,a8)+~P2(x801,a8)), % 1.04/1.11 inference(equality_inference,[],[55])). % 1.04/1.11 cnf(82,plain, % 1.04/1.11 (~P5(x821,a1)), % 1.04/1.11 inference(scs_inference,[],[38,46])). % 1.04/1.11 cnf(85,plain, % 1.04/1.11 (P2(x851,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(89,plain, % 1.04/1.11 (P2(a1,a2)), % 1.04/1.11 inference(scs_inference,[],[38,85,34,46,41,80,45])). % 1.04/1.11 cnf(90,plain, % 1.04/1.11 (P2(x901,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(93,plain, % 1.04/1.11 (P2(x931,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(95,plain, % 1.04/1.11 (~P5(f18(a1,a1),f9(a1))), % 1.04/1.11 inference(scs_inference,[],[38,85,90,93,34,35,46,41,80,45,49,72])). % 1.04/1.11 cnf(96,plain, % 1.04/1.11 (P2(x961,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(97,plain, % 1.04/1.11 (P2(x971,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(100,plain, % 1.04/1.11 (E(f9(a5),a1)), % 1.04/1.11 inference(scs_inference,[],[40,38,85,90,93,97,96,34,35,46,41,80,45,49,72,25,54])). % 1.04/1.11 cnf(102,plain, % 1.04/1.11 (P2(x1021,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(104,plain, % 1.04/1.11 (E(a1,f9(a5))), % 1.04/1.11 inference(scs_inference,[],[40,38,85,90,93,97,96,34,35,46,41,80,45,49,72,25,54,2])). % 1.04/1.11 cnf(105,plain, % 1.04/1.11 (P1(f9(a5))), % 1.04/1.11 inference(scs_inference,[],[40,38,85,90,93,97,96,34,35,46,41,80,45,49,72,25,54,2,24])). % 1.04/1.11 cnf(107,plain, % 1.04/1.11 (P3(f9(a5),a8)), % 1.04/1.11 inference(scs_inference,[],[40,38,85,90,93,97,102,96,34,35,37,46,41,80,45,49,72,25,54,2,24,26,29])). % 1.04/1.11 cnf(117,plain, % 1.04/1.11 (P2(f9(a5),a2)), % 1.04/1.11 inference(scs_inference,[],[104,89,25])). % 1.04/1.11 cnf(118,plain, % 1.04/1.11 (~P5(f9(a5),f9(a5))), % 1.04/1.11 inference(scs_inference,[],[105,104,38,89,25,56])). % 1.04/1.11 cnf(120,plain, % 1.04/1.11 (P2(x1201,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(123,plain, % 1.04/1.11 (P2(x1231,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(124,plain, % 1.04/1.11 (P2(x1241,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(125,plain, % 1.04/1.11 (~P5(x1251,a1)), % 1.04/1.11 inference(rename_variables,[],[82])). % 1.04/1.11 cnf(128,plain, % 1.04/1.11 (P2(x1281,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(129,plain, % 1.04/1.11 (P2(x1291,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(136,plain, % 1.04/1.11 (P2(x1361,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(137,plain, % 1.04/1.11 (P2(x1371,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(144,plain, % 1.04/1.11 (~E(f16(a1),f9(a5))), % 1.04/1.11 inference(scs_inference,[],[40,105,95,82,125,104,107,38,120,124,129,137,123,128,136,89,25,56,64,72,27,28,30,54,75,31])). % 1.04/1.11 cnf(160,plain, % 1.04/1.11 (P2(x1601,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(161,plain, % 1.04/1.11 (P2(x1611,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(165,plain, % 1.04/1.11 (P2(x1651,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(166,plain, % 1.04/1.11 (P2(x1661,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(169,plain, % 1.04/1.11 (~P5(x1691,f9(a5))), % 1.04/1.11 inference(scs_inference,[],[144,105,118,117,38,161,166,165,160,72,75,26,56])). % 1.04/1.11 cnf(170,plain, % 1.04/1.11 (P2(x1701,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(172,plain, % 1.04/1.11 (P5(a1,f16(x1721))), % 1.04/1.11 inference(scs_inference,[],[144,105,118,117,82,38,161,166,170,165,160,72,75,26,56,64])). % 1.04/1.11 cnf(275,plain, % 1.04/1.11 (~P1(f16(a1))), % 1.04/1.11 inference(scs_inference,[],[38,100,42,25])). % 1.04/1.11 cnf(642,plain, % 1.04/1.11 (P2(x6421,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(643,plain, % 1.04/1.11 (P2(x6431,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(646,plain, % 1.04/1.11 (P2(x6461,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(647,plain, % 1.04/1.11 (P2(x6471,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(649,plain, % 1.04/1.11 (~P5(x6491,a5)+P5(f16(a1),f16(a1))), % 1.04/1.11 inference(scs_inference,[],[275,38,643,646,642,647,169,61,65,68])). % 1.04/1.11 cnf(669,plain, % 1.04/1.11 (~P2(f16(a1),a8)+~P5(x6691,a5)), % 1.04/1.11 inference(scs_inference,[],[38,82,172,649,73])). % 1.04/1.11 cnf(671,plain, % 1.04/1.11 (P2(x6711,a8)), % 1.04/1.11 inference(rename_variables,[],[38])). % 1.04/1.11 cnf(672,plain, % 1.04/1.11 ($false), % 1.04/1.11 inference(scs_inference,[],[39,38,671,669,50]), % 1.04/1.11 ['proof']). % 1.04/1.11 % SZS output end Proof % 1.04/1.11 % Total time :0.470000s %------------------------------------------------------------------------------