%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET640+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 : n025.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:06 EDT 2024 % Result : Theorem 116.94s 116.97s % Output : CNFRefutation 117.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SET640+3 : TPTP v8.2.0. Released v2.2.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Jun 23 12:33:39 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 116.87/116.94 %------------------------------------------- % 116.87/116.94 % File :CSE---1.7 % 116.87/116.94 % Problem :theBenchmark % 116.87/116.94 % Transform :cnf % 116.87/116.94 % Format :tptp:raw % 116.87/116.94 % Command :java -jar mcs_scs.jar %d %s % 116.87/116.94 % 116.87/116.94 % Result :Theorem 116.320000s % 116.87/116.94 % Output :CNFRefutation 116.320000s % 116.87/116.94 %------------------------------------------- % 116.94/116.96 %------------------------------------------------------------------------------ % 116.94/116.96 % File : SET640+3 : TPTP v8.2.0. Released v2.2.0. % 116.94/116.96 % Domain : Set Theory (Relations) % 116.94/116.96 % Problem : A a subset of R (X to Y) => A a subset of X x Y % 116.94/116.96 % Version : [Wor90] axioms : Reduced > Incomplete. % 116.94/116.96 % English : If A is a subset of a relation R from X to Y then A is a subset % 116.94/116.96 % of X x Y. % 116.94/116.96 % 116.94/116.96 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 116.94/116.96 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 116.94/116.96 % Source : [ILF] % 116.94/116.96 % Names : RELSET_1 (2) [Wor90] % 116.94/116.96 % 116.94/116.96 % Status : Theorem % 116.94/116.96 % Rating : 0.36 v7.5.0, 0.41 v7.4.0, 0.30 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.26 v7.0.0, 0.23 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.47 v6.0.0, 0.43 v5.5.0, 0.44 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.33 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.0, 0.38 v3.7.0, 0.35 v3.5.0, 0.32 v3.4.0, 0.16 v3.3.0, 0.21 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.33 v2.6.0, 0.29 v2.5.0, 0.38 v2.4.0, 0.50 v2.3.0, 0.67 v2.2.1 % 116.94/116.96 % Syntax : Number of formulae : 20 ( 1 unt; 0 def) % 116.94/116.96 % Number of atoms : 86 ( 2 equ) % 116.94/116.96 % Maximal formula atoms : 9 ( 4 avg) % 116.94/116.96 % Number of connectives : 70 ( 4 ~; 0 |; 12 &) % 116.94/116.96 % ( 7 <=>; 47 =>; 0 <=; 0 <~>) % 116.94/116.96 % Maximal formula depth : 14 ( 7 avg) % 116.94/116.96 % Maximal term depth : 3 ( 1 avg) % 116.94/116.96 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 116.94/116.96 % Number of functors : 7 ( 7 usr; 1 con; 0-2 aty) % 116.94/116.96 % Number of variables : 50 ( 43 !; 7 ?) % 116.94/116.96 % SPC : FOF_THM_RFO_SEQ % 116.94/116.96 % 116.94/116.96 % Comments : % 116.94/116.96 %------------------------------------------------------------------------------ % 116.94/116.96 %---- line(boole - th(29),1909428) % 116.94/116.96 fof(p1,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ! [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 => ( ( subset(B,C) % 116.94/116.96 & subset(C,D) ) % 116.94/116.96 => subset(B,D) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(zfmisc_1 - df(1),1903822) % 116.94/116.96 fof(p2,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ! [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 => ( member(D,cross_product(B,C)) % 116.94/116.96 <=> ? [E] : % 116.94/116.96 ( ilf_type(E,set_type) % 116.94/116.96 & ? [F] : % 116.94/116.96 ( ilf_type(F,set_type) % 116.94/116.96 & member(E,B) % 116.94/116.96 & member(F,C) % 116.94/116.96 & D = ordered_pair(E,F) ) ) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- declaration(line(zfmisc_1 - df(1),1903822)) % 116.94/116.96 fof(p3,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ilf_type(cross_product(B,C),set_type) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(relset_1 - df(1),1916080) % 116.94/116.96 fof(p4,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ( ! [D] : % 116.94/116.96 ( ilf_type(D,subset_type(cross_product(B,C))) % 116.94/116.96 => ilf_type(D,relation_type(B,C)) ) % 116.94/116.96 & ! [E] : % 116.94/116.96 ( ilf_type(E,relation_type(B,C)) % 116.94/116.96 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 116.94/116.96 fof(p5,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(tarski - df(3),1832749) % 116.94/116.96 fof(p6,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ( subset(B,C) % 116.94/116.96 <=> ! [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 => ( member(D,B) % 116.94/116.96 => member(D,C) ) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- declaration(op(ordered_pair,2,function)) % 116.94/116.96 fof(p7,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(hidden - axiom1,1832648) % 116.94/116.96 fof(p8,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ( ilf_type(C,subset_type(B)) % 116.94/116.96 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- type_nonempty(line(hidden - axiom1,1832648)) % 116.94/116.96 fof(p9,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 116.94/116.96 % 116.94/116.96 %---- property(reflexivity,op(subset,2,predicate)) % 116.94/116.96 fof(p10,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => subset(B,B) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(hidden - axiom3,1832644) % 116.94/116.96 fof(p11,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ( member(B,power_set(C)) % 116.94/116.96 <=> ! [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 => ( member(D,B) % 116.94/116.96 => member(D,C) ) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- declaration(line(hidden - axiom3,1832644)) % 116.94/116.96 fof(p12,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ( ~ empty(power_set(B)) % 116.94/116.96 & ilf_type(power_set(B),set_type) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(hidden - axiom4,1832640) % 116.94/116.96 fof(p13,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ( ~ empty(C) % 116.94/116.96 & ilf_type(C,set_type) ) % 116.94/116.96 => ( ilf_type(B,member_type(C)) % 116.94/116.96 <=> member(B,C) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- type_nonempty(line(hidden - axiom4,1832640)) % 116.94/116.96 fof(p14,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ( ~ empty(B) % 116.94/116.96 & ilf_type(B,set_type) ) % 116.94/116.96 => ? [C] : ilf_type(C,member_type(B)) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(hidden - axiom5,1832628) % 116.94/116.96 fof(p15,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ( empty(B) % 116.94/116.96 <=> ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ~ member(C,B) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- line(relat_1 - df(1),1917627) % 116.94/116.96 fof(p16,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ( relation_like(B) % 116.94/116.96 <=> ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ( member(C,B) % 116.94/116.96 => ? [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 & ? [E] : % 116.94/116.96 ( ilf_type(E,set_type) % 116.94/116.96 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- conditional_cluster(axiom7,relation_like) % 116.94/116.96 fof(p17,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ( empty(B) % 116.94/116.96 & ilf_type(B,set_type) ) % 116.94/116.96 => relation_like(B) ) ). % 116.94/116.96 % 116.94/116.96 %---- conditional_cluster(axiom8,relation_like) % 116.94/116.96 fof(p18,axiom, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ! [D] : % 116.94/116.96 ( ilf_type(D,subset_type(cross_product(B,C))) % 116.94/116.96 => relation_like(D) ) ) ) ). % 116.94/116.96 % 116.94/116.96 %---- declaration(set) % 116.94/116.96 fof(p19,axiom, % 116.94/116.96 ! [B] : ilf_type(B,set_type) ). % 116.94/116.96 % 116.94/116.96 %---- line(relset_1 - th(2),1916093) % 116.94/116.96 fof(prove_relset_1_2,conjecture, % 116.94/116.96 ! [B] : % 116.94/116.96 ( ilf_type(B,set_type) % 116.94/116.96 => ! [C] : % 116.94/116.96 ( ilf_type(C,set_type) % 116.94/116.96 => ! [D] : % 116.94/116.96 ( ilf_type(D,set_type) % 116.94/116.96 => ! [E] : % 116.94/116.96 ( ilf_type(E,relation_type(C,D)) % 116.94/116.96 => ( subset(B,E) % 116.94/116.97 => subset(B,cross_product(C,D)) ) ) ) ) ) ). % 116.94/116.97 % 116.94/116.97 %------------------------------------------------------------------------------ % 116.94/116.97 %------------------------------------------- % 116.94/116.97 % Proof found % 116.94/116.97 % SZS status Theorem for theBenchmark % 116.94/116.97 % SZS output start Proof % 116.94/116.97 %ClaNum:87(EqnAxiom:40) % 116.94/116.97 %VarNum:203(SingletonVarNum:65) % 116.94/116.97 %MaxLitNum:9 % 116.94/116.97 %MaxfuncDepth:2 % 116.94/116.97 %SharedTerms:13 % 116.94/116.97 %goalClause: 44 46 47 % 116.94/116.97 %singleGoalClaCount:3 % 116.94/116.97 [44]P3(a1,a8) % 116.94/116.97 [46]P1(a8,f9(a6,a7)) % 116.94/116.97 [47]~P3(a1,f2(a6,a7)) % 116.94/116.97 [45]P1(x451,a5) % 116.94/116.97 [49]P3(x491,x491)+~P1(x491,a5) % 116.94/116.97 [50]~P1(x501,a5)+~P2(f10(x501)) % 116.94/116.97 [56]~P1(x561,a5)+P1(f12(x561),f22(x561)) % 116.94/116.97 [48]~P2(x481)+P4(x481)+~P1(x481,a5) % 116.94/116.97 [54]P2(x541)+P5(f11(x541),x541)+~P1(x541,a5) % 116.94/116.97 [55]P4(x551)+P5(f3(x551),x551)+~P1(x551,a5) % 116.94/116.97 [57]P2(x571)+P1(f17(x571),f19(x571))+~P1(x571,a5) % 116.94/116.97 [69]~P1(x692,a5)+~P1(x691,a5)+P1(f14(x691,x692),f9(x692,x691)) % 116.94/116.97 [58]~P2(x581)+~P5(x582,x581)+~P1(x582,a5)+~P1(x581,a5) % 116.94/116.97 [65]P3(x651,x652)+P5(f13(x651,x652),x651)+~P1(x652,a5)+~P1(x651,a5) % 116.94/116.97 [67]P5(f18(x671,x672),x671)+~P1(x672,a5)+~P1(x671,a5)+P5(x671,f10(x672)) % 116.94/116.97 [73]P3(x731,x732)+~P1(x732,a5)+~P1(x731,a5)+~P5(f13(x731,x732),x732) % 116.94/116.97 [76]~P1(x762,a5)+~P1(x761,a5)+~P5(f18(x761,x762),x762)+P5(x761,f10(x762)) % 116.94/116.97 [68]~P1(x682,a5)+~P1(x681,a5)+~P1(x681,f22(x682))+P1(x681,f19(f10(x682))) % 116.94/116.97 [72]~P1(x722,a5)+~P1(x721,a5)+P1(x721,f22(x722))+~P1(x721,f19(f10(x722))) % 116.94/116.97 [79]P4(x791)+~P1(x792,a5)+~P1(x793,a5)+~P1(x791,f22(f2(x793,x792))) % 116.94/116.97 [80]~P1(x803,a5)+~P1(x802,a5)+~P1(x801,f9(x802,x803))+P1(x801,f22(f2(x802,x803))) % 116.94/116.97 [81]~P1(x813,a5)+~P1(x812,a5)+P1(x811,f9(x812,x813))+~P1(x811,f22(f2(x812,x813))) % 116.94/116.97 [61]~P5(x612,x611)+P2(x611)+~P1(x611,a5)+~P1(x612,a5)+P1(x612,f19(x611)) % 116.94/116.97 [62]P2(x621)+P5(x622,x621)+~P1(x621,a5)+~P1(x622,a5)+~P1(x622,f19(x621)) % 116.94/116.97 [78]~P4(x781)+~P5(x782,x781)+~P1(x781,a5)+~P1(x782,a5)+E(f21(f20(x781,x782),f4(x781,x782)),x782) % 116.94/116.97 [64]P4(x641)+~P1(x641,a5)+~P1(x643,a5)+~P1(x642,a5)+~E(f3(x641),f21(x642,x643)) % 116.94/116.97 [85]~P1(x853,a5)+~P1(x852,a5)+~P1(x851,a5)+~P5(x853,f2(x851,x852))+P5(f15(x851,x852,x853),x851) % 116.94/116.97 [86]~P1(x863,a5)+~P1(x862,a5)+~P1(x861,a5)+~P5(x863,f2(x861,x862))+P5(f16(x861,x862,x863),x862) % 116.94/116.97 [87]~P1(x872,a5)+~P1(x871,a5)+~P1(x873,a5)+~P5(x873,f2(x871,x872))+E(f21(f15(x871,x872,x873),f16(x871,x872,x873)),x873) % 116.94/116.97 [74]~P3(x741,x743)+P3(x741,x742)+~P3(x743,x742)+~P1(x742,a5)+~P1(x743,a5)+~P1(x741,a5) % 116.94/116.97 [75]~P5(x751,x753)+P5(x751,x752)+~P3(x753,x752)+~P1(x751,a5)+~P1(x752,a5)+~P1(x753,a5) % 116.94/116.97 [77]P5(x771,x772)+~P5(x771,x773)+~P1(x771,a5)+~P1(x772,a5)+~P1(x773,a5)+~P5(x773,f10(x772)) % 116.94/116.97 [82]~P5(x825,x823)+~P5(x824,x822)+~P1(x821,a5)+~P1(x823,a5)+~P1(x822,a5)+~P1(x825,a5)+~P1(x824,a5)+P5(x821,f2(x822,x823))+~E(x821,f21(x824,x825)) % 116.94/116.97 %EqnAxiom % 116.94/116.97 [1]E(x11,x11) % 116.94/116.97 [2]E(x22,x21)+~E(x21,x22) % 116.94/116.97 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.94/116.97 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 116.94/116.97 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 116.94/116.97 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 116.94/116.97 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 116.94/116.97 [8]~E(x81,x82)+E(f10(x81),f10(x82)) % 116.94/116.97 [9]~E(x91,x92)+E(f21(x91,x93),f21(x92,x93)) % 116.94/116.97 [10]~E(x101,x102)+E(f21(x103,x101),f21(x103,x102)) % 116.94/116.97 [11]~E(x111,x112)+E(f11(x111),f11(x112)) % 116.94/116.97 [12]~E(x121,x122)+E(f3(x121),f3(x122)) % 116.94/116.97 [13]~E(x131,x132)+E(f20(x131,x133),f20(x132,x133)) % 116.94/116.97 [14]~E(x141,x142)+E(f20(x143,x141),f20(x143,x142)) % 116.94/116.97 [15]~E(x151,x152)+E(f16(x151,x153,x154),f16(x152,x153,x154)) % 116.94/116.97 [16]~E(x161,x162)+E(f16(x163,x161,x164),f16(x163,x162,x164)) % 116.94/116.97 [17]~E(x171,x172)+E(f16(x173,x174,x171),f16(x173,x174,x172)) % 116.94/116.97 [18]~E(x181,x182)+E(f12(x181),f12(x182)) % 116.94/116.97 [19]~E(x191,x192)+E(f22(x191),f22(x192)) % 116.94/116.97 [20]~E(x201,x202)+E(f17(x201),f17(x202)) % 116.94/116.97 [21]~E(x211,x212)+E(f19(x211),f19(x212)) % 116.94/116.97 [22]~E(x221,x222)+E(f15(x221,x223,x224),f15(x222,x223,x224)) % 116.94/116.97 [23]~E(x231,x232)+E(f15(x233,x231,x234),f15(x233,x232,x234)) % 116.94/116.97 [24]~E(x241,x242)+E(f15(x243,x244,x241),f15(x243,x244,x242)) % 116.94/116.97 [25]~E(x251,x252)+E(f4(x251,x253),f4(x252,x253)) % 116.94/116.97 [26]~E(x261,x262)+E(f4(x263,x261),f4(x263,x262)) % 116.94/116.97 [27]~E(x271,x272)+E(f14(x271,x273),f14(x272,x273)) % 116.94/116.97 [28]~E(x281,x282)+E(f14(x283,x281),f14(x283,x282)) % 116.94/116.97 [29]~E(x291,x292)+E(f13(x291,x293),f13(x292,x293)) % 116.94/116.97 [30]~E(x301,x302)+E(f13(x303,x301),f13(x303,x302)) % 116.94/116.97 [31]~E(x311,x312)+E(f18(x311,x313),f18(x312,x313)) % 116.94/116.97 [32]~E(x321,x322)+E(f18(x323,x321),f18(x323,x322)) % 116.94/116.97 [33]P1(x332,x333)+~E(x331,x332)+~P1(x331,x333) % 116.94/116.97 [34]P1(x343,x342)+~E(x341,x342)+~P1(x343,x341) % 116.94/116.97 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353) % 116.94/116.97 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361) % 116.94/116.97 [37]~P4(x371)+P4(x372)+~E(x371,x372) % 116.94/116.97 [38]P3(x382,x383)+~E(x381,x382)+~P3(x381,x383) % 116.94/116.97 [39]P3(x393,x392)+~E(x391,x392)+~P3(x393,x391) % 116.94/116.97 [40]~P2(x401)+P2(x402)+~E(x401,x402) % 116.94/116.97 % 116.94/116.97 %------------------------------------------- % 116.99/117.03 cnf(88,plain, % 116.99/117.03 (~P5(x881,x882)+~P5(x883,x884)+~P1(x882,a5)+~P1(x884,a5)+~P1(x881,a5)+~P1(x883,a5)+P5(f21(x883,x881),f2(x884,x882))+~P1(f21(x883,x881),a5)), % 116.99/117.03 inference(equality_inference,[],[82])). % 116.99/117.03 cnf(89,plain, % 116.99/117.03 (P3(x891,x891)), % 116.99/117.03 inference(scs_inference,[],[45,49])). % 116.99/117.03 cnf(96,plain, % 116.99/117.03 (P1(x961,a5)), % 116.99/117.03 inference(rename_variables,[],[45])). % 116.99/117.03 cnf(100,plain, % 116.99/117.03 (P5(x1001,f10(x1001))+P5(f18(x1001,x1001),x1001)), % 116.99/117.03 inference(scs_inference,[],[44,46,47,45,96,49,38,39,33,34,48,58,67])). % 116.99/117.03 cnf(115,plain, % 116.99/117.03 (P1(x1151,x1152)+~E(a5,x1152)), % 116.99/117.03 inference(scs_inference,[],[47,89,45,39,48,34])). % 116.99/117.03 cnf(399,plain, % 116.99/117.03 (E(f9(x3991,x3992),f9(x3993,x3992))+~E(x3993,x3991)), % 116.99/117.03 inference(scs_inference,[],[2,4])). % 116.99/117.03 cnf(766,plain, % 116.99/117.03 (~E(x7661,x7662)+E(f10(x7662),f10(x7661))), % 116.99/117.03 inference(scs_inference,[],[8,2])). % 116.99/117.03 cnf(1732,plain, % 116.99/117.03 (P1(x17321,f22(x17322))+~E(f12(x17322),x17321)), % 116.99/117.03 inference(scs_inference,[],[45,56,33])). % 116.99/117.03 cnf(1733,plain, % 116.99/117.03 (P1(f12(x17331),f22(x17331))), % 116.99/117.03 inference(equality_inference,[],[1732])). % 116.99/117.03 cnf(1735,plain, % 116.99/117.03 (P1(f12(x17351),f22(x17351))), % 116.99/117.03 inference(rename_variables,[],[1733])). % 116.99/117.03 cnf(1737,plain, % 116.99/117.03 (P1(f12(f2(x17371,x17371)),f9(x17371,x17371))), % 116.99/117.03 inference(scs_inference,[],[1733,1735,45,79,81])). % 116.99/117.03 cnf(1746,plain, % 116.99/117.03 (P1(f12(f2(x17461,x17461)),x17462)+~E(f9(x17461,x17461),x17462)), % 116.99/117.03 inference(scs_inference,[],[1737,34])). % 116.99/117.03 cnf(2244,plain, % 116.99/117.03 (P5(x22441,f10(x22441))), % 116.99/117.03 inference(scs_inference,[],[45,100,76])). % 116.99/117.03 cnf(2245,plain, % 116.99/117.03 (P5(x22451,f10(x22452))+~E(x22452,x22451)), % 116.99/117.03 inference(scs_inference,[],[2244,35])). % 116.99/117.03 cnf(2271,plain, % 116.99/117.03 (P5(x22711,x22712)+~E(f10(x22711),x22712)), % 116.99/117.03 inference(scs_inference,[],[2244,36])). % 116.99/117.03 cnf(4609,plain, % 116.99/117.03 (~E(x46091,x46092)+E(f20(x46092,x46093),f20(x46091,x46093))), % 116.99/117.03 inference(scs_inference,[],[13,2])). % 116.99/117.03 cnf(5501,plain, % 116.99/117.03 (~E(x55011,x55012)+E(f14(f2(x55013,x55011),x55014),f14(f2(x55013,x55012),x55014))), % 116.99/117.03 inference(scs_inference,[],[27,7])). % 116.99/117.03 cnf(5698,plain, % 116.99/117.03 (~E(x56981,x56982)+E(f14(x56983,f10(x56981)),f14(x56983,f10(x56982)))), % 116.99/117.03 inference(scs_inference,[],[28,8])). % 116.99/117.03 cnf(14295,plain, % 116.99/117.03 (P1(f17(f10(x142951)),f19(f10(x142951)))+~P1(x142951,a5)), % 116.99/117.03 inference(scs_inference,[],[45,57,50])). % 116.99/117.03 cnf(14296,plain, % 116.99/117.03 (P1(f17(f10(x142961)),f19(f10(x142961)))), % 116.99/117.03 inference(scs_inference,[],[45,14295])). % 116.99/117.03 cnf(14314,plain, % 116.99/117.03 (P1(f17(f10(x143141)),f22(x143141))+~P1(f17(f10(x143141)),a5)), % 116.99/117.03 inference(scs_inference,[],[45,14296,72])). % 116.99/117.03 cnf(14319,plain, % 116.99/117.03 (P1(x143191,a5)), % 116.99/117.03 inference(rename_variables,[],[45])). % 116.99/117.03 cnf(14320,plain, % 116.99/117.03 (P1(f17(f10(x143201)),x143202)+~E(f22(x143201),x143202)), % 116.99/117.03 inference(scs_inference,[],[45,14314,34])). % 116.99/117.03 cnf(14323,plain, % 116.99/117.03 (~E(f22(x143231),f22(f2(x143232,x143232)))+P1(f17(f10(x143231)),f9(x143232,x143232))), % 116.99/117.03 inference(scs_inference,[],[45,14319,14314,34,79,81])). % 116.99/117.03 cnf(14335,plain, % 116.99/117.03 (P1(f17(f10(f2(x143351,x143351))),f9(x143351,x143351))), % 116.99/117.03 inference(equality_inference,[],[14323])). % 116.99/117.03 cnf(15699,plain, % 116.99/117.03 (P1(f14(x156991,x156991),f22(f2(x156991,x156991)))), % 116.99/117.03 inference(scs_inference,[],[45,69,80])). % 116.99/117.03 cnf(15700,plain, % 116.99/117.03 (P4(f14(x157001,x157001))), % 116.99/117.03 inference(scs_inference,[],[15699,45,79])). % 116.99/117.03 cnf(15701,plain, % 116.99/117.03 (P1(f14(x157011,x157011),f22(f2(x157011,x157011)))), % 116.99/117.03 inference(rename_variables,[],[15699])). % 116.99/117.03 cnf(15704,plain, % 116.99/117.03 (P1(f14(x157041,x157041),f22(f2(x157041,x157041)))), % 116.99/117.03 inference(rename_variables,[],[15699])). % 116.99/117.03 cnf(15706,plain, % 116.99/117.03 (P1(x157061,f22(f2(x157062,x157062)))+~E(f14(x157062,x157062),x157061)), % 116.99/117.03 inference(scs_inference,[],[15699,15701,15704,45,79,81,33])). % 116.99/117.03 cnf(30863,plain, % 116.99/117.03 (E(f9(x308631,x308632),f9(x308631,x308633))+~E(x308633,x308632)), % 116.99/117.03 inference(scs_inference,[],[2,5])). % 116.99/117.03 cnf(32115,plain, % 116.99/117.03 (E(f2(x321151,x321152),f2(x321153,x321152))+~E(x321153,x321151)), % 116.99/117.03 inference(scs_inference,[],[2,6])). % 116.99/117.03 cnf(32376,plain, % 116.99/117.03 (E(f2(x323761,x323762),f2(x323761,x323763))+~E(x323763,x323762)), % 116.99/117.03 inference(scs_inference,[],[2,7])). % 116.99/117.03 cnf(32629,plain, % 116.99/117.03 (E(f21(x326291,x326292),f21(x326293,x326292))+~E(x326293,x326291)), % 116.99/117.03 inference(scs_inference,[],[2,9])). % 116.99/117.03 cnf(32872,plain, % 116.99/117.03 (E(f21(x328721,x328722),f21(x328721,x328723))+~E(x328723,x328722)), % 116.99/117.03 inference(scs_inference,[],[2,10])). % 116.99/117.03 cnf(33125,plain, % 116.99/117.03 (E(f11(x331251),f11(x331252))+~E(x331252,x331251)), % 116.99/117.03 inference(scs_inference,[],[2,11])). % 116.99/117.03 cnf(33386,plain, % 116.99/117.03 (E(f3(x333861),f3(x333862))+~E(x333862,x333861)), % 116.99/117.03 inference(scs_inference,[],[2,12])). % 116.99/117.03 cnf(33639,plain, % 116.99/117.03 (E(f20(x336391,x336392),f20(x336391,x336393))+~E(x336393,x336392)), % 116.99/117.03 inference(scs_inference,[],[2,14])). % 116.99/117.03 cnf(33900,plain, % 116.99/117.03 (E(f16(x339001,x339002,x339003),f16(x339004,x339002,x339003))+~E(x339004,x339001)), % 116.99/117.03 inference(scs_inference,[],[2,15])). % 116.99/117.03 cnf(34153,plain, % 116.99/117.03 (E(f16(x341531,x341532,x341533),f16(x341531,x341534,x341533))+~E(x341534,x341532)), % 116.99/117.03 inference(scs_inference,[],[2,16])). % 116.99/117.03 cnf(34414,plain, % 116.99/117.03 (E(f16(x344141,x344142,x344143),f16(x344141,x344142,x344144))+~E(x344144,x344143)), % 116.99/117.03 inference(scs_inference,[],[2,17])). % 116.99/117.03 cnf(34651,plain, % 116.99/117.03 (E(f12(x346511),f12(x346512))+~E(x346512,x346511)), % 116.99/117.03 inference(scs_inference,[],[2,18])). % 116.99/117.03 cnf(34904,plain, % 116.99/117.03 (E(f22(x349041),f22(x349042))+~E(x349042,x349041)), % 116.99/117.03 inference(scs_inference,[],[2,19])). % 116.99/117.03 cnf(35181,plain, % 116.99/117.03 (E(f17(x351811),f17(x351812))+~E(x351812,x351811)), % 116.99/117.03 inference(scs_inference,[],[2,20])). % 116.99/117.03 cnf(35458,plain, % 116.99/117.03 (E(f19(x354581),f19(x354582))+~E(x354582,x354581)), % 116.99/117.03 inference(scs_inference,[],[2,21])). % 116.99/117.03 cnf(35735,plain, % 116.99/117.03 (E(f15(x357351,x357352,x357353),f15(x357354,x357352,x357353))+~E(x357354,x357351)), % 116.99/117.03 inference(scs_inference,[],[2,22])). % 116.99/117.03 cnf(36012,plain, % 116.99/117.03 (E(f15(x360121,x360122,x360123),f15(x360121,x360124,x360123))+~E(x360124,x360122)), % 116.99/117.03 inference(scs_inference,[],[2,23])). % 116.99/117.03 cnf(36289,plain, % 116.99/117.03 (E(f15(x362891,x362892,x362893),f15(x362891,x362892,x362894))+~E(x362894,x362893)), % 116.99/117.03 inference(scs_inference,[],[2,24])). % 116.99/117.03 cnf(36566,plain, % 116.99/117.03 (E(f4(x365661,x365662),f4(x365663,x365662))+~E(x365663,x365661)), % 116.99/117.03 inference(scs_inference,[],[2,25])). % 116.99/117.03 cnf(36843,plain, % 116.99/117.03 (E(f4(x368431,x368432),f4(x368431,x368433))+~E(x368433,x368432)), % 116.99/117.03 inference(scs_inference,[],[2,26])). % 116.99/117.03 cnf(37120,plain, % 116.99/117.03 (E(f14(x371201,x371202),f14(x371203,x371202))+~E(x371203,x371201)), % 116.99/117.03 inference(scs_inference,[],[2,27])). % 116.99/117.03 cnf(37397,plain, % 116.99/117.03 (E(f14(x373971,x373972),f14(x373971,x373973))+~E(x373973,x373972)), % 116.99/117.03 inference(scs_inference,[],[2,28])). % 116.99/117.03 cnf(37674,plain, % 116.99/117.03 (E(f13(x376741,x376742),f13(x376743,x376742))+~E(x376743,x376741)), % 116.99/117.03 inference(scs_inference,[],[2,29])). % 116.99/117.03 cnf(37951,plain, % 116.99/117.03 (E(f13(x379511,x379512),f13(x379511,x379513))+~E(x379513,x379512)), % 116.99/117.03 inference(scs_inference,[],[2,30])). % 116.99/117.03 cnf(38228,plain, % 116.99/117.03 (E(f18(x382281,x382282),f18(x382283,x382282))+~E(x382283,x382281)), % 116.99/117.03 inference(scs_inference,[],[2,31])). % 116.99/117.03 cnf(38505,plain, % 116.99/117.03 (E(f18(x385051,x385052),f18(x385051,x385053))+~E(x385053,x385052)), % 116.99/117.03 inference(scs_inference,[],[2,32])). % 116.99/117.03 cnf(40520,plain, % 116.99/117.03 (E(f14(f2(x405201,x405202),x405203),f14(f2(x405201,x405204),x405203))+~E(x405204,x405202)), % 116.99/117.03 inference(scs_inference,[],[2,5501])). % 116.99/117.03 cnf(49596,plain, % 116.99/117.03 (~E(x495961,f10(x495962))+~P2(x495961)), % 116.99/117.03 inference(scs_inference,[],[45,50,40])). % 116.99/117.03 cnf(49597,plain, % 116.99/117.03 (~P2(f10(x495971))), % 116.99/117.03 inference(equality_inference,[],[49596])). % 116.99/117.03 cnf(49658,plain, % 116.99/117.03 (~E(f14(x496581,x496581),x496582)+P4(x496582)), % 116.99/117.03 inference(scs_inference,[],[15700,37])). % 116.99/117.03 cnf(49899,plain, % 116.99/117.03 (P1(x498991,a5)), % 116.99/117.03 inference(rename_variables,[],[45])). % 116.99/117.03 cnf(49902,plain, % 116.99/117.03 (P5(f17(f10(x499021)),f10(x499021))+~E(x499022,f17(f10(x499021)))), % 116.99/117.03 inference(scs_inference,[],[45,49899,14296,49597,62,33])). % 116.99/117.03 cnf(49907,plain, % 116.99/117.03 (P5(f17(f10(x499071)),f10(x499071))), % 116.99/117.03 inference(equality_inference,[],[49902])). % 116.99/117.03 cnf(50273,plain, % 116.99/117.03 (~E(x502731,a5)+P1(x502732,x502731)), % 116.99/117.03 inference(scs_inference,[],[115,2])). % 116.99/117.03 cnf(51100,plain, % 116.99/117.03 (~E(x511001,x511002)+P1(x511003,x511002)+~E(a5,x511001)), % 116.99/117.03 inference(scs_inference,[],[115,3])). % 116.99/117.03 cnf(51146,plain, % 116.99/117.03 (~E(x511461,x511462)+P1(x511463,x511461)+~E(a5,x511462)), % 116.99/117.03 inference(scs_inference,[],[51100,2])). % 116.99/117.03 cnf(54135,plain, % 116.99/117.03 (~E(x541351,f10(x541352))+P5(f11(x541351),x541351)), % 116.99/117.03 inference(scs_inference,[],[45,49596,54])). % 116.99/117.03 cnf(54136,plain, % 116.99/117.03 (P5(f11(f10(x541361)),f10(x541361))), % 116.99/117.03 inference(equality_inference,[],[54135])). % 116.99/117.03 cnf(56028,plain, % 116.99/117.03 (~E(x560281,x560282)+P5(x560281,f10(x560282))), % 116.99/117.03 inference(scs_inference,[],[2245,2])). % 116.99/117.03 cnf(56273,plain, % 116.99/117.03 (P5(f9(x562731,x562732),f10(f9(x562731,x562733)))+~E(x562733,x562732)), % 116.99/117.03 inference(scs_inference,[],[2245,5])). % 116.99/117.03 cnf(56397,plain, % 116.99/117.03 (P5(f2(x563971,x563972),f10(f2(x563971,x563973)))+~E(x563973,x563972)), % 116.99/117.03 inference(scs_inference,[],[2245,7])). % 116.99/117.03 cnf(56769,plain, % 116.99/117.03 (P5(f20(x567691,x567692),f10(f20(x567693,x567692)))+~E(x567693,x567691)), % 116.99/117.03 inference(scs_inference,[],[2245,13])). % 116.99/117.03 cnf(56893,plain, % 116.99/117.03 (P5(f16(x568931,x568932,x568933),f10(f16(x568934,x568932,x568933)))+~E(x568934,x568931)), % 116.99/117.03 inference(scs_inference,[],[2245,15])). % 116.99/117.03 cnf(57017,plain, % 116.99/117.03 (P5(f16(x570171,x570172,x570173),f10(f16(x570171,x570172,x570174)))+~E(x570174,x570173)), % 116.99/117.03 inference(scs_inference,[],[2245,17])). % 116.99/117.03 cnf(57141,plain, % 116.99/117.03 (P5(f22(x571411),f10(f22(x571412)))+~E(x571412,x571411)), % 116.99/117.03 inference(scs_inference,[],[2245,19])). % 116.99/117.03 cnf(57265,plain, % 116.99/117.03 (P5(f19(x572651),f10(f19(x572652)))+~E(x572652,x572651)), % 116.99/117.03 inference(scs_inference,[],[2245,21])). % 116.99/117.03 cnf(57389,plain, % 116.99/117.03 (P5(f15(x573891,x573892,x573893),f10(f15(x573891,x573894,x573893)))+~E(x573894,x573892)), % 116.99/117.03 inference(scs_inference,[],[2245,23])). % 116.99/117.03 cnf(57513,plain, % 116.99/117.03 (P5(f4(x575131,x575132),f10(f4(x575133,x575132)))+~E(x575133,x575131)), % 116.99/117.03 inference(scs_inference,[],[2245,25])). % 116.99/117.03 cnf(57637,plain, % 116.99/117.03 (P5(f14(x576371,x576372),f10(f14(x576373,x576372)))+~E(x576373,x576371)), % 116.99/117.03 inference(scs_inference,[],[2245,27])). % 116.99/117.03 cnf(57761,plain, % 116.99/117.03 (P5(f13(x577611,x577612),f10(f13(x577613,x577612)))+~E(x577613,x577611)), % 116.99/117.03 inference(scs_inference,[],[2245,29])). % 116.99/117.03 cnf(57885,plain, % 116.99/117.03 (P5(f18(x578851,x578852),f10(f18(x578853,x578852)))+~E(x578853,x578851)), % 116.99/117.03 inference(scs_inference,[],[2245,31])). % 116.99/117.03 cnf(58009,plain, % 116.99/117.03 (~E(x580091,x580092)+P5(f9(x580091,x580093),f10(f9(x580092,x580093)))), % 116.99/117.03 inference(scs_inference,[],[2245,399])). % 116.99/117.03 cnf(58071,plain, % 116.99/117.03 (P5(f10(x580711),f10(f10(x580712)))+~E(x580711,x580712)), % 116.99/117.03 inference(scs_inference,[],[2245,766])). % 116.99/117.03 cnf(58505,plain, % 116.99/117.03 (P5(f20(x585051,x585052),f10(f20(x585053,x585052)))+~E(x585051,x585053)), % 116.99/117.03 inference(scs_inference,[],[2245,4609])). % 116.99/117.03 cnf(59435,plain, % 116.99/117.03 (~E(x594351,x594352)+P5(f9(x594353,x594351),f10(f9(x594353,x594352)))), % 116.99/117.03 inference(scs_inference,[],[2245,30863])). % 116.99/117.03 cnf(59497,plain, % 116.99/117.03 (~E(x594971,x594972)+P5(f2(x594971,x594973),f10(f2(x594972,x594973)))), % 116.99/117.03 inference(scs_inference,[],[2245,32115])). % 116.99/117.03 cnf(59559,plain, % 116.99/117.03 (~E(x595591,x595592)+P5(f2(x595593,x595591),f10(f2(x595593,x595592)))), % 116.99/117.03 inference(scs_inference,[],[2245,32376])). % 116.99/117.03 cnf(59621,plain, % 116.99/117.03 (~E(x596211,x596212)+P5(f21(x596211,x596213),f10(f21(x596212,x596213)))), % 116.99/117.03 inference(scs_inference,[],[2245,32629])). % 116.99/117.03 cnf(59683,plain, % 116.99/117.03 (~E(x596831,x596832)+P5(f21(x596833,x596831),f10(f21(x596833,x596832)))), % 116.99/117.03 inference(scs_inference,[],[2245,32872])). % 116.99/117.03 cnf(59745,plain, % 116.99/117.03 (~E(x597451,x597452)+P5(f11(x597451),f10(f11(x597452)))), % 116.99/117.03 inference(scs_inference,[],[2245,33125])). % 116.99/117.03 cnf(59807,plain, % 116.99/117.03 (~E(x598071,x598072)+P5(f3(x598071),f10(f3(x598072)))), % 116.99/117.03 inference(scs_inference,[],[2245,33386])). % 116.99/117.03 cnf(59869,plain, % 116.99/117.03 (~E(x598691,x598692)+P5(f20(x598693,x598691),f10(f20(x598693,x598692)))), % 116.99/117.03 inference(scs_inference,[],[2245,33639])). % 116.99/117.03 cnf(59931,plain, % 116.99/117.03 (~E(x599311,x599312)+P5(f16(x599311,x599313,x599314),f10(f16(x599312,x599313,x599314)))), % 116.99/117.03 inference(scs_inference,[],[2245,33900])). % 116.99/117.03 cnf(59993,plain, % 116.99/117.03 (~E(x599931,x599932)+P5(f16(x599933,x599931,x599934),f10(f16(x599933,x599932,x599934)))), % 116.99/117.03 inference(scs_inference,[],[2245,34153])). % 116.99/117.03 cnf(60055,plain, % 116.99/117.03 (~E(x600551,x600552)+P5(f16(x600553,x600554,x600551),f10(f16(x600553,x600554,x600552)))), % 116.99/117.03 inference(scs_inference,[],[2245,34414])). % 116.99/117.03 cnf(60117,plain, % 116.99/117.03 (~E(x601171,x601172)+P5(f12(x601171),f10(f12(x601172)))), % 116.99/117.03 inference(scs_inference,[],[2245,34651])). % 116.99/117.03 cnf(60179,plain, % 116.99/117.03 (~E(x601791,x601792)+P5(f22(x601791),f10(f22(x601792)))), % 116.99/117.03 inference(scs_inference,[],[2245,34904])). % 116.99/117.03 cnf(60241,plain, % 116.99/117.03 (~E(x602411,x602412)+P5(f17(x602411),f10(f17(x602412)))), % 116.99/117.03 inference(scs_inference,[],[2245,35181])). % 116.99/117.03 cnf(60303,plain, % 116.99/117.03 (~E(x603031,x603032)+P5(f19(x603031),f10(f19(x603032)))), % 116.99/117.03 inference(scs_inference,[],[2245,35458])). % 116.99/117.03 cnf(60365,plain, % 116.99/117.03 (~E(x603651,x603652)+P5(f15(x603651,x603653,x603654),f10(f15(x603652,x603653,x603654)))), % 116.99/117.03 inference(scs_inference,[],[2245,35735])). % 116.99/117.03 cnf(60427,plain, % 116.99/117.03 (~E(x604271,x604272)+P5(f15(x604273,x604271,x604274),f10(f15(x604273,x604272,x604274)))), % 116.99/117.03 inference(scs_inference,[],[2245,36012])). % 116.99/117.03 cnf(60489,plain, % 116.99/117.03 (~E(x604891,x604892)+P5(f15(x604893,x604894,x604891),f10(f15(x604893,x604894,x604892)))), % 116.99/117.03 inference(scs_inference,[],[2245,36289])). % 116.99/117.03 cnf(60551,plain, % 116.99/117.03 (~E(x605511,x605512)+P5(f4(x605511,x605513),f10(f4(x605512,x605513)))), % 116.99/117.03 inference(scs_inference,[],[2245,36566])). % 116.99/117.03 cnf(60613,plain, % 116.99/117.03 (~E(x606131,x606132)+P5(f4(x606133,x606131),f10(f4(x606133,x606132)))), % 116.99/117.03 inference(scs_inference,[],[2245,36843])). % 116.99/117.03 cnf(60675,plain, % 116.99/117.03 (~E(x606751,x606752)+P5(f14(x606751,x606753),f10(f14(x606752,x606753)))), % 116.99/117.03 inference(scs_inference,[],[2245,37120])). % 116.99/117.03 cnf(60737,plain, % 116.99/117.03 (~E(x607371,x607372)+P5(f14(x607373,x607371),f10(f14(x607373,x607372)))), % 116.99/117.03 inference(scs_inference,[],[2245,37397])). % 116.99/117.03 cnf(60799,plain, % 116.99/117.03 (~E(x607991,x607992)+P5(f13(x607991,x607993),f10(f13(x607992,x607993)))), % 116.99/117.03 inference(scs_inference,[],[2245,37674])). % 116.99/117.03 cnf(60861,plain, % 116.99/117.03 (~E(x608611,x608612)+P5(f13(x608613,x608611),f10(f13(x608613,x608612)))), % 116.99/117.03 inference(scs_inference,[],[2245,37951])). % 116.99/117.03 cnf(60923,plain, % 116.99/117.03 (~E(x609231,x609232)+P5(f18(x609231,x609233),f10(f18(x609232,x609233)))), % 116.99/117.03 inference(scs_inference,[],[2245,38228])). % 116.99/117.03 cnf(60985,plain, % 116.99/117.03 (~E(x609851,x609852)+P5(f18(x609853,x609851),f10(f18(x609853,x609852)))), % 116.99/117.03 inference(scs_inference,[],[2245,38505])). % 116.99/117.04 cnf(61399,plain, % 116.99/117.04 (P5(x613991,f10(x613992))+~E(f11(f10(x613992)),x613991)), % 116.99/117.04 inference(scs_inference,[],[54136,35])). % 116.99/117.04 cnf(64181,plain, % 116.99/117.04 (~E(x641811,f10(x641812))+P5(x641812,x641811)), % 116.99/117.04 inference(scs_inference,[],[2271,2])). % 116.99/117.04 cnf(65337,plain, % 116.99/117.04 (~E(x653371,x653372)+P5(x653373,x653372)+~E(f10(x653373),x653371)), % 116.99/117.04 inference(scs_inference,[],[2271,3])). % 116.99/117.04 cnf(69286,plain, % 116.99/117.04 (P4(x692861)+~E(x692861,f14(x692862,x692862))), % 116.99/117.04 inference(scs_inference,[],[49658,2])). % 116.99/117.04 cnf(69348,plain, % 116.99/117.04 (P4(f14(x693481,x693482))+~E(x693482,x693481)), % 116.99/117.04 inference(scs_inference,[],[49658,27])). % 116.99/117.04 cnf(69410,plain, % 116.99/117.04 (P4(f14(x694101,x694102))+~E(x694101,x694102)), % 116.99/117.04 inference(scs_inference,[],[49658,28])). % 116.99/117.04 cnf(69534,plain, % 116.99/117.04 (P4(f14(f10(x695341),f10(x695342)))+~E(x695341,x695342)), % 116.99/117.04 inference(scs_inference,[],[49658,5698])). % 116.99/117.04 cnf(69596,plain, % 116.99/117.04 (P4(f14(f2(x695961,x695962),f2(x695961,x695963)))+~E(x695962,x695963)), % 116.99/117.04 inference(scs_inference,[],[49658,40520])). % 116.99/117.04 cnf(69962,plain, % 116.99/117.04 (P4(x699621)+~E(x699622,x699621)+~E(f14(x699623,x699623),x699622)), % 116.99/117.04 inference(scs_inference,[],[49658,3])). % 116.99/117.04 cnf(73061,plain, % 116.99/117.04 (P4(f14(f2(x730611,x730612),f2(x730613,x730612)))+~E(x730613,x730611)), % 116.99/117.04 inference(scs_inference,[],[69348,6])). % 116.99/117.04 cnf(73185,plain, % 116.99/117.04 (P4(f14(f21(x731851,x731852),f21(x731851,x731853)))+~E(x731853,x731852)), % 116.99/117.04 inference(scs_inference,[],[69348,10])). % 116.99/117.04 cnf(73309,plain, % 116.99/117.04 (P4(f14(f3(x733091),f3(x733092)))+~E(x733092,x733091)), % 116.99/117.04 inference(scs_inference,[],[69348,12])). % 116.99/117.04 cnf(74301,plain, % 116.99/117.04 (P4(f14(f13(x743011,x743012),f13(x743013,x743012)))+~E(x743013,x743011)), % 116.99/117.04 inference(scs_inference,[],[69348,29])). % 116.99/117.04 cnf(74425,plain, % 116.99/117.04 (P4(f14(f18(x744251,x744252),f18(x744253,x744252)))+~E(x744253,x744251)), % 116.99/117.04 inference(scs_inference,[],[69348,31])). % 116.99/117.04 cnf(74549,plain, % 116.99/117.04 (~E(x745491,x745492)+P4(f14(f9(x745491,x745493),f9(x745492,x745493)))), % 116.99/117.04 inference(scs_inference,[],[69348,399])). % 116.99/117.04 cnf(74983,plain, % 116.99/117.04 (P4(f14(f20(x749831,x749832),f20(x749833,x749832)))+~E(x749831,x749833)), % 116.99/117.04 inference(scs_inference,[],[69348,4609])). % 116.99/117.04 cnf(75913,plain, % 116.99/117.04 (~E(x759131,x759132)+P4(f14(f9(x759133,x759131),f9(x759133,x759132)))), % 116.99/117.04 inference(scs_inference,[],[69348,30863])). % 116.99/117.04 cnf(75975,plain, % 116.99/117.04 (~E(x759751,x759752)+P4(f14(f2(x759751,x759753),f2(x759752,x759753)))), % 116.99/117.04 inference(scs_inference,[],[69348,32115])). % 116.99/117.04 cnf(76037,plain, % 116.99/117.04 (~E(x760371,x760372)+P4(f14(f21(x760371,x760373),f21(x760372,x760373)))), % 116.99/117.04 inference(scs_inference,[],[69348,32629])). % 116.99/117.04 cnf(76099,plain, % 116.99/117.04 (~E(x760991,x760992)+P4(f14(f21(x760993,x760991),f21(x760993,x760992)))), % 116.99/117.04 inference(scs_inference,[],[69348,32872])). % 116.99/117.04 cnf(76161,plain, % 116.99/117.04 (~E(x761611,x761612)+P4(f14(f11(x761611),f11(x761612)))), % 116.99/117.04 inference(scs_inference,[],[69348,33125])). % 116.99/117.04 cnf(76223,plain, % 116.99/117.04 (~E(x762231,x762232)+P4(f14(f3(x762231),f3(x762232)))), % 116.99/117.04 inference(scs_inference,[],[69348,33386])). % 116.99/117.04 cnf(76285,plain, % 116.99/117.04 (~E(x762851,x762852)+P4(f14(f20(x762853,x762851),f20(x762853,x762852)))), % 116.99/117.04 inference(scs_inference,[],[69348,33639])). % 116.99/117.04 cnf(76347,plain, % 116.99/117.04 (~E(x763471,x763472)+P4(f14(f16(x763471,x763473,x763474),f16(x763472,x763473,x763474)))), % 116.99/117.04 inference(scs_inference,[],[69348,33900])). % 116.99/117.04 cnf(76409,plain, % 116.99/117.04 (~E(x764091,x764092)+P4(f14(f16(x764093,x764091,x764094),f16(x764093,x764092,x764094)))), % 116.99/117.04 inference(scs_inference,[],[69348,34153])). % 116.99/117.04 cnf(76471,plain, % 116.99/117.04 (~E(x764711,x764712)+P4(f14(f16(x764713,x764714,x764711),f16(x764713,x764714,x764712)))), % 116.99/117.04 inference(scs_inference,[],[69348,34414])). % 116.99/117.04 cnf(76533,plain, % 116.99/117.04 (~E(x765331,x765332)+P4(f14(f12(x765331),f12(x765332)))), % 116.99/117.04 inference(scs_inference,[],[69348,34651])). % 116.99/117.04 cnf(76595,plain, % 116.99/117.04 (~E(x765951,x765952)+P4(f14(f22(x765951),f22(x765952)))), % 116.99/117.04 inference(scs_inference,[],[69348,34904])). % 116.99/117.04 cnf(76657,plain, % 116.99/117.04 (~E(x766571,x766572)+P4(f14(f17(x766571),f17(x766572)))), % 116.99/117.04 inference(scs_inference,[],[69348,35181])). % 116.99/117.04 cnf(76719,plain, % 116.99/117.04 (~E(x767191,x767192)+P4(f14(f19(x767191),f19(x767192)))), % 116.99/117.04 inference(scs_inference,[],[69348,35458])). % 116.99/117.04 cnf(76781,plain, % 116.99/117.04 (~E(x767811,x767812)+P4(f14(f15(x767811,x767813,x767814),f15(x767812,x767813,x767814)))), % 116.99/117.04 inference(scs_inference,[],[69348,35735])). % 116.99/117.04 cnf(76843,plain, % 116.99/117.04 (~E(x768431,x768432)+P4(f14(f15(x768433,x768431,x768434),f15(x768433,x768432,x768434)))), % 116.99/117.04 inference(scs_inference,[],[69348,36012])). % 116.99/117.04 cnf(76905,plain, % 116.99/117.04 (~E(x769051,x769052)+P4(f14(f15(x769053,x769054,x769051),f15(x769053,x769054,x769052)))), % 116.99/117.04 inference(scs_inference,[],[69348,36289])). % 116.99/117.04 cnf(76967,plain, % 116.99/117.04 (~E(x769671,x769672)+P4(f14(f4(x769671,x769673),f4(x769672,x769673)))), % 116.99/117.04 inference(scs_inference,[],[69348,36566])). % 116.99/117.04 cnf(77029,plain, % 116.99/117.04 (~E(x770291,x770292)+P4(f14(f4(x770293,x770291),f4(x770293,x770292)))), % 116.99/117.04 inference(scs_inference,[],[69348,36843])). % 116.99/117.04 cnf(77091,plain, % 116.99/117.04 (~E(x770911,x770912)+P4(f14(f14(x770911,x770913),f14(x770912,x770913)))), % 116.99/117.04 inference(scs_inference,[],[69348,37120])). % 116.99/117.04 cnf(77153,plain, % 116.99/117.04 (~E(x771531,x771532)+P4(f14(f14(x771533,x771531),f14(x771533,x771532)))), % 116.99/117.04 inference(scs_inference,[],[69348,37397])). % 116.99/117.04 cnf(77215,plain, % 116.99/117.04 (~E(x772151,x772152)+P4(f14(f13(x772151,x772153),f13(x772152,x772153)))), % 116.99/117.04 inference(scs_inference,[],[69348,37674])). % 116.99/117.04 cnf(77277,plain, % 116.99/117.04 (~E(x772771,x772772)+P4(f14(f13(x772773,x772771),f13(x772773,x772772)))), % 116.99/117.04 inference(scs_inference,[],[69348,37951])). % 116.99/117.04 cnf(77339,plain, % 116.99/117.04 (~E(x773391,x773392)+P4(f14(f18(x773391,x773393),f18(x773392,x773393)))), % 116.99/117.04 inference(scs_inference,[],[69348,38228])). % 116.99/117.04 cnf(77401,plain, % 116.99/117.04 (~E(x774011,x774012)+P4(f14(f18(x774013,x774011),f18(x774013,x774012)))), % 116.99/117.04 inference(scs_inference,[],[69348,38505])). % 116.99/117.04 cnf(79191,plain, % 116.99/117.04 (P5(f13(a1,f2(a6,a7)),a1)), % 116.99/117.04 inference(scs_inference,[],[47,45,65,115])). % 116.99/117.04 cnf(79201,plain, % 116.99/117.04 (P1(f12(x792011),f19(f10(x792011)))), % 116.99/117.04 inference(scs_inference,[],[1733,45,68,50273])). % 116.99/117.04 cnf(79207,plain, % 116.99/117.04 (P1(a8,f22(f2(a6,a7)))), % 116.99/117.04 inference(scs_inference,[],[46,45,80,115])). % 116.99/117.04 cnf(79209,plain, % 116.99/117.04 (~P5(x792091,f2(x792091,x792091))+E(f21(f15(x792091,x792091,x792091),f16(x792091,x792091,x792091)),x792091)), % 116.99/117.04 inference(scs_inference,[],[45,87])). % 116.99/117.04 cnf(79212,plain, % 116.99/117.04 (~P2(a1)+~P1(f13(a1,f2(a6,a7)),a5)), % 116.99/117.04 inference(scs_inference,[],[79191,45,58])). % 116.99/117.04 cnf(79213,plain, % 116.99/117.04 (P1(x792131,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79215,plain, % 116.99/117.04 (P5(f11(a1),a1)+~P1(f13(a1,f2(a6,a7)),a5)), % 116.99/117.04 inference(scs_inference,[],[79191,45,79213,58,54])). % 116.99/117.04 cnf(79219,plain, % 116.99/117.04 (~P2(a1)), % 116.99/117.04 inference(scs_inference,[],[45,79212])). % 116.99/117.04 cnf(79220,plain, % 116.99/117.04 (P1(x792201,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79221,plain, % 116.99/117.04 (P5(f11(a1),a1)), % 116.99/117.04 inference(scs_inference,[],[45,79220,79212,79215])). % 116.99/117.04 cnf(79222,plain, % 116.99/117.04 (P1(x792221,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79225,plain, % 116.99/117.04 (P1(f17(a1),f19(a1))), % 116.99/117.04 inference(scs_inference,[],[45,79220,79222,79212,79215,72,57])). % 116.99/117.04 cnf(79237,plain, % 116.99/117.04 (~P5(f13(a1,f2(a6,a7)),f2(a6,a7))+~P1(f2(a6,a7),a5)), % 116.99/117.04 inference(scs_inference,[],[47,45,73])). % 116.99/117.04 cnf(79243,plain, % 116.99/117.04 (~P5(f13(a1,f2(a6,a7)),f2(a6,a7))), % 116.99/117.04 inference(scs_inference,[],[45,79237])). % 116.99/117.04 cnf(79250,plain, % 116.99/117.04 (~P5(x792501,f2(a6,a7))+~E(x792501,f13(a1,f2(a6,a7)))), % 116.99/117.04 inference(scs_inference,[],[79243,35])). % 116.99/117.04 cnf(79265,plain, % 116.99/117.04 (P5(f17(a1),a1)+~P1(a1,a5)), % 116.99/117.04 inference(scs_inference,[],[79225,79219,45,62])). % 116.99/117.04 cnf(79268,plain, % 116.99/117.04 (P5(f17(a1),a1)), % 116.99/117.04 inference(scs_inference,[],[45,79265])). % 116.99/117.04 cnf(79269,plain, % 116.99/117.04 (P1(x792691,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79270,plain, % 116.99/117.04 (P5(f12(x792701),f10(x792701))+~P1(f10(x792701),a5)), % 116.99/117.04 inference(scs_inference,[],[79201,49597,45,79269,79265,62])). % 116.99/117.04 cnf(79275,plain, % 116.99/117.04 (P5(f12(x792751),f10(x792751))), % 116.99/117.04 inference(scs_inference,[],[45,79270])). % 116.99/117.04 cnf(79289,plain, % 116.99/117.04 (P5(f17(a1),a8)+~P1(a8,a5)+~P1(f17(a1),a5)), % 116.99/117.04 inference(scs_inference,[],[44,79268,45,75])). % 116.99/117.04 cnf(79291,plain, % 116.99/117.04 (P1(x792911,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79296,plain, % 116.99/117.04 (P5(f17(a1),a8)), % 116.99/117.04 inference(scs_inference,[],[79207,45,79291,79289,34,33,79209,50273])). % 116.99/117.04 cnf(79302,plain, % 116.99/117.04 (~P2(a8)+~P1(f17(a1),a5)), % 116.99/117.04 inference(scs_inference,[],[79296,45,58])). % 116.99/117.04 cnf(79305,plain, % 116.99/117.04 (~P2(a8)), % 116.99/117.04 inference(scs_inference,[],[45,79302])). % 116.99/117.04 cnf(79306,plain, % 116.99/117.04 (P1(x793061,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79308,plain, % 116.99/117.04 (P1(x793081,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79311,plain, % 116.99/117.04 (P1(x793111,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79313,plain, % 116.99/117.04 (P5(f11(a8),a8)), % 116.99/117.04 inference(scs_inference,[],[79296,45,79306,79308,79311,79302,61,57,54])). % 116.99/117.04 cnf(79344,plain, % 116.99/117.04 (~P3(a8,f2(a6,a7))+~P1(f2(a6,a7),a5)+~P1(a8,a5)), % 116.99/117.04 inference(scs_inference,[],[44,47,45,74])). % 116.99/117.04 cnf(79346,plain, % 116.99/117.04 (P1(x793461,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79347,plain, % 116.99/117.04 (~P3(a8,f2(a6,a7))), % 116.99/117.04 inference(scs_inference,[],[45,79346,79344,34])). % 116.99/117.04 cnf(79355,plain, % 116.99/117.04 (P5(f13(a8,f2(a6,a7)),a8)), % 116.99/117.04 inference(scs_inference,[],[79347,45,65,115])). % 116.99/117.04 cnf(79358,plain, % 116.99/117.04 (~P5(f13(a8,f2(a6,a7)),f2(a6,a7))+~P1(f2(a6,a7),a5)), % 116.99/117.04 inference(scs_inference,[],[79347,45,73])). % 116.99/117.04 cnf(79359,plain, % 116.99/117.04 (P1(x793591,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79361,plain, % 116.99/117.04 (P1(f13(a8,f2(a6,a7)),f19(a8))+~P1(a8,a5)), % 116.99/117.04 inference(scs_inference,[],[79355,79347,79305,45,79359,73,61])). % 116.99/117.04 cnf(79365,plain, % 116.99/117.04 (P1(x793651,a5)), % 116.99/117.04 inference(rename_variables,[],[45])). % 116.99/117.04 cnf(79366,plain, % 116.99/117.04 (~P5(f13(a8,f2(a6,a7)),f2(a6,a7))), % 116.99/117.04 inference(scs_inference,[],[45,79365,79361,79358])). % 117.11/117.04 cnf(79367,plain, % 117.11/117.04 (P1(x793671,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79368,plain, % 117.11/117.04 (P1(f13(a1,f2(a6,a7)),f19(a1))+~P1(a1,a5)), % 117.11/117.04 inference(scs_inference,[],[79191,79219,45,79365,79367,79361,79358,61])). % 117.11/117.04 cnf(79371,plain, % 117.11/117.04 (~P5(x793711,f2(a6,a7))+~E(x793711,f13(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79191,79219,45,79365,79367,79361,79358,61,35])). % 117.11/117.04 cnf(79373,plain, % 117.11/117.04 (P1(f13(a1,f2(a6,a7)),f19(a1))), % 117.11/117.04 inference(scs_inference,[],[45,79368])). % 117.11/117.04 cnf(79374,plain, % 117.11/117.04 (P1(x793741,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79377,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+~P1(f13(a8,f2(a6,a7)),a5)+~P5(a8,f10(f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79366,79355,45,79374,79368,77])). % 117.11/117.04 cnf(79380,plain, % 117.11/117.04 (~P5(a8,f10(f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[45,79377,50273])). % 117.11/117.04 cnf(79386,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+P5(f18(a8,f2(a6,a7)),a8)), % 117.11/117.04 inference(scs_inference,[],[79380,2244,45,36,65337,67])). % 117.11/117.04 cnf(79389,plain, % 117.11/117.04 (P5(f18(a8,f2(a6,a7)),a8)), % 117.11/117.04 inference(scs_inference,[],[45,79386])). % 117.11/117.04 cnf(79391,plain, % 117.11/117.04 (~E(f12(f2(a6,a7)),a8)), % 117.11/117.04 inference(scs_inference,[],[79275,79380,45,79386,35])). % 117.11/117.04 cnf(79413,plain, % 117.11/117.04 (P5(f11(a1),a8)+~P1(a8,a5)+~P1(f11(a1),a5)), % 117.11/117.04 inference(scs_inference,[],[44,79221,45,75])). % 117.11/117.04 cnf(79415,plain, % 117.11/117.04 (P1(x794151,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79420,plain, % 117.11/117.04 (P5(f11(a1),a8)), % 117.11/117.04 inference(scs_inference,[],[79207,45,79415,79413,34,33,79209,115])). % 117.11/117.04 cnf(79424,plain, % 117.11/117.04 (P1(f11(a1),f19(a8))+~P1(a8,a5)), % 117.11/117.04 inference(scs_inference,[],[79420,79305,45,61])). % 117.11/117.04 cnf(79429,plain, % 117.11/117.04 (P1(x794291,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79433,plain, % 117.11/117.04 (~P5(f13(a8,f2(a6,a7)),f12(f2(a6,a7)))+~P1(f13(a8,f2(a6,a7)),a5)+~P1(f12(f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[79275,79366,45,79429,79424,77])). % 117.11/117.04 cnf(79436,plain, % 117.11/117.04 (~P5(f13(a8,f2(a6,a7)),f12(f2(a6,a7)))+~P1(f12(f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[45,79433])). % 117.11/117.04 cnf(79444,plain, % 117.11/117.04 (~P5(f13(a8,f2(a6,a7)),f12(f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[45,79436])). % 117.11/117.04 cnf(79454,plain, % 117.11/117.04 (~P4(a8)+~P1(f11(a1),a5)+E(f21(f20(a8,f11(a1)),f4(a8,f11(a1))),f11(a1))), % 117.11/117.04 inference(scs_inference,[],[79420,45,78])). % 117.11/117.04 cnf(79456,plain, % 117.11/117.04 (E(f21(f20(a8,f11(a1)),f4(a8,f11(a1))),f11(a1))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,79454])). % 117.11/117.04 cnf(79459,plain, % 117.11/117.04 (~P1(f10(a8),a5)+~P1(a8,a5)+~P5(f10(a8),f10(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[79380,2244,45,77])). % 117.11/117.04 cnf(79462,plain, % 117.11/117.04 (~P1(f10(a8),a5)+~P5(f10(a8),f10(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[45,79459])). % 117.11/117.04 cnf(79466,plain, % 117.11/117.04 (~P5(f10(a8),f10(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[45,79462])). % 117.11/117.04 cnf(79471,plain, % 117.11/117.04 (P1(x794711,f19(f10(x794711)))+~P1(f10(x794711),a5)), % 117.11/117.04 inference(scs_inference,[],[2244,49597,45,61])). % 117.11/117.04 cnf(79478,plain, % 117.11/117.04 (P1(x794781,f19(f10(x794781)))), % 117.11/117.04 inference(scs_inference,[],[45,79471])). % 117.11/117.04 cnf(79479,plain, % 117.11/117.04 (P1(x794791,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79480,plain, % 117.11/117.04 (P1(x794801,f22(x794801))), % 117.11/117.04 inference(scs_inference,[],[45,79479,79471,72])). % 117.11/117.04 cnf(79481,plain, % 117.11/117.04 (P1(x794811,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79482,plain, % 117.11/117.04 (P1(x794821,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79484,plain, % 117.11/117.04 (P1(f14(x794841,x794842),f9(x794842,x794841))), % 117.11/117.04 inference(scs_inference,[],[45,79479,79482,79481,79471,72,69])). % 117.11/117.04 cnf(79486,plain, % 117.11/117.04 (P5(f16(x794861,x794861,x794862),x794861)+~P5(x794862,f2(x794861,x794861))), % 117.11/117.04 inference(scs_inference,[],[45,79479,79482,79481,79471,72,69,86])). % 117.11/117.04 cnf(79488,plain, % 117.11/117.04 (~P5(f18(a8,f2(a6,a7)),f2(a6,a7))), % 117.11/117.04 inference(scs_inference,[],[79380,45,79479,79482,79481,79471,72,69,86,76])). % 117.11/117.04 cnf(79489,plain, % 117.11/117.04 (P1(x794891,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79490,plain, % 117.11/117.04 (P1(x794901,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79492,plain, % 117.11/117.04 (~P5(x794921,f2(x794922,x794921))+E(f21(f15(x794922,x794921,x794921),f16(x794922,x794921,x794921)),x794921)), % 117.11/117.04 inference(scs_inference,[],[79380,45,79479,79482,79490,79481,79489,79471,72,69,86,76,87])). % 117.11/117.04 cnf(79496,plain, % 117.11/117.04 (P1(f2(x794961,x794961),f9(x794961,x794961))), % 117.11/117.04 inference(scs_inference,[],[79480,45,81])). % 117.11/117.04 cnf(79497,plain, % 117.11/117.04 (P1(x794971,f22(x794971))), % 117.11/117.04 inference(rename_variables,[],[79480])). % 117.11/117.04 cnf(79499,plain, % 117.11/117.04 (P4(f2(x794991,x794991))), % 117.11/117.04 inference(scs_inference,[],[79480,79497,45,81,79])). % 117.11/117.04 cnf(79502,plain, % 117.11/117.04 (~P5(x795021,f2(a6,a7))+~E(x795021,f18(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79480,79497,79488,45,81,79,35])). % 117.11/117.04 cnf(79513,plain, % 117.11/117.04 (P1(x795131,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79515,plain, % 117.11/117.04 (P5(f21(f11(a1),f11(a1)),f2(a8,a8))+~P1(f21(f11(a1),f11(a1)),a5)+~P1(a8,a5)), % 117.11/117.04 inference(scs_inference,[],[79420,79488,79389,45,79513,88])). % 117.11/117.04 cnf(79516,plain, % 117.11/117.04 (P5(f21(f11(a1),f11(a1)),f2(a8,a8))+~P1(f21(f11(a1),f11(a1)),a5)), % 117.11/117.04 inference(scs_inference,[],[45,79515])). % 117.11/117.04 cnf(79520,plain, % 117.11/117.04 (P5(f21(f11(a1),f11(a1)),f2(a8,a8))), % 117.11/117.04 inference(scs_inference,[],[45,79516])). % 117.11/117.04 cnf(79521,plain, % 117.11/117.04 (P1(x795211,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79522,plain, % 117.11/117.04 (~P2(f2(a8,a8))+~P1(f21(f11(a1),f11(a1)),a5)), % 117.11/117.04 inference(scs_inference,[],[45,79521,79516,58])). % 117.11/117.04 cnf(79526,plain, % 117.11/117.04 (~P2(f2(a8,a8))), % 117.11/117.04 inference(scs_inference,[],[45,79522])). % 117.11/117.04 cnf(79678,plain, % 117.11/117.04 (~P1(a1,a5)+~P1(f13(a1,f2(a6,a7)),a5)+~P5(a1,f10(f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79191,79243,45,77])). % 117.11/117.04 cnf(79680,plain, % 117.11/117.04 (P1(x796801,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79686,plain, % 117.11/117.04 (~P5(a1,f10(f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79478,45,79680,79678,34,33,79492,50273])). % 117.11/117.04 cnf(79694,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+P5(f18(a1,f2(a6,a7)),a1)), % 117.11/117.04 inference(scs_inference,[],[79686,79275,2244,45,35,36,67])). % 117.11/117.04 cnf(79705,plain, % 117.11/117.04 (P5(f18(a1,f2(a6,a7)),a1)), % 117.11/117.04 inference(scs_inference,[],[45,79694])). % 117.11/117.04 cnf(79739,plain, % 117.11/117.04 (P1(f18(a1,f2(a6,a7)),f19(a1))+~P1(a1,a5)), % 117.11/117.04 inference(scs_inference,[],[79705,79219,45,61])). % 117.11/117.04 cnf(79740,plain, % 117.11/117.04 (P1(x797401,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79743,plain, % 117.11/117.04 (P1(x797431,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79745,plain, % 117.11/117.04 (P5(f18(a1,f2(a6,a7)),a8)+~P1(f18(a1,f2(a6,a7)),a5)+~P1(a1,a5)), % 117.11/117.04 inference(scs_inference,[],[79705,79219,79686,49907,44,45,79740,79743,75])). % 117.11/117.04 cnf(79748,plain, % 117.11/117.04 (P1(x797481,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(79751,plain, % 117.11/117.04 (P5(f18(a1,f2(a6,a7)),a8)), % 117.11/117.04 inference(scs_inference,[],[45,79748,79739,79745,50273])). % 117.11/117.04 cnf(80567,plain, % 117.11/117.04 (~P4(a8)+~P1(f13(a8,f2(a6,a7)),a5)+E(f21(f20(a8,f13(a8,f2(a6,a7))),f4(a8,f13(a8,f2(a6,a7)))),f13(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79355,45,78])). % 117.11/117.04 cnf(80568,plain, % 117.11/117.04 (E(f21(f20(a8,f13(a8,f2(a6,a7))),f4(a8,f13(a8,f2(a6,a7)))),f13(a8,f2(a6,a7)))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,80567])). % 117.11/117.04 cnf(80590,plain, % 117.11/117.04 (~P4(a8)+~P1(a8,a5)+E(f21(f20(a8,f18(a1,f2(a6,a7))),f4(a8,f18(a1,f2(a6,a7)))),f18(a1,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79751,45,78])). % 117.11/117.04 cnf(80592,plain, % 117.11/117.04 (P5(f13(a1,f2(a6,a7)),a8)+~P1(a8,a5)+~P1(f13(a1,f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[79191,44,45,75])). % 117.11/117.04 cnf(80593,plain, % 117.11/117.04 (E(f21(f20(a8,f18(a1,f2(a6,a7))),f4(a8,f18(a1,f2(a6,a7)))),f18(a1,f2(a6,a7)))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,80590])). % 117.11/117.04 cnf(80595,plain, % 117.11/117.04 (P1(x805951,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(80598,plain, % 117.11/117.04 (P5(f13(a1,f2(a6,a7)),a8)), % 117.11/117.04 inference(scs_inference,[],[79373,45,80595,80592,34,33,50273])). % 117.11/117.04 cnf(80603,plain, % 117.11/117.04 (P1(x806031,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(80606,plain, % 117.11/117.04 (~P4(a8)+~P1(f13(a1,f2(a6,a7)),a5)+E(f21(f20(a8,f13(a1,f2(a6,a7))),f4(a8,f13(a1,f2(a6,a7)))),f13(a1,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[80598,79305,45,80603,78])). % 117.11/117.04 cnf(80612,plain, % 117.11/117.04 (E(f21(f20(a8,f13(a1,f2(a6,a7))),f4(a8,f13(a1,f2(a6,a7)))),f13(a1,f2(a6,a7)))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,80606])). % 117.11/117.04 cnf(80723,plain, % 117.11/117.04 (P5(f21(f13(a1,f2(a6,a7)),f13(a1,f2(a6,a7))),f2(a8,a8))+~P1(f13(a1,f2(a6,a7)),a5)+~P1(f21(f13(a1,f2(a6,a7)),f13(a1,f2(a6,a7))),a5)), % 117.11/117.04 inference(scs_inference,[],[80598,45,88])). % 117.11/117.04 cnf(80728,plain, % 117.11/117.04 (P5(f21(f13(a1,f2(a6,a7)),f13(a1,f2(a6,a7))),f2(a8,a8))+~P1(f21(f13(a1,f2(a6,a7)),f13(a1,f2(a6,a7))),a5)), % 117.11/117.04 inference(scs_inference,[],[45,80723])). % 117.11/117.04 cnf(80737,plain, % 117.11/117.04 (P5(f21(f13(a1,f2(a6,a7)),f13(a1,f2(a6,a7))),f2(a8,a8))), % 117.11/117.04 inference(scs_inference,[],[45,80728])). % 117.11/117.04 cnf(80776,plain, % 117.11/117.04 (~P4(a8)+~P1(f11(a8),a5)+E(f21(f20(a8,f11(a8)),f4(a8,f11(a8))),f11(a8))), % 117.11/117.04 inference(scs_inference,[],[79313,45,78])). % 117.11/117.04 cnf(80780,plain, % 117.11/117.04 (E(f21(f20(a8,f11(a8)),f4(a8,f11(a8))),f11(a8))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,80776])). % 117.11/117.04 cnf(84095,plain, % 117.11/117.04 (P5(x840951,f10(x840951))), % 117.11/117.04 inference(rename_variables,[],[2244])). % 117.11/117.04 cnf(84096,plain, % 117.11/117.04 (P1(x840961,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(84097,plain, % 117.11/117.04 (P1(x840971,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(84098,plain, % 117.11/117.04 (P5(x840981,f10(x840981))), % 117.11/117.04 inference(rename_variables,[],[2244])). % 117.11/117.04 cnf(84101,plain, % 117.11/117.04 (P5(f21(x841011,x841011),f2(f10(x841011),f10(x841011)))+~P1(f21(x841011,x841011),a5)+~P1(f10(x841011),a5)), % 117.11/117.04 inference(scs_inference,[],[2244,84095,84098,79380,45,84096,84097,88])). % 117.11/117.04 cnf(84102,plain, % 117.11/117.04 (P5(f21(x841021,x841021),f2(f10(x841021),f10(x841021)))+~P1(f10(x841021),a5)), % 117.11/117.04 inference(scs_inference,[],[45,84101])). % 117.11/117.04 cnf(84110,plain, % 117.11/117.04 (P5(f21(x841101,x841101),f2(f10(x841101),f10(x841101)))), % 117.11/117.04 inference(scs_inference,[],[45,84102])). % 117.11/117.04 cnf(84120,plain, % 117.11/117.04 (~P2(f2(f10(x841201),f10(x841201)))+~P1(f21(x841201,x841201),a5)), % 117.11/117.04 inference(scs_inference,[],[84110,45,58])). % 117.11/117.04 cnf(84127,plain, % 117.11/117.04 (~P2(f2(f10(x841271),f10(x841271)))), % 117.11/117.04 inference(scs_inference,[],[45,84120])). % 117.11/117.04 cnf(85763,plain, % 117.11/117.04 (~P4(a8)+~P1(a8,a5)+E(f21(f20(a8,f18(a8,f2(a6,a7))),f4(a8,f18(a8,f2(a6,a7)))),f18(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[79389,45,78])). % 117.11/117.04 cnf(85766,plain, % 117.11/117.04 (E(f21(f20(a8,f18(a8,f2(a6,a7))),f4(a8,f18(a8,f2(a6,a7)))),f18(a8,f2(a6,a7)))+~P4(a8)), % 117.11/117.04 inference(scs_inference,[],[45,85763])). % 117.11/117.04 cnf(87222,plain, % 117.11/117.04 (P5(f21(f11(a1),f11(a1)),f2(a1,a1))+~P1(f11(a1),a5)+~P1(f21(f11(a1),f11(a1)),a5)), % 117.11/117.04 inference(scs_inference,[],[79221,45,88])). % 117.11/117.04 cnf(87225,plain, % 117.11/117.04 (~E(a5,x872251)+P5(f21(f11(a1),f11(a1)),f2(a1,a1))), % 117.11/117.04 inference(scs_inference,[],[45,87222,51146])). % 117.11/117.04 cnf(87235,plain, % 117.11/117.04 (P5(f21(f11(a1),f11(a1)),f2(a1,a1))), % 117.11/117.04 inference(equality_inference,[],[87225])). % 117.11/117.04 cnf(88908,plain, % 117.11/117.04 (P5(x889081,f2(f10(x889082),f10(x889082)))+~E(f21(x889082,x889082),x889081)), % 117.11/117.04 inference(scs_inference,[],[84110,35])). % 117.11/117.04 cnf(88982,plain, % 117.11/117.04 (P5(x889821,f2(a1,a1))+~E(f21(f11(a1),f11(a1)),x889821)), % 117.11/117.04 inference(scs_inference,[],[87235,35])). % 117.11/117.04 cnf(89205,plain, % 117.11/117.04 (P5(x892051,f2(a8,a8))+~E(f21(f11(a1),f11(a1)),x892051)), % 117.11/117.04 inference(scs_inference,[],[79520,35])). % 117.11/117.04 cnf(89217,plain, % 117.11/117.04 (P1(f2(x892171,x892171),x892172)+~E(f9(x892171,x892171),x892172)), % 117.11/117.04 inference(scs_inference,[],[79496,34])). % 117.11/117.04 cnf(89393,plain, % 117.11/117.04 (P5(x893931,a8)+~E(f11(a1),x893931)), % 117.11/117.04 inference(scs_inference,[],[79420,35])). % 117.11/117.04 cnf(89395,plain, % 117.11/117.04 (P1(x893951,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(89397,plain, % 117.11/117.04 (~E(f11(a1),x893971)+~P1(f2(a6,a7),a5)+P1(a8,f19(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[79207,79347,79420,45,89395,35,68])). % 117.11/117.04 cnf(89399,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+P1(a8,f19(f10(f2(a6,a7))))), % 117.11/117.04 inference(equality_inference,[],[89397])). % 117.11/117.04 cnf(89400,plain, % 117.11/117.04 (P1(a8,f19(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[45,89399])). % 117.11/117.04 cnf(89412,plain, % 117.11/117.04 (P5(f18(a1,f2(a6,a7)),x894121)+~E(a8,x894121)), % 117.11/117.04 inference(scs_inference,[],[79751,36])). % 117.11/117.04 cnf(89503,plain, % 117.11/117.04 (P1(f14(x895031,x895032),x895033)+~E(f9(x895032,x895031),x895033)), % 117.11/117.04 inference(scs_inference,[],[79484,34])). % 117.11/117.04 cnf(89525,plain, % 117.11/117.04 (P5(x895251,a1)+~E(f11(a1),x895251)), % 117.11/117.04 inference(scs_inference,[],[79221,35])). % 117.11/117.04 cnf(89681,plain, % 117.11/117.04 (P5(f18(a1,f2(a6,a7)),x896811)+~E(a1,x896811)), % 117.11/117.04 inference(scs_inference,[],[79705,36])). % 117.11/117.04 cnf(89787,plain, % 117.11/117.04 (P1(x897871,x897872)+~E(f19(f10(x897871)),x897872)), % 117.11/117.04 inference(scs_inference,[],[79478,34])). % 117.11/117.04 cnf(89848,plain, % 117.11/117.04 (P1(x898481,x898482)+~E(f22(x898481),x898482)), % 117.11/117.04 inference(scs_inference,[],[79480,34])). % 117.11/117.04 cnf(91461,plain, % 117.11/117.04 (P1(x914611,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(91462,plain, % 117.11/117.04 (P1(x914621,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(91463,plain, % 117.11/117.04 (P1(x914631,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(91464,plain, % 117.11/117.04 (P5(x914641,f2(f10(x914642),f10(x914642)))+~E(x914641,f21(x914642,x914642))), % 117.11/117.04 inference(scs_inference,[],[2244,45,91463,91462,91461,88,82])). % 117.11/117.04 cnf(91549,plain, % 117.11/117.04 (P5(x915491,f10(x915491))), % 117.11/117.04 inference(rename_variables,[],[2244])). % 117.11/117.04 cnf(91550,plain, % 117.11/117.04 (P1(x915501,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(91553,plain, % 117.11/117.04 (~P3(f10(f13(a8,f2(a6,a7))),f2(a6,a7))+~P1(f2(a6,a7),a5)+~P1(f13(a8,f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[2244,91549,45,91550,79366,75])). % 117.11/117.04 cnf(91566,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+~P3(f10(f13(a8,f2(a6,a7))),f2(a6,a7))), % 117.11/117.04 inference(scs_inference,[],[45,91553])). % 117.11/117.04 cnf(91572,plain, % 117.11/117.04 (~P3(f10(f13(a8,f2(a6,a7))),f2(a6,a7))), % 117.11/117.04 inference(scs_inference,[],[45,91566])). % 117.11/117.04 cnf(93055,plain, % 117.11/117.04 (~P5(f18(a1,f2(a6,a7)),f2(a6,a7))+~P1(f2(a6,a7),a5)), % 117.11/117.04 inference(scs_inference,[],[45,79686,76])). % 117.11/117.04 cnf(93061,plain, % 117.11/117.04 (~P5(f18(a1,f2(a6,a7)),f2(a6,a7))), % 117.11/117.04 inference(scs_inference,[],[45,93055])). % 117.11/117.04 cnf(93063,plain, % 117.11/117.04 (~P5(x930631,f2(a6,a7))+~E(x930631,f18(a1,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[45,93055,35])). % 117.11/117.04 cnf(93073,plain, % 117.11/117.04 (P1(x930731,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(93076,plain, % 117.11/117.04 (~P5(f18(a1,f2(a6,a7)),f11(f10(f2(a6,a7))))+~P1(f2(a6,a7),a5)+~P1(f18(a1,f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[93061,44,79705,54136,45,93073,77])). % 117.11/117.04 cnf(93083,plain, % 117.11/117.04 (~P1(f2(a6,a7),a5)+~P5(f18(a1,f2(a6,a7)),f11(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[45,93076])). % 117.11/117.04 cnf(93092,plain, % 117.11/117.04 (~P5(f18(a1,f2(a6,a7)),f11(f10(f2(a6,a7))))), % 117.11/117.04 inference(scs_inference,[],[45,93083])). % 117.11/117.04 cnf(93269,plain, % 117.11/117.04 (~E(a5,x932691)+P4(a8)), % 117.11/117.04 inference(scs_inference,[],[79391,79207,45,79,89848,89787,3,51146])). % 117.11/117.04 cnf(93271,plain, % 117.11/117.04 (P4(a8)), % 117.11/117.04 inference(equality_inference,[],[93269])). % 117.11/117.04 cnf(93273,plain, % 117.11/117.04 (E(f21(f20(a8,f11(a1)),f4(a8,f11(a1))),f11(a1))), % 117.11/117.04 inference(scs_inference,[],[93271,79456])). % 117.11/117.04 cnf(93274,plain, % 117.11/117.04 (E(f21(f20(a8,f13(a8,f2(a6,a7))),f4(a8,f13(a8,f2(a6,a7)))),f13(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[93271,80568])). % 117.11/117.04 cnf(93275,plain, % 117.11/117.04 (E(f21(f20(a8,f18(a1,f2(a6,a7))),f4(a8,f18(a1,f2(a6,a7)))),f18(a1,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[93271,80593])). % 117.11/117.04 cnf(93276,plain, % 117.11/117.04 (E(f21(f20(a8,f13(a1,f2(a6,a7))),f4(a8,f13(a1,f2(a6,a7)))),f13(a1,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[93271,80612])). % 117.11/117.04 cnf(93278,plain, % 117.11/117.04 (E(f21(f20(a8,f11(a8)),f4(a8,f11(a8))),f11(a8))), % 117.11/117.04 inference(scs_inference,[],[93271,80780])). % 117.11/117.04 cnf(93279,plain, % 117.11/117.04 (E(f21(f20(a8,f18(a8,f2(a6,a7))),f4(a8,f18(a8,f2(a6,a7)))),f18(a8,f2(a6,a7)))), % 117.11/117.04 inference(scs_inference,[],[93271,85766])). % 117.11/117.04 cnf(94676,plain, % 117.11/117.04 (P1(x946761,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(94679,plain, % 117.11/117.04 (P3(x946791,x946791)), % 117.11/117.04 inference(rename_variables,[],[89])). % 117.11/117.04 cnf(94784,plain, % 117.11/117.04 (P1(x947841,a5)), % 117.11/117.04 inference(rename_variables,[],[45])). % 117.11/117.04 cnf(94786,plain, % 117.11/117.04 (~P1(f10(f2(a6,a7)),a5)), % 117.11/117.04 inference(scs_inference,[],[79444,14335,91572,89400,79466,80737,93273,93278,93092,93276,93275,93274,93279,79478,79499,49597,79526,84127,87235,49907,45,94676,94784,89,94679,79380,69348,33125,34651,19,21,399,4609,32376,32629,33639,36843,37397,37951,38505,58071,59745,60117,60241,76161,76533,76657,89503,10,14,25,26,27,29,30,31,32,34153,35735,36289,58009,59497,59621,59869,60613,60737,60861,60985,69596,74549,74983,75913,76037,76285,77029,77153,77277,77401,17,22,23,24,59993,60365,60489,76409,76781,76905,79250,79502,89205,89681,2245,56028,2271,766,6,8,2,57,39,36,35,34,37,38,69286,69410,1732,33386,34904,35181,35458,89393,89525,11,12,18,20,14320,30863,32115,32872,36566,37120,37674,38228,57141,57265,59807,60179,60303,61399,69534,73309,76223,76595,76719,89217,4,5,7,9,13,28,1746,15706,33900,34414,36012,56273,56397,56769,57513,57637,57761,57885,58505,59435,59559,59683,60551,60675,60799,60923,73061,73185,74301,74425,75975,76099,76967,77091,77215,77339,15,16,56893,57017,57389,59931,60055,60427,76347,76471,76843,88908,91464,79371,88982,93063,89412,64181,79486,89848,69962,33,54,62])). % 117.11/117.04 cnf(94806,plain, % 117.11/117.04 ($false), % 117.11/117.04 inference(scs_inference,[],[94786,45]), % 117.11/117.04 ['proof']). % 117.17/117.08 % SZS output end Proof % 117.17/117.08 % Total time :116.320000s %------------------------------------------------------------------------------