%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET662+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 : 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:10 EDT 2024 % Result : Theorem 116.84s 117.15s % Output : CNFRefutation 116.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.15 % Problem : SET662+3 : TPTP v8.2.0. Released v2.2.0. % 0.05/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.37 % Computer : n021.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Sun Jun 23 13:03:09 EDT 2024 % 0.14/0.37 % CPUTime : % 0.54/0.69 start to proof:theBenchmark % 116.84/117.13 %------------------------------------------- % 116.84/117.13 % File :CSE---1.7 % 116.84/117.13 % Problem :theBenchmark % 116.84/117.13 % Transform :cnf % 116.84/117.13 % Format :tptp:raw % 116.84/117.13 % Command :java -jar mcs_scs.jar %d %s % 116.84/117.13 % 116.84/117.13 % Result :Theorem 116.140000s % 116.84/117.13 % Output :CNFRefutation 116.140000s % 116.84/117.13 %------------------------------------------- % 116.84/117.14 %-------------------------------------------------------------------------- % 116.84/117.14 % File : SET662+3 : TPTP v8.2.0. Released v2.2.0. % 116.84/117.14 % Domain : Set Theory (Relations) % 116.84/117.14 % Problem : The empty set is a relation from X to Y % 116.84/117.14 % Version : [Wor90] axioms : Reduced > Incomplete. % 116.84/117.14 % English : % 116.84/117.14 % 116.84/117.14 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 116.84/117.14 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 116.84/117.14 % Source : [ILF] % 116.84/117.14 % Names : RELSET_1 (25) [Wor90] % 116.84/117.14 % 116.84/117.14 % Status : Theorem % 116.84/117.14 % Rating : 0.25 v8.2.0, 0.19 v8.1.0, 0.25 v7.5.0, 0.22 v7.4.0, 0.27 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.26 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.35 v5.5.0, 0.26 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.11 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 % 116.84/117.14 % Syntax : Number of formulae : 22 ( 3 unt; 0 def) % 116.84/117.14 % Number of atoms : 75 ( 1 equ) % 116.84/117.14 % Maximal formula atoms : 7 ( 3 avg) % 116.84/117.14 % Number of connectives : 58 ( 5 ~; 0 |; 7 &) % 116.84/117.14 % ( 6 <=>; 40 =>; 0 <=; 0 <~>) % 116.84/117.14 % Maximal formula depth : 11 ( 5 avg) % 116.84/117.14 % Maximal term depth : 3 ( 1 avg) % 116.84/117.14 % Number of predicates : 7 ( 6 usr; 0 prp; 1-2 aty) % 116.84/117.14 % Number of functors : 8 ( 8 usr; 2 con; 0-2 aty) % 116.84/117.14 % Number of variables : 43 ( 38 !; 5 ?) % 116.84/117.14 % SPC : FOF_THM_RFO_SEQ % 116.84/117.14 % 116.84/117.14 % Comments : % 116.84/117.14 %-------------------------------------------------------------------------- % 116.84/117.14 %---- line(relat_1 - th(58),1918738) % 116.84/117.14 fof(p1,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => subset(empty_set,cross_product(B,C)) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- line(relset_1 - df(1),1916080) % 116.84/117.14 fof(p2,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => ( ! [D] : % 116.84/117.14 ( ilf_type(D,subset_type(cross_product(B,C))) % 116.84/117.14 => ilf_type(D,relation_type(B,C)) ) % 116.84/117.14 & ! [E] : % 116.84/117.14 ( ilf_type(E,relation_type(B,C)) % 116.84/117.14 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 116.84/117.14 fof(p3,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- line(hidden - axiom233,1832636) % 116.84/117.14 fof(p4,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ~ member(B,empty_set) ) ). % 116.84/117.14 % 116.84/117.14 %---- declaration(line(hidden - axiom233,1832636)) Part 1 % 116.84/117.14 fof(p5a,axiom, % 116.84/117.14 empty(empty_set) ). % 116.84/117.14 % 116.84/117.14 %---- declaration(line(hidden - axiom233,1832636)) Part 2 % 116.84/117.14 fof(p5b,axiom, % 116.84/117.14 type(empty_set,set_type) ). % 116.84/117.14 % 116.84/117.14 %---- declaration(op(cross_product,2,function)) % 116.84/117.14 fof(p6,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => ilf_type(cross_product(B,C),set_type) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- line(hidden - axiom234,1832648) % 116.84/117.14 fof(p7,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => ( ilf_type(C,subset_type(B)) % 116.84/117.14 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- type_nonempty(line(hidden - axiom234,1832648)) % 116.84/117.14 fof(p8,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 116.84/117.14 % 116.84/117.14 %---- line(tarski - df(3),1832749) % 116.84/117.14 fof(p9,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => ! [C] : % 116.84/117.14 ( ilf_type(C,set_type) % 116.84/117.14 => ( subset(B,C) % 116.84/117.14 <=> ! [D] : % 116.84/117.14 ( ilf_type(D,set_type) % 116.84/117.14 => ( member(D,B) % 116.84/117.14 => member(D,C) ) ) ) ) ) ). % 116.84/117.14 % 116.84/117.14 %---- property(reflexivity,op(subset,2,predicate)) % 116.84/117.14 fof(p10,axiom, % 116.84/117.14 ! [B] : % 116.84/117.14 ( ilf_type(B,set_type) % 116.84/117.14 => subset(B,B) ) ). % 116.84/117.14 % 116.84/117.14 %---- line(hidden - axiom236,1832628) % 116.84/117.15 fof(p11,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ( empty(B) % 116.84/117.15 <=> ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ~ member(C,B) ) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- line(hidden - axiom238,1832644) % 116.84/117.15 fof(p12,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ( member(B,power_set(C)) % 116.84/117.15 <=> ! [D] : % 116.84/117.15 ( ilf_type(D,set_type) % 116.84/117.15 => ( member(D,B) % 116.84/117.15 => member(D,C) ) ) ) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- declaration(line(hidden - axiom238,1832644)) % 116.84/117.15 fof(p13,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ( ~ empty(power_set(B)) % 116.84/117.15 & ilf_type(power_set(B),set_type) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- line(hidden - axiom239,1832640) % 116.84/117.15 fof(p14,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ! [C] : % 116.84/117.15 ( ( ~ empty(C) % 116.84/117.15 & ilf_type(C,set_type) ) % 116.84/117.15 => ( ilf_type(B,member_type(C)) % 116.84/117.15 <=> member(B,C) ) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- type_nonempty(line(hidden - axiom239,1832640)) % 116.84/117.15 fof(p15,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ( ~ empty(B) % 116.84/117.15 & ilf_type(B,set_type) ) % 116.84/117.15 => ? [C] : ilf_type(C,member_type(B)) ) ). % 116.84/117.15 % 116.84/117.15 %---- line(relat_1 - df(1),1917627) % 116.84/117.15 fof(p16,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ( relation_like(B) % 116.84/117.15 <=> ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ( member(C,B) % 116.84/117.15 => ? [D] : % 116.84/117.15 ( ilf_type(D,set_type) % 116.84/117.15 & ? [E] : % 116.84/117.15 ( ilf_type(E,set_type) % 116.84/117.15 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- conditional_cluster(axiom240,relation_like) % 116.84/117.15 fof(p17,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ( empty(B) % 116.84/117.15 & ilf_type(B,set_type) ) % 116.84/117.15 => relation_like(B) ) ). % 116.84/117.15 % 116.84/117.15 %---- conditional_cluster(axiom241,relation_like) % 116.84/117.15 fof(p18,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ! [D] : % 116.84/117.15 ( ilf_type(D,subset_type(cross_product(B,C))) % 116.84/117.15 => relation_like(D) ) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- declaration(op(ordered_pair,2,function)) % 116.84/117.15 fof(p19,axiom, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 116.84/117.15 % 116.84/117.15 %---- declaration(set) % 116.84/117.15 fof(p20,axiom, % 116.84/117.15 ! [B] : ilf_type(B,set_type) ). % 116.84/117.15 % 116.84/117.15 %---- line(relset_1 - th(25),1916495) % 116.84/117.15 fof(prove_relset_1_25,conjecture, % 116.84/117.15 ! [B] : % 116.84/117.15 ( ilf_type(B,set_type) % 116.84/117.15 => ! [C] : % 116.84/117.15 ( ilf_type(C,set_type) % 116.84/117.15 => ilf_type(empty_set,relation_type(B,C)) ) ) ). % 116.84/117.15 % 116.84/117.15 %-------------------------------------------------------------------------- % 116.84/117.15 %------------------------------------------- % 116.84/117.15 % Proof found % 116.84/117.15 % SZS status Theorem for theBenchmark % 116.84/117.15 % SZS output start Proof % 116.84/117.15 %ClaNum:77(EqnAxiom:36) % 116.84/117.15 %VarNum:152(SingletonVarNum:51) % 116.84/117.15 %MaxLitNum:6 % 116.84/117.15 %MaxfuncDepth:2 % 116.84/117.15 %SharedTerms:10 % 116.84/117.15 %goalClause: 42 % 116.84/117.15 %singleGoalClaCount:1 % 116.84/117.15 [37]P1(a1) % 116.84/117.15 [40]P3(a1,a4) % 116.84/117.15 [42]~P2(a1,f6(a3,a5)) % 116.84/117.15 [41]P2(x411,a4) % 116.84/117.15 [44]P6(x441,x441)+~P2(x441,a4) % 116.84/117.15 [47]~P5(x471,a1)+~P2(x471,a4) % 116.84/117.15 [45]~P2(x451,a4)+~P1(f7(x451)) % 116.84/117.15 [52]~P2(x521,a4)+P2(f9(x521),f19(x521)) % 116.84/117.15 [43]~P1(x431)+P4(x431)+~P2(x431,a4) % 116.84/117.15 [50]P1(x501)+P5(f8(x501),x501)+~P2(x501,a4) % 116.84/117.15 [51]P4(x511)+P5(f12(x511),x511)+~P2(x511,a4) % 116.84/117.15 [53]P1(x531)+P2(f13(x531),f17(x531))+~P2(x531,a4) % 116.84/117.15 [55]~P2(x552,a4)+~P2(x551,a4)+P6(a1,f2(x551,x552)) % 116.84/117.15 [66]~P2(x662,a4)+~P2(x661,a4)+P2(f10(x661,x662),f6(x662,x661)) % 116.84/117.15 [54]~P1(x541)+~P5(x542,x541)+~P2(x542,a4)+~P2(x541,a4) % 116.84/117.15 [62]P6(x621,x622)+P5(f11(x621,x622),x621)+~P2(x622,a4)+~P2(x621,a4) % 116.84/117.15 [64]P5(f14(x641,x642),x641)+~P2(x642,a4)+~P2(x641,a4)+P5(x641,f7(x642)) % 116.84/117.15 [70]P6(x701,x702)+~P2(x702,a4)+~P2(x701,a4)+~P5(f11(x701,x702),x702) % 116.84/117.15 [72]~P2(x722,a4)+~P2(x721,a4)+~P5(f14(x721,x722),x722)+P5(x721,f7(x722)) % 116.84/117.15 [65]~P2(x652,a4)+~P2(x651,a4)+~P2(x651,f19(x652))+P2(x651,f17(f7(x652))) % 116.84/117.15 [69]~P2(x692,a4)+~P2(x691,a4)+P2(x691,f19(x692))+~P2(x691,f17(f7(x692))) % 116.84/117.15 [75]P4(x751)+~P2(x752,a4)+~P2(x753,a4)+~P2(x751,f19(f2(x753,x752))) % 116.84/117.15 [76]~P2(x763,a4)+~P2(x762,a4)+~P2(x761,f6(x762,x763))+P2(x761,f19(f2(x762,x763))) % 116.84/117.15 [77]~P2(x773,a4)+~P2(x772,a4)+P2(x771,f6(x772,x773))+~P2(x771,f19(f2(x772,x773))) % 116.84/117.15 [58]~P5(x582,x581)+P1(x581)+~P2(x581,a4)+~P2(x582,a4)+P2(x582,f17(x581)) % 116.84/117.15 [59]P1(x591)+P5(x592,x591)+~P2(x591,a4)+~P2(x592,a4)+~P2(x592,f17(x591)) % 116.84/117.15 [74]~P4(x741)+~P5(x742,x741)+~P2(x741,a4)+~P2(x742,a4)+E(f18(f15(x741,x742),f16(x741,x742)),x742) % 116.84/117.15 [61]P4(x611)+~P2(x611,a4)+~P2(x613,a4)+~P2(x612,a4)+~E(f12(x611),f18(x612,x613)) % 116.84/117.15 [71]~P5(x711,x713)+P5(x711,x712)+~P6(x713,x712)+~P2(x711,a4)+~P2(x712,a4)+~P2(x713,a4) % 116.84/117.15 [73]P5(x731,x732)+~P5(x731,x733)+~P2(x731,a4)+~P2(x732,a4)+~P2(x733,a4)+~P5(x733,f7(x732)) % 116.84/117.15 %EqnAxiom % 116.84/117.15 [1]E(x11,x11) % 116.84/117.15 [2]E(x22,x21)+~E(x21,x22) % 116.84/117.15 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.84/117.15 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43)) % 116.84/117.15 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52)) % 116.84/117.15 [6]~E(x61,x62)+E(f7(x61),f7(x62)) % 116.84/117.15 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73)) % 116.84/117.15 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82)) % 116.84/117.15 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 116.84/117.15 [10]~E(x101,x102)+E(f12(x101),f12(x102)) % 116.84/117.15 [11]~E(x111,x112)+E(f11(x111,x113),f11(x112,x113)) % 116.84/117.15 [12]~E(x121,x122)+E(f11(x123,x121),f11(x123,x122)) % 116.84/117.15 [13]~E(x131,x132)+E(f17(x131),f17(x132)) % 116.84/117.15 [14]~E(x141,x142)+E(f9(x141),f9(x142)) % 116.84/117.15 [15]~E(x151,x152)+E(f19(x151),f19(x152)) % 116.84/117.15 [16]~E(x161,x162)+E(f13(x161),f13(x162)) % 116.84/117.15 [17]~E(x171,x172)+E(f15(x171,x173),f15(x172,x173)) % 116.84/117.15 [18]~E(x181,x182)+E(f15(x183,x181),f15(x183,x182)) % 116.84/117.15 [19]~E(x191,x192)+E(f14(x191,x193),f14(x192,x193)) % 116.84/117.15 [20]~E(x201,x202)+E(f14(x203,x201),f14(x203,x202)) % 116.84/117.15 [21]~E(x211,x212)+E(f16(x211,x213),f16(x212,x213)) % 116.84/117.15 [22]~E(x221,x222)+E(f16(x223,x221),f16(x223,x222)) % 116.84/117.15 [23]~E(x231,x232)+E(f18(x231,x233),f18(x232,x233)) % 116.84/117.15 [24]~E(x241,x242)+E(f18(x243,x241),f18(x243,x242)) % 116.84/117.15 [25]~E(x251,x252)+E(f10(x251,x253),f10(x252,x253)) % 116.84/117.15 [26]~E(x261,x262)+E(f10(x263,x261),f10(x263,x262)) % 116.84/117.15 [27]~P1(x271)+P1(x272)+~E(x271,x272) % 116.84/117.15 [28]P2(x282,x283)+~E(x281,x282)+~P2(x281,x283) % 116.84/117.15 [29]P2(x293,x292)+~E(x291,x292)+~P2(x293,x291) % 116.84/117.15 [30]~P4(x301)+P4(x302)+~E(x301,x302) % 116.84/117.15 [31]P3(x312,x313)+~E(x311,x312)+~P3(x311,x313) % 116.84/117.15 [32]P3(x323,x322)+~E(x321,x322)+~P3(x323,x321) % 116.84/117.15 [33]P5(x332,x333)+~E(x331,x332)+~P5(x331,x333) % 116.84/117.15 [34]P5(x343,x342)+~E(x341,x342)+~P5(x343,x341) % 116.84/117.15 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353) % 116.84/117.15 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361) % 116.84/117.15 % 116.84/117.15 %------------------------------------------- % 116.84/117.16 cnf(78,plain, % 116.84/117.16 (P6(x781,x781)), % 116.84/117.16 inference(scs_inference,[],[41,44])). % 116.84/117.16 cnf(80,plain, % 116.84/117.16 (~P5(x801,a1)), % 116.84/117.16 inference(scs_inference,[],[41,44,47])). % 116.84/117.16 cnf(83,plain, % 116.84/117.16 (P2(x831,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(85,plain, % 116.84/117.16 (P2(x851,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(91,plain, % 116.84/117.16 (P5(x911,f7(x911))+P5(f14(x911,x911),x911)), % 116.84/117.16 inference(scs_inference,[],[42,41,83,85,37,40,44,47,29,43,35,31,32,36,64])). % 116.84/117.16 cnf(99,plain, % 116.84/117.16 (P5(a1,f7(a1))), % 116.84/117.16 inference(scs_inference,[],[80,91])). % 116.84/117.16 cnf(100,plain, % 116.84/117.16 (~P5(x1001,a1)), % 116.84/117.16 inference(rename_variables,[],[80])). % 116.84/117.16 cnf(104,plain, % 116.84/117.16 (P5(x1041,f7(a1))+~E(a1,x1041)), % 116.84/117.16 inference(scs_inference,[],[80,100,91,34,33])). % 116.84/117.16 cnf(116,plain, % 116.84/117.16 (P6(x1161,x1162)+~E(x1161,x1162)), % 116.84/117.16 inference(scs_inference,[],[78,36])). % 116.84/117.16 cnf(117,plain, % 116.84/117.16 (P6(x1171,x1172)+~E(x1172,x1171)), % 116.84/117.16 inference(scs_inference,[],[78,36,35])). % 116.84/117.16 cnf(152,plain, % 116.84/117.16 (~E(x1521,x1522)+~P1(f7(x1522))), % 116.84/117.16 inference(scs_inference,[],[41,45,28])). % 116.84/117.16 cnf(153,plain, % 116.84/117.16 (~P1(f7(x1531))), % 116.84/117.16 inference(equality_inference,[],[152])). % 116.84/117.16 cnf(154,plain, % 116.84/117.16 (P5(f7(x1541),f7(x1541))+~P2(f7(x1541),f17(f7(x1541)))), % 116.84/117.16 inference(scs_inference,[],[41,153,59])). % 116.84/117.16 cnf(181,plain, % 116.84/117.16 (P2(f9(x1811),x1812)+~E(f19(x1811),x1812)), % 116.84/117.16 inference(scs_inference,[],[41,52,29])). % 116.84/117.16 cnf(182,plain, % 116.84/117.16 (P2(f9(x1821),f19(x1821))), % 116.84/117.16 inference(equality_inference,[],[181])). % 116.84/117.16 cnf(184,plain, % 116.84/117.16 (P2(f9(x1841),f19(x1841))), % 116.84/117.16 inference(rename_variables,[],[182])). % 116.84/117.16 cnf(187,plain, % 116.84/117.16 (P2(f9(x1871),f19(x1871))), % 116.84/117.16 inference(rename_variables,[],[182])). % 116.84/117.16 cnf(189,plain, % 116.84/117.16 (P2(x1891,f19(x1892))+~E(f9(x1892),x1891)), % 116.84/117.16 inference(scs_inference,[],[41,182,184,187,77,75,28])). % 116.84/117.16 cnf(267,plain, % 116.84/117.16 (~P2(f7(a1),f17(f7(a1)))+~P2(f7(a1),a4)), % 116.84/117.16 inference(scs_inference,[],[41,80,99,154,73])). % 116.84/117.16 cnf(269,plain, % 116.84/117.16 (P2(x2691,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(270,plain, % 116.84/117.16 (~P5(f7(a1),f7(a1))), % 116.84/117.16 inference(scs_inference,[],[41,269,153,267,58])). % 116.84/117.16 cnf(271,plain, % 116.84/117.16 (P2(x2711,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(272,plain, % 116.84/117.16 (P2(x2721,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(277,plain, % 116.84/117.16 (P2(x2771,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(278,plain, % 116.84/117.16 (P2(x2781,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(280,plain, % 116.84/117.16 (P6(x2801,x2802)+~P5(f11(x2801,x2802),x2802)), % 116.84/117.16 inference(scs_inference,[],[41,269,272,277,271,278,99,153,267,58,33,65,70])). % 116.84/117.16 cnf(282,plain, % 116.84/117.16 (P5(f14(f7(a1),a1),f7(a1))), % 116.84/117.16 inference(scs_inference,[],[41,269,272,277,271,278,99,153,267,58,33,65,70,64])). % 116.84/117.16 cnf(290,plain, % 116.84/117.16 (P6(x2901,f7(a1))+~E(a1,f11(x2901,f7(a1)))), % 116.84/117.16 inference(scs_inference,[],[280,104])). % 116.84/117.16 cnf(294,plain, % 116.84/117.16 (~E(f11(x2941,f7(a1)),a1)+P6(x2941,f7(a1))), % 116.84/117.16 inference(scs_inference,[],[290,2])). % 116.84/117.16 cnf(295,plain, % 116.84/117.16 (~E(x2951,a1)+~E(f11(x2952,f7(a1)),x2951)+P6(x2952,f7(a1))), % 116.84/117.16 inference(scs_inference,[],[294,3])). % 116.84/117.16 cnf(312,plain, % 116.84/117.16 (P2(x3121,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(315,plain, % 116.84/117.16 (~E(x3151,f14(f7(a1),a1))+~P5(a1,f14(f7(a1),a1))), % 116.84/117.16 inference(scs_inference,[],[282,41,312,80,73,28])). % 116.84/117.16 cnf(339,plain, % 116.84/117.16 (~P5(a1,f14(f7(a1),a1))), % 116.84/117.16 inference(equality_inference,[],[315])). % 116.84/117.16 cnf(344,plain, % 116.84/117.16 (~E(f7(a1),f14(f7(a1),a1))), % 116.84/117.16 inference(scs_inference,[],[339,99,34])). % 116.84/117.16 cnf(575,plain, % 116.84/117.16 (E(f17(x5751),f17(x5752))+~E(x5752,x5751)), % 116.84/117.16 inference(scs_inference,[],[2,13])). % 116.84/117.16 cnf(1119,plain, % 116.84/117.16 (~E(a1,x11191)+P5(a1,f7(x11191))), % 116.84/117.16 inference(scs_inference,[],[99,6,34])). % 116.84/117.16 cnf(1121,plain, % 116.84/117.16 (~P6(f7(x11211),a1)+~P2(f7(x11211),a4)+~E(a1,x11211)), % 116.84/117.16 inference(scs_inference,[],[41,80,1119,71])). % 116.84/117.16 cnf(1122,plain, % 116.84/117.16 (~P6(f7(a1),a1)+~P2(f7(a1),a4)), % 116.84/117.16 inference(equality_inference,[],[1121])). % 116.84/117.16 cnf(1123,plain, % 116.84/117.16 (~P6(f7(a1),a1)), % 116.84/117.16 inference(scs_inference,[],[41,1122])). % 116.84/117.16 cnf(2368,plain, % 116.84/117.16 (~E(x23681,x23682)+~E(x23683,x23681)+E(f17(x23683),f17(x23682))), % 116.84/117.16 inference(scs_inference,[],[13,3])). % 116.84/117.16 cnf(2371,plain, % 116.84/117.16 (P5(f8(f7(x23711)),f7(x23711))), % 116.84/117.16 inference(scs_inference,[],[153,41,55,50])). % 116.84/117.16 cnf(2389,plain, % 116.84/117.16 (~P2(f7(a1),a4)+P5(f11(f7(a1),a1),f7(a1))), % 116.84/117.16 inference(scs_inference,[],[1123,41,62])). % 116.84/117.16 cnf(2394,plain, % 116.84/117.16 (~E(x23941,f7(a1))+P5(f11(f7(a1),a1),f7(a1))), % 116.84/117.16 inference(scs_inference,[],[41,2389,28])). % 116.84/117.16 cnf(2395,plain, % 116.84/117.16 (P5(f11(f7(a1),a1),f7(a1))), % 116.84/117.16 inference(equality_inference,[],[2394])). % 116.84/117.16 cnf(2403,plain, % 116.84/117.16 (~P2(a3,a4)+~P2(a1,f19(f2(a3,a5)))), % 116.84/117.16 inference(scs_inference,[],[42,41,77])). % 116.84/117.16 cnf(2404,plain, % 116.84/117.16 (P2(x24041,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(2406,plain, % 116.84/117.16 (P5(x24061,f7(x24061))+~P5(f14(x24061,x24061),x24061)), % 116.84/117.16 inference(scs_inference,[],[42,41,2404,77,72])). % 116.84/117.16 cnf(2409,plain, % 116.84/117.16 (~P2(a1,f19(f2(a3,a5)))), % 116.84/117.16 inference(scs_inference,[],[41,2403])). % 116.84/117.16 cnf(2410,plain, % 116.84/117.16 (P2(x24101,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(2413,plain, % 116.84/117.16 (~E(a4,f19(f2(a3,a5)))), % 116.84/117.16 inference(scs_inference,[],[41,2410,2403,189,2,29])). % 116.84/117.16 cnf(2414,plain, % 116.84/117.16 (P2(x24141,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(2415,plain, % 116.84/117.16 (P2(a1,f17(f7(a1)))+~P2(f7(a1),a4)), % 116.84/117.16 inference(scs_inference,[],[99,153,41,2410,2414,2403,189,2,29,58])). % 116.84/117.16 cnf(2424,plain, % 116.84/117.16 (P2(x24241,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(2427,plain, % 116.84/117.16 (P2(x24271,a4)), % 116.84/117.16 inference(rename_variables,[],[41])). % 116.84/117.16 cnf(2428,plain, % 116.84/117.17 (P2(x24281,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2430,plain, % 116.84/117.17 (P2(f10(x24301,x24302),f6(x24302,x24301))), % 116.84/117.17 inference(scs_inference,[],[2413,339,41,2424,2428,2427,2,2415,33,69,66])). % 116.84/117.17 cnf(2432,plain, % 116.84/117.17 (P6(a1,f2(x24321,x24322))), % 116.84/117.17 inference(scs_inference,[],[2413,339,41,2424,2428,2427,2,2415,33,69,66,55])). % 116.84/117.17 cnf(2502,plain, % 116.84/117.17 (~P2(f9(x25021),a4)+P2(f9(x25021),f17(f7(x25021)))), % 116.84/117.17 inference(scs_inference,[],[182,41,65])). % 116.84/117.17 cnf(2510,plain, % 116.84/117.17 (P2(x25101,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2511,plain, % 116.84/117.17 (P5(f9(x25111),f7(x25111))+~P2(f7(x25111),a4)), % 116.84/117.17 inference(scs_inference,[],[153,41,2510,2502,59])). % 116.84/117.17 cnf(2514,plain, % 116.84/117.17 (P5(f9(x25141),f7(x25141))), % 116.84/117.17 inference(scs_inference,[],[41,2511])). % 116.84/117.17 cnf(2515,plain, % 116.84/117.17 (P2(x25151,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2516,plain, % 116.84/117.17 (~P5(a1,f11(f7(a1),a1))+~P2(f11(f7(a1),a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2395,80,41,2515,2511,73])). % 116.84/117.17 cnf(2524,plain, % 116.84/117.17 (~P5(a1,f11(f7(a1),a1))), % 116.84/117.17 inference(scs_inference,[],[41,2516])). % 116.84/117.17 cnf(2534,plain, % 116.84/117.17 (~P6(f7(x25341),a1)+~P2(f7(x25341),a4)+~P2(f9(x25341),a4)), % 116.84/117.17 inference(scs_inference,[],[2514,80,41,71])). % 116.84/117.17 cnf(2535,plain, % 116.84/117.17 (~P2(f9(x25351),a4)+~P6(f7(x25351),a1)), % 116.84/117.17 inference(scs_inference,[],[41,2534])). % 116.84/117.17 cnf(2536,plain, % 116.84/117.17 (P2(x25361,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2537,plain, % 116.84/117.17 (~P5(f7(a1),f9(f7(a1)))+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2514,270,41,2536,2534,73])). % 116.84/117.17 cnf(2541,plain, % 116.84/117.17 (~P6(f7(x25411),a1)), % 116.84/117.17 inference(scs_inference,[],[41,2535])). % 116.84/117.17 cnf(2542,plain, % 116.84/117.17 (P2(x25421,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2543,plain, % 116.84/117.17 (~P5(f7(a1),f9(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,2542,2535,2537])). % 116.84/117.17 cnf(2557,plain, % 116.84/117.17 (P5(f11(f7(x25571),a1),f7(x25571))+~P2(f7(x25571),a4)), % 116.84/117.17 inference(scs_inference,[],[2541,41,62])). % 116.84/117.17 cnf(2562,plain, % 116.84/117.17 (P5(f11(f7(x25621),a1),f7(x25621))), % 116.84/117.17 inference(scs_inference,[],[41,2557])). % 116.84/117.17 cnf(2592,plain, % 116.84/117.17 (~P2(f7(a1),a4)+~P2(a1,a4)+~P5(f7(a1),f7(f11(f7(a1),a1)))), % 116.84/117.17 inference(scs_inference,[],[2524,99,41,73])). % 116.84/117.17 cnf(2594,plain, % 116.84/117.17 (~P2(a1,a4)+~P5(f7(a1),f7(f11(f7(a1),a1)))), % 116.84/117.17 inference(scs_inference,[],[41,2592])). % 116.84/117.17 cnf(2606,plain, % 116.84/117.17 (~P5(f7(a1),f7(f11(f7(a1),a1)))), % 116.84/117.17 inference(scs_inference,[],[41,2594])). % 116.84/117.17 cnf(2749,plain, % 116.84/117.17 (P2(x27491,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2751,plain, % 116.84/117.17 (P2(x27511,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2753,plain, % 116.84/117.17 (~E(x27531,f14(f7(a1),a1))+~P2(a5,a4)+~P2(f2(a3,a5),a4)+~P2(a1,f17(f7(f2(a3,a5))))), % 116.84/117.17 inference(scs_inference,[],[42,344,2409,270,41,2749,2751,3,2,77,69])). % 116.84/117.17 cnf(2754,plain, % 116.84/117.17 (~P2(a1,f17(f7(f2(a3,a5))))+~P2(a5,a4)+~P2(f2(a3,a5),a4)), % 116.84/117.17 inference(equality_inference,[],[2753])). % 116.84/117.17 cnf(2755,plain, % 116.84/117.17 (~P2(a1,f17(f7(f2(a3,a5))))+~P2(f2(a3,a5),a4)), % 116.84/117.17 inference(scs_inference,[],[41,2754])). % 116.84/117.17 cnf(2764,plain, % 116.84/117.17 (~P2(a1,f17(f7(f2(a3,a5))))), % 116.84/117.17 inference(scs_inference,[],[41,2755])). % 116.84/117.17 cnf(2811,plain, % 116.84/117.17 (~P5(f9(a1),f9(a1))+~P2(a1,a4)), % 116.84/117.17 inference(scs_inference,[],[2514,80,41,73])). % 116.84/117.17 cnf(2813,plain, % 116.84/117.17 (P2(x28131,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2815,plain, % 116.84/117.17 (P2(x28151,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2817,plain, % 116.84/117.17 (P2(f10(x28171,x28172),f19(f2(x28172,x28171)))), % 116.84/117.17 inference(scs_inference,[],[2430,2514,80,41,2815,2813,73,76])). % 116.84/117.17 cnf(2823,plain, % 116.84/117.17 (~P5(f9(a1),f9(a1))), % 116.84/117.17 inference(scs_inference,[],[41,2811])). % 116.84/117.17 cnf(2840,plain, % 116.84/117.17 (P2(x28401,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2841,plain, % 116.84/117.17 (~P5(f9(a1),f9(f9(a1)))+~P2(f9(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2823,2432,2514,41,2840,71,73])). % 116.84/117.17 cnf(2845,plain, % 116.84/117.17 (~P5(f9(a1),f9(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,2841])). % 116.84/117.17 cnf(2861,plain, % 116.84/117.17 (~P6(f7(a1),f9(a1))+~P2(f9(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2823,2514,41,71])). % 116.84/117.17 cnf(2865,plain, % 116.84/117.17 (~P5(f11(f7(a1),f9(a1)),f9(a1))+~P2(f9(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2823,2514,41,71,280])). % 116.84/117.17 cnf(2870,plain, % 116.84/117.17 (~P6(f7(a1),f9(a1))), % 116.84/117.17 inference(scs_inference,[],[41,2861])). % 116.84/117.17 cnf(2871,plain, % 116.84/117.17 (P2(x28711,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2872,plain, % 116.84/117.17 (~P5(f11(f7(a1),f9(a1)),f9(a1))), % 116.84/117.17 inference(scs_inference,[],[41,2871,2861,2865])). % 116.84/117.17 cnf(2887,plain, % 116.84/117.17 (~P5(f7(a1),f7(f9(a1)))+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2823,2872,2514,41,33,73])). % 116.84/117.17 cnf(2892,plain, % 116.84/117.17 (~P5(f7(a1),f7(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,2887])). % 116.84/117.17 cnf(2898,plain, % 116.84/117.17 (~P5(f14(f7(a1),f9(a1)),f9(a1))+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2892,41,72])). % 116.84/117.17 cnf(2907,plain, % 116.84/117.17 (~P5(f14(f7(a1),f9(a1)),f9(a1))), % 116.84/117.17 inference(scs_inference,[],[41,2898])). % 116.84/117.17 cnf(2908,plain, % 116.84/117.17 (P2(x29081,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2909,plain, % 116.84/117.17 (~P2(f9(a1),a4)+P5(f14(f7(a1),f9(a1)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[2892,41,2908,2898,64])). % 116.84/117.17 cnf(2912,plain, % 116.84/117.17 (~P5(f7(a1),x29121)+~E(x29121,f7(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[2892,41,2908,2898,64,34])). % 116.84/117.17 cnf(2919,plain, % 116.84/117.17 (P2(x29191,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(2921,plain, % 116.84/117.17 (~P2(f7(a1),a4)+P5(f11(f7(a1),f9(a1)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[2907,2870,41,2919,2909,33,62])). % 116.84/117.17 cnf(2931,plain, % 116.84/117.17 (P5(f11(f7(a1),f9(a1)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[41,2921])). % 116.84/117.17 cnf(3230,plain, % 116.84/117.17 (P2(x32301,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(3231,plain, % 116.84/117.17 (P2(x32311,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(3232,plain, % 116.84/117.17 (~P5(f7(x32321),f7(a1))+~P2(f8(f7(x32321)),a4)), % 116.84/117.17 inference(scs_inference,[],[2371,2432,80,41,3231,3230,71,73])). % 116.84/117.17 cnf(3237,plain, % 116.84/117.17 (~P5(f7(x32371),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[41,3232])). % 116.84/117.17 cnf(3246,plain, % 116.84/117.17 (~P2(a1,a4)+P5(f14(f7(x32461),a1),f7(x32461))), % 116.84/117.17 inference(scs_inference,[],[3237,41,64])). % 116.84/117.17 cnf(3252,plain, % 116.84/117.17 (P5(f14(f7(x32521),a1),f7(x32521))), % 116.84/117.17 inference(scs_inference,[],[41,3246])). % 116.84/117.17 cnf(3347,plain, % 116.84/117.17 (~P5(f7(x33471),f14(f7(f7(a1)),a1))+~P2(f7(x33471),a4)+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[3237,3252,41,73])). % 116.84/117.17 cnf(3350,plain, % 116.84/117.17 (~P5(f7(x33501),f14(f7(f7(a1)),a1))+~P2(f7(x33501),a4)), % 116.84/117.17 inference(scs_inference,[],[41,3347])). % 116.84/117.17 cnf(3400,plain, % 116.84/117.17 (P5(x34001,f7(x34001))), % 116.84/117.17 inference(scs_inference,[],[2406,91])). % 116.84/117.17 cnf(3409,plain, % 116.84/117.17 (P2(x34091,f17(f7(x34091)))+~P2(f7(x34091),a4)), % 116.84/117.17 inference(scs_inference,[],[3400,153,41,58])). % 116.84/117.17 cnf(3414,plain, % 116.84/117.17 (P2(x34141,f17(f7(x34141)))), % 116.84/117.17 inference(scs_inference,[],[41,3409])). % 116.84/117.17 cnf(3503,plain, % 116.84/117.17 (~P6(f7(f9(a1)),f9(f9(a1)))+~P2(f9(f9(a1)),a4)+~P2(f9(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[3400,2845,41,71])). % 116.84/117.17 cnf(3506,plain, % 116.84/117.17 (~P2(f9(f9(a1)),a4)+~P6(f7(f9(a1)),f9(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,3503])). % 116.84/117.17 cnf(3510,plain, % 116.84/117.17 (~P6(f7(f9(a1)),f9(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,3506])). % 116.84/117.17 cnf(3773,plain, % 116.84/117.17 (P2(x37731,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(3776,plain, % 116.84/117.17 (~P6(f7(f7(a1)),f9(f7(a1)))+~P2(f9(f7(a1)),a4)+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[2543,2931,3400,41,3773,71])). % 116.84/117.17 cnf(3777,plain, % 116.84/117.17 (~P2(f9(f7(a1)),a4)+~P6(f7(f7(a1)),f9(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,3776])). % 116.84/117.17 cnf(3788,plain, % 116.84/117.17 (~P6(f7(f7(a1)),f9(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,3777])). % 116.84/117.17 cnf(3941,plain, % 116.84/117.17 (~P5(f7(f7(x39411)),f7(f7(a1)))+~P2(f7(x39411),a4)+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[3237,3400,41,73])). % 116.84/117.17 cnf(3943,plain, % 116.84/117.17 (~P5(f7(f7(x39431)),f7(f7(a1)))+~P2(f7(x39431),a4)), % 116.84/117.17 inference(scs_inference,[],[41,3941])). % 116.84/117.17 cnf(3974,plain, % 116.84/117.17 (~P6(f7(f7(x39741)),f7(a1))+~P2(f7(a1),a4)+~P2(f7(x39741),a4)), % 116.84/117.17 inference(scs_inference,[],[3237,3400,41,71])). % 116.84/117.17 cnf(3975,plain, % 116.84/117.17 (~P6(f7(f7(x39751)),f7(a1))+~P2(f7(x39751),a4)), % 116.84/117.17 inference(scs_inference,[],[41,3974])). % 116.84/117.17 cnf(3976,plain, % 116.84/117.17 (~P6(f7(f7(x39761)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[41,3975])). % 116.84/117.17 cnf(4056,plain, % 116.84/117.17 (P2(x40561,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(4058,plain, % 116.84/117.17 (~E(x40581,f8(f7(a1)))+~P5(a1,f8(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[2371,80,41,4056,73,28])). % 116.84/117.17 cnf(4063,plain, % 116.84/117.17 (~P5(a1,f8(f7(a1)))), % 116.84/117.17 inference(equality_inference,[],[4058])). % 116.84/117.17 cnf(4209,plain, % 116.84/117.17 (~P6(f7(a1),f8(f7(a1)))+~P2(a1,a4)+~P2(f7(a1),a4)), % 116.84/117.17 inference(scs_inference,[],[4063,3400,41,71])). % 116.84/117.17 cnf(4211,plain, % 116.84/117.17 (P2(x42111,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(4212,plain, % 116.84/117.17 (~E(x42121,f7(a1))+~P6(f7(a1),f8(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[41,4211,4209,28])). % 116.84/117.17 cnf(4218,plain, % 116.84/117.17 (~P6(f7(a1),f8(f7(a1)))), % 116.84/117.17 inference(equality_inference,[],[4212])). % 116.84/117.17 cnf(5038,plain, % 116.84/117.17 (~P5(f7(x50381),f11(f7(f7(a1)),a1))+~P2(f7(a1),a4)+~P2(f7(x50381),a4)), % 116.84/117.17 inference(scs_inference,[],[3237,2562,41,73])). % 116.84/117.17 cnf(5040,plain, % 116.84/117.17 (~P5(f7(x50401),f11(f7(f7(a1)),a1))+~P2(f7(x50401),a4)), % 116.84/117.17 inference(scs_inference,[],[41,5038])). % 116.84/117.17 cnf(5187,plain, % 116.84/117.17 (P2(x51871,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5193,plain, % 116.84/117.17 (P6(x51931,x51931)), % 116.84/117.17 inference(rename_variables,[],[78])). % 116.84/117.17 cnf(5198,plain, % 116.84/117.17 (~E(f7(f7(a1)),f7(f9(a1)))), % 116.84/117.17 inference(scs_inference,[],[3510,3788,2606,3976,2562,78,5193,3400,41,290,294,5040,280,117,116,36,35,33,2912])). % 116.84/117.17 cnf(5199,plain, % 116.84/117.17 (P5(x51991,f7(x51991))), % 116.84/117.17 inference(rename_variables,[],[3400])). % 116.84/117.17 cnf(5200,plain, % 116.84/117.17 (~P5(f7(f7(x52001)),f7(f7(a1)))), % 116.84/117.17 inference(scs_inference,[],[3510,3788,2606,3976,2562,78,5193,3400,41,5187,290,294,5040,280,117,116,36,35,33,2912,3943])). % 116.84/117.17 cnf(5201,plain, % 116.84/117.17 (P2(x52011,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5209,plain, % 116.84/117.17 (~E(f17(f7(a1)),f17(f7(f2(a3,a5))))), % 116.84/117.17 inference(scs_inference,[],[3510,3788,2764,2606,3414,3976,2562,78,5193,3400,5199,41,5187,5201,290,294,5040,280,117,116,36,35,33,2912,3943,3350,2,295,34,29])). % 116.84/117.17 cnf(5211,plain, % 116.84/117.17 (~E(f7(f2(a3,a5)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[3510,3788,2764,2606,3414,3976,2562,78,5193,3400,5199,41,5187,5201,290,294,5040,280,117,116,36,35,33,2912,3943,3350,2,295,34,29,575])). % 116.84/117.17 cnf(5220,plain, % 116.84/117.17 (~P5(f7(f7(x52201)),f7(f7(a1)))), % 116.84/117.17 inference(rename_variables,[],[5200])). % 116.84/117.17 cnf(5221,plain, % 116.84/117.17 (P2(x52211,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5222,plain, % 116.84/117.17 (~P1(f7(x52221))), % 116.84/117.17 inference(rename_variables,[],[153])). % 116.84/117.17 cnf(5223,plain, % 116.84/117.17 (P2(x52231,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5226,plain, % 116.84/117.17 (P2(x52261,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5227,plain, % 116.84/117.17 (~P5(f7(f7(x52271)),f7(f7(a1)))), % 116.84/117.17 inference(rename_variables,[],[5200])). % 116.84/117.17 cnf(5230,plain, % 116.84/117.17 (P2(x52301,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5234,plain, % 116.84/117.17 (P2(x52341,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5235,plain, % 116.84/117.17 (P2(x52351,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5238,plain, % 116.84/117.17 (P2(x52381,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5239,plain, % 116.84/117.17 (P2(x52391,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5241,plain, % 116.84/117.17 (~P5(f14(f7(f7(x52411)),f7(a1)),f7(a1))), % 116.84/117.17 inference(scs_inference,[],[2817,5211,5200,5220,5227,5209,4218,153,3400,41,5223,5226,5235,5238,5221,5230,5234,5239,280,2,59,73,2368,75,62,72])). % 116.84/117.17 cnf(5242,plain, % 116.84/117.17 (P2(x52421,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5243,plain, % 116.84/117.17 (P2(x52431,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5246,plain, % 116.84/117.17 (P2(x52461,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5247,plain, % 116.84/117.17 (P2(x52471,a4)), % 116.84/117.17 inference(rename_variables,[],[41])). % 116.84/117.17 cnf(5249,plain, % 116.84/117.17 (~P5(a1,f7(f2(a3,a5)))), % 116.84/117.17 inference(scs_inference,[],[2817,5211,5200,5220,5227,5209,4218,2764,153,5222,3400,41,5223,5226,5235,5238,5242,5246,5221,5230,5234,5239,5243,5247,280,2,59,73,2368,75,62,72,65,58])). % 116.84/117.17 cnf(5266,plain, % 116.84/117.17 (~P2(f2(a3,a5),a4)), % 116.84/117.17 inference(scs_inference,[],[5249,5241,5198,3788,80,41,104,280,2,64])). % 116.84/117.17 cnf(5320,plain, % 116.84/117.17 ($false), % 116.84/117.17 inference(scs_inference,[],[5266,41]), % 116.84/117.17 ['proof']). % 116.84/117.17 % SZS output end Proof % 116.84/117.17 % Total time :116.140000s %------------------------------------------------------------------------------