%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET647+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 : n001.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:07 EDT 2024 % Result : Theorem 247.69s 247.81s % Output : CNFRefutation 247.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SET647+3 : TPTP v8.2.0. Released v2.2.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n001.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 12:33:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 247.66/247.78 %------------------------------------------- % 247.66/247.78 % File :CSE---1.7 % 247.66/247.78 % Problem :theBenchmark % 247.66/247.78 % Transform :cnf % 247.66/247.78 % Format :tptp:raw % 247.66/247.78 % Command :java -jar mcs_scs.jar %d %s % 247.66/247.78 % 247.66/247.78 % Result :Theorem 247.010000s % 247.66/247.78 % Output :CNFRefutation 247.010000s % 247.66/247.78 %------------------------------------------- % 247.66/247.80 %------------------------------------------------------------------------------ % 247.66/247.80 % File : SET647+3 : TPTP v8.2.0. Released v2.2.0. % 247.66/247.80 % Domain : Set Theory (Relations) % 247.66/247.80 % Problem : Domain of R (X to Y) a subset of X => R is (X to range of R) % 247.66/247.80 % Version : [Wor90] axioms : Reduced > Incomplete. % 247.66/247.80 % English : If the domain of a relation R from X to Y is a subset of X, % 247.66/247.80 % R is a relation from X to the range of R. % 247.66/247.80 % 247.66/247.80 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 247.66/247.80 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 247.66/247.80 % Source : [ILF] % 247.66/247.80 % Names : RELSET_1 (9) [Wor90] % 247.66/247.80 % 247.66/247.80 % Status : Theorem % 247.66/247.80 % Rating : 0.39 v8.1.0, 0.44 v7.5.0, 0.41 v7.4.0, 0.33 v7.3.0, 0.41 v7.2.0, 0.38 v7.1.0, 0.30 v7.0.0, 0.40 v6.4.0, 0.38 v6.3.0, 0.42 v6.2.0, 0.48 v6.1.0, 0.63 v6.0.0, 0.57 v5.5.0, 0.56 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.45 v5.1.0, 0.38 v4.1.0, 0.48 v4.0.1, 0.52 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.42 v3.4.0, 0.37 v3.3.0, 0.36 v3.2.0, 0.45 v3.1.0, 0.56 v2.7.0, 0.50 v2.6.0, 0.43 v2.5.0, 0.38 v2.4.0, 0.75 v2.3.0, 0.67 v2.2.1 % 247.66/247.80 % Syntax : Number of formulae : 27 ( 2 unt; 0 def) % 247.66/247.80 % Number of atoms : 102 ( 1 equ) % 247.66/247.80 % Maximal formula atoms : 7 ( 3 avg) % 247.66/247.80 % Number of connectives : 79 ( 4 ~; 0 |; 12 &) % 247.66/247.80 % ( 9 <=>; 54 =>; 0 <=; 0 <~>) % 247.66/247.80 % Maximal formula depth : 11 ( 6 avg) % 247.66/247.80 % Maximal term depth : 3 ( 1 avg) % 247.66/247.80 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 247.66/247.80 % Number of functors : 10 ( 10 usr; 2 con; 0-2 aty) % 247.66/247.80 % Number of variables : 57 ( 49 !; 8 ?) % 247.66/247.80 % SPC : FOF_THM_RFO_SEQ % 247.66/247.80 % 247.66/247.80 % Comments : % 247.66/247.80 %------------------------------------------------------------------------------ % 247.66/247.80 %---- line(boole - th(29),1909428) % 247.66/247.80 fof(p1,axiom, % 247.66/247.80 ! [B] : % 247.66/247.80 ( ilf_type(B,set_type) % 247.66/247.80 => ! [C] : % 247.66/247.80 ( ilf_type(C,set_type) % 247.66/247.80 => ! [D] : % 247.66/247.80 ( ilf_type(D,set_type) % 247.66/247.80 => ( ( subset(B,C) % 247.66/247.80 & subset(C,D) ) % 247.66/247.80 => subset(B,D) ) ) ) ) ). % 247.66/247.80 % 247.66/247.80 %---- line(relat_1 - th(21),1917997) % 247.66/247.80 fof(p2,axiom, % 247.66/247.80 ! [B] : % 247.66/247.80 ( ilf_type(B,binary_relation_type) % 247.66/247.80 => subset(B,cross_product(domain_of(B),range_of(B))) ) ). % 247.66/247.80 % 247.66/247.80 %---- line(zfmisc_1 - th(118),1905443) % 247.66/247.80 fof(p3,axiom, % 247.66/247.80 ! [B] : % 247.66/247.80 ( ilf_type(B,set_type) % 247.66/247.80 => ! [C] : % 247.66/247.80 ( ilf_type(C,set_type) % 247.66/247.80 => ! [D] : % 247.66/247.80 ( ilf_type(D,set_type) % 247.66/247.80 => ( subset(B,C) % 247.66/247.80 => ( subset(cross_product(B,D),cross_product(C,D)) % 247.66/247.80 & subset(cross_product(D,B),cross_product(D,C)) ) ) ) ) ) ). % 247.66/247.80 % 247.69/247.80 %---- line(relset_1 - df(1),1916080) % 247.69/247.80 fof(p4,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ( ! [D] : % 247.69/247.80 ( ilf_type(D,subset_type(cross_product(B,C))) % 247.69/247.80 => ilf_type(D,relation_type(B,C)) ) % 247.69/247.80 & ! [E] : % 247.69/247.80 ( ilf_type(E,relation_type(B,C)) % 247.69/247.80 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 247.69/247.80 fof(p5,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- line(relat_1 - df(4),1917872) % 247.69/247.80 fof(p6,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,binary_relation_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ( member(C,domain_of(B)) % 247.69/247.80 <=> ? [D] : % 247.69/247.80 ( ilf_type(D,set_type) % 247.69/247.80 & member(ordered_pair(C,D),B) ) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- declaration(line(relat_1 - df(4),1917872)) % 247.69/247.80 fof(p7,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,binary_relation_type) % 247.69/247.80 => ilf_type(domain_of(B),set_type) ) ). % 247.69/247.80 % 247.69/247.80 %---- line(relat_1 - df(5),1917958) % 247.69/247.80 fof(p8,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,binary_relation_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ( member(C,range_of(B)) % 247.69/247.80 <=> ? [D] : % 247.69/247.80 ( ilf_type(D,set_type) % 247.69/247.80 & member(ordered_pair(D,C),B) ) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- declaration(line(relat_1 - df(5),1917958)) % 247.69/247.80 fof(p9,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,binary_relation_type) % 247.69/247.80 => ilf_type(range_of(B),set_type) ) ). % 247.69/247.80 % 247.69/247.80 %---- line(relat_1 - axiom61,1917641) % 247.69/247.80 fof(p10,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ( ilf_type(B,binary_relation_type) % 247.69/247.80 <=> ( relation_like(B) % 247.69/247.80 & ilf_type(B,set_type) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- type_nonempty(line(relat_1 - axiom61,1917641)) % 247.69/247.80 fof(p11,axiom, % 247.69/247.80 ? [B] : ilf_type(B,binary_relation_type) ). % 247.69/247.80 % 247.69/247.80 %---- line(tarski - df(3),1832749) % 247.69/247.80 fof(p12,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ( subset(B,C) % 247.69/247.80 <=> ! [D] : % 247.69/247.80 ( ilf_type(D,set_type) % 247.69/247.80 => ( member(D,B) % 247.69/247.80 => member(D,C) ) ) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- declaration(op(cross_product,2,function)) % 247.69/247.80 fof(p13,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ilf_type(cross_product(B,C),set_type) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- declaration(op(ordered_pair,2,function)) % 247.69/247.80 fof(p14,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- line(hidden - axiom62,1832648) % 247.69/247.80 fof(p15,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ! [C] : % 247.69/247.80 ( ilf_type(C,set_type) % 247.69/247.80 => ( ilf_type(C,subset_type(B)) % 247.69/247.80 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 247.69/247.80 % 247.69/247.80 %---- type_nonempty(line(hidden - axiom62,1832648)) % 247.69/247.80 fof(p16,axiom, % 247.69/247.80 ! [B] : % 247.69/247.80 ( ilf_type(B,set_type) % 247.69/247.80 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 247.69/247.80 % 247.69/247.81 %---- property(reflexivity,op(subset,2,predicate)) % 247.69/247.81 fof(p17,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => subset(B,B) ) ). % 247.69/247.81 % 247.69/247.81 %---- line(relat_1 - df(1),1917627) % 247.69/247.81 fof(p18,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ( relation_like(B) % 247.69/247.81 <=> ! [C] : % 247.69/247.81 ( ilf_type(C,set_type) % 247.69/247.81 => ( member(C,B) % 247.69/247.81 => ? [D] : % 247.69/247.81 ( ilf_type(D,set_type) % 247.69/247.81 & ? [E] : % 247.69/247.81 ( ilf_type(E,set_type) % 247.69/247.81 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- conditional_cluster(axiom65,relation_like) % 247.69/247.81 fof(p19,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ! [C] : % 247.69/247.81 ( ilf_type(C,set_type) % 247.69/247.81 => ! [D] : % 247.69/247.81 ( ilf_type(D,subset_type(cross_product(B,C))) % 247.69/247.81 => relation_like(D) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- line(hidden - axiom66,1832644) % 247.69/247.81 fof(p20,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ! [C] : % 247.69/247.81 ( ilf_type(C,set_type) % 247.69/247.81 => ( member(B,power_set(C)) % 247.69/247.81 <=> ! [D] : % 247.69/247.81 ( ilf_type(D,set_type) % 247.69/247.81 => ( member(D,B) % 247.69/247.81 => member(D,C) ) ) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- declaration(line(hidden - axiom66,1832644)) % 247.69/247.81 fof(p21,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ( ~ empty(power_set(B)) % 247.69/247.81 & ilf_type(power_set(B),set_type) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- line(hidden - axiom67,1832640) % 247.69/247.81 fof(p22,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ! [C] : % 247.69/247.81 ( ( ~ empty(C) % 247.69/247.81 & ilf_type(C,set_type) ) % 247.69/247.81 => ( ilf_type(B,member_type(C)) % 247.69/247.81 <=> member(B,C) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- type_nonempty(line(hidden - axiom67,1832640)) % 247.69/247.81 fof(p23,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ( ~ empty(B) % 247.69/247.81 & ilf_type(B,set_type) ) % 247.69/247.81 => ? [C] : ilf_type(C,member_type(B)) ) ). % 247.69/247.81 % 247.69/247.81 %---- line(hidden - axiom68,1832628) % 247.69/247.81 fof(p24,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ( empty(B) % 247.69/247.81 <=> ! [C] : % 247.69/247.81 ( ilf_type(C,set_type) % 247.69/247.81 => ~ member(C,B) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %---- conditional_cluster(axiom69,empty) % 247.69/247.81 fof(p25,axiom, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ( empty(B) % 247.69/247.81 & ilf_type(B,set_type) ) % 247.69/247.81 => relation_like(B) ) ). % 247.69/247.81 % 247.69/247.81 %---- declaration(set) % 247.69/247.81 fof(p26,axiom, % 247.69/247.81 ! [B] : ilf_type(B,set_type) ). % 247.69/247.81 % 247.69/247.81 %---- line(relset_1 - th(9),1916152) % 247.69/247.81 fof(prove_relset_1_9,conjecture, % 247.69/247.81 ! [B] : % 247.69/247.81 ( ilf_type(B,set_type) % 247.69/247.81 => ! [C] : % 247.69/247.81 ( ilf_type(C,binary_relation_type) % 247.69/247.81 => ( subset(domain_of(C),B) % 247.69/247.81 => ilf_type(C,relation_type(B,range_of(C))) ) ) ) ). % 247.69/247.81 % 247.69/247.81 %------------------------------------------------------------------------------ % 247.69/247.81 %------------------------------------------- % 247.69/247.81 % Proof found % 247.69/247.81 % SZS status Theorem for theBenchmark % 247.69/247.81 % SZS output start Proof % 247.69/247.81 %ClaNum:93(EqnAxiom:40) % 247.69/247.81 %VarNum:215(SingletonVarNum:70) % 247.69/247.81 %MaxLitNum:6 % 247.69/247.81 %MaxfuncDepth:2 % 247.69/247.81 %SharedTerms:13 % 247.69/247.81 %goalClause: 43 45 46 % 247.69/247.81 %singleGoalClaCount:3 % 247.69/247.81 [41]P1(a1,a2) % 247.69/247.81 [43]P1(a9,a2) % 247.69/247.81 [45]P3(f4(a9),a3) % 247.69/247.81 [46]~P1(a9,f23(a3,f14(a9))) % 247.69/247.81 [44]P1(x441,a13) % 247.69/247.81 [48]P3(x481,x481)+~P1(x481,a13) % 247.69/247.81 [49]~P1(x491,a13)+~P2(f15(x491)) % 247.69/247.81 [59]~P1(x591,a13)+P1(f17(x591),f24(x591)) % 247.69/247.81 [64]~P1(x641,a2)+P3(x641,f5(f4(x641),f14(x641))) % 247.69/247.81 [47]~P2(x471)+P4(x471)+~P1(x471,a13) % 247.69/247.81 [53]~P4(x531)+~P1(x531,a13)+P1(x531,a2) % 247.69/247.81 [56]P4(x561)+~P1(x561,a13)+~P1(x561,a2) % 247.69/247.81 [57]P4(x571)+P5(f16(x571),x571)+~P1(x571,a13) % 247.69/247.81 [58]P2(x581)+P5(f6(x581),x581)+~P1(x581,a13) % 247.69/247.81 [60]P2(x601)+P1(f7(x601),f21(x601))+~P1(x601,a13) % 247.69/247.81 [73]~P1(x732,a13)+~P1(x731,a13)+P1(f10(x731,x732),f23(x732,x731)) % 247.69/247.81 [61]~P2(x611)+~P5(x612,x611)+~P1(x612,a13)+~P1(x611,a13) % 247.69/247.81 [69]P3(x691,x692)+P5(f18(x691,x692),x691)+~P1(x692,a13)+~P1(x691,a13) % 247.69/247.81 [71]P5(f8(x711,x712),x711)+~P1(x712,a13)+~P1(x711,a13)+P5(x711,f15(x712)) % 247.69/247.81 [79]P3(x791,x792)+~P1(x792,a13)+~P1(x791,a13)+~P5(f18(x791,x792),x792) % 247.69/247.81 [82]~P1(x822,a13)+~P1(x821,a13)+~P5(f8(x821,x822),x822)+P5(x821,f15(x822)) % 247.69/247.81 [72]~P1(x722,a13)+~P1(x721,a13)+~P1(x721,f24(x722))+P1(x721,f21(f15(x722))) % 247.69/247.81 [78]~P1(x782,a13)+~P1(x781,a13)+P1(x781,f24(x782))+~P1(x781,f21(f15(x782))) % 247.69/247.81 [90]~P1(x902,a2)+~P1(x901,a13)+~P5(x901,f4(x902))+P5(f22(x901,f11(x902,x901)),x902) % 247.69/247.81 [91]~P1(x912,a13)+~P1(x911,a2)+~P5(x912,f14(x911))+P5(f22(f12(x911,x912),x912),x911) % 247.69/247.81 [89]P4(x891)+~P1(x892,a13)+~P1(x893,a13)+~P1(x891,f24(f5(x893,x892))) % 247.69/247.81 [92]~P1(x923,a13)+~P1(x922,a13)+~P1(x921,f23(x922,x923))+P1(x921,f24(f5(x922,x923))) % 247.69/247.81 [93]~P1(x933,a13)+~P1(x932,a13)+P1(x931,f23(x932,x933))+~P1(x931,f24(f5(x932,x933))) % 247.69/247.81 [65]~P5(x652,x651)+P2(x651)+~P1(x651,a13)+~P1(x652,a13)+P1(x652,f21(x651)) % 247.69/247.81 [66]P2(x661)+P5(x662,x661)+~P1(x661,a13)+~P1(x662,a13)+~P1(x662,f21(x661)) % 247.69/247.81 [84]~P4(x841)+~P5(x842,x841)+~P1(x841,a13)+~P1(x842,a13)+E(f22(f19(x841,x842),f20(x841,x842)),x842) % 247.69/247.81 [68]P4(x681)+~P1(x681,a13)+~P1(x683,a13)+~P1(x682,a13)+~E(f16(x681),f22(x682,x683)) % 247.69/247.81 [85]~P1(x852,a2)+~P1(x851,a13)+~P5(f22(x851,x853),x852)+P5(x851,f4(x852))+~P1(x853,a13) % 247.69/247.81 [86]~P1(x862,a2)+~P1(x861,a13)+~P5(f22(x863,x861),x862)+P5(x861,f14(x862))+~P1(x863,a13) % 247.69/247.81 [87]~P3(x871,x873)+~P1(x873,a13)+~P1(x872,a13)+~P1(x871,a13)+P3(f5(x871,x872),f5(x873,x872)) % 247.69/247.81 [88]~P3(x882,x883)+~P1(x883,a13)+~P1(x882,a13)+~P1(x881,a13)+P3(f5(x881,x882),f5(x881,x883)) % 247.69/247.81 [80]~P3(x801,x803)+P3(x801,x802)+~P3(x803,x802)+~P1(x802,a13)+~P1(x803,a13)+~P1(x801,a13) % 247.69/247.81 [81]~P5(x811,x813)+P5(x811,x812)+~P3(x813,x812)+~P1(x811,a13)+~P1(x812,a13)+~P1(x813,a13) % 247.69/247.81 [83]P5(x831,x832)+~P5(x831,x833)+~P1(x831,a13)+~P1(x832,a13)+~P1(x833,a13)+~P5(x833,f15(x832)) % 247.69/247.81 %EqnAxiom % 247.69/247.81 [1]E(x11,x11) % 247.69/247.81 [2]E(x22,x21)+~E(x21,x22) % 247.69/247.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 247.69/247.81 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 247.69/247.81 [5]~E(x51,x52)+E(f14(x51),f14(x52)) % 247.69/247.81 [6]~E(x61,x62)+E(f23(x61,x63),f23(x62,x63)) % 247.69/247.81 [7]~E(x71,x72)+E(f23(x73,x71),f23(x73,x72)) % 247.69/247.81 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 247.69/247.81 [9]~E(x91,x92)+E(f24(x91),f24(x92)) % 247.69/247.81 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 247.69/247.81 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 247.69/247.81 [12]~E(x121,x122)+E(f19(x121,x123),f19(x122,x123)) % 247.69/247.81 [13]~E(x131,x132)+E(f19(x133,x131),f19(x133,x132)) % 247.69/247.81 [14]~E(x141,x142)+E(f16(x141),f16(x142)) % 247.69/247.81 [15]~E(x151,x152)+E(f6(x151),f6(x152)) % 247.69/247.81 [16]~E(x161,x162)+E(f11(x161,x163),f11(x162,x163)) % 247.69/247.81 [17]~E(x171,x172)+E(f11(x173,x171),f11(x173,x172)) % 247.69/247.81 [18]~E(x181,x182)+E(f20(x181,x183),f20(x182,x183)) % 247.69/247.81 [19]~E(x191,x192)+E(f20(x193,x191),f20(x193,x192)) % 247.69/247.81 [20]~E(x201,x202)+E(f17(x201),f17(x202)) % 247.69/247.81 [21]~E(x211,x212)+E(f22(x211,x213),f22(x212,x213)) % 247.69/247.81 [22]~E(x221,x222)+E(f22(x223,x221),f22(x223,x222)) % 247.69/247.81 [23]~E(x231,x232)+E(f7(x231),f7(x232)) % 247.69/247.81 [24]~E(x241,x242)+E(f21(x241),f21(x242)) % 247.69/247.81 [25]~E(x251,x252)+E(f8(x251,x253),f8(x252,x253)) % 247.69/247.81 [26]~E(x261,x262)+E(f8(x263,x261),f8(x263,x262)) % 247.69/247.81 [27]~E(x271,x272)+E(f10(x271,x273),f10(x272,x273)) % 247.69/247.81 [28]~E(x281,x282)+E(f10(x283,x281),f10(x283,x282)) % 247.69/247.81 [29]~E(x291,x292)+E(f12(x291,x293),f12(x292,x293)) % 247.69/247.81 [30]~E(x301,x302)+E(f12(x303,x301),f12(x303,x302)) % 247.69/247.81 [31]~E(x311,x312)+E(f18(x311,x313),f18(x312,x313)) % 247.69/247.81 [32]~E(x321,x322)+E(f18(x323,x321),f18(x323,x322)) % 247.69/247.81 [33]P1(x332,x333)+~E(x331,x332)+~P1(x331,x333) % 247.69/247.81 [34]P1(x343,x342)+~E(x341,x342)+~P1(x343,x341) % 247.69/247.81 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353) % 247.69/247.81 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361) % 247.69/247.81 [37]P3(x372,x373)+~E(x371,x372)+~P3(x371,x373) % 247.69/247.81 [38]P3(x383,x382)+~E(x381,x382)+~P3(x383,x381) % 247.69/247.81 [39]~P4(x391)+P4(x392)+~E(x391,x392) % 247.69/247.81 [40]~P2(x401)+P2(x402)+~E(x401,x402) % 247.69/247.81 % 247.69/247.81 %------------------------------------------- % 247.74/247.87 cnf(96,plain, % 247.74/247.87 (P4(a9)), % 247.74/247.87 inference(scs_inference,[],[43,44,48,56])). % 247.74/247.87 cnf(97,plain, % 247.74/247.87 (P1(x971,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(101,plain, % 247.74/247.87 (P3(x1011,a3)+~E(f4(a9),x1011)), % 247.74/247.87 inference(scs_inference,[],[43,45,46,44,48,56,34,33,37])). % 247.74/247.87 cnf(107,plain, % 247.74/247.87 (P5(x1071,f15(x1071))+P5(f8(x1071,x1071),x1071)), % 247.74/247.87 inference(scs_inference,[],[43,45,46,44,97,48,56,34,33,37,38,47,61,71])). % 247.74/247.87 cnf(114,plain, % 247.74/247.87 (P1(x1141,a2)+~E(a1,x1141)), % 247.74/247.87 inference(scs_inference,[],[46,41,44,34,33])). % 247.74/247.87 cnf(1809,plain, % 247.74/247.87 (P1(x18091,f24(x18092))+~E(f17(x18092),x18091)), % 247.74/247.87 inference(scs_inference,[],[44,59,33])). % 247.74/247.87 cnf(1810,plain, % 247.74/247.87 (P1(f17(x18101),f24(x18101))), % 247.74/247.87 inference(equality_inference,[],[1809])). % 247.74/247.87 cnf(1811,plain, % 247.74/247.87 (P4(f17(f5(x18111,x18111)))), % 247.74/247.87 inference(scs_inference,[],[1810,44,89])). % 247.74/247.87 cnf(2342,plain, % 247.74/247.87 (P5(x23421,f15(x23421))), % 247.74/247.87 inference(scs_inference,[],[44,107,82])). % 247.74/247.87 cnf(6529,plain, % 247.74/247.87 (P3(a9,f5(f4(a9),f14(a9)))), % 247.74/247.87 inference(scs_inference,[],[44,96,64,53])). % 247.74/247.87 cnf(10016,plain, % 247.74/247.87 (P5(f16(x100161),x100161)+P1(x100161,a2)), % 247.74/247.87 inference(scs_inference,[],[44,57,53])). % 247.74/247.87 cnf(10513,plain, % 247.74/247.87 (P1(f7(f15(x105131)),f21(f15(x105131)))+~P1(x105131,a13)), % 247.74/247.87 inference(scs_inference,[],[44,60,49])). % 247.74/247.87 cnf(10514,plain, % 247.74/247.87 (P1(f7(f15(x105141)),f21(f15(x105141)))), % 247.74/247.87 inference(scs_inference,[],[44,10513])). % 247.74/247.87 cnf(10555,plain, % 247.74/247.87 (P1(f7(f15(x105551)),f24(x105551))+~P1(f7(f15(x105551)),a13)), % 247.74/247.87 inference(scs_inference,[],[44,10514,78])). % 247.74/247.87 cnf(10559,plain, % 247.74/247.87 (P1(f7(f15(x105591)),f24(x105591))), % 247.74/247.87 inference(scs_inference,[],[44,10555])). % 247.74/247.87 cnf(10568,plain, % 247.74/247.87 (P4(f7(f15(x105681)))+~E(f24(x105681),f24(f5(x105682,x105682)))), % 247.74/247.87 inference(scs_inference,[],[44,10559,34,89])). % 247.74/247.87 cnf(10574,plain, % 247.74/247.87 (P4(f7(f15(f5(x105741,x105741))))), % 247.74/247.87 inference(equality_inference,[],[10568])). % 247.74/247.87 cnf(11284,plain, % 247.74/247.87 (P1(f17(f5(x112841,x112841)),a2)), % 247.74/247.87 inference(scs_inference,[],[1811,44,53])). % 247.74/247.87 cnf(14500,plain, % 247.74/247.87 (P1(f10(x145001,x145001),f24(f5(x145001,x145001)))), % 247.74/247.87 inference(scs_inference,[],[44,73,92])). % 247.74/247.87 cnf(14501,plain, % 247.74/247.87 (P4(f10(x145011,x145011))), % 247.74/247.87 inference(scs_inference,[],[44,14500,89])). % 247.74/247.87 cnf(23092,plain, % 247.74/247.87 (P1(f10(x230921,x230921),a2)), % 247.74/247.87 inference(scs_inference,[],[14501,44,53])). % 247.74/247.87 cnf(73809,plain, % 247.74/247.87 (~E(x738091,f15(x738092))+~P2(x738091)), % 247.74/247.87 inference(scs_inference,[],[44,49,40])). % 247.74/247.87 cnf(73810,plain, % 247.74/247.87 (~P2(f15(x738101))), % 247.74/247.87 inference(equality_inference,[],[73809])). % 247.74/247.87 cnf(73846,plain, % 247.74/247.87 (~E(a1,x738461)+P3(x738461,f5(f4(x738461),f14(x738461)))), % 247.74/247.87 inference(scs_inference,[],[114,64])). % 247.74/247.87 cnf(73847,plain, % 247.74/247.87 (P3(a1,f5(f4(a1),f14(a1)))), % 247.74/247.87 inference(equality_inference,[],[73846])). % 247.74/247.87 cnf(74190,plain, % 247.74/247.87 (P1(x741901,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(74193,plain, % 247.74/247.87 (P5(f7(f15(x741931)),f15(x741931))+~E(x741932,f7(f15(x741931)))), % 247.74/247.87 inference(scs_inference,[],[73810,44,74190,10514,66,33])). % 247.74/247.87 cnf(74217,plain, % 247.74/247.87 (P5(f7(f15(x742171)),f15(x742171))), % 247.74/247.87 inference(equality_inference,[],[74193])). % 247.74/247.87 cnf(74287,plain, % 247.74/247.87 (~E(x742871,f15(x742872))+P5(f6(x742871),x742871)), % 247.74/247.87 inference(scs_inference,[],[44,73809,58])). % 247.74/247.87 cnf(74288,plain, % 247.74/247.87 (P5(f6(f15(x742881)),f15(x742881))), % 247.74/247.87 inference(equality_inference,[],[74287])). % 247.74/247.87 cnf(74315,plain, % 247.74/247.87 (~E(a9,x743151)+P3(f4(x743151),a3)), % 247.74/247.87 inference(scs_inference,[],[101,4])). % 247.74/247.87 cnf(74609,plain, % 247.74/247.87 (P1(f15(x746091),a2)+~P1(f16(f15(x746091)),a13)+P1(f16(f15(x746091)),f21(f15(x746091)))), % 247.74/247.87 inference(scs_inference,[],[44,73810,10016,65])). % 247.74/247.87 cnf(74610,plain, % 247.74/247.87 (P1(x746101,f21(f15(x746102)))+~E(f16(f15(x746102)),x746101)+P1(f15(x746102),a2)), % 247.74/247.87 inference(scs_inference,[],[44,74609,33])). % 247.74/247.87 cnf(74821,plain, % 247.74/247.87 (~P1(f4(x748211),a13)+P3(f5(f4(x748211),a3),f5(a3,a3))+~E(a9,x748211)), % 247.74/247.87 inference(scs_inference,[],[44,74315,87])). % 247.74/247.87 cnf(74822,plain, % 247.74/247.87 (P3(f5(f4(a9),a3),f5(a3,a3))+~P1(f4(a9),a13)), % 247.74/247.87 inference(equality_inference,[],[74821])). % 247.74/247.87 cnf(74823,plain, % 247.74/247.87 (P3(f5(f4(a9),a3),f5(a3,a3))), % 247.74/247.87 inference(scs_inference,[],[44,74822])). % 247.74/247.87 cnf(74825,plain, % 247.74/247.87 (~P1(f4(x748251),a13)+P3(f5(a3,f4(x748251)),f5(a3,a3))+~E(a9,x748251)), % 247.74/247.87 inference(scs_inference,[],[44,74315,88])). % 247.74/247.87 cnf(74826,plain, % 247.74/247.87 (P3(f5(a3,f4(a9)),f5(a3,a3))+~P1(f4(a9),a13)), % 247.74/247.87 inference(equality_inference,[],[74825])). % 247.74/247.87 cnf(74827,plain, % 247.74/247.87 (P3(f5(a3,f4(a9)),f5(a3,a3))), % 247.74/247.87 inference(scs_inference,[],[44,74826])). % 247.74/247.87 cnf(74931,plain, % 247.74/247.87 (P1(x749311,f24(x749311))+~P1(x749311,f21(f15(x749311)))), % 247.74/247.87 inference(scs_inference,[],[44,78])). % 247.74/247.87 cnf(74940,plain, % 247.74/247.87 (~P1(f15(x749401),a13)+P1(x749401,f21(f15(x749401)))), % 247.74/247.87 inference(scs_inference,[],[73810,2342,44,72,78,65])). % 247.74/247.87 cnf(74948,plain, % 247.74/247.87 (P1(x749481,f21(f15(x749481)))), % 247.74/247.87 inference(scs_inference,[],[44,74940])). % 247.74/247.87 cnf(74949,plain, % 247.74/247.87 (P1(x749491,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(74950,plain, % 247.74/247.87 (P1(x749501,f24(x749501))), % 247.74/247.87 inference(scs_inference,[],[44,74940,74931])). % 247.74/247.87 cnf(74952,plain, % 247.74/247.87 (~P1(x749521,a13)+P1(f17(x749521),f21(f15(x749521)))), % 247.74/247.87 inference(scs_inference,[],[1810,44,74949,74940,74931,72])). % 247.74/247.87 cnf(74960,plain, % 247.74/247.87 (P1(f17(x749601),f21(f15(x749601)))), % 247.74/247.87 inference(scs_inference,[],[44,74952])). % 247.74/247.87 cnf(74963,plain, % 247.74/247.87 (P1(x749631,f24(x749631))), % 247.74/247.87 inference(rename_variables,[],[74950])). % 247.74/247.87 cnf(74965,plain, % 247.74/247.87 (P4(f5(x749651,x749651))), % 247.74/247.87 inference(scs_inference,[],[74950,74963,44,74952,93,89])). % 247.74/247.87 cnf(74977,plain, % 247.74/247.87 (P1(f5(x749771,x749771),a2)), % 247.74/247.87 inference(scs_inference,[],[74965,44,53])). % 247.74/247.87 cnf(74985,plain, % 247.74/247.87 (P5(f17(x749851),f15(x749851))+~P1(f15(x749851),a13)), % 247.74/247.87 inference(scs_inference,[],[74960,73810,44,66])). % 247.74/247.87 cnf(74991,plain, % 247.74/247.87 (P5(f17(x749911),f15(x749911))), % 247.74/247.87 inference(scs_inference,[],[44,74985])). % 247.74/247.87 cnf(77159,plain, % 247.74/247.87 (P3(f17(f5(x771591,x771591)),f5(f4(f17(f5(x771591,x771591))),f14(f17(f5(x771591,x771591)))))), % 247.74/247.87 inference(scs_inference,[],[11284,64])). % 247.74/247.87 cnf(77161,plain, % 247.74/247.87 (P1(f7(f15(f5(x771611,x771611))),a2)), % 247.74/247.87 inference(scs_inference,[],[10574,11284,44,64,53])). % 247.74/247.87 cnf(77199,plain, % 247.74/247.87 (P3(f5(x771991,x771991),f5(f4(f5(x771991,x771991)),f14(f5(x771991,x771991))))), % 247.74/247.87 inference(scs_inference,[],[74977,64])). % 247.74/247.87 cnf(80629,plain, % 247.74/247.87 (P3(f5(f4(a9),f4(a9)),f5(f4(a9),a3))+~P1(a3,a13)), % 247.74/247.87 inference(scs_inference,[],[45,44,88])). % 247.74/247.87 cnf(80643,plain, % 247.74/247.87 (P3(f5(f4(a9),f4(a9)),f5(f4(a9),a3))), % 247.74/247.87 inference(scs_inference,[],[44,80629])). % 247.74/247.87 cnf(85292,plain, % 247.74/247.87 (P1(x852921,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(85293,plain, % 247.74/247.87 (P1(x852931,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(85295,plain, % 247.74/247.87 (P5(x852951,f15(x852952))+P5(f8(x852951,x852952),x852951)), % 247.74/247.87 inference(scs_inference,[],[6529,44,85293,85292,88,71])). % 247.74/247.87 cnf(93298,plain, % 247.74/247.87 (P1(x932981,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(93299,plain, % 247.74/247.87 (P1(x932991,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(93301,plain, % 247.74/247.87 (P3(x933011,x933012)+~P5(f18(x933011,x933012),x933012)), % 247.74/247.87 inference(scs_inference,[],[73847,44,93299,93298,88,79])). % 247.74/247.87 cnf(95453,plain, % 247.74/247.87 (P5(x954531,f4(f15(f22(x954531,x954531))))+~P1(f15(f22(x954531,x954531)),a2)), % 247.74/247.87 inference(scs_inference,[],[44,2342,85])). % 247.74/247.87 cnf(95472,plain, % 247.74/247.87 (P5(x954721,x954722)+~E(f4(f15(f22(x954721,x954721))),x954722)+~P1(f15(f22(x954721,x954721)),a2)), % 247.74/247.87 inference(scs_inference,[],[95453,36])). % 247.74/247.87 cnf(96185,plain, % 247.74/247.87 (P3(f10(x961851,x961851),f5(f4(f10(x961851,x961851)),f14(f10(x961851,x961851))))), % 247.74/247.87 inference(scs_inference,[],[23092,64])). % 247.74/247.87 cnf(97828,plain, % 247.74/247.87 (~P1(a3,a13)+~P1(a9,f24(f5(a3,f14(a9))))), % 247.74/247.87 inference(scs_inference,[],[44,46,93])). % 247.74/247.87 cnf(97839,plain, % 247.74/247.87 (~P1(a9,f24(f5(a3,f14(a9))))), % 247.74/247.87 inference(scs_inference,[],[44,97828])). % 247.74/247.87 cnf(97840,plain, % 247.74/247.87 (P1(x978401,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(97843,plain, % 247.74/247.87 (~E(a13,f24(f5(a3,f14(a9))))), % 247.74/247.87 inference(scs_inference,[],[44,97840,1810,97828,33,34])). % 247.74/247.87 cnf(97890,plain, % 247.74/247.87 (P1(x978901,a13)), % 247.74/247.87 inference(rename_variables,[],[44])). % 247.74/247.87 cnf(97892,plain, % 247.74/247.87 (~E(x978921,a9)+~P1(a9,f21(f15(f5(a3,f14(a9)))))), % 247.74/247.87 inference(scs_inference,[],[44,97890,97839,78,33])). % 247.74/247.87 cnf(97895,plain, % 247.74/247.87 (~P1(a9,f21(f15(f5(a3,f14(a9)))))), % 247.74/247.87 inference(equality_inference,[],[97892])). % 247.74/247.87 cnf(97898,plain, % 247.74/247.87 (~E(a13,f21(f15(f5(a3,f14(a9)))))), % 247.74/247.87 inference(scs_inference,[],[44,10514,97895,33,34])). % 247.74/247.87 cnf(97911,plain, % 247.74/247.87 (~E(f21(f15(f5(a3,f14(a9)))),a13)), % 247.74/247.87 inference(scs_inference,[],[97898,2])). % 247.74/247.87 cnf(97937,plain, % 247.74/247.87 (P1(f6(f15(x979371)),f21(f15(x979371)))+~P1(f6(f15(x979371)),a13)), % 247.74/247.87 inference(scs_inference,[],[74288,44,73810,65])). % 247.74/247.87 cnf(97951,plain, % 247.74/247.87 (P1(f6(f15(x979511)),f21(f15(x979511)))), % 247.74/247.87 inference(scs_inference,[],[44,97937])). % 247.74/247.87 cnf(101115,plain, % 247.74/247.88 (P1(x1011151,f21(f15(x1011152)))+~E(f6(f15(x1011152)),x1011151)), % 247.74/247.88 inference(scs_inference,[],[97951,33])). % 247.74/247.88 cnf(101130,plain, % 247.74/247.88 (P3(f5(f4(a9),f4(a9)),f5(a3,a3))+~P1(f5(f4(a9),f4(a9)),a13)+~P1(f5(a3,a3),a13)), % 247.74/247.88 inference(scs_inference,[],[44,80643,74823,80])). % 247.74/247.88 cnf(101134,plain, % 247.74/247.88 (~P1(f5(a3,a3),a13)+P3(f5(f4(a9),f4(a9)),f5(a3,a3))), % 247.74/247.88 inference(scs_inference,[],[44,101130])). % 247.74/247.88 cnf(101135,plain, % 247.74/247.88 (P3(f5(f4(a9),f4(a9)),f5(a3,a3))), % 247.74/247.88 inference(scs_inference,[],[44,101134])). % 247.74/247.88 cnf(101326,plain, % 247.74/247.88 (P3(f5(f4(a9),f4(a9)),f5(a3,f4(a9)))+~P1(a3,a13)), % 247.74/247.88 inference(scs_inference,[],[45,101135,44,37,38,87])). % 247.74/247.88 cnf(101343,plain, % 247.74/247.88 (P3(x1013431,f5(a3,f4(a9)))+~E(f5(f4(a9),f4(a9)),x1013431)), % 247.74/247.88 inference(scs_inference,[],[44,101326,37])). % 247.74/247.88 cnf(101344,plain, % 247.74/247.88 (P3(f5(f4(a9),f4(a9)),f5(a3,f4(a9)))), % 247.74/247.88 inference(equality_inference,[],[101343])). % 247.74/247.88 cnf(101346,plain, % 247.74/247.88 (P3(x1013461,x1013462)+~E(f5(a3,f4(a9)),x1013462)+~E(f5(f4(a9),f4(a9)),x1013461)), % 247.74/247.88 inference(scs_inference,[],[101344,38,37])). % 247.74/247.88 cnf(101442,plain, % 247.74/247.88 (~E(a2,f21(f15(f5(a3,f14(a9)))))), % 247.74/247.88 inference(scs_inference,[],[43,97895,77161,101115,64,2,34])). % 247.74/247.88 cnf(101448,plain, % 247.74/247.88 (~P1(f10(x1014481,x1014481),a13)+P1(f10(x1014481,x1014481),f21(f15(f5(x1014481,x1014481))))), % 247.74/247.88 inference(scs_inference,[],[43,44,97895,77161,14500,97898,101115,64,2,34,74610,3,37,38,72])). % 247.74/247.88 cnf(101454,plain, % 247.74/247.88 (~E(f21(f15(f5(a3,f14(a9)))),a2)), % 247.74/247.88 inference(scs_inference,[],[101442,2])). % 247.74/247.88 cnf(101455,plain, % 247.74/247.88 (~E(a2,f24(f5(a3,f14(a9))))), % 247.74/247.88 inference(scs_inference,[],[43,97839,101442,2,34])). % 247.74/247.88 cnf(101458,plain, % 247.74/247.88 (P1(x1014581,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101459,plain, % 247.74/247.88 (P1(x1014591,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101461,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(a3,a3)))), % 247.74/247.88 inference(scs_inference,[],[43,44,101459,101458,74823,1811,97843,97839,101442,2,34,3,84,88])). % 247.74/247.88 cnf(101462,plain, % 247.74/247.88 (P1(x1014621,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101463,plain, % 247.74/247.88 (P1(x1014631,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101466,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(a3,a3),f5(f4(a9),a3)))), % 247.74/247.88 inference(scs_inference,[],[43,44,101459,101463,101462,101458,74823,1811,97843,97839,101442,2,34,3,84,88,87])). % 247.74/247.88 cnf(101482,plain, % 247.74/247.88 (~E(f24(f5(a3,f14(a9))),a2)), % 247.74/247.88 inference(scs_inference,[],[101455,2])). % 247.74/247.88 cnf(101487,plain, % 247.74/247.88 (P1(x1014871,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101488,plain, % 247.74/247.88 (P1(x1014881,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101490,plain, % 247.74/247.88 (P3(f5(f5(a3,f4(a9)),f5(a3,f4(a9))),f5(f5(a3,f4(a9)),f5(a3,a3)))), % 247.74/247.88 inference(scs_inference,[],[44,101488,101487,74827,10574,101442,101455,101461,2,3,37,38,84,88])). % 247.74/247.88 cnf(101491,plain, % 247.74/247.88 (P1(x1014911,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101492,plain, % 247.74/247.88 (P1(x1014921,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101495,plain, % 247.74/247.88 (P3(f5(f5(a3,f4(a9)),f5(a3,f4(a9))),f5(f5(a3,a3),f5(a3,f4(a9))))), % 247.74/247.88 inference(scs_inference,[],[44,101488,101492,101491,101487,74827,10574,101442,101455,101461,2,3,37,38,84,88,87])). % 247.74/247.88 cnf(101530,plain, % 247.74/247.88 (P3(f5(f17(f5(x1015301,x1015301)),f17(f5(x1015301,x1015301))),f5(f17(f5(x1015301,x1015301)),f5(f4(f17(f5(x1015301,x1015301))),f14(f17(f5(x1015301,x1015301))))))+~P1(f5(f4(f17(f5(x1015301,x1015301))),f14(f17(f5(x1015301,x1015301)))),a13)), % 247.74/247.88 inference(scs_inference,[],[44,77159,101490,101482,3,37,38,88])). % 247.74/247.88 cnf(101531,plain, % 247.74/247.88 (P1(x1015311,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101532,plain, % 247.74/247.88 (P1(x1015321,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101534,plain, % 247.74/247.88 (P3(f5(a9,a9),f5(f5(f4(a9),f14(a9)),a9))), % 247.74/247.88 inference(scs_inference,[],[44,101532,101531,6529,77159,101490,101482,3,37,38,88,87])). % 247.74/247.88 cnf(101562,plain, % 247.74/247.88 (~E(x1015621,a2)+P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),a3)))+~P1(f5(f4(a9),a3),a13)), % 247.74/247.88 inference(scs_inference,[],[44,80643,101466,101454,3,2,37,38,88])). % 247.74/247.88 cnf(101563,plain, % 247.74/247.88 (P1(x1015631,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101564,plain, % 247.74/247.88 (P1(x1015641,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101566,plain, % 247.74/247.88 (~E(x1015661,a2)+P3(f5(f17(f5(x1015662,x1015662)),f17(f5(x1015662,x1015662))),f5(f5(f4(f17(f5(x1015662,x1015662))),f14(f17(f5(x1015662,x1015662)))),f17(f5(x1015662,x1015662))))), % 247.74/247.88 inference(scs_inference,[],[44,101564,101563,77159,80643,101466,101454,3,2,37,38,88,87])). % 247.74/247.88 cnf(101580,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),a3)))+~P1(f5(f4(a9),a3),a13)), % 247.74/247.88 inference(equality_inference,[],[101562])). % 247.74/247.88 cnf(101581,plain, % 247.74/247.88 (P3(f5(f17(f5(x1015811,x1015811)),f17(f5(x1015811,x1015811))),f5(f5(f4(f17(f5(x1015811,x1015811))),f14(f17(f5(x1015811,x1015811)))),f17(f5(x1015811,x1015811))))), % 247.74/247.88 inference(equality_inference,[],[101566])). % 247.74/247.88 cnf(101582,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),a3)))), % 247.74/247.88 inference(scs_inference,[],[44,101580])). % 247.74/247.88 cnf(101588,plain, % 247.74/247.88 (~E(x1015881,a13)+P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3)))+~P1(f5(a3,a3),a13)), % 247.74/247.88 inference(scs_inference,[],[44,101135,101466,97911,3,2,37,38,88])). % 247.74/247.88 cnf(101589,plain, % 247.74/247.88 (P1(x1015891,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101590,plain, % 247.74/247.88 (P1(x1015901,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101592,plain, % 247.74/247.88 (~E(x1015921,a13)+P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),a3),f5(f4(a9),f4(a9))))), % 247.74/247.88 inference(scs_inference,[],[44,101590,101589,80643,101135,101466,97911,3,2,37,38,88,87])). % 247.74/247.88 cnf(101606,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3)))+~P1(f5(a3,a3),a13)), % 247.74/247.88 inference(equality_inference,[],[101588])). % 247.74/247.88 cnf(101607,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),a3),f5(f4(a9),f4(a9))))), % 247.74/247.88 inference(equality_inference,[],[101592])). % 247.74/247.88 cnf(101608,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3)))), % 247.74/247.88 inference(scs_inference,[],[44,101606])). % 247.74/247.88 cnf(101690,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(a3,a3),f5(f4(a9),a3))))+~P1(f5(f5(a3,a3),f5(f4(a9),a3)),a13)), % 247.74/247.88 inference(scs_inference,[],[44,101466,37,38,88])). % 247.74/247.88 cnf(101691,plain, % 247.74/247.88 (P1(x1016911,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101692,plain, % 247.74/247.88 (P1(x1016921,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101694,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(a3,a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))))), % 247.74/247.88 inference(scs_inference,[],[44,101692,101691,101466,37,38,88,87])). % 247.74/247.88 cnf(101711,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(a3,a3),f5(f4(a9),a3))))), % 247.74/247.88 inference(scs_inference,[],[44,101690])). % 247.74/247.88 cnf(101739,plain, % 247.74/247.88 (P1(x1017391,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101740,plain, % 247.74/247.88 (P1(x1017401,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101742,plain, % 247.74/247.88 (P3(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(a3,a3),f5(f4(a9),f4(a9))))), % 247.74/247.88 inference(scs_inference,[],[44,101740,101739,101135,101490,101608,37,38,88,87])). % 247.74/247.88 cnf(101758,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9)))),f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3))))+~P1(f5(f5(f4(a9),f4(a9)),f5(a3,a3)),a13)), % 247.74/247.88 inference(scs_inference,[],[44,101608,101495,37,38,88])). % 247.74/247.88 cnf(101775,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9)))),f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3))))), % 247.74/247.88 inference(scs_inference,[],[44,101758])). % 247.74/247.88 cnf(101819,plain, % 247.74/247.88 (P1(x1018191,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101820,plain, % 247.74/247.88 (P1(x1018201,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101822,plain, % 247.74/247.88 (P3(f5(f5(a9,a9),f5(a9,a9)),f5(f5(f5(f4(a9),f14(a9)),a9),f5(a9,a9)))), % 247.74/247.88 inference(scs_inference,[],[44,101820,101819,101534,101581,101582,37,38,88,87])). % 247.74/247.88 cnf(101857,plain, % 247.74/247.88 (P3(f5(f5(f5(a9,a9),f5(a9,a9)),f5(f5(a9,a9),f5(a9,a9))),f5(f5(f5(a9,a9),f5(a9,a9)),f5(f5(f5(f4(a9),f14(a9)),a9),f5(a9,a9))))+~P1(f5(f5(f5(f4(a9),f14(a9)),a9),f5(a9,a9)),a13)), % 247.74/247.88 inference(scs_inference,[],[44,101822,101607,38,37,88])). % 247.74/247.88 cnf(101874,plain, % 247.74/247.88 (P3(f5(f5(f5(a9,a9),f5(a9,a9)),f5(f5(a9,a9),f5(a9,a9))),f5(f5(f5(a9,a9),f5(a9,a9)),f5(f5(f5(f4(a9),f14(a9)),a9),f5(a9,a9))))), % 247.74/247.88 inference(scs_inference,[],[44,101857])). % 247.74/247.88 cnf(101878,plain, % 247.74/247.88 (P1(x1018781,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101879,plain, % 247.74/247.88 (P1(x1018791,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101881,plain, % 247.74/247.88 (P3(f5(f5(f5(a9,a9),f5(a9,a9)),f5(f5(a9,a9),f5(a9,a9))),f5(f5(f5(f5(f4(a9),f14(a9)),a9),f5(a9,a9)),f5(f5(a9,a9),f5(a9,a9))))), % 247.74/247.88 inference(scs_inference,[],[44,101879,101878,101822,101607,101742,37,38,88,87])). % 247.74/247.88 cnf(101958,plain, % 247.74/247.88 (P1(x1019581,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101959,plain, % 247.74/247.88 (P1(x1019591,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(101961,plain, % 247.74/247.88 (P3(f5(f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9)))),f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))))),f5(f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(a3,a3))),f5(f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))),f5(f5(f4(a9),f4(a9)),f5(f4(a9),f4(a9))))))), % 247.74/247.88 inference(scs_inference,[],[44,101959,101958,101775,101874,101881,37,38,88,87])). % 247.74/247.88 cnf(101997,plain, % 247.74/247.88 (P3(f5(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3)))),f5(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(a3,a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3)))))+~P1(f5(f5(f5(a3,a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),a13)), % 247.74/247.88 inference(scs_inference,[],[44,101694,101711,38,37,88])). % 247.74/247.88 cnf(102014,plain, % 247.74/247.88 (P3(f5(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3)))),f5(f5(f5(f5(f4(a9),a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3))),f5(f5(f5(a3,a3),f5(f4(a9),a3)),f5(f5(f4(a9),a3),f5(f4(a9),a3)))))), % 247.74/247.88 inference(scs_inference,[],[44,101997])). % 247.74/247.88 cnf(102936,plain, % 247.74/247.88 (P3(f5(f10(x1029361,x1029361),f10(x1029361,x1029361)),f5(f10(x1029361,x1029361),f5(f4(f10(x1029361,x1029361)),f14(f10(x1029361,x1029361)))))+~P1(f5(f4(f10(x1029361,x1029361)),f14(f10(x1029361,x1029361))),a13)), % 247.74/247.88 inference(scs_inference,[],[44,96185,101961,37,38,88])). % 247.74/247.88 cnf(102952,plain, % 247.74/247.88 (P3(x1029521,f5(f10(x1029522,x1029522),f5(f4(f10(x1029522,x1029522)),f14(f10(x1029522,x1029522)))))+~E(f5(f10(x1029522,x1029522),f10(x1029522,x1029522)),x1029521)), % 247.74/247.88 inference(scs_inference,[],[44,102936,37])). % 247.74/247.88 cnf(102953,plain, % 247.74/247.88 (P3(f5(f10(x1029531,x1029531),f10(x1029531,x1029531)),f5(f10(x1029531,x1029531),f5(f4(f10(x1029531,x1029531)),f14(f10(x1029531,x1029531)))))), % 247.74/247.88 inference(equality_inference,[],[102952])). % 247.74/247.88 cnf(102957,plain, % 247.74/247.88 (P1(x1029571,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(102958,plain, % 247.74/247.88 (P1(x1029581,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(102960,plain, % 247.74/247.88 (P3(f5(f10(x1029601,x1029601),f10(x1029601,x1029601)),f5(f5(f4(f10(x1029601,x1029601)),f14(f10(x1029601,x1029601))),f10(x1029601,x1029601)))), % 247.74/247.88 inference(scs_inference,[],[44,102958,102957,96185,77199,102953,102014,37,38,88,87])). % 247.74/247.88 cnf(102977,plain, % 247.74/247.88 (P1(x1029771,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(102978,plain, % 247.74/247.88 (P1(x1029781,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(102980,plain, % 247.74/247.88 (P3(f5(f5(x1029801,x1029801),f5(x1029801,x1029801)),f5(f5(f4(f5(x1029801,x1029801)),f14(f5(x1029801,x1029801))),f5(x1029801,x1029801)))), % 247.74/247.88 inference(scs_inference,[],[44,102978,102977,77199,101344,102014,102960,37,38,88,87])). % 247.74/247.88 cnf(102993,plain, % 247.74/247.88 (P1(f6(f15(x1029931)),f24(x1029931))+~P1(f6(f15(x1029931)),a13)), % 247.74/247.88 inference(scs_inference,[],[97951,44,78])). % 247.74/247.88 cnf(102998,plain, % 247.74/247.88 (P1(x1029981,f24(x1029982))+~E(f6(f15(x1029982)),x1029981)), % 247.74/247.88 inference(scs_inference,[],[44,102993,33])). % 247.74/247.88 cnf(102999,plain, % 247.74/247.88 (P1(f6(f15(x1029991)),f24(x1029991))), % 247.74/247.88 inference(equality_inference,[],[102998])). % 247.74/247.88 cnf(103026,plain, % 247.74/247.88 (P1(x1030261,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103027,plain, % 247.74/247.88 (P1(f10(x1030271,x1030271),f21(f15(f5(x1030271,x1030271))))), % 247.74/247.88 inference(scs_inference,[],[44,103026,101530,101448])). % 247.74/247.88 cnf(103028,plain, % 247.74/247.88 (P1(x1030281,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103031,plain, % 247.74/247.88 (P1(f6(f15(f5(x1030311,x1030311))),f23(x1030311,x1030311))), % 247.74/247.88 inference(scs_inference,[],[102999,97839,74950,44,103026,103028,101530,101448,34,93])). % 247.74/247.88 cnf(103046,plain, % 247.74/247.88 (P5(f10(x1030461,x1030461),f15(f5(x1030461,x1030461)))+~P1(f15(f5(x1030461,x1030461)),a13)), % 247.74/247.88 inference(scs_inference,[],[103031,103027,97839,74948,73810,44,34,33,66])). % 247.74/247.88 cnf(103047,plain, % 247.74/247.88 (P1(x1030471,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103048,plain, % 247.74/247.88 (~P2(f15(x1030481))), % 247.74/247.88 inference(rename_variables,[],[73810])). % 247.74/247.88 cnf(103050,plain, % 247.74/247.88 (~P5(a9,f15(f5(a3,f14(a9))))+~P1(f15(f5(a3,f14(a9))),a13)), % 247.74/247.88 inference(scs_inference,[],[103031,103027,97839,74948,97895,73810,103048,44,103047,34,33,66,65])). % 247.74/247.88 cnf(103056,plain, % 247.74/247.88 (P1(x1030561,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103057,plain, % 247.74/247.88 (~P5(a9,f15(f5(a3,f14(a9))))), % 247.74/247.88 inference(scs_inference,[],[44,103056,103046,103050])). % 247.74/247.88 cnf(103063,plain, % 247.74/247.88 (P5(f8(a9,f5(a3,f14(a9))),a9)), % 247.74/247.88 inference(scs_inference,[],[2342,44,103056,103046,103050,95472,36,85295])). % 247.74/247.88 cnf(103089,plain, % 247.74/247.88 (P1(x1030891,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103090,plain, % 247.74/247.88 (P1(x1030901,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103093,plain, % 247.74/247.88 (P1(x1030931,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103094,plain, % 247.74/247.88 (P1(x1030941,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103095,plain, % 247.74/247.88 (P1(x1030951,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103097,plain, % 247.74/247.88 (P5(f8(a9,f5(a3,f14(a9))),f5(f4(a9),f14(a9)))), % 247.74/247.88 inference(scs_inference,[],[102980,103063,6529,44,103090,103094,103093,103089,103095,88,87,81])). % 247.74/247.88 cnf(103236,plain, % 247.74/247.88 (P3(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))+~P1(a9,a13)), % 247.74/247.88 inference(scs_inference,[],[6529,44,87])). % 247.74/247.88 cnf(103251,plain, % 247.74/247.88 (P3(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))), % 247.74/247.88 inference(scs_inference,[],[44,103236])). % 247.74/247.88 cnf(103276,plain, % 247.74/247.88 (P3(f5(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))))+~P1(f5(a9,f5(f4(a9),f14(a9))),a13)), % 247.74/247.88 inference(scs_inference,[],[103251,44,87])). % 247.74/247.88 cnf(103277,plain, % 247.74/247.88 (P1(x1032771,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103278,plain, % 247.74/247.88 (P1(x1032781,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103280,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(a9,f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))))), % 247.74/247.88 inference(scs_inference,[],[103251,44,103278,103277,87,88])). % 247.74/247.88 cnf(103294,plain, % 247.74/247.88 (P3(f5(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))))), % 247.74/247.88 inference(scs_inference,[],[44,103276])). % 247.74/247.88 cnf(103316,plain, % 247.74/247.88 (P3(f5(a1,f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))))+~P1(a1,a13)), % 247.74/247.88 inference(scs_inference,[],[73847,44,87])). % 247.74/247.88 cnf(103317,plain, % 247.74/247.88 (P1(x1033171,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103318,plain, % 247.74/247.88 (P1(x1033181,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103324,plain, % 247.74/247.88 (~P5(a9,f17(f15(f5(a3,f14(a9)))))+~P1(a9,a13)), % 247.74/247.88 inference(scs_inference,[],[73847,103057,11284,74991,44,103318,103317,87,86,85,83])). % 247.74/247.88 cnf(103330,plain, % 247.74/247.88 (P3(f5(a1,f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))))), % 247.74/247.88 inference(scs_inference,[],[44,103316])). % 247.74/247.88 cnf(103331,plain, % 247.74/247.88 (~P5(a9,f17(f15(f5(a3,f14(a9)))))), % 247.74/247.88 inference(scs_inference,[],[44,103324])). % 247.74/247.88 cnf(103338,plain, % 247.74/247.88 (P1(x1033381,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103339,plain, % 247.74/247.88 (P1(x1033391,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103341,plain, % 247.74/247.88 (P3(f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(a1,f5(f4(a1),f14(a1)))),f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1)))))), % 247.74/247.88 inference(scs_inference,[],[103330,103331,2342,44,103339,103338,36,95472,87,88])). % 247.74/247.88 cnf(103342,plain, % 247.74/247.88 (P1(x1033421,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103343,plain, % 247.74/247.88 (P1(x1033431,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103344,plain, % 247.74/247.88 (P1(x1033441,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103347,plain, % 247.74/247.88 (P1(x1033471,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103348,plain, % 247.74/247.88 (P1(x1033481,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103350,plain, % 247.74/247.88 (P1(x1033501,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103352,plain, % 247.74/247.88 (~P5(a9,f7(f15(f17(f15(f5(a3,f14(a9)))))))), % 247.74/247.88 inference(scs_inference,[],[74217,103330,103331,77199,2342,44,103339,103343,103348,103342,103347,103338,103344,103350,36,95472,87,88,80,83])). % 247.74/247.88 cnf(103366,plain, % 247.74/247.88 (~P5(a9,f7(f15(f7(f15(f17(f15(f5(a3,f14(a9)))))))))+~P1(f7(f15(f17(f15(f5(a3,f14(a9)))))),a13)+~P1(a9,a13)), % 247.74/247.88 inference(scs_inference,[],[74217,103352,2342,44,36,83])). % 247.74/247.88 cnf(103368,plain, % 247.74/247.88 (~P1(a9,a13)+~P5(a9,f7(f15(f7(f15(f17(f15(f5(a3,f14(a9)))))))))), % 247.74/247.88 inference(scs_inference,[],[44,103366])). % 247.74/247.88 cnf(103369,plain, % 247.74/247.88 (~P5(a9,f7(f15(f7(f15(f17(f15(f5(a3,f14(a9)))))))))), % 247.74/247.88 inference(scs_inference,[],[44,103368])). % 247.74/247.88 cnf(103801,plain, % 247.74/247.88 (P1(x1038011,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103802,plain, % 247.74/247.88 (P1(x1038021,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103805,plain, % 247.74/247.88 (P1(x1038051,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103806,plain, % 247.74/247.88 (P1(x1038061,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103807,plain, % 247.74/247.88 (P1(x1038071,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103811,plain, % 247.74/247.88 (P1(x1038111,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103812,plain, % 247.74/247.88 (P1(x1038121,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103818,plain, % 247.74/247.88 (~P5(f8(a9,f5(a3,f14(a9))),f5(a3,f14(a9)))), % 247.74/247.88 inference(scs_inference,[],[77199,103369,103057,2342,44,103802,103806,103811,103805,103812,103801,103807,87,88,81,93301,101346,82])). % 247.74/247.88 cnf(103864,plain, % 247.74/247.88 (P3(f5(f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(a9,f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))),f5(f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))))+~P1(f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(a9,f5(f4(a9),f14(a9)))),a13)), % 247.74/247.88 inference(scs_inference,[],[103280,44,87])). % 247.74/247.88 cnf(103874,plain, % 247.74/247.88 (P1(x1038741,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103875,plain, % 247.74/247.88 (P3(f5(f5(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))),f5(f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),f5(f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9))))))+~P1(f5(f5(a9,f5(f4(a9),f14(a9))),f5(f5(f4(a9),f14(a9)),f5(f4(a9),f14(a9)))),a13)), % 247.74/247.88 inference(scs_inference,[],[103294,44,103874,103864,87])). % 247.74/247.88 cnf(103885,plain, % 247.74/247.88 (P1(x1038851,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103886,plain, % 247.74/247.88 (P3(f5(f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(a1,f5(f4(a1),f14(a1)))),f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))))),f5(f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1)))),f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))))))+~P1(f5(f5(f5(f4(a1),f14(a1)),f5(f4(a1),f14(a1))),f5(a1,f5(f4(a1),f14(a1)))),a13)), % 247.74/247.88 inference(scs_inference,[],[103341,44,103885,103875,87])). % 247.74/247.88 cnf(103887,plain, % 247.74/247.88 (P1(x1038871,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103888,plain, % 247.74/247.88 (P1(x1038881,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103891,plain, % 247.74/247.88 (P1(x1038911,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103892,plain, % 247.74/247.88 (P1(x1038921,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103893,plain, % 247.74/247.88 (P1(x1038931,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103895,plain, % 247.74/247.88 (~P3(f5(f4(a9),f14(a9)),f5(a3,f14(a9)))), % 247.74/247.88 inference(scs_inference,[],[103341,103097,103818,44,103885,103888,103892,103891,103887,103893,103875,87,88,81])). % 247.74/247.88 cnf(103915,plain, % 247.74/247.88 (P1(x1039151,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103917,plain, % 247.74/247.88 (P1(x1039171,a13)), % 247.74/247.88 inference(rename_variables,[],[44])). % 247.74/247.88 cnf(103920,plain, % 247.74/247.88 (~E(x1039201,f14(a9))+~P1(f4(a9),a13)), % 247.74/247.88 inference(scs_inference,[],[103895,45,44,103915,103917,103886,87,101346,33])). % 247.74/247.88 cnf(103923,plain, % 247.74/247.88 (~P1(f4(a9),a13)), % 247.74/247.88 inference(equality_inference,[],[103920])). % 247.74/247.88 cnf(103924,plain, % 247.74/247.88 ($false), % 247.74/247.88 inference(scs_inference,[],[103923,44]), % 247.74/247.88 ['proof']). % 247.91/247.93 % SZS output end Proof % 247.91/247.93 % Total time :247.010000s %------------------------------------------------------------------------------