%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS117+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 10:08:33 EDT 2024 % Result : Unsatisfiable 116.83s 117.26s % Output : CNFRefutation 116.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS117+1 : TPTP v8.2.0. Released v3.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jun 19 12:08:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 116.74/117.24 %------------------------------------------- % 116.74/117.24 % File :CSE---1.7 % 116.74/117.24 % Problem :theBenchmark % 116.74/117.24 % Transform :cnf % 116.74/117.24 % Format :tptp:raw % 116.74/117.24 % Command :java -jar mcs_scs.jar %d %s % 116.74/117.24 % 116.74/117.24 % Result :Theorem 116.200000s % 116.74/117.24 % Output :CNFRefutation 116.200000s % 116.74/117.24 %------------------------------------------- % 116.74/117.25 %------------------------------------------------------------------------------ % 116.74/117.25 % File : KRS117+1 : TPTP v8.2.0. Released v3.1.0. % 116.74/117.25 % Domain : Knowledge Representation (Semantic Web) % 116.74/117.25 % Problem : DL Test: t6.1 Double blocking example % 116.74/117.25 % Version : Especial. % 116.74/117.25 % English : % 116.74/117.25 % 116.74/117.25 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 116.74/117.25 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 116.74/117.25 % Source : [Bec03] % 116.74/117.25 % Names : inconsistent_description-logic-Manifest626 [Bec03] % 116.74/117.25 % 116.74/117.25 % Status : Unsatisfiable % 116.74/117.25 % Rating : 0.00 v3.1.0 % 116.74/117.25 % Syntax : Number of formulae : 32 ( 1 unt; 0 def) % 116.74/117.25 % Number of atoms : 92 ( 20 equ) % 116.74/117.25 % Maximal formula atoms : 6 ( 2 avg) % 116.74/117.25 % Number of connectives : 63 ( 3 ~; 0 |; 28 &) % 116.74/117.25 % ( 8 <=>; 24 =>; 0 <=; 0 <~>) % 116.74/117.25 % Maximal formula depth : 7 ( 5 avg) % 116.74/117.25 % Maximal term depth : 1 ( 1 avg) % 116.74/117.25 % Number of predicates : 15 ( 14 usr; 0 prp; 1-2 aty) % 116.74/117.25 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 116.74/117.25 % Number of variables : 73 ( 68 !; 5 ?) % 116.74/117.25 % SPC : FOF_UNS_RFO_SEQ % 116.74/117.25 % 116.74/117.25 % Comments : Sean Bechhofer says there are some errors in the encoding of % 116.74/117.25 % datatypes, so this problem may not be perfect. At least it's % 116.74/117.25 % still representative of the type of reasoning required for OWL. % 116.74/117.25 % : The concept should be incoherent but needs double blocking % 116.74/117.25 %------------------------------------------------------------------------------ % 116.74/117.25 fof(cUnsatisfiable_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & cUnsatisfiable(A) ) % 116.74/117.25 => cUnsatisfiable(B) ) ). % 116.74/117.25 % 116.74/117.25 fof(ca_Vx3_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & ca_Vx3(A) ) % 116.74/117.25 => ca_Vx3(B) ) ). % 116.74/117.25 % 116.74/117.25 fof(cc_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & cc(A) ) % 116.74/117.25 => cc(B) ) ). % 116.74/117.25 % 116.74/117.25 fof(ccxcomp_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & ccxcomp(A) ) % 116.74/117.25 => ccxcomp(B) ) ). % 116.74/117.25 % 116.74/117.25 fof(cd_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & cd(A) ) % 116.74/117.25 => cd(B) ) ). % 116.74/117.25 % 116.74/117.25 fof(cowlNothing_substitution_1,axiom, % 116.74/117.25 ! [A,B] : % 116.74/117.25 ( ( A = B % 116.74/117.25 & cowlNothing(A) ) % 116.74/117.25 => cowlNothing(B) ) ). % 116.74/117.26 % 116.74/117.26 fof(cowlThing_substitution_1,axiom, % 116.74/117.26 ! [A,B] : % 116.74/117.26 ( ( A = B % 116.74/117.26 & cowlThing(A) ) % 116.74/117.26 => cowlThing(B) ) ). % 116.74/117.26 % 116.74/117.26 fof(ra_Px1_substitution_1,axiom, % 116.74/117.26 ! [A,B,C] : % 116.74/117.26 ( ( A = B % 116.74/117.26 & ra_Px1(A,C) ) % 116.74/117.26 => ra_Px1(B,C) ) ). % 116.74/117.26 % 116.74/117.26 fof(ra_Px1_substitution_2,axiom, % 116.74/117.26 ! [A,B,C] : % 116.74/117.26 ( ( A = B % 116.74/117.26 & ra_Px1(C,A) ) % 116.74/117.26 => ra_Px1(C,B) ) ). % 116.74/117.26 % 116.74/117.26 fof(rf_substitution_1,axiom, % 116.74/117.26 ! [A,B,C] : % 116.74/117.26 ( ( A = B % 116.74/117.26 & rf(A,C) ) % 116.74/117.26 => rf(B,C) ) ). % 116.74/117.26 % 116.74/117.26 fof(rf_substitution_2,axiom, % 116.74/117.26 ! [A,B,C] : % 116.74/117.26 ( ( A = B % 116.74/117.26 & rf(C,A) ) % 116.74/117.26 => rf(C,B) ) ). % 116.74/117.26 % 116.74/117.26 fof(rinvF_substitution_1,axiom, % 116.74/117.26 ! [A,B,C] : % 116.74/117.26 ( ( A = B % 116.83/117.26 & rinvF(A,C) ) % 116.83/117.26 => rinvF(B,C) ) ). % 116.83/117.26 % 116.83/117.26 fof(rinvF_substitution_2,axiom, % 116.83/117.26 ! [A,B,C] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & rinvF(C,A) ) % 116.83/117.26 => rinvF(C,B) ) ). % 116.83/117.26 % 116.83/117.26 fof(rinvR_substitution_1,axiom, % 116.83/117.26 ! [A,B,C] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & rinvR(A,C) ) % 116.83/117.26 => rinvR(B,C) ) ). % 116.83/117.26 % 116.83/117.26 fof(rinvR_substitution_2,axiom, % 116.83/117.26 ! [A,B,C] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & rinvR(C,A) ) % 116.83/117.26 => rinvR(C,B) ) ). % 116.83/117.26 % 116.83/117.26 fof(rr_substitution_1,axiom, % 116.83/117.26 ! [A,B,C] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & rr(A,C) ) % 116.83/117.26 => rr(B,C) ) ). % 116.83/117.26 % 116.83/117.26 fof(rr_substitution_2,axiom, % 116.83/117.26 ! [A,B,C] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & rr(C,A) ) % 116.83/117.26 => rr(C,B) ) ). % 116.83/117.26 % 116.83/117.26 fof(xsd_integer_substitution_1,axiom, % 116.83/117.26 ! [A,B] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & xsd_integer(A) ) % 116.83/117.26 => xsd_integer(B) ) ). % 116.83/117.26 % 116.83/117.26 fof(xsd_string_substitution_1,axiom, % 116.83/117.26 ! [A,B] : % 116.83/117.26 ( ( A = B % 116.83/117.26 & xsd_string(A) ) % 116.83/117.26 => xsd_string(B) ) ). % 116.83/117.26 % 116.83/117.26 %----Thing and Nothing % 116.83/117.26 fof(axiom_0,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( cowlThing(X) % 116.83/117.26 & ~ cowlNothing(X) ) ). % 116.83/117.26 % 116.83/117.26 %----String and Integer disjoint % 116.83/117.26 fof(axiom_1,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( xsd_string(X) % 116.83/117.26 <=> ~ xsd_integer(X) ) ). % 116.83/117.26 % 116.83/117.26 %----Equality cUnsatisfiable % 116.83/117.26 fof(axiom_2,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( cUnsatisfiable(X) % 116.83/117.26 <=> ( ccxcomp(X) % 116.83/117.26 & ! [Y] : % 116.83/117.26 ( rinvR(X,Y) % 116.83/117.26 => ca_Vx3(Y) ) % 116.83/117.26 & ? [Y] : % 116.83/117.26 ( rinvF(X,Y) % 116.83/117.26 & cd(Y) ) ) ) ). % 116.83/117.26 % 116.83/117.26 %----Equality cc % 116.83/117.26 fof(axiom_3,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( cc(X) % 116.83/117.26 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 116.83/117.26 % 116.83/117.26 %----Equality ccxcomp % 116.83/117.26 fof(axiom_4,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( ccxcomp(X) % 116.83/117.26 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 116.83/117.26 % 116.83/117.26 %----Equality cd % 116.83/117.26 fof(axiom_5,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( cd(X) % 116.83/117.26 <=> ( ? [Y] : % 116.83/117.26 ( rf(X,Y) % 116.83/117.26 & ccxcomp(Y) ) % 116.83/117.26 & cc(X) ) ) ). % 116.83/117.26 % 116.83/117.26 %----Equality ca_Vx3 % 116.83/117.26 fof(axiom_6,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( ca_Vx3(X) % 116.83/117.26 <=> ? [Y] : % 116.83/117.26 ( rinvF(X,Y) % 116.83/117.26 & cd(Y) ) ) ). % 116.83/117.26 % 116.83/117.26 %----Super cowlThing % 116.83/117.26 fof(axiom_7,axiom, % 116.83/117.26 ! [X] : % 116.83/117.26 ( cowlThing(X) % 116.83/117.26 => ! [Y0,Y1] : % 116.83/117.26 ( ( rf(X,Y0) % 116.83/117.26 & rf(X,Y1) ) % 116.83/117.26 => Y0 = Y1 ) ) ). % 116.83/117.26 % 116.83/117.26 %----Inverse: rinvF % 116.83/117.26 fof(axiom_8,axiom, % 116.83/117.26 ! [X,Y] : % 116.83/117.26 ( rinvF(X,Y) % 116.83/117.26 <=> rf(Y,X) ) ). % 116.83/117.26 % 116.83/117.26 %----Inverse: rinvR % 116.83/117.26 fof(axiom_9,axiom, % 116.83/117.26 ! [X,Y] : % 116.83/117.26 ( rinvR(X,Y) % 116.83/117.26 <=> rr(Y,X) ) ). % 116.83/117.26 % 116.83/117.26 %----Transitive: rr % 116.83/117.26 fof(axiom_10,axiom, % 116.83/117.26 ! [X,Y,Z] : % 116.83/117.26 ( ( rr(X,Y) % 116.83/117.26 & rr(Y,Z) ) % 116.83/117.26 => rr(X,Z) ) ). % 116.83/117.26 % 116.83/117.26 %----i2003_11_14_17_21_37349 % 116.83/117.26 fof(axiom_11,axiom, % 116.83/117.26 cUnsatisfiable(i2003_11_14_17_21_37349) ). % 116.83/117.26 % 116.83/117.26 fof(axiom_12,axiom, % 116.83/117.26 ! [X,Y] : % 116.83/117.26 ( rf(X,Y) % 116.83/117.26 => rr(X,Y) ) ). % 116.83/117.26 % 116.83/117.26 %------------------------------------------------------------------------------ % 116.83/117.26 %------------------------------------------- % 116.83/117.26 % Proof found % 116.83/117.26 % SZS status Theorem for theBenchmark % 116.83/117.26 % SZS output start Proof % 116.83/117.26 %ClaNum:55(EqnAxiom:27) % 116.83/117.26 %VarNum:94(SingletonVarNum:43) % 116.83/117.26 %MaxLitNum:5 % 116.83/117.26 %MaxfuncDepth:1 % 116.83/117.26 %SharedTerms:2 % 116.83/117.26 [28]P1(a1) % 116.83/117.26 [29]~P2(x291) % 116.83/117.26 [30]P13(x301)+P7(x301) % 116.83/117.26 [31]~P5(x311)+P3(x311) % 116.83/117.26 [32]~P1(x321)+P6(x321) % 116.83/117.26 [33]~P13(x331)+~P7(x331) % 116.83/117.26 [34]~P5(x341)+P6(f2(x341)) % 116.83/117.26 [35]~P1(x351)+P5(f3(x351)) % 116.83/117.26 [36]~P4(x361)+P5(f7(x361)) % 116.83/117.26 [37]P3(x371)+P8(x371,f4(x371)) % 116.83/117.26 [39]~P6(x391)+P8(x391,f6(x391)) % 116.83/117.26 [40]~P5(x401)+P9(x401,f2(x401)) % 116.83/117.26 [41]~P1(x411)+P10(x411,f3(x411)) % 116.83/117.26 [42]~P4(x421)+P10(x421,f7(x421)) % 116.83/117.26 [38]P6(x381)+~P8(x381,x382) % 116.83/117.26 [43]~P3(x431)+~P8(x431,x432) % 116.83/117.26 [46]~P10(x462,x461)+P9(x461,x462) % 116.83/117.26 [47]~P9(x472,x471)+P10(x471,x472) % 116.83/117.26 [48]~P12(x482,x481)+P11(x481,x482) % 116.83/117.26 [49]~P11(x492,x491)+P12(x491,x492) % 116.83/117.26 [50]~P9(x501,x502)+P12(x501,x502) % 116.83/117.26 [44]~P11(x442,x441)+P4(x441)+~P1(x442) % 116.83/117.26 [45]~P10(x451,x452)+P4(x451)+~P5(x452) % 116.83/117.26 [52]~P9(x523,x521)+E(x521,x522)+~P9(x523,x522) % 116.83/117.26 [54]~P12(x541,x543)+P12(x541,x542)+~P12(x543,x542) % 116.83/117.26 [51]~P3(x511)+~P9(x511,x512)+P5(x511)+~P6(x512) % 116.83/117.26 [53]~P6(x531)+~P10(x531,x532)+P1(x531)+~P5(x532)+~P4(f5(x531)) % 116.83/117.26 [55]~P6(x551)+~P10(x551,x552)+P1(x551)+~P5(x552)+P11(x551,f5(x551)) % 116.83/117.26 %EqnAxiom % 116.83/117.26 [1]E(x11,x11) % 116.83/117.26 [2]E(x22,x21)+~E(x21,x22) % 116.83/117.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.83/117.26 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 116.83/117.26 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 116.83/117.26 [6]~E(x61,x62)+E(f7(x61),f7(x62)) % 116.83/117.26 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 116.83/117.26 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 116.83/117.26 [9]~E(x91,x92)+E(f5(x91),f5(x92)) % 116.83/117.26 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 116.83/117.26 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 116.83/117.26 [12]~P7(x121)+P7(x122)+~E(x121,x122) % 116.83/117.26 [13]~P13(x131)+P13(x132)+~E(x131,x132) % 116.83/117.26 [14]~P3(x141)+P3(x142)+~E(x141,x142) % 116.83/117.26 [15]~P5(x151)+P5(x152)+~E(x151,x152) % 116.83/117.26 [16]~P6(x161)+P6(x162)+~E(x161,x162) % 116.83/117.26 [17]P10(x172,x173)+~E(x171,x172)+~P10(x171,x173) % 116.83/117.26 [18]P10(x183,x182)+~E(x181,x182)+~P10(x183,x181) % 116.83/117.26 [19]P12(x192,x193)+~E(x191,x192)+~P12(x191,x193) % 116.83/117.26 [20]P12(x203,x202)+~E(x201,x202)+~P12(x203,x201) % 116.83/117.26 [21]~P4(x211)+P4(x212)+~E(x211,x212) % 116.83/117.26 [22]P9(x222,x223)+~E(x221,x222)+~P9(x221,x223) % 116.83/117.26 [23]P9(x233,x232)+~E(x231,x232)+~P9(x233,x231) % 116.83/117.26 [24]P11(x242,x243)+~E(x241,x242)+~P11(x241,x243) % 116.83/117.26 [25]P11(x253,x252)+~E(x251,x252)+~P11(x253,x251) % 116.83/117.26 [26]P8(x262,x263)+~E(x261,x262)+~P8(x261,x263) % 116.83/117.26 [27]P8(x273,x272)+~E(x271,x272)+~P8(x273,x271) % 116.83/117.26 % 116.83/117.26 %------------------------------------------- % 116.83/117.27 cnf(57,plain, % 116.83/117.27 (~P5(x571)+~P8(x571,x572)), % 116.83/117.27 inference(scs_inference,[],[31,43])). % 116.83/117.27 cnf(58,plain, % 116.83/117.27 (P8(a1,f6(a1))), % 116.83/117.27 inference(scs_inference,[],[28,32,39])). % 116.83/117.27 cnf(59,plain, % 116.83/117.27 (P8(x591,f6(a1))+~E(a1,x591)), % 116.83/117.27 inference(scs_inference,[],[58,26])). % 116.83/117.27 cnf(64,plain, % 116.83/117.27 (~P11(a1,x641)+P5(f7(x641))), % 116.83/117.27 inference(scs_inference,[],[28,36,44])). % 116.83/117.27 cnf(65,plain, % 116.83/117.27 (~E(a1,x651)+P6(x651)), % 116.83/117.27 inference(scs_inference,[],[58,38,16])). % 116.83/117.27 cnf(66,plain, % 116.83/117.27 (P6(a1)), % 116.83/117.27 inference(equality_inference,[],[65])). % 116.83/117.27 cnf(67,plain, % 116.83/117.27 (~P8(f3(a1),x671)), % 116.83/117.27 inference(scs_inference,[],[28,57,35])). % 116.83/117.27 cnf(68,plain, % 116.83/117.27 (P3(f3(a1))), % 116.83/117.27 inference(scs_inference,[],[67,37])). % 116.83/117.27 cnf(69,plain, % 116.83/117.27 (~P8(f3(a1),x691)), % 116.83/117.27 inference(rename_variables,[],[67])). % 116.83/117.27 cnf(71,plain, % 116.83/117.27 (~P6(f3(a1))), % 116.83/117.27 inference(scs_inference,[],[67,69,37,39])). % 116.83/117.27 cnf(80,plain, % 116.83/117.27 (P9(f3(a1),f2(f3(a1)))), % 116.83/117.27 inference(scs_inference,[],[28,40,35])). % 116.83/117.27 cnf(82,plain, % 116.83/117.27 (P9(f3(a1),x821)+~E(f2(f3(a1)),x821)), % 116.83/117.27 inference(scs_inference,[],[80,22,23])). % 116.83/117.27 cnf(85,plain, % 116.83/117.27 (~E(a1,x851)+P10(x851,f3(x851))), % 116.83/117.27 inference(scs_inference,[],[28,41,10])). % 116.83/117.27 cnf(86,plain, % 116.83/117.27 (P10(a1,f3(a1))), % 116.83/117.27 inference(equality_inference,[],[85])). % 116.83/117.27 cnf(87,plain, % 116.83/117.27 (P10(x871,f3(a1))+~E(a1,x871)), % 116.83/117.27 inference(scs_inference,[],[86,17])). % 116.83/117.27 cnf(88,plain, % 116.83/117.27 (P10(a1,x881)+~E(f3(a1),x881)), % 116.83/117.27 inference(scs_inference,[],[86,17,18])). % 116.83/117.27 cnf(91,plain, % 116.83/117.27 (~P5(f3(a1))+P10(a1,f7(a1))), % 116.83/117.27 inference(scs_inference,[],[86,42,45])). % 116.83/117.27 cnf(92,plain, % 116.83/117.27 (P12(f3(a1),a1)), % 116.83/117.27 inference(scs_inference,[],[86,46,50])). % 116.83/117.27 cnf(93,plain, % 116.83/117.27 (~P12(x931,f3(a1))+P12(x931,a1)), % 116.83/117.27 inference(scs_inference,[],[92,54])). % 116.83/117.27 cnf(99,plain, % 116.83/117.27 (P10(x991,f3(a1))+~E(f2(f3(a1)),x991)), % 116.83/117.27 inference(scs_inference,[],[80,47,17])). % 116.83/117.27 cnf(104,plain, % 116.83/117.27 (P5(f7(f3(a1)))), % 116.83/117.27 inference(scs_inference,[],[92,48,64])). % 116.83/117.27 cnf(108,plain, % 116.83/117.27 (P10(a1,f7(a1))), % 116.83/117.27 inference(scs_inference,[],[28,91,35])). % 116.83/117.27 cnf(109,plain, % 116.83/117.27 (P10(x1091,f7(a1))+~E(a1,x1091)), % 116.83/117.27 inference(scs_inference,[],[108,17])). % 116.83/117.27 cnf(110,plain, % 116.83/117.27 (P10(a1,x1101)+~E(f7(a1),x1101)), % 116.83/117.27 inference(scs_inference,[],[108,17,18])). % 116.83/117.27 cnf(137,plain, % 116.83/117.27 (P11(a1,x1371)+~E(f3(a1),x1371)), % 116.83/117.27 inference(scs_inference,[],[92,25,48])). % 116.83/117.27 cnf(138,plain, % 116.83/117.28 (P11(a1,f3(a1))), % 116.83/117.28 inference(equality_inference,[],[137])). % 116.83/117.28 cnf(143,plain, % 116.83/117.28 (P4(a1)+~P9(f3(a1),a1)), % 116.83/117.28 inference(scs_inference,[],[66,68,86,51,45])). % 116.83/117.28 cnf(144,plain, % 116.83/117.28 (P4(a1)), % 116.83/117.28 inference(scs_inference,[],[86,143,46])). % 116.83/117.28 cnf(150,plain, % 116.83/117.28 (P3(f7(a1))), % 116.83/117.28 inference(scs_inference,[],[144,31,36])). % 116.83/117.28 cnf(151,plain, % 116.83/117.28 (~P8(f7(a1),x1511)), % 116.83/117.28 inference(scs_inference,[],[150,43])). % 116.83/117.28 cnf(157,plain, % 116.83/117.28 (~E(f7(f3(a1)),x1571)+P3(x1571)), % 116.83/117.28 inference(scs_inference,[],[104,31,14])). % 116.83/117.28 cnf(159,plain, % 116.83/117.28 (P5(f3(a1))+~P9(f3(a1),a1)), % 116.83/117.28 inference(scs_inference,[],[28,68,32,51])). % 116.83/117.28 cnf(160,plain, % 116.83/117.28 (P5(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[86,159,46])). % 116.83/117.28 cnf(161,plain, % 116.83/117.28 (~E(x1611,x1612)+~P13(x1612)+~P7(x1611)), % 116.83/117.28 inference(scs_inference,[],[33,12])). % 116.83/117.28 cnf(166,plain, % 116.83/117.28 (~E(a1,f7(a1))), % 116.83/117.28 inference(scs_inference,[],[151,58,26])). % 116.83/117.28 cnf(170,plain, % 116.83/117.28 (P6(f2(f7(a1)))), % 116.83/117.28 inference(scs_inference,[],[144,34,36])). % 116.83/117.28 cnf(171,plain, % 116.83/117.28 (P8(f2(f7(f3(a1))),f6(f2(f7(f3(a1)))))), % 116.83/117.28 inference(scs_inference,[],[104,34,39])). % 116.83/117.28 cnf(172,plain, % 116.83/117.28 (P6(f2(f7(f3(a1))))), % 116.83/117.28 inference(scs_inference,[],[138,34,64])). % 116.83/117.28 cnf(180,plain, % 116.83/117.28 (~E(a1,x1801)+P5(f3(x1801))), % 116.83/117.28 inference(scs_inference,[],[28,35,10])). % 116.83/117.28 cnf(184,plain, % 116.83/117.28 (P9(f7(a1),f2(f7(a1)))), % 116.83/117.28 inference(scs_inference,[],[144,36,40])). % 116.83/117.28 cnf(185,plain, % 116.83/117.28 (P9(f7(a1),x1851)+~E(f2(f7(a1)),x1851)), % 116.83/117.28 inference(scs_inference,[],[184,23])). % 116.83/117.28 cnf(186,plain, % 116.83/117.28 (P9(x1861,f2(f7(a1)))+~E(f7(a1),x1861)), % 116.83/117.28 inference(scs_inference,[],[184,23,22])). % 116.83/117.28 cnf(189,plain, % 116.83/117.28 (~P10(x1891,f7(f3(a1)))+P5(f7(x1891))), % 116.83/117.28 inference(scs_inference,[],[104,36,45])). % 116.83/117.28 cnf(190,plain, % 116.83/117.28 (P3(f7(x1901))+~P10(x1901,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[189,31])). % 116.83/117.28 cnf(191,plain, % 116.83/117.28 (~P8(f7(x1911),x1912)+~P10(x1911,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[190,43])). % 116.83/117.28 cnf(192,plain, % 116.83/117.28 (~P6(f7(x1921))+~P10(x1921,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[191,39])). % 116.83/117.28 cnf(193,plain, % 116.83/117.28 (~P1(f7(x1931))+~P10(x1931,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[192,32])). % 116.83/117.28 cnf(194,plain, % 116.83/117.28 (~E(a1,f7(x1941))+~P10(x1941,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[28,193,10])). % 116.83/117.28 cnf(197,plain, % 116.83/117.28 (~P5(a1)), % 116.83/117.28 inference(scs_inference,[],[58,43,31])). % 116.83/117.28 cnf(234,plain, % 116.83/117.28 (P8(a1,f4(a1))), % 116.83/117.28 inference(scs_inference,[],[58,43,37])). % 116.83/117.28 cnf(237,plain, % 116.83/117.28 (~E(f7(f3(a1)),a1)), % 116.83/117.28 inference(scs_inference,[],[58,43,157])). % 116.83/117.28 cnf(257,plain, % 116.83/117.28 (~P9(x2571,f3(a1))+~P9(x2571,a1)), % 116.83/117.28 inference(scs_inference,[],[71,65,52])). % 116.83/117.28 cnf(258,plain, % 116.83/117.28 (~P10(f3(a1),x2581)+~P9(x2581,a1)), % 116.83/117.28 inference(scs_inference,[],[257,46])). % 116.83/117.28 cnf(259,plain, % 116.83/117.28 (~P4(f3(a1))+~P9(f7(f3(a1)),a1)), % 116.83/117.28 inference(scs_inference,[],[258,42])). % 116.83/117.28 cnf(260,plain, % 116.83/117.28 (~P10(a1,f7(f3(a1)))+~P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[259,46])). % 116.83/117.28 cnf(261,plain, % 116.83/117.28 (~E(f3(a1),f7(f3(a1)))+~P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[260,88])). % 116.83/117.28 cnf(262,plain, % 116.83/117.28 (~E(f7(f3(a1)),f3(a1))+~P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[261,2])). % 116.83/117.28 cnf(263,plain, % 116.83/117.28 (~E(x2631,f3(a1))+~E(f7(f3(a1)),x2631)+~P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[262,3])). % 116.83/117.28 cnf(273,plain, % 116.83/117.28 (E(f3(x2731),f3(x2732))+~E(x2732,x2731)), % 116.83/117.28 inference(scs_inference,[],[2,5])). % 116.83/117.28 cnf(276,plain, % 116.83/117.28 (E(f7(x2761),f7(x2762))+~E(x2762,x2761)), % 116.83/117.28 inference(scs_inference,[],[2,6])). % 116.83/117.28 cnf(279,plain, % 116.83/117.28 (E(f4(x2791),f4(x2792))+~E(x2792,x2791)), % 116.83/117.28 inference(scs_inference,[],[2,7])). % 116.83/117.28 cnf(286,plain, % 116.83/117.28 (~E(x2861,f7(f3(a1)))+~E(x2861,f3(a1))+~P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[2,263])). % 116.83/117.28 cnf(303,plain, % 116.83/117.28 (~E(f7(a1),a1)), % 116.83/117.28 inference(scs_inference,[],[151,2,59])). % 116.83/117.28 cnf(315,plain, % 116.83/117.28 (~E(x3151,f7(a1))+~E(a1,x3151)), % 116.83/117.28 inference(scs_inference,[],[303,2,3])). % 116.83/117.28 cnf(331,plain, % 116.83/117.28 (~E(f3(a1),x3311)+P3(x3311)), % 116.83/117.28 inference(scs_inference,[],[67,37,14])). % 116.83/117.28 cnf(333,plain, % 116.83/117.28 (~P3(a1)), % 116.83/117.28 inference(scs_inference,[],[66,39,43])). % 116.83/117.28 cnf(336,plain, % 116.83/117.28 (P10(f2(f7(f3(a1))),f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[104,40,47])). % 116.83/117.28 cnf(337,plain, % 116.83/117.28 (P9(f7(f3(a1)),f2(f7(f3(a1))))), % 116.83/117.28 inference(scs_inference,[],[138,40,64])). % 116.83/117.28 cnf(338,plain, % 116.83/117.28 (P12(f7(f3(a1)),f2(f7(f3(a1))))), % 116.83/117.28 inference(scs_inference,[],[104,40,50])). % 116.83/117.28 cnf(341,plain, % 116.83/117.28 (P9(x3411,f2(f7(f3(a1))))+~E(f7(f3(a1)),x3411)), % 116.83/117.28 inference(scs_inference,[],[104,40,22])). % 116.83/117.28 cnf(345,plain, % 116.83/117.28 (P9(f7(f3(a1)),x3451)+~E(f2(f7(f3(a1))),x3451)), % 116.83/117.28 inference(scs_inference,[],[104,40,23])). % 116.83/117.28 cnf(347,plain, % 116.83/117.28 (P9(f3(a1),a1)), % 116.83/117.28 inference(scs_inference,[],[28,41,46])). % 116.83/117.28 cnf(353,plain, % 116.83/117.28 (~P10(f3(a1),f3(a1))), % 116.83/117.28 inference(scs_inference,[],[347,257,258])). % 116.83/117.28 cnf(355,plain, % 116.83/117.28 (P9(x3551,a1)+~E(f3(a1),x3551)), % 116.83/117.28 inference(scs_inference,[],[347,257,258,22])). % 116.83/117.28 cnf(368,plain, % 116.83/117.28 (P9(f7(a1),a1)), % 116.83/117.28 inference(scs_inference,[],[144,42,46])). % 116.83/117.28 cnf(373,plain, % 116.83/117.28 (P9(x3731,a1)+~E(f7(a1),x3731)), % 116.83/117.28 inference(scs_inference,[],[368,258,257,22])). % 116.83/117.28 cnf(380,plain, % 116.83/117.28 (P10(f3(a1),f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[28,138,42,44])). % 116.83/117.28 cnf(386,plain, % 116.83/117.28 (P10(x3861,f7(f3(a1)))+~E(f3(a1),x3861)), % 116.83/117.28 inference(scs_inference,[],[353,368,380,237,52,18,46,17])). % 116.83/117.28 cnf(387,plain, % 116.83/117.28 (P3(f7(x3871))+~E(f3(a1),x3871)), % 116.83/117.28 inference(scs_inference,[],[353,368,380,237,52,18,46,17,190])). % 116.83/117.28 cnf(404,plain, % 116.83/117.28 (~P10(f7(a1),f3(a1))), % 116.83/117.28 inference(scs_inference,[],[347,303,52,82,46])). % 116.83/117.28 cnf(406,plain, % 116.83/117.28 (~P9(f7(a1),f7(a1))), % 116.83/117.28 inference(scs_inference,[],[303,368,52])). % 116.83/117.28 cnf(408,plain, % 116.83/117.28 (~E(f2(f7(a1)),f7(a1))), % 116.83/117.28 inference(scs_inference,[],[303,368,52,185])). % 116.83/117.28 cnf(409,plain, % 116.83/117.28 (~P10(f7(a1),f7(a1))), % 116.83/117.28 inference(scs_inference,[],[303,368,52,185,46])). % 116.83/117.28 cnf(411,plain, % 116.83/117.28 (~P9(f7(f3(a1)),a1)), % 116.83/117.28 inference(scs_inference,[],[380,46,257])). % 116.83/117.28 cnf(414,plain, % 116.83/117.28 (~P10(a1,f7(f3(a1)))), % 116.83/117.28 inference(scs_inference,[],[411,355,373,46])). % 116.83/117.28 cnf(418,plain, % 116.83/117.28 (P11(f2(f3(a1)),f3(a1))), % 116.83/117.28 inference(scs_inference,[],[80,48,50])). % 116.83/117.28 cnf(419,plain, % 116.83/117.28 (P11(f2(f3(a1)),x4191)+~E(f3(a1),x4191)), % 116.83/117.28 inference(scs_inference,[],[418,25])). % 116.83/117.28 cnf(420,plain, % 116.83/117.28 (P11(x4201,f3(a1))+~E(f2(f3(a1)),x4201)), % 116.83/117.28 inference(scs_inference,[],[418,25,24])). % 116.83/117.28 cnf(423,plain, % 116.83/117.28 (P4(f3(a1))), % 116.83/117.28 inference(scs_inference,[],[92,28,48,44])). % 116.83/117.28 cnf(424,plain, % 116.90/117.28 (~E(f7(f3(a1)),x4241)+~E(x4241,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[423,263])). % 116.90/117.28 cnf(426,plain, % 116.90/117.28 (~E(x4261,f7(f3(a1)))+~E(x4261,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[423,286])). % 116.90/117.28 cnf(427,plain, % 116.90/117.28 (~E(x4271,a1)+~E(f7(f3(a1)),f3(x4271))), % 116.90/117.28 inference(scs_inference,[],[424,5])). % 116.90/117.28 cnf(429,plain, % 116.90/117.28 (~E(a1,x4291)+~E(f3(x4291),f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[426,273])). % 116.90/117.28 cnf(433,plain, % 116.90/117.28 (~P9(x4331,f7(f3(a1)))+~P9(x4331,f3(x4332))+~E(a1,x4332)), % 116.90/117.28 inference(scs_inference,[],[429,52])). % 116.90/117.28 cnf(434,plain, % 116.90/117.28 (~P9(x4341,f3(a1))+~P9(x4341,f7(f3(a1)))), % 116.90/117.28 inference(equality_inference,[],[433])). % 116.90/117.28 cnf(436,plain, % 116.90/117.28 (~P10(f7(f3(a1)),x4361)+~P9(x4361,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[434,46])). % 116.90/117.28 cnf(437,plain, % 116.90/117.28 (~P10(f7(f3(a1)),x4371)+~E(x4371,x4372)+~P9(x4372,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[436,18])). % 116.90/117.28 cnf(452,plain, % 116.90/117.28 (P11(a1,x4521)+~P12(x4521,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[92,48,54])). % 116.90/117.28 cnf(453,plain, % 116.90/117.28 (~P11(f3(a1),x4531)+P11(a1,x4531)), % 116.90/117.28 inference(scs_inference,[],[452,49])). % 116.90/117.28 cnf(454,plain, % 116.90/117.28 (P5(f7(x4541))+~P11(f3(a1),x4541)), % 116.90/117.28 inference(scs_inference,[],[453,64])). % 116.90/117.28 cnf(463,plain, % 116.90/117.28 (P12(x4631,f2(f3(a1)))+~E(f3(a1),x4631)), % 116.90/117.28 inference(scs_inference,[],[49,419])). % 116.90/117.28 cnf(464,plain, % 116.90/117.28 (P12(f3(a1),f2(f3(a1)))), % 116.90/117.28 inference(equality_inference,[],[463])). % 116.90/117.28 cnf(465,plain, % 116.90/117.28 (~P12(x4651,f3(a1))+P12(x4651,f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[464,54])). % 116.90/117.28 cnf(468,plain, % 116.90/117.28 (P11(f2(f3(a1)),x4681)+~P12(x4681,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[465,48])). % 116.90/117.28 cnf(469,plain, % 116.90/117.28 (P12(f3(a1),x4691)+~E(f2(f3(a1)),x4691)), % 116.90/117.28 inference(scs_inference,[],[464,20])). % 116.90/117.28 cnf(473,plain, % 116.90/117.28 (P11(x4731,x4732)+~E(f2(f3(a1)),x4731)+~P12(x4732,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[468,24])). % 116.90/117.28 cnf(499,plain, % 116.90/117.28 (~P11(f3(a1),x4991)+P11(x4992,x4991)+~E(f2(f3(a1)),x4992)), % 116.90/117.28 inference(scs_inference,[],[49,473])). % 116.90/117.28 cnf(501,plain, % 116.90/117.28 (P12(x5011,x5012)+~E(f2(f3(a1)),x5012)+~P11(f3(a1),x5011)), % 116.90/117.28 inference(scs_inference,[],[49,499])). % 116.90/117.28 cnf(510,plain, % 116.90/117.28 (~P9(x5101,f3(a1))+P12(x5101,a1)), % 116.90/117.28 inference(scs_inference,[],[50,93])). % 116.90/117.28 cnf(511,plain, % 116.90/117.28 (P12(f7(f3(a1)),a1)), % 116.90/117.28 inference(scs_inference,[],[380,510,46])). % 116.90/117.28 cnf(512,plain, % 116.90/117.28 (~P12(x5121,f7(f3(a1)))+P12(x5121,a1)), % 116.90/117.28 inference(scs_inference,[],[511,54])). % 116.90/117.28 cnf(514,plain, % 116.90/117.28 (P12(x5141,a1)+~E(f7(f3(a1)),x5141)), % 116.90/117.28 inference(scs_inference,[],[511,54,19])). % 116.90/117.28 cnf(523,plain, % 116.90/117.28 (~P9(x5231,f3(a1))+P11(a1,x5231)), % 116.90/117.28 inference(scs_inference,[],[50,452])). % 116.90/117.28 cnf(524,plain, % 116.90/117.28 (P11(a1,f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[380,523,46])). % 116.90/117.28 cnf(525,plain, % 116.90/117.28 (P11(a1,x5251)+~E(f7(f3(a1)),x5251)), % 116.90/117.28 inference(scs_inference,[],[524,25])). % 116.90/117.28 cnf(556,plain, % 116.90/117.28 (P5(f7(x5561))+~P12(x5561,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[64,452])). % 116.90/117.28 cnf(557,plain, % 116.90/117.28 (P3(f7(x5571))+~P12(x5571,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[556,31])). % 116.90/117.28 cnf(558,plain, % 116.90/117.28 (~P8(f7(x5581),x5582)+~P12(x5581,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[557,43])). % 116.90/117.28 cnf(559,plain, % 116.90/117.28 (~P6(f7(x5591))+~P12(x5591,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[558,39])). % 116.90/117.28 cnf(560,plain, % 116.90/117.28 (~P1(f7(x5601))+~P12(x5601,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[559,32])). % 116.90/117.28 cnf(567,plain, % 116.90/117.28 (P3(f3(x5671))+~E(a1,x5671)), % 116.90/117.28 inference(scs_inference,[],[180,31])). % 116.90/117.28 cnf(572,plain, % 116.90/117.28 (P9(f3(x5721),f2(f3(x5721)))+~E(a1,x5721)), % 116.90/117.28 inference(scs_inference,[],[180,40])). % 116.90/117.28 cnf(576,plain, % 116.90/117.28 (P3(f3(f2(f3(a1))))), % 116.90/117.28 inference(scs_inference,[],[80,347,567,52])). % 116.90/117.28 cnf(604,plain, % 116.90/117.28 (P9(f3(x6041),x6041)+~E(a1,x6041)), % 116.90/117.28 inference(scs_inference,[],[85,46])). % 116.90/117.28 cnf(607,plain, % 116.90/117.28 (P4(x6071)+~E(a1,x6071)), % 116.90/117.28 inference(scs_inference,[],[160,87,45])). % 116.90/117.28 cnf(609,plain, % 116.90/117.28 (~E(a1,x6091)+P5(f7(x6091))), % 116.90/117.28 inference(scs_inference,[],[607,36])). % 116.90/117.28 cnf(613,plain, % 116.90/117.28 (~E(x6131,x6132)+P4(x6132)+~E(a1,x6131)), % 116.90/117.28 inference(scs_inference,[],[607,21])). % 116.90/117.28 cnf(614,plain, % 116.90/117.28 (~E(x6141,x6142)+~E(a1,x6141)+P5(f7(x6142))), % 116.90/117.28 inference(scs_inference,[],[613,36])). % 116.90/117.28 cnf(615,plain, % 116.90/117.28 (P3(f7(x6151))+~E(x6152,x6151)+~E(a1,x6152)), % 116.90/117.28 inference(scs_inference,[],[614,31])). % 116.90/117.28 cnf(616,plain, % 116.90/117.28 (~E(x6161,x6162)+~P8(f7(x6162),x6163)+~E(a1,x6161)), % 116.90/117.28 inference(scs_inference,[],[615,43])). % 116.90/117.28 cnf(623,plain, % 116.90/117.28 (P9(f7(x6231),f2(f7(x6231)))+~E(a1,x6231)), % 116.90/117.28 inference(scs_inference,[],[609,40])). % 116.90/117.28 cnf(653,plain, % 116.90/117.28 (~E(x6531,f7(f3(a1)))+~E(f7(a1),x6531)), % 116.90/117.28 inference(scs_inference,[],[414,110,3])). % 116.90/117.28 cnf(654,plain, % 116.90/117.28 (~E(f7(f3(a1)),x6541)+~E(f7(a1),x6541)), % 116.90/117.28 inference(scs_inference,[],[653,2])). % 116.90/117.28 cnf(655,plain, % 116.90/117.28 (~E(f3(a1),x6551)+~E(f7(a1),f7(x6551))), % 116.90/117.28 inference(scs_inference,[],[654,6])). % 116.90/117.28 cnf(656,plain, % 116.90/117.28 (~E(f7(x6561),f7(a1))+~E(f3(a1),x6561)), % 116.90/117.28 inference(scs_inference,[],[655,2])). % 116.90/117.28 cnf(657,plain, % 116.90/117.28 (~E(a1,x6571)+~E(f7(f3(x6571)),f7(a1))), % 116.90/117.28 inference(scs_inference,[],[656,5])). % 116.90/117.28 cnf(658,plain, % 116.90/117.28 (~E(f7(a1),f7(f3(x6581)))+~E(a1,x6581)), % 116.90/117.28 inference(scs_inference,[],[657,2])). % 116.90/117.28 cnf(659,plain, % 116.90/117.28 (~P9(x6591,f7(f3(x6592)))+~P9(x6591,f7(a1))+~E(a1,x6592)), % 116.90/117.28 inference(scs_inference,[],[658,52])). % 116.90/117.28 cnf(660,plain, % 116.90/117.28 (~P9(x6601,f7(f3(a1)))+~P9(x6601,f7(a1))), % 116.90/117.28 inference(equality_inference,[],[659])). % 116.90/117.28 cnf(661,plain, % 116.90/117.28 (~P10(f7(f3(a1)),x6611)+~P9(x6611,f7(a1))), % 116.90/117.28 inference(scs_inference,[],[660,46])). % 116.90/117.28 cnf(662,plain, % 116.90/117.28 (~P10(f7(f3(a1)),x6621)+~E(x6621,x6622)+~P9(x6622,f7(a1))), % 116.90/117.28 inference(scs_inference,[],[661,18])). % 116.90/117.28 cnf(682,plain, % 116.90/117.28 (P4(x6821)+~E(f3(a1),x6821)), % 116.90/117.28 inference(scs_inference,[],[28,137,44])). % 116.90/117.28 cnf(684,plain, % 116.90/117.28 (~E(f3(a1),x6841)+P10(x6841,f7(x6841))), % 116.90/117.28 inference(scs_inference,[],[682,42])). % 116.90/117.28 cnf(686,plain, % 116.90/117.28 (P4(f3(x6861))+~E(a1,x6861)), % 116.90/117.28 inference(scs_inference,[],[682,5])). % 116.90/117.28 cnf(701,plain, % 116.90/117.28 (~E(a1,x7011)+P10(f3(x7011),f7(f3(x7011)))), % 116.90/117.28 inference(scs_inference,[],[686,42])). % 116.90/117.28 cnf(704,plain, % 116.90/117.28 (~E(f3(x7041),x7042)+P4(x7042)+~E(a1,x7041)), % 116.90/117.28 inference(scs_inference,[],[686,21])). % 116.90/117.28 cnf(705,plain, % 116.90/117.28 (~E(f3(x7051),x7052)+~E(a1,x7051)+P5(f7(x7052))), % 116.90/117.28 inference(scs_inference,[],[704,36])). % 116.90/117.28 cnf(706,plain, % 116.90/117.28 (P3(f7(x7061))+~E(f3(x7062),x7061)+~E(a1,x7062)), % 116.90/117.28 inference(scs_inference,[],[705,31])). % 116.90/117.28 cnf(751,plain, % 116.90/117.28 (~P9(f7(f3(a1)),x7511)+~E(x7511,a1)), % 116.90/117.28 inference(scs_inference,[],[380,258,23])). % 116.90/117.28 cnf(753,plain, % 116.90/117.28 (~E(f7(a1),x7531)+~E(a1,x7531)), % 116.90/117.28 inference(scs_inference,[],[315,2])). % 116.90/117.28 cnf(754,plain, % 116.90/117.28 (~E(f7(a1),f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[80,347,753,52])). % 116.90/117.28 cnf(762,plain, % 116.90/117.28 (E(a1,f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[80,355,52])). % 116.90/117.28 cnf(767,plain, % 116.90/117.28 (E(f2(f3(a1)),a1)), % 116.90/117.28 inference(scs_inference,[],[762,59,109,2])). % 116.90/117.28 cnf(768,plain, % 116.90/117.28 (P1(f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,28,59,109,2,10])). % 116.90/117.28 cnf(769,plain, % 116.90/117.28 (~P3(f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[333,762,28,59,109,2,10,14])). % 116.90/117.28 cnf(770,plain, % 116.90/117.28 (~P5(f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[197,333,762,28,59,109,2,10,14,15])). % 116.90/117.28 cnf(804,plain, % 116.90/117.28 (~E(f7(x8041),a1)+~E(f3(a1),x8041)), % 116.90/117.28 inference(scs_inference,[],[333,387,14])). % 116.90/117.28 cnf(805,plain, % 116.90/117.28 (~E(f7(x8051),f2(f3(a1)))+~E(f3(a1),x8051)), % 116.90/117.28 inference(scs_inference,[],[767,804,3])). % 116.90/117.28 cnf(806,plain, % 116.90/117.28 (~E(f2(f3(a1)),f7(x8061))+~E(f3(a1),x8061)), % 116.90/117.28 inference(scs_inference,[],[805,2])). % 116.90/117.28 cnf(807,plain, % 116.90/117.28 (~P9(f3(a1),f7(x8071))+~E(f3(a1),x8071)), % 116.90/117.28 inference(scs_inference,[],[80,806,52])). % 116.90/117.28 cnf(816,plain, % 116.90/117.28 (P4(x8161)+~P12(x8161,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[28,452,44])). % 116.90/117.28 cnf(817,plain, % 116.90/117.28 (~P12(x8171,f3(a1))+P10(x8171,f7(x8171))), % 116.90/117.28 inference(scs_inference,[],[816,42])). % 116.90/117.28 cnf(818,plain, % 116.90/117.28 (P9(f7(x8181),x8181)+~P12(x8181,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[817,46])). % 116.90/117.28 cnf(819,plain, % 116.90/117.28 (P12(f7(x8191),x8191)+~P12(x8191,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[818,50])). % 116.90/117.28 cnf(820,plain, % 116.90/117.28 (P11(x8201,f7(x8201))+~P12(x8201,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[819,48])). % 116.90/117.28 cnf(834,plain, % 116.90/117.28 (P4(x8341)+~P9(x8341,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[816,50])). % 116.90/117.28 cnf(835,plain, % 116.90/117.28 (~P9(x8351,f3(a1))+P10(x8351,f7(x8351))), % 116.90/117.28 inference(scs_inference,[],[834,42])). % 116.90/117.28 cnf(836,plain, % 116.90/117.28 (P9(f7(x8361),x8361)+~P9(x8361,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[835,46])). % 116.90/117.28 cnf(837,plain, % 116.90/117.28 (P12(f7(x8371),x8371)+~P9(x8371,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[836,50])). % 116.90/117.28 cnf(838,plain, % 116.90/117.28 (P11(x8381,f7(x8381))+~P9(x8381,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[837,48])). % 116.90/117.28 cnf(858,plain, % 116.90/117.28 (~P11(f3(a1),x8581)+P6(f2(f7(x8581)))), % 116.90/117.28 inference(scs_inference,[],[454,34])). % 116.90/117.28 cnf(859,plain, % 116.90/117.28 (~E(f2(f7(x8591)),f3(a1))+~P11(f3(a1),x8591)), % 116.90/117.28 inference(scs_inference,[],[71,858,16])). % 116.90/117.28 cnf(860,plain, % 116.90/117.28 (~E(f3(a1),f2(f7(x8601)))+~P11(f3(a1),x8601)), % 116.90/117.28 inference(scs_inference,[],[859,2])). % 116.90/117.28 cnf(862,plain, % 116.90/117.28 (~E(f7(x8621),a1)+~P11(f3(a1),x8621)), % 116.90/117.28 inference(scs_inference,[],[197,454,15])). % 116.90/117.28 cnf(863,plain, % 116.90/117.28 (~E(f7(x8631),f2(f3(a1)))+~P11(f3(a1),x8631)), % 116.90/117.28 inference(scs_inference,[],[767,862,3])). % 116.90/117.28 cnf(864,plain, % 116.90/117.28 (~E(f2(f3(a1)),f7(x8641))+~P11(f3(a1),x8641)), % 116.90/117.28 inference(scs_inference,[],[863,2])). % 116.90/117.28 cnf(865,plain, % 116.90/117.28 (~P9(f3(a1),f7(x8651))+~P11(f3(a1),x8651)), % 116.90/117.28 inference(scs_inference,[],[80,864,52])). % 116.90/117.28 cnf(866,plain, % 116.90/117.28 (~P10(f7(x8661),f3(a1))+~P11(f3(a1),x8661)), % 116.90/117.28 inference(scs_inference,[],[865,46])). % 116.90/117.28 cnf(867,plain, % 116.90/117.28 (~P10(f7(x8671),x8672)+~E(x8672,f3(a1))+~P11(f3(a1),x8671)), % 116.90/117.28 inference(scs_inference,[],[866,18])). % 116.90/117.28 cnf(925,plain, % 116.90/117.28 (~P12(x9251,f3(a1))+P6(f2(f7(x9251)))), % 116.90/117.28 inference(scs_inference,[],[556,34])). % 116.90/117.28 cnf(926,plain, % 116.90/117.28 (~E(f2(f7(x9261)),f3(a1))+~P12(x9261,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[71,925,16])). % 116.90/117.28 cnf(941,plain, % 116.90/117.28 (~E(f2(f7(a1)),f7(x9411))+~P12(x9411,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[170,559,16])). % 116.90/117.28 cnf(942,plain, % 116.90/117.28 (~E(f7(x9421),f2(f7(a1)))+~P12(x9421,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[941,2])). % 116.90/117.28 cnf(943,plain, % 116.90/117.28 (~P9(f7(a1),f7(x9431))+~P12(x9431,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[184,942,52])). % 116.90/117.28 cnf(944,plain, % 116.90/117.28 (~P11(f3(a1),x9441)+~P9(f7(a1),f7(x9441))), % 116.90/117.28 inference(scs_inference,[],[943,49])). % 116.90/117.28 cnf(945,plain, % 116.90/117.28 (~P10(f7(x9451),f7(a1))+~P11(f3(a1),x9451)), % 116.90/117.28 inference(scs_inference,[],[944,46])). % 116.90/117.28 cnf(946,plain, % 116.90/117.28 (~P12(x9461,f3(a1))+~P10(f7(x9461),f7(a1))), % 116.90/117.28 inference(scs_inference,[],[945,48])). % 116.90/117.28 cnf(947,plain, % 116.90/117.28 (~P10(f7(x9471),x9472)+~E(x9472,f7(a1))+~P12(x9471,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[946,18])). % 116.90/117.28 cnf(958,plain, % 116.90/117.28 (~E(f2(f3(a1)),f7(x9581))+~P12(x9581,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[768,560,10])). % 116.90/117.28 cnf(959,plain, % 116.90/117.28 (~E(f7(x9591),f2(f3(a1)))+~P12(x9591,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[958,2])). % 116.90/117.28 cnf(960,plain, % 116.90/117.28 (~P9(f3(a1),f7(x9601))+~P12(x9601,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[80,959,52])). % 116.90/117.28 cnf(961,plain, % 116.90/117.28 (~P9(x9611,f3(a1))+~P9(f3(a1),f7(x9611))), % 116.90/117.28 inference(scs_inference,[],[960,50])). % 116.90/117.28 cnf(962,plain, % 116.90/117.28 (~P10(f7(x9621),f3(a1))+~P9(x9621,f3(a1))), % 116.90/117.28 inference(scs_inference,[],[961,46])). % 116.90/117.28 cnf(963,plain, % 116.90/117.28 (~P10(f7(f7(f3(a1))),f3(a1))), % 116.90/117.28 inference(scs_inference,[],[380,962,46])). % 116.90/117.28 cnf(976,plain, % 116.90/117.28 (~P9(f3(f2(f3(a1))),f7(a1))), % 116.90/117.28 inference(scs_inference,[],[762,754,604,52])). % 116.90/117.28 cnf(1039,plain, % 116.90/117.28 (E(f2(f7(a1)),f2(f7(f2(f3(a1)))))), % 116.90/117.28 inference(scs_inference,[],[762,4,6])). % 116.90/117.28 cnf(1049,plain, % 116.90/117.28 (E(f2(f3(a1)),f2(f3(f2(f3(a1)))))), % 116.90/117.28 inference(scs_inference,[],[762,4,5])). % 116.90/117.28 cnf(1085,plain, % 116.90/117.28 (E(f2(a1),f2(f2(f3(a1))))), % 116.90/117.28 inference(scs_inference,[],[767,4,2])). % 116.90/117.28 cnf(1105,plain, % 116.90/117.28 (E(f3(f2(f3(a1))),f3(a1))), % 116.90/117.28 inference(scs_inference,[],[762,5,2])). % 116.90/117.28 cnf(1111,plain, % 116.90/117.28 (E(f7(f3(f2(f3(a1)))),f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,5,276])). % 116.90/117.28 cnf(1121,plain, % 116.90/117.28 (P10(f3(f2(f3(a1))),f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,5,386])). % 116.90/117.28 cnf(1132,plain, % 116.90/117.28 (E(f7(f3(a1)),f7(f3(f2(f3(a1)))))), % 116.90/117.28 inference(scs_inference,[],[762,5,6])). % 116.90/117.28 cnf(1139,plain, % 116.90/117.28 (E(f7(f2(f3(a1))),f7(a1))), % 116.90/117.28 inference(scs_inference,[],[762,6,2])). % 116.90/117.28 cnf(1142,plain, % 116.90/117.28 (E(f7(f7(f2(f3(a1)))),f7(f7(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,6,276])). % 116.90/117.28 cnf(1143,plain, % 116.90/117.28 (P9(f7(f2(f3(a1))),f2(f7(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,6,186])). % 116.90/117.28 cnf(1384,plain, % 116.90/117.28 (P5(f7(x13841))+~P9(f7(f3(a1)),x13841)), % 116.90/117.28 inference(scs_inference,[],[189,47])). % 116.90/117.28 cnf(1385,plain, % 116.90/117.28 (P3(f7(x13851))+~P9(f7(f3(a1)),x13851)), % 116.90/117.28 inference(scs_inference,[],[1384,31])). % 116.90/117.28 cnf(1386,plain, % 116.90/117.28 (~P8(f7(x13861),x13862)+~P9(f7(f3(a1)),x13861)), % 116.90/117.28 inference(scs_inference,[],[1385,43])). % 116.90/117.28 cnf(1387,plain, % 116.90/117.28 (~P6(f7(x13871))+~P9(f7(f3(a1)),x13871)), % 116.90/117.28 inference(scs_inference,[],[1386,39])). % 116.90/117.28 cnf(1388,plain, % 116.90/117.28 (~P1(f7(x13881))+~P9(f7(f3(a1)),x13881)), % 116.90/117.28 inference(scs_inference,[],[1387,32])). % 116.90/117.28 cnf(1389,plain, % 116.90/117.28 (~E(f2(f3(a1)),f7(x13891))+~P9(f7(f3(a1)),x13891)), % 116.90/117.28 inference(scs_inference,[],[768,1388,10])). % 116.90/117.28 cnf(1390,plain, % 116.90/117.28 (~E(f7(x13901),f2(f3(a1)))+~P9(f7(f3(a1)),x13901)), % 116.90/117.28 inference(scs_inference,[],[1389,2])). % 116.90/117.28 cnf(1392,plain, % 116.90/117.28 (E(f3(a1),f3(f2(f3(a1))))), % 116.90/117.28 inference(scs_inference,[],[762,273,2])). % 116.90/117.28 cnf(1402,plain, % 116.90/117.28 (E(f4(a1),f4(f2(f3(a1))))), % 116.90/117.28 inference(scs_inference,[],[762,279,2])). % 116.90/117.28 cnf(1526,plain, % 116.90/117.28 (P11(a1,x15261)+~P12(x15261,f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[512,48])). % 116.90/117.28 cnf(1541,plain, % 116.90/117.28 (P12(x15411,f2(f3(a1)))+~P12(x15411,f7(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[762,512,20])). % 116.90/117.28 cnf(1542,plain, % 116.90/117.28 (~P11(f7(f3(a1)),x15421)+P12(x15421,f2(f3(a1)))), % 116.90/117.28 inference(scs_inference,[],[1541,49])). % 116.90/117.28 cnf(1543,plain, % 116.90/117.28 (P11(f2(f3(a1)),x15431)+~P11(f7(f3(a1)),x15431)), % 116.90/117.28 inference(scs_inference,[],[1542,48])). % 116.90/117.28 cnf(1548,plain, % 116.90/117.29 (P12(x15481,f2(f3(a1)))+~E(f7(f3(a1)),x15481)), % 116.90/117.29 inference(scs_inference,[],[762,514,20])). % 116.90/117.29 cnf(1562,plain, % 116.90/117.29 (~E(f3(a1),x15621)+P11(a1,f7(x15621))), % 116.90/117.29 inference(scs_inference,[],[525,6])). % 116.90/117.29 cnf(1564,plain, % 116.90/117.29 (P4(x15641)+~E(f7(f3(a1)),x15641)), % 116.90/117.29 inference(scs_inference,[],[28,525,44])). % 116.90/117.29 cnf(1566,plain, % 116.90/117.29 (~E(f7(f3(a1)),x15661)+P10(x15661,f7(x15661))), % 116.90/117.29 inference(scs_inference,[],[1564,42])). % 116.90/117.29 cnf(1567,plain, % 116.90/117.29 (P10(f7(f3(a1)),f7(f7(f3(a1))))), % 116.90/117.29 inference(equality_inference,[],[1566])). % 116.90/117.29 cnf(1568,plain, % 116.90/117.29 (~E(x15681,f3(a1))+P4(f7(x15681))), % 116.90/117.29 inference(scs_inference,[],[1564,276])). % 116.90/117.29 cnf(1574,plain, % 116.90/117.29 (~E(x15741,f3(a1))+P5(f7(f7(x15741)))), % 116.90/117.29 inference(scs_inference,[],[1568,36])). % 116.90/117.29 cnf(1654,plain, % 116.90/117.29 (P9(f7(x16541),x16541)+~E(f3(a1),x16541)), % 116.90/117.29 inference(scs_inference,[],[684,46])). % 116.90/117.29 cnf(1655,plain, % 116.90/117.29 (P9(f7(f3(a1)),f3(a1))), % 116.90/117.29 inference(equality_inference,[],[1654])). % 116.90/117.29 cnf(1656,plain, % 116.90/117.29 (~E(x16561,f7(f3(a1)))+~P10(f7(f3(a1)),x16561)), % 116.90/117.29 inference(scs_inference,[],[1655,437])). % 116.90/117.29 cnf(1658,plain, % 116.90/117.29 (~P9(x16581,f7(f3(a1)))+~E(x16581,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1655,437,47])). % 116.90/117.29 cnf(1661,plain, % 116.90/117.29 (~P10(f7(f3(a1)),f7(f3(a1)))), % 116.90/117.29 inference(equality_inference,[],[1656])). % 116.90/117.29 cnf(1662,plain, % 116.90/117.29 (~P9(f7(f3(a1)),f7(f3(a1)))), % 116.90/117.29 inference(equality_inference,[],[1658])). % 116.90/117.29 cnf(1677,plain, % 116.90/117.29 (P9(f7(f7(f3(a1))),f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1655,818,50])). % 116.90/117.29 cnf(1698,plain, % 116.90/117.29 (P12(f7(f7(f3(a1))),f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1655,819,50])). % 116.90/117.29 cnf(1724,plain, % 116.90/117.29 (P11(f7(f3(a1)),f7(f7(f3(a1))))), % 116.90/117.29 inference(scs_inference,[],[1655,820,50])). % 116.90/117.29 cnf(1880,plain, % 116.90/117.29 (P11(x18801,f7(f7(f3(a1))))+~E(f7(f3(a1)),x18801)), % 116.90/117.29 inference(scs_inference,[],[1655,838,24])). % 116.90/117.29 cnf(1929,plain, % 116.90/117.29 (P5(f7(x19291))+~P12(x19291,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1526,64])). % 116.90/117.29 cnf(1930,plain, % 116.90/117.29 (P3(f7(x19301))+~P12(x19301,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1929,31])). % 116.90/117.29 cnf(1931,plain, % 116.90/117.29 (~P8(f7(x19311),x19312)+~P12(x19311,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1930,43])). % 116.90/117.29 cnf(1932,plain, % 116.90/117.29 (~P6(f7(x19321))+~P12(x19321,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1931,39])). % 116.90/117.29 cnf(1933,plain, % 116.90/117.29 (~P1(f7(x19331))+~P12(x19331,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1932,32])). % 116.90/117.29 cnf(1934,plain, % 116.90/117.29 (~E(f2(f3(a1)),f7(x19341))+~P12(x19341,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[768,1933,10])). % 116.90/117.29 cnf(1935,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x19351)+~E(f2(f3(a1)),f7(x19351))), % 116.90/117.29 inference(scs_inference,[],[1934,49])). % 116.90/117.29 cnf(1936,plain, % 116.90/117.29 (~E(f7(x19361),f2(f3(a1)))+~P11(f7(f3(a1)),x19361)), % 116.90/117.29 inference(scs_inference,[],[1935,2])). % 116.90/117.29 cnf(1937,plain, % 116.90/117.29 (~P12(x19371,f7(f3(a1)))+~E(f7(x19371),f2(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1936,48])). % 116.90/117.29 cnf(1938,plain, % 116.90/117.29 (~E(f7(x19381),a1)+~P12(x19381,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[762,1937,3])). % 116.90/117.29 cnf(1939,plain, % 116.90/117.29 (~P9(x19391,f7(f3(a1)))+~E(f7(x19391),a1)), % 116.90/117.29 inference(scs_inference,[],[1938,50])). % 116.90/117.29 cnf(1940,plain, % 116.90/117.29 (~P10(f7(f3(a1)),x19401)+~E(f7(x19401),a1)), % 116.90/117.29 inference(scs_inference,[],[1939,46])). % 116.90/117.29 cnf(1941,plain, % 116.90/117.29 (~E(a1,f7(x19411))+~P10(f7(f3(a1)),x19411)), % 116.90/117.29 inference(scs_inference,[],[1940,2])). % 116.90/117.29 cnf(1942,plain, % 116.90/117.29 (~P9(x19421,f7(f3(a1)))+~E(a1,f7(x19421))), % 116.90/117.29 inference(scs_inference,[],[1941,47])). % 116.90/117.29 cnf(1943,plain, % 116.90/117.29 (~P9(f3(a1),f7(x19431))+~P9(x19431,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[347,1942,52])). % 116.90/117.29 cnf(1952,plain, % 116.90/117.29 (P4(x19521)+~P12(x19521,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[28,1526,44])). % 116.90/117.29 cnf(1953,plain, % 116.90/117.29 (~P12(x19531,f7(f3(a1)))+P10(x19531,f7(x19531))), % 116.90/117.29 inference(scs_inference,[],[1952,42])). % 116.90/117.29 cnf(1954,plain, % 116.90/117.29 (P9(f7(x19541),x19541)+~P12(x19541,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1953,46])). % 116.90/117.29 cnf(1955,plain, % 116.90/117.29 (P12(f7(x19551),x19551)+~P12(x19551,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1954,50])). % 116.90/117.29 cnf(1956,plain, % 116.90/117.29 (P11(x19561,f7(x19561))+~P12(x19561,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1955,48])). % 116.90/117.29 cnf(1959,plain, % 116.90/117.29 (P4(x19591)+~P11(f7(f3(a1)),x19591)), % 116.90/117.29 inference(scs_inference,[],[1952,49])). % 116.90/117.29 cnf(1960,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x19601)+P5(f7(x19601))), % 116.90/117.29 inference(scs_inference,[],[1959,36])). % 116.90/117.29 cnf(1965,plain, % 116.90/117.29 (P4(x19651)+~P9(x19651,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1952,50])). % 116.90/117.29 cnf(1966,plain, % 116.90/117.29 (~P9(x19661,f7(f3(a1)))+P5(f7(x19661))), % 116.90/117.29 inference(scs_inference,[],[1965,36])). % 116.90/117.29 cnf(1967,plain, % 116.90/117.29 (P3(f7(x19671))+~P9(x19671,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1966,31])). % 116.90/117.29 cnf(1968,plain, % 116.90/117.29 (~P8(f7(x19681),x19682)+~P9(x19681,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1967,43])). % 116.90/117.29 cnf(1969,plain, % 116.90/117.29 (~P6(f7(x19691))+~P9(x19691,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1968,39])). % 116.90/117.29 cnf(1970,plain, % 116.90/117.29 (~P1(f7(x19701))+~P9(x19701,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1969,32])). % 116.90/117.29 cnf(1972,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x19721)+P10(x19721,f7(x19721))), % 116.90/117.29 inference(scs_inference,[],[1959,42])). % 116.90/117.29 cnf(1973,plain, % 116.90/117.29 (P9(f7(x19731),x19731)+~P11(f7(f3(a1)),x19731)), % 116.90/117.29 inference(scs_inference,[],[1972,46])). % 116.90/117.29 cnf(1974,plain, % 116.90/117.29 (P12(f7(x19741),x19741)+~P11(f7(f3(a1)),x19741)), % 116.90/117.29 inference(scs_inference,[],[1973,50])). % 116.90/117.29 cnf(2015,plain, % 116.90/117.29 (P11(f2(f3(a1)),f7(x20151))+~E(f3(a1),x20151)), % 116.90/117.29 inference(scs_inference,[],[762,1562,24])). % 116.90/117.29 cnf(2020,plain, % 116.90/117.29 (~P8(f7(f7(x20201)),x20202)+~E(x20201,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[1574,57])). % 116.90/117.29 cnf(2041,plain, % 116.90/117.29 (P12(f7(x20411),x20411)+~E(f3(a1),x20411)), % 116.90/117.29 inference(scs_inference,[],[1654,50])). % 116.90/117.29 cnf(2042,plain, % 116.90/117.29 (P12(f7(f3(a1)),f3(a1))), % 116.90/117.29 inference(equality_inference,[],[2041])). % 116.90/117.29 cnf(2043,plain, % 116.90/117.29 (~P12(x20431,f7(f3(a1)))+P12(x20431,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2042,54])). % 116.90/117.29 cnf(2055,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x20551)+P12(x20551,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2043,49])). % 116.90/117.29 cnf(2071,plain, % 116.90/117.29 (~E(f7(f3(a1)),x20711)+~P9(f3(a1),f7(x20711))), % 116.90/117.29 inference(scs_inference,[],[2042,19,559,560,926,941,943,958,959,960])). % 116.90/117.29 cnf(2075,plain, % 116.90/117.29 (~P10(f7(x20751),f7(a1))+~E(f7(f3(a1)),x20751)), % 116.90/117.29 inference(scs_inference,[],[2042,19,559,560,926,941,943,958,959,960,942,46])). % 116.90/117.29 cnf(2149,plain, % 116.90/117.29 (~P12(x21491,f7(f3(a1)))+P6(f2(f7(x21491)))), % 116.90/117.29 inference(scs_inference,[],[1929,34])). % 116.90/117.29 cnf(2150,plain, % 116.90/117.29 (~E(f2(f7(x21501)),f3(a1))+~P12(x21501,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[71,2149,16])). % 116.90/117.29 cnf(2151,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x21511)+~E(f2(f7(x21511)),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2150,49])). % 116.90/117.29 cnf(2152,plain, % 116.90/117.29 (~E(f3(a1),f2(f7(x21521)))+~P11(f7(f3(a1)),x21521)), % 116.90/117.29 inference(scs_inference,[],[2151,2])). % 116.90/117.29 cnf(2153,plain, % 116.90/117.29 (~P12(x21531,f7(f3(a1)))+~E(f3(a1),f2(f7(x21531)))), % 116.90/117.29 inference(scs_inference,[],[2152,48])). % 116.90/117.29 cnf(2160,plain, % 116.90/117.29 (~P12(x21601,f7(f3(a1)))+~E(a1,f7(x21601))), % 116.90/117.29 inference(scs_inference,[],[1932,65])). % 116.90/117.29 cnf(2161,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x21611)+~E(a1,f7(x21611))), % 116.90/117.29 inference(scs_inference,[],[2160,49])). % 116.90/117.29 cnf(2162,plain, % 116.90/117.29 (~E(f7(x21621),a1)+~P11(f7(f3(a1)),x21621)), % 116.90/117.29 inference(scs_inference,[],[2161,2])). % 116.90/117.29 cnf(2163,plain, % 116.90/117.29 (~P9(f3(a1),f7(x21631))+~P11(f7(f3(a1)),x21631)), % 116.90/117.29 inference(scs_inference,[],[347,2162,52])). % 116.90/117.29 cnf(2164,plain, % 116.90/117.29 (~P12(x21641,f7(f3(a1)))+~P9(f3(a1),f7(x21641))), % 116.90/117.29 inference(scs_inference,[],[2163,48])). % 116.90/117.29 cnf(2165,plain, % 116.90/117.29 (~P10(f7(x21651),f3(a1))+~P12(x21651,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[2164,46])). % 116.90/117.29 cnf(2166,plain, % 116.90/117.29 (~P9(x21661,f7(f3(a1)))+~P10(f7(x21661),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2165,50])). % 116.90/117.29 cnf(2167,plain, % 116.90/117.29 (~P10(f7(f3(a1)),x21671)+~P10(f7(x21671),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2166,46])). % 116.90/117.29 cnf(2168,plain, % 116.90/117.29 (~P10(f7(x21681),x21682)+~E(x21682,f3(a1))+~P10(f7(f3(a1)),x21681)), % 116.90/117.29 inference(scs_inference,[],[2167,18])). % 116.90/117.29 cnf(2170,plain, % 116.90/117.29 (~E(f2(f7(a1)),f7(x21701))+~P12(x21701,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[170,1932,16])). % 116.90/117.29 cnf(2172,plain, % 116.90/117.29 (~P11(f7(f3(a1)),x21721)+P6(f2(f7(x21721)))), % 116.90/117.29 inference(scs_inference,[],[1960,34])). % 116.90/117.29 cnf(2181,plain, % 116.90/117.29 (P11(x21811,f7(x21811))+~E(f3(a1),x21811)), % 116.90/117.29 inference(scs_inference,[],[2041,48])). % 116.90/117.29 cnf(2182,plain, % 116.90/117.29 (P11(f3(a1),f7(f3(a1)))), % 116.90/117.29 inference(equality_inference,[],[2181])). % 116.90/117.29 cnf(2183,plain, % 116.90/117.29 (P11(f3(a1),x21831)+~E(f7(f3(a1)),x21831)), % 116.90/117.29 inference(scs_inference,[],[2182,25])). % 116.90/117.29 cnf(2186,plain, % 116.90/117.29 (~E(f7(f3(a1)),x21861)+~P10(f7(x21861),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2182,25,860,866])). % 116.90/117.29 cnf(2192,plain, % 116.90/117.29 (P11(x21921,f7(f3(a1)))+~E(f3(a1),x21921)), % 116.90/117.29 inference(scs_inference,[],[2182,24])). % 116.90/117.29 cnf(2201,plain, % 116.90/117.29 (~P10(f7(f7(f3(a1))),x22011)+~E(x22011,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2041,947])). % 116.90/117.29 cnf(2227,plain, % 116.90/117.29 (~P10(f7(f7(f3(a1))),x22271)+~E(x22271,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2181,867])). % 116.90/117.29 cnf(2249,plain, % 116.90/117.29 (~E(x22491,f3(f2(f3(a1))))+~E(f7(f3(a1)),x22491)), % 116.90/117.29 inference(scs_inference,[],[767,427,3])). % 116.90/117.29 cnf(2252,plain, % 116.90/117.29 (~E(f7(f3(a1)),x22521)+~P9(x22521,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[1655,434,22])). % 116.90/117.29 cnf(2294,plain, % 116.90/117.29 (P9(f3(f2(f3(a1))),x22941)+~E(f2(f3(f2(f3(a1)))),x22941)), % 116.90/117.29 inference(scs_inference,[],[762,572,23])). % 116.90/117.29 cnf(2301,plain, % 116.90/117.29 (P12(f7(f2(f3(a1))),f2(f7(f2(f3(a1)))))), % 116.90/117.29 inference(scs_inference,[],[762,623,50])). % 116.90/117.29 cnf(2304,plain, % 116.90/117.29 (P9(f7(f2(f3(a1))),x23041)+~E(f2(f7(f2(f3(a1)))),x23041)), % 116.90/117.29 inference(scs_inference,[],[762,623,23])). % 116.90/117.29 cnf(2306,plain, % 116.90/117.29 (~E(x23061,f3(a1))+~E(f7(a1),f7(x23061))), % 116.90/117.29 inference(scs_inference,[],[653,6])). % 116.90/117.29 cnf(2314,plain, % 116.90/117.29 (~P9(x23141,f7(a1))+~P9(x23141,f7(f3(f2(f3(a1)))))), % 116.90/117.29 inference(scs_inference,[],[762,657,52])). % 116.90/117.29 cnf(2315,plain, % 116.90/117.29 (~P10(f7(a1),x23151)+~P9(x23151,f7(f3(a1)))), % 116.90/117.29 inference(scs_inference,[],[660,46])). % 116.90/117.29 cnf(2316,plain, % 116.90/117.29 (~P10(f7(f3(a1)),x23161)+~P10(f7(a1),x23161)), % 116.90/117.29 inference(scs_inference,[],[2315,46])). % 116.90/117.29 cnf(2331,plain, % 116.90/117.29 (P10(x23311,f7(f3(f2(f3(a1)))))+~E(f3(f2(f3(a1))),x23311)), % 116.90/117.29 inference(scs_inference,[],[762,701,17])). % 116.90/117.29 cnf(2337,plain, % 116.90/117.29 (~P10(f7(x23371),f3(a1))+~E(f3(a1),x23371)), % 116.90/117.29 inference(scs_inference,[],[807,46])). % 116.90/117.29 cnf(2647,plain, % 116.90/117.29 (P12(f7(a1),a1)), % 116.90/117.29 inference(scs_inference,[],[368,50])). % 116.90/117.29 cnf(2649,plain, % 116.90/117.29 (P11(a1,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[368,50,48])). % 116.90/117.29 cnf(2656,plain, % 116.90/117.29 (P4(f7(a1))), % 116.90/117.29 inference(scs_inference,[],[28,2649,44])). % 116.90/117.29 cnf(2664,plain, % 116.90/117.29 (~E(f7(a1),x26641)+P4(x26641)), % 116.90/117.29 inference(scs_inference,[],[2656,21])). % 116.90/117.29 cnf(2668,plain, % 116.90/117.29 (~P9(x26681,f7(a1))+~E(x26681,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[406,22])). % 116.90/117.29 cnf(2676,plain, % 116.90/117.29 (~P10(f7(a1),x26761)+~E(x26761,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[409,18])). % 116.90/117.29 cnf(2692,plain, % 116.90/117.29 (~P10(f7(a1),x26921)+~E(x26921,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[404,18])). % 116.90/117.29 cnf(2704,plain, % 116.90/117.29 (~E(f7(a1),x27041)+P5(f7(x27041))), % 116.90/117.29 inference(scs_inference,[],[2664,36])). % 116.90/117.29 cnf(2705,plain, % 116.90/117.29 (P5(f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2704])). % 116.90/117.29 cnf(2707,plain, % 116.90/117.29 (P4(x27071)+~E(x27071,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2664,2])). % 116.90/117.29 cnf(2709,plain, % 116.90/117.29 (~E(f7(a1),x27091)+P10(x27091,f7(x27091))), % 116.90/117.29 inference(scs_inference,[],[2664,42])). % 116.90/117.29 cnf(2710,plain, % 116.90/117.29 (P10(f7(a1),f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2709])). % 116.90/117.29 cnf(2711,plain, % 116.90/117.29 (P4(f7(x27111))+~E(a1,x27111)), % 116.90/117.29 inference(scs_inference,[],[2664,6])). % 116.90/117.29 cnf(2713,plain, % 116.90/117.29 (P4(f7(x27131))+~E(x27131,a1)), % 116.90/117.29 inference(scs_inference,[],[2664,276])). % 116.90/117.29 cnf(2715,plain, % 116.90/117.29 (~E(x27151,f7(a1))+P5(f7(x27151))), % 116.90/117.29 inference(scs_inference,[],[2707,36])). % 116.90/117.29 cnf(2718,plain, % 116.90/117.29 (~E(x27181,f7(a1))+P10(x27181,f7(x27181))), % 116.90/117.29 inference(scs_inference,[],[2707,42])). % 116.90/117.29 cnf(2721,plain, % 116.90/117.29 (~E(a1,x27211)+P5(f7(f7(x27211)))), % 116.90/117.29 inference(scs_inference,[],[2711,36])). % 116.90/117.29 cnf(2725,plain, % 116.90/117.29 (~E(f7(x27251),x27252)+P4(x27252)+~E(a1,x27251)), % 116.90/117.29 inference(scs_inference,[],[2711,21])). % 116.90/117.29 cnf(2726,plain, % 116.90/117.29 (~E(f7(x27261),x27262)+~E(a1,x27261)+P5(f7(x27262))), % 116.90/117.29 inference(scs_inference,[],[2725,36])). % 116.90/117.29 cnf(2727,plain, % 116.90/117.29 (P3(f7(x27271))+~E(f7(x27272),x27271)+~E(a1,x27272)), % 116.90/117.29 inference(scs_inference,[],[2726,31])). % 116.90/117.29 cnf(2728,plain, % 116.90/117.29 (~E(f7(x27281),x27282)+~P8(f7(x27282),x27283)+~E(a1,x27281)), % 116.90/117.29 inference(scs_inference,[],[2727,43])). % 116.90/117.29 cnf(2730,plain, % 116.90/117.29 (~E(f7(x27301),x27302)+~P6(f7(x27302))+~E(a1,x27301)), % 116.90/117.29 inference(scs_inference,[],[2728,39])). % 116.90/117.29 cnf(2731,plain, % 116.90/117.29 (~E(f7(x27311),x27312)+~P1(f7(x27312))+~E(a1,x27311)), % 116.90/117.29 inference(scs_inference,[],[2730,32])). % 116.90/117.29 cnf(2733,plain, % 116.90/117.29 (~E(a1,f7(x27331))+~E(f7(x27332),x27331)+~E(a1,x27332)), % 116.90/117.29 inference(scs_inference,[],[28,2731,10])). % 116.90/117.29 cnf(2734,plain, % 116.90/117.29 (~E(f7(a1),x27341)+~E(a1,f7(x27341))), % 116.90/117.29 inference(scs_inference,[],[368,2733,52])). % 116.90/117.29 cnf(2735,plain, % 116.90/117.29 (~E(x27351,f7(a1))+~E(a1,f7(x27351))), % 116.90/117.29 inference(scs_inference,[],[2734,2])). % 116.90/117.29 cnf(2736,plain, % 116.90/117.29 (~E(x27361,a1)+~E(a1,f7(f7(x27361)))), % 116.90/117.29 inference(scs_inference,[],[2735,6])). % 116.90/117.29 cnf(2742,plain, % 116.90/117.29 (~E(f7(x27421),x27422)+P4(x27422)+~E(x27421,a1)), % 116.90/117.29 inference(scs_inference,[],[2713,21])). % 116.90/117.29 cnf(2744,plain, % 116.90/117.29 (~E(f7(x27441),x27442)+~E(x27441,a1)+P5(f7(x27442))), % 116.90/117.29 inference(scs_inference,[],[2742,36])). % 116.90/117.29 cnf(2745,plain, % 116.90/117.29 (P3(f7(x27451))+~E(f7(x27452),x27451)+~E(x27452,a1)), % 116.90/117.29 inference(scs_inference,[],[2744,31])). % 116.90/117.29 cnf(2746,plain, % 116.90/117.29 (~E(f7(x27461),x27462)+~P8(f7(x27462),x27463)+~E(x27461,a1)), % 116.90/117.29 inference(scs_inference,[],[2745,43])). % 116.90/117.29 cnf(2747,plain, % 116.90/117.29 (~E(f7(x27471),x27472)+~P6(f7(x27472))+~E(x27471,a1)), % 116.90/117.29 inference(scs_inference,[],[2746,39])). % 116.90/117.29 cnf(2748,plain, % 116.90/117.29 (~E(f7(x27481),x27482)+~P1(f7(x27482))+~E(x27481,a1)), % 116.90/117.29 inference(scs_inference,[],[2747,32])). % 116.90/117.29 cnf(2749,plain, % 116.90/117.29 (~E(a1,f7(x27491))+~E(f7(x27492),x27491)+~E(x27492,a1)), % 116.90/117.29 inference(scs_inference,[],[28,2748,10])). % 116.90/117.29 cnf(2750,plain, % 116.90/117.29 (~P9(f7(a1),f7(x27501))+~E(f7(x27502),x27501)+~E(x27502,a1)), % 116.90/117.29 inference(scs_inference,[],[368,2749,52])). % 116.90/117.29 cnf(2752,plain, % 116.90/117.29 (~E(f7(a1),x27521)+~P9(f7(a1),f7(x27521))), % 116.90/117.29 inference(scs_inference,[],[368,2750,52])). % 116.90/117.29 cnf(2753,plain, % 116.90/117.29 (~P9(f7(a1),f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2752])). % 116.90/117.29 cnf(2804,plain, % 116.90/117.29 (~E(f7(a1),x28041)+P6(f2(f7(x28041)))), % 116.90/117.29 inference(scs_inference,[],[2704,34])). % 116.90/117.29 cnf(2805,plain, % 116.90/117.29 (P6(f2(f7(f7(a1))))), % 116.90/117.29 inference(equality_inference,[],[2804])). % 116.90/117.29 cnf(2809,plain, % 116.90/117.29 (~P8(f7(x28091),x28092)+~E(f7(a1),x28091)), % 116.90/117.29 inference(scs_inference,[],[2704,57])). % 116.90/117.29 cnf(2810,plain, % 116.90/117.29 (~P8(f7(f7(a1)),x28101)), % 116.90/117.29 inference(equality_inference,[],[2809])). % 116.90/117.29 cnf(2811,plain, % 116.90/117.29 (~E(f7(x28111),a1)+~E(f7(a1),x28111)), % 116.90/117.29 inference(scs_inference,[],[197,2704,15])). % 116.90/117.29 cnf(2813,plain, % 116.90/117.29 (~E(x28131,f7(a1))+~E(f7(x28131),a1)), % 116.90/117.29 inference(scs_inference,[],[2811,2])). % 116.90/117.29 cnf(2815,plain, % 116.90/117.29 (P3(f7(x28151))+~E(x28151,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2715,31])). % 116.90/117.29 cnf(2817,plain, % 116.90/117.29 (~E(x28171,f7(a1))+P6(f2(f7(x28171)))), % 116.90/117.29 inference(scs_inference,[],[2715,34])). % 116.90/117.29 cnf(2879,plain, % 116.90/117.29 (~E(x28791,a1)+~P9(f7(x28791),f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2668,6])). % 116.90/117.29 cnf(2885,plain, % 116.90/117.29 (~E(f7(a1),x28851)+~P10(f7(a1),x28851)), % 116.90/117.29 inference(scs_inference,[],[2676,2])). % 116.90/117.29 cnf(2896,plain, % 116.90/117.29 (~E(f3(a1),x28961)+~P10(f7(a1),x28961)), % 116.90/117.29 inference(scs_inference,[],[2692,2])). % 116.90/117.29 cnf(2898,plain, % 116.90/117.29 (~E(f7(f7(a1)),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2656,2692,42])). % 116.90/117.29 cnf(2909,plain, % 116.90/117.29 (P9(f7(x29091),x29091)+~E(f7(a1),x29091)), % 116.90/117.29 inference(scs_inference,[],[2709,46])). % 116.90/117.29 cnf(2910,plain, % 116.90/117.29 (P9(f7(f7(a1)),f7(a1))), % 116.90/117.29 inference(equality_inference,[],[2909])). % 116.90/117.29 cnf(2911,plain, % 116.90/117.29 (~E(f7(a1),f7(f7(a1)))), % 116.90/117.29 inference(scs_inference,[],[2709,2885])). % 116.90/117.29 cnf(2917,plain, % 116.90/117.29 (P9(f7(x29171),x29171)+~E(x29171,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2718,46])). % 116.90/117.29 cnf(2929,plain, % 116.90/117.29 (~P9(f7(a1),f7(x29291))+~E(x29291,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[368,2735,52])). % 116.90/117.29 cnf(2932,plain, % 116.90/117.29 (~P6(f7(x29321))+~E(f7(a1),x29321)), % 116.90/117.29 inference(scs_inference,[],[2809,39])). % 116.90/117.29 cnf(2933,plain, % 116.90/117.29 (~P6(f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2932])). % 116.90/117.29 cnf(2934,plain, % 116.90/117.29 (~P1(f7(x29341))+~E(f7(a1),x29341)), % 116.90/117.29 inference(scs_inference,[],[2932,32])). % 116.90/117.29 cnf(2935,plain, % 116.90/117.29 (~P1(f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2934])). % 116.90/117.29 cnf(2936,plain, % 116.90/117.29 (~E(x29361,f7(a1))+~P6(f7(x29361))), % 116.90/117.29 inference(scs_inference,[],[2932,2])). % 116.90/117.29 cnf(2943,plain, % 116.90/117.29 (~E(x29431,f7(a1))+~P1(f7(x29431))), % 116.90/117.29 inference(scs_inference,[],[2934,2])). % 116.90/117.29 cnf(2959,plain, % 116.90/117.29 (~P10(f7(a1),x29591)+~E(x29591,x29592)+~E(f7(a1),x29592)), % 116.90/117.29 inference(scs_inference,[],[2885,18])). % 116.90/117.29 cnf(2966,plain, % 116.90/117.29 (~P10(f7(a1),x29661)+~E(x29661,x29662)+~E(f3(a1),x29662)), % 116.90/117.29 inference(scs_inference,[],[2896,18])). % 116.90/117.29 cnf(2967,plain, % 116.90/117.29 (~E(f7(f7(a1)),x29671)+~E(f3(a1),x29671)), % 116.90/117.29 inference(scs_inference,[],[2656,2966,42])). % 116.90/117.29 cnf(2981,plain, % 116.90/117.29 (P12(f7(x29811),x29811)+~E(f7(a1),x29811)), % 116.90/117.29 inference(scs_inference,[],[2909,50])). % 116.90/117.29 cnf(2982,plain, % 116.90/117.29 (P12(f7(f7(a1)),f7(a1))), % 116.90/117.29 inference(equality_inference,[],[2981])). % 116.90/117.29 cnf(2985,plain, % 116.90/117.29 (~E(x29851,a1)+P9(f7(f7(x29851)),f7(x29851))), % 116.90/117.29 inference(scs_inference,[],[2909,276])). % 116.90/117.29 cnf(2987,plain, % 116.90/117.29 (~P9(f7(f7(a1)),a1)), % 116.90/117.29 inference(scs_inference,[],[166,2909,52])). % 116.90/117.29 cnf(2990,plain, % 116.90/117.29 (P12(f7(x29901),x29901)+~E(x29901,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2917,50])). % 116.90/117.29 cnf(2992,plain, % 116.90/117.29 (P11(x29921,f7(x29921))+~E(f7(a1),x29921)), % 116.90/117.29 inference(scs_inference,[],[2981,48])). % 116.90/117.29 cnf(2993,plain, % 116.90/117.29 (P11(f7(a1),f7(f7(a1)))), % 116.90/117.29 inference(equality_inference,[],[2992])). % 116.90/117.29 cnf(2994,plain, % 116.90/117.29 (P12(f7(f7(x29941)),f7(x29941))+~E(a1,x29941)), % 116.90/117.29 inference(scs_inference,[],[2981,6])). % 116.90/117.29 cnf(3003,plain, % 116.90/117.29 (P11(f7(x30031),f7(f7(x30031)))+~E(a1,x30031)), % 116.90/117.29 inference(scs_inference,[],[2992,6])). % 116.90/117.29 cnf(3018,plain, % 116.90/117.29 (~E(f7(x30181),f7(a1))+~E(x30181,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[2306,2])). % 116.90/117.29 cnf(3026,plain, % 116.90/117.29 (~P10(f7(x30261),x30262)+~E(x30262,f3(a1))+~E(f3(a1),x30261)), % 116.90/117.29 inference(scs_inference,[],[2337,18])). % 116.90/117.29 cnf(3027,plain, % 116.90/117.29 (~P9(x30271,f7(x30272))+~E(f3(a1),x30272)+~E(x30271,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[3026,47])). % 116.90/117.29 cnf(3039,plain, % 116.90/117.29 (~P10(f7(x30391),f7(a1))+~E(f7(a1),x30391)), % 116.90/117.29 inference(scs_inference,[],[2752,46])). % 116.90/117.29 cnf(3046,plain, % 116.90/117.29 (~P10(f7(x30461),f7(a1))+~E(x30461,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[2929,46])). % 116.90/117.29 cnf(3050,plain, % 116.90/117.29 (~E(x30501,f7(a1))+~E(f7(x30502),x30501)+~E(x30502,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[3018,3])). % 116.90/117.29 cnf(3051,plain, % 116.90/117.29 (~E(x30511,f7(x30512))+~E(x30512,f3(a1))+~E(x30511,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3050,2])). % 116.90/117.29 cnf(3058,plain, % 116.90/117.29 (~P10(f7(x30581),x30582)+~E(x30582,f7(a1))+~E(f7(a1),x30581)), % 116.90/117.29 inference(scs_inference,[],[3039,18])). % 116.90/117.29 cnf(3059,plain, % 116.90/117.29 (~P9(x30591,f7(x30592))+~E(f7(a1),x30592)+~E(x30591,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3058,47])). % 116.90/117.29 cnf(3115,plain, % 116.90/117.29 (~E(f7(x31151),a1)+~E(x31152,x31151)+~E(a1,x31152)), % 116.90/117.29 inference(scs_inference,[],[333,14,615])). % 116.90/117.29 cnf(3116,plain, % 116.90/117.29 (~E(x31161,x31162)+~P9(f7(a1),f7(x31162))+~E(a1,x31161)), % 116.90/117.29 inference(scs_inference,[],[368,3115,52])). % 116.90/117.29 cnf(3118,plain, % 116.90/117.29 (~E(x31181,x31182)+~E(a1,f7(x31182))+~E(a1,x31181)), % 116.90/117.29 inference(scs_inference,[],[368,3116,23])). % 116.90/117.29 cnf(3121,plain, % 116.90/117.29 (~E(f7(x31211),a1)+~E(f3(x31212),x31211)+~E(a1,x31212)), % 116.90/117.29 inference(scs_inference,[],[333,14,706])). % 116.90/117.29 cnf(3122,plain, % 116.90/117.29 (~E(f3(x31221),x31222)+~P9(f7(a1),f7(x31222))+~E(a1,x31221)), % 116.90/117.29 inference(scs_inference,[],[368,3121,52])). % 116.90/117.29 cnf(3123,plain, % 116.90/117.29 (~E(f3(a1),x31231)+~P9(f7(a1),f7(x31231))), % 116.90/117.29 inference(scs_inference,[],[368,3122,52])). % 116.90/117.29 cnf(3126,plain, % 116.90/117.29 (~P10(f7(x31261),f7(a1))+~E(f3(a1),x31261)), % 116.90/117.29 inference(scs_inference,[],[3123,46])). % 116.90/117.29 cnf(3137,plain, % 116.90/117.29 (~P10(f7(x31371),x31372)+~E(x31372,f7(a1))+~E(f3(a1),x31371)), % 116.90/117.29 inference(scs_inference,[],[3126,18])). % 116.90/117.29 cnf(3138,plain, % 116.90/117.29 (~P9(x31381,f7(x31382))+~E(f3(a1),x31382)+~E(x31381,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3137,47])). % 116.90/117.29 cnf(3170,plain, % 116.90/117.29 (P12(x31701,a1)+~E(f7(a1),x31701)), % 116.90/117.29 inference(scs_inference,[],[2649,19,49])). % 116.90/117.29 cnf(3173,plain, % 116.90/117.29 (~E(x31731,f7(a1))+P12(x31731,a1)), % 116.90/117.29 inference(scs_inference,[],[3170,2])). % 116.90/117.29 cnf(3175,plain, % 116.90/117.29 (P11(a1,x31751)+~E(f7(a1),x31751)), % 116.90/117.29 inference(scs_inference,[],[3170,48])). % 116.90/117.29 cnf(3177,plain, % 116.90/117.29 (~E(a1,x31771)+P12(f7(x31771),a1)), % 116.90/117.29 inference(scs_inference,[],[3170,6])). % 116.90/117.29 cnf(3189,plain, % 116.90/117.29 (~E(x31891,a1)+P11(a1,f7(x31891))), % 116.90/117.29 inference(scs_inference,[],[3175,276])). % 116.90/117.29 cnf(3194,plain, % 116.90/117.29 (P12(f7(x31941),x31942)+~E(a1,x31942)+~E(a1,x31941)), % 116.90/117.29 inference(scs_inference,[],[3177,20])). % 116.90/117.29 cnf(3195,plain, % 116.90/117.29 (P12(f7(a1),x31951)+~E(a1,x31951)), % 116.90/117.29 inference(scs_inference,[],[368,3194,52])). % 116.90/117.29 cnf(3197,plain, % 116.90/117.29 (~P12(x31971,f7(x31972))+P12(x31971,a1)+~E(a1,x31972)), % 116.90/117.29 inference(scs_inference,[],[3177,54])). % 116.90/117.29 cnf(3198,plain, % 116.90/117.29 (~P12(x31981,f7(a1))+P12(x31981,a1)), % 116.90/117.29 inference(equality_inference,[],[3197])). % 116.90/117.29 cnf(3216,plain, % 116.90/117.29 (P11(x32161,f7(a1))+~E(a1,x32161)), % 116.90/117.29 inference(scs_inference,[],[3195,48])). % 116.90/117.29 cnf(3218,plain, % 116.90/117.29 (P11(a1,x32181)+~P12(x32181,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3198,48])). % 116.90/117.29 cnf(3223,plain, % 116.90/117.29 (~P9(x32231,f7(a1))+P12(x32231,a1)), % 116.90/117.29 inference(scs_inference,[],[3198,50])). % 116.90/117.29 cnf(3224,plain, % 116.90/117.29 (~P10(f7(a1),x32241)+P12(x32241,a1)), % 116.90/117.29 inference(scs_inference,[],[3223,46])). % 116.90/117.29 cnf(3246,plain, % 116.90/117.29 (P5(f7(x32461))+~P12(x32461,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3218,64])). % 116.90/117.29 cnf(3247,plain, % 116.90/117.29 (P3(f7(x32471))+~P12(x32471,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3246,31])). % 116.90/117.29 cnf(3249,plain, % 116.90/117.29 (~P8(f7(x32491),x32492)+~P12(x32491,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3247,43])). % 116.90/117.29 cnf(3250,plain, % 116.90/117.29 (~P6(f7(x32501))+~P12(x32501,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3249,39])). % 116.90/117.29 cnf(3252,plain, % 116.90/117.29 (~P1(f7(x32521))+~P12(x32521,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3250,32])). % 116.90/117.29 cnf(3253,plain, % 116.90/117.29 (~E(a1,f7(x32531))+~P12(x32531,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[28,3252,10])). % 116.90/117.29 cnf(3260,plain, % 116.90/117.29 (P4(x32601)+~P12(x32601,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[28,3218,44])). % 116.90/117.29 cnf(3262,plain, % 116.90/117.29 (~P12(x32621,f7(a1))+P10(x32621,f7(x32621))), % 116.90/117.29 inference(scs_inference,[],[3260,42])). % 116.90/117.29 cnf(3263,plain, % 116.90/117.29 (P9(f7(x32631),x32631)+~P12(x32631,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3262,46])). % 116.90/117.29 cnf(3264,plain, % 116.90/117.29 (P12(f7(x32641),x32641)+~P12(x32641,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3263,50])). % 116.90/117.29 cnf(3267,plain, % 116.90/117.29 (P4(x32671)+~P11(f7(a1),x32671)), % 116.90/117.29 inference(scs_inference,[],[3260,49])). % 116.90/117.29 cnf(3269,plain, % 116.90/117.29 (~P11(f7(a1),x32691)+P5(f7(x32691))), % 116.90/117.29 inference(scs_inference,[],[3267,36])). % 116.90/117.29 cnf(3270,plain, % 116.90/117.29 (P3(f7(x32701))+~P11(f7(a1),x32701)), % 116.90/117.29 inference(scs_inference,[],[3269,31])). % 116.90/117.29 cnf(3272,plain, % 116.90/117.29 (~P8(f7(x32721),x32722)+~P11(f7(a1),x32721)), % 116.90/117.29 inference(scs_inference,[],[3270,43])). % 116.90/117.29 cnf(3273,plain, % 116.90/117.29 (~P6(f7(x32731))+~P11(f7(a1),x32731)), % 116.90/117.29 inference(scs_inference,[],[3272,39])). % 116.90/117.29 cnf(3276,plain, % 116.90/117.29 (P4(x32761)+~P9(x32761,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3260,50])). % 116.90/117.29 cnf(3303,plain, % 116.90/117.29 (P4(x33031)+~P10(f7(a1),x33031)), % 116.90/117.29 inference(scs_inference,[],[3276,46])). % 116.90/117.29 cnf(3320,plain, % 116.90/117.29 (~P10(f7(a1),x33201)+P10(x33201,f7(x33201))), % 116.90/117.29 inference(scs_inference,[],[3303,42])). % 116.90/117.29 cnf(3322,plain, % 116.90/117.29 (P9(f7(x33221),x33221)+~P10(f7(a1),x33221)), % 116.90/117.29 inference(scs_inference,[],[3320,46])). % 116.90/117.29 cnf(3323,plain, % 116.90/117.29 (P12(f7(x33231),x33231)+~P10(f7(a1),x33231)), % 116.90/117.29 inference(scs_inference,[],[3322,50])). % 116.90/117.29 cnf(3324,plain, % 116.90/117.29 (P11(x33241,f7(x33241))+~P10(f7(a1),x33241)), % 116.90/117.29 inference(scs_inference,[],[3323,48])). % 116.90/117.29 cnf(3325,plain, % 116.90/117.29 (P11(f7(f7(a1)),f7(f7(f7(a1))))), % 116.90/117.29 inference(scs_inference,[],[2656,3324,42])). % 116.90/117.29 cnf(3342,plain, % 116.90/117.29 (P5(f7(f7(f7(a1))))), % 116.90/117.29 inference(scs_inference,[],[3246,2981])). % 116.90/117.29 cnf(3343,plain, % 116.90/117.29 (~E(f7(x33431),a1)+~P12(x33431,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[197,3246,15])). % 116.90/117.29 cnf(3395,plain, % 116.90/117.29 (~P9(f3(a1),f7(x33951))+~P12(x33951,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[347,3253,52])). % 116.90/117.29 cnf(3397,plain, % 116.90/117.29 (~P11(f7(a1),x33971)+~P9(f3(a1),f7(x33971))), % 116.90/117.29 inference(scs_inference,[],[3395,49])). % 116.90/117.29 cnf(3399,plain, % 116.90/117.29 (~P10(f7(x33991),f3(a1))+~P11(f7(a1),x33991)), % 116.90/117.29 inference(scs_inference,[],[3397,46])). % 116.90/117.29 cnf(3404,plain, % 116.90/117.29 (~P9(f7(a1),f7(x34041))+~P12(x34041,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[368,3253,52])). % 116.90/117.29 cnf(3405,plain, % 116.90/117.29 (~P11(f7(a1),x34051)+~P9(f7(a1),f7(x34051))), % 116.90/117.29 inference(scs_inference,[],[3404,49])). % 116.90/117.29 cnf(3407,plain, % 116.90/117.29 (~P10(f7(x34071),f7(a1))+~P11(f7(a1),x34071)), % 116.90/117.29 inference(scs_inference,[],[3405,46])). % 116.90/117.29 cnf(3426,plain, % 116.90/117.29 (P10(f7(f7(a1)),f7(f7(f7(a1))))), % 116.90/117.29 inference(scs_inference,[],[3262,2981])). % 116.90/117.29 cnf(3442,plain, % 116.90/117.29 (P9(f7(f7(f7(a1))),f7(f7(a1)))), % 116.90/117.29 inference(scs_inference,[],[3263,2981])). % 116.90/117.29 cnf(3458,plain, % 116.90/117.29 (P12(f7(f7(f7(a1))),f7(f7(a1)))), % 116.90/117.29 inference(scs_inference,[],[3264,2981])). % 116.90/117.29 cnf(3590,plain, % 116.90/117.29 (~P9(f3(a1),f7(f7(f7(a1))))), % 116.90/117.29 inference(scs_inference,[],[3395,2981])). % 116.90/117.29 cnf(3611,plain, % 116.90/117.29 (~P10(f7(x36111),x36112)+~E(x36112,f3(a1))+~P11(f7(a1),x36111)), % 116.90/117.29 inference(scs_inference,[],[3399,18])). % 116.90/117.29 cnf(3660,plain, % 116.90/117.29 (~P10(f7(x36601),x36602)+~E(x36602,f7(a1))+~P11(f7(a1),x36601)), % 116.90/117.29 inference(scs_inference,[],[3407,18])). % 116.90/117.29 cnf(3722,plain, % 116.90/117.29 (P12(x37221,x37222)+~E(f7(x37222),x37221)+~E(f3(a1),x37222)), % 116.90/117.29 inference(scs_inference,[],[19,2041])). % 116.90/117.29 cnf(3731,plain, % 116.90/117.29 (P12(x37311,x37312)+~E(f7(x37312),x37311)+~E(f7(a1),x37312)), % 116.90/117.29 inference(scs_inference,[],[19,2981])). % 116.90/117.29 cnf(3768,plain, % 116.90/117.29 (P12(f7(x37681),x37682)+~E(x37681,x37682)+~P12(x37681,f3(a1))), % 116.90/117.29 inference(scs_inference,[],[20,819])). % 116.90/117.29 cnf(3790,plain, % 116.90/117.29 (P12(f7(x37901),x37902)+~E(x37901,x37902)+~E(f7(a1),x37901)), % 116.90/117.29 inference(scs_inference,[],[20,2981])). % 116.90/117.29 cnf(3797,plain, % 116.90/117.29 (P12(f7(x37971),x37972)+~E(x37971,x37972)+~E(x37971,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[20,2990])). % 116.90/117.29 cnf(3798,plain, % 116.90/117.29 (~E(x37981,f7(a1))+P12(f7(x37981),a1)), % 116.90/117.29 inference(scs_inference,[],[2647,3797,54])). % 116.90/117.29 cnf(3800,plain, % 116.90/117.29 (~E(f7(a1),x38001)+P12(f7(x38001),a1)), % 116.90/117.29 inference(scs_inference,[],[3798,2])). % 116.90/117.29 cnf(3802,plain, % 116.90/117.29 (P11(a1,f7(x38021))+~E(x38021,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3798,48])). % 116.90/117.29 cnf(3804,plain, % 116.90/117.29 (~E(x38041,a1)+P12(f7(f7(x38041)),a1)), % 116.90/117.29 inference(scs_inference,[],[3798,6])). % 116.90/117.29 cnf(3810,plain, % 116.90/117.29 (P12(f7(x38101),x38102)+~E(a1,x38102)+~E(x38101,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[3798,20])). % 116.90/117.29 cnf(3816,plain, % 116.90/117.29 (~P12(x38161,f7(x38162))+P12(x38161,a1)+~E(f7(a1),x38162)), % 116.90/117.29 inference(scs_inference,[],[3800,54])). % 116.90/117.29 cnf(3817,plain, % 116.90/117.29 (~P12(x38171,f7(f7(a1)))+P12(x38171,a1)), % 116.90/117.29 inference(equality_inference,[],[3816])). % 116.90/117.29 cnf(3828,plain, % 116.90/117.29 (P4(f7(x38281))+~E(x38281,f7(a1))), % 116.90/117.29 inference(scs_inference,[],[28,3802,44])). % 116.90/117.29 cnf(3848,plain, % 116.90/117.29 (~E(a1,x38481)+P4(f7(f7(x38481)))), % 116.90/117.29 inference(scs_inference,[],[3828,276])). % 116.90/117.29 cnf(3869,plain, % 116.90/117.29 (P12(f7(a1),x38691)+~E(x38692,x38691)+~E(a1,x38692)), % 116.90/117.29 inference(scs_inference,[],[20,3195])). % 116.90/117.29 cnf(3876,plain, % 116.90/117.29 (P12(x38761,x38762)+~E(a1,x38762)+~P10(f7(a1),x38761)), % 116.90/117.29 inference(scs_inference,[],[20,3224])). % 116.90/117.29 cnf(3949,plain, % 116.90/117.29 (~E(x39491,x39492)+~P6(f7(x39492))+~E(a1,x39491)), % 116.90/117.29 inference(scs_inference,[],[616,39])). % 116.90/117.29 cnf(3950,plain, % 116.90/117.29 (~E(x39501,x39502)+~P1(f7(x39502))+~E(a1,x39501)), % 116.90/117.29 inference(scs_inference,[],[3949,32])). % 116.90/117.29 cnf(3994,plain, % 116.90/117.29 (~E(x39941,x39942)+~P9(f3(a1),f7(x39942))+~E(a1,x39941)), % 116.90/117.29 inference(scs_inference,[],[347,3115,52])). % 116.90/117.29 cnf(4002,plain, % 116.90/117.29 (P11(a1,x40021)+~P12(x40021,f7(x40022))+~E(a1,x40022)), % 116.90/117.29 inference(scs_inference,[],[3197,48])). % 116.90/117.29 cnf(4098,plain, % 116.90/117.29 (P12(f7(f7(a1)),x40981)+~E(a1,x40981)), % 116.90/117.29 inference(scs_inference,[],[2656,3876,42])). % 116.90/117.29 cnf(4223,plain, % 116.90/117.29 (P12(f7(f7(f7(f3(a1)))),f7(f7(f3(a1))))), % 116.90/117.29 inference(scs_inference,[],[1105,1139,1085,1392,1402,3342,1677,1698,3458,1724,337,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974])). % 116.90/117.29 cnf(4227,plain, % 116.90/117.29 (P9(f7(f7(f2(f3(a1)))),f7(f2(f3(a1))))), % 116.90/117.29 inference(scs_inference,[],[1105,1139,1085,1392,1402,3342,1677,1698,3458,1724,337,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985])). % 116.90/117.29 cnf(4243,plain, % 116.90/117.29 (P12(f7(f7(f3(a1))),f3(a1))), % 116.90/117.29 inference(scs_inference,[],[1105,1139,1085,1392,1402,3342,1677,1698,3458,336,1567,1724,337,1049,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055])). % 116.90/117.29 cnf(4307,plain, % 116.90/117.29 (E(f7(a1),f7(f2(f3(a1))))), % 116.90/117.29 inference(scs_inference,[],[2910,2710,1105,1139,976,1085,1392,1402,3342,1677,1698,3458,336,1567,1724,337,1111,1049,1132,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6])). % 116.90/117.29 cnf(4404,plain, % 116.90/117.29 (~P9(f7(f2(f3(a1))),f7(f7(a1)))), % 116.90/117.29 inference(scs_inference,[],[408,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,1661,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,2042,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22])). % 116.90/117.29 cnf(4408,plain, % 116.90/117.29 (P11(f2(f3(a1)),f7(a1))), % 116.90/117.29 inference(scs_inference,[],[408,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,1661,963,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,2042,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22,18,157,3195,3216])). % 116.90/117.29 cnf(4422,plain, % 116.90/117.29 (~P10(f7(f7(f7(f3(a1)))),f7(a1))), % 116.90/117.29 inference(scs_inference,[],[408,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,1661,963,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,2042,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22,18,157,3195,3216,3252,3273,3272,2817,3343,944,946])). % 116.90/117.29 cnf(4448,plain, % 116.90/117.29 (~E(f3(a1),f2(f7(f3(a1))))), % 116.90/117.29 inference(scs_inference,[],[408,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,1661,963,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,2042,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22,18,157,3195,3216,3252,3273,3272,2817,3343,944,946,3395,3399,3404,2071,2075,2252,1390,1880,2170,2249,1384,1388,1386,331])). % 116.90/117.29 cnf(4459,plain, % 116.90/117.29 (P12(f7(f7(f7(a1))),f7(a1))), % 116.90/117.29 inference(scs_inference,[],[408,2982,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,2935,1661,963,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,768,2042,104,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22,18,157,3195,3216,3252,3273,3272,2817,3343,944,946,3395,3399,3404,2071,2075,2252,1390,1880,2170,2249,1384,1388,1386,331,87,161,45,613,614,10,54])). % 116.90/117.29 cnf(4468,plain, % 116.90/117.29 (~P6(f7(f7(f7(f7(a1)))))), % 116.90/117.29 inference(scs_inference,[],[408,2982,2910,2898,2710,2993,2753,2911,2810,2987,2705,2933,2935,1661,963,1105,1139,976,1085,1392,1402,172,576,2805,3342,1677,1698,3442,3458,1143,1121,336,1567,1724,337,338,1111,1142,1039,1049,171,2301,1132,770,769,2182,768,2042,104,767,762,34,40,2707,1952,2721,2815,2936,2943,3173,3189,3848,4,5,7,2718,751,1526,1930,1932,1966,1970,2676,2692,2736,2813,2879,3804,3817,4098,1954,1956,1968,1972,1974,2020,2985,2994,3003,194,420,434,469,1939,1941,2055,2172,2183,2192,2315,2316,2337,2929,2967,3046,3123,3126,1541,1543,1548,1656,1658,1943,2015,2165,2186,2201,2227,1389,1934,1936,2151,2153,2314,2294,2304,2331,1385,1387,36,49,6,99,65,31,39,48,50,43,37,258,185,82,47,57,2,46,3949,3950,3115,3118,3194,3869,4002,3722,3731,3768,3790,2959,3116,3810,3994,662,947,3026,3027,3051,3058,3059,3137,3138,3611,3660,2168,473,615,501,16,3,433,616,15,14,52,23,24,17,26,19,22,18,157,3195,3216,3252,3273,3272,2817,3343,944,946,3395,3399,3404,2071,2075,2252,1390,1880,2170,2249,1384,1388,1386,331,87,161,45,613,614,10,54,25,3260,3218,3246,3250])). % 116.90/117.29 cnf(4528,plain, % 116.90/117.29 ($false), % 116.90/117.29 inference(scs_inference,[],[762,1655,1139,1049,768,1698,1132,337,1142,336,3458,2910,234,3442,338,2753,2987,4307,4227,3426,4408,3325,4243,4459,4223,4448,1662,4404,3590,4422,4468,46,32,2,185,47,82,942,2304,3343,3395,3404,341,345,3262,3264,3247,661,18,20,22,19,26,17,25,24,54,23,10,52]), % 116.90/117.29 ['proof']). % 116.90/117.29 % SZS output end Proof % 116.90/117.29 % Total time :116.200000s %------------------------------------------------------------------------------