%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS161+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 : n028.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:44 EDT 2024 % Result : Theorem 58.78s 58.88s % Output : CNFRefutation 58.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.12 % Problem : KRS161+1 : TPTP v8.2.0. Released v3.1.0. % 0.05/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n028.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 : Wed Jun 19 12:24:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.50/0.58 start to proof:theBenchmark % 58.76/58.84 %------------------------------------------- % 58.76/58.84 % File :CSE---1.7 % 58.76/58.84 % Problem :theBenchmark % 58.76/58.84 % Transform :cnf % 58.76/58.84 % Format :tptp:raw % 58.76/58.84 % Command :java -jar mcs_scs.jar %d %s % 58.76/58.84 % 58.76/58.84 % Result :Theorem 58.150000s % 58.76/58.84 % Output :CNFRefutation 58.150000s % 58.76/58.84 %------------------------------------------- % 58.78/58.85 %------------------------------------------------------------------------------ % 58.78/58.85 % File : KRS161+1 : TPTP v8.2.0. Released v3.1.0. % 58.78/58.85 % Domain : Knowledge Representation (Semantic Web) % 58.78/58.85 % Problem : DL Test: k_poly ABox test from DL98 systems comparison % 58.78/58.85 % Version : Especial. % 58.78/58.85 % English : % 58.78/58.85 % 58.78/58.85 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.78/58.85 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.78/58.85 % Source : [Bec03] % 58.78/58.85 % Names : positive_description-logic-Manifest668 [Bec03] % 58.78/58.85 % 58.78/58.85 % Status : Theorem % 58.78/58.85 % Rating : 0.00 v8.2.0, 0.07 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.20 v6.0.0, 0.25 v5.4.0, 0.26 v5.3.0, 0.30 v5.2.0, 0.21 v5.0.0, 0.20 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0, 0.20 v3.7.0, 0.67 v3.5.0, 0.38 v3.4.0, 0.25 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0 % 58.78/58.85 % Syntax : Number of formulae : 287 ( 99 unt; 0 def) % 58.78/58.85 % Number of atoms : 580 ( 0 equ) % 58.78/58.85 % Maximal formula atoms : 49 ( 2 avg) % 58.78/58.85 % Number of connectives : 340 ( 47 ~; 0 |; 106 &) % 58.78/58.85 % ( 146 <=>; 41 =>; 0 <=; 0 <~>) % 58.78/58.85 % Maximal formula depth : 47 ( 3 avg) % 58.78/58.85 % Maximal term depth : 1 ( 1 avg) % 58.78/58.85 % Number of predicates : 158 ( 158 usr; 0 prp; 1-2 aty) % 58.78/58.85 % Number of functors : 16 ( 16 usr; 16 con; 0-0 aty) % 58.78/58.85 % Number of variables : 303 ( 189 !; 114 ?) % 58.78/58.85 % SPC : FOF_THM_RFO_NEQ % 58.78/58.85 % 58.78/58.85 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.78/58.85 % datatypes, so this problem may not be perfect. At least it's % 58.78/58.85 % still representative of the type of reasoning required for OWL. % 58.78/58.85 %------------------------------------------------------------------------------ % 58.78/58.85 %----Thing and Nothing % 58.78/58.85 fof(axiom_0,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cowlThing(X) % 58.78/58.85 & ~ cowlNothing(X) ) ). % 58.78/58.85 % 58.78/58.85 %----String and Integer disjoint % 58.78/58.85 fof(axiom_1,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( xsd_string(X) % 58.78/58.85 <=> ~ xsd_integer(X) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC10 % 58.78/58.85 fof(axiom_2,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cC10(X) % 58.78/58.85 <=> ( cC8(X) % 58.78/58.85 & cC6(X) ) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC10 % 58.78/58.85 fof(axiom_3,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cC10(X) % 58.78/58.85 <=> ~ ? [Y] : ra_Px73(X,Y) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC10xcomp % 58.78/58.85 fof(axiom_4,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cC10xcomp(X) % 58.78/58.85 <=> ? [Y0] : ra_Px73(X,Y0) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC100 % 58.78/58.85 fof(axiom_5,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cC100(X) % 58.78/58.85 <=> ? [Y] : % 58.78/58.85 ( rR1(X,Y) % 58.78/58.85 & cC98xcomp(Y) ) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC100 % 58.78/58.85 fof(axiom_6,axiom, % 58.78/58.85 ! [X] : % 58.78/58.85 ( cC100(X) % 58.78/58.85 <=> ~ ? [Y] : ra_Px37(X,Y) ) ). % 58.78/58.85 % 58.78/58.85 %----Equality cC100xcomp % 58.78/58.86 fof(axiom_7,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC100xcomp(X) % 58.78/58.86 <=> ? [Y0] : ra_Px37(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC102 % 58.78/58.86 fof(axiom_8,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC102(X) % 58.78/58.86 <=> ? [Y0] : ra_Px36(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC102xcomp % 58.78/58.86 fof(axiom_9,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC102xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px36(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC104 % 58.78/58.86 fof(axiom_10,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC104(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC102xcomp(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC106 % 58.78/58.86 fof(axiom_11,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC106(X) % 58.78/58.86 <=> ( cC104(X) % 58.78/58.86 & cC100xcomp(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC108 % 58.78/58.86 fof(axiom_12,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC108(X) % 58.78/58.86 <=> ( cC28(X) % 58.78/58.86 & cC106(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC110 % 58.78/58.86 fof(axiom_13,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC110(X) % 58.78/58.86 <=> ( cC4xcomp(X) % 58.78/58.86 & cC12xcomp(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC112 % 58.78/58.86 fof(axiom_14,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC112(X) % 58.78/58.86 <=> ( cC110(X) % 58.78/58.86 & cC102xcomp(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC114 % 58.78/58.86 fof(axiom_15,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC114(X) % 58.78/58.86 <=> ? [Y0] : ra_Px41(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC114xcomp % 58.78/58.86 fof(axiom_16,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC114xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px41(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC116 % 58.78/58.86 fof(axiom_17,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC116(X) % 58.78/58.86 <=> ( cC112(X) % 58.78/58.86 & cC114xcomp(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC118 % 58.78/58.86 fof(axiom_18,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC118(X) % 58.78/58.86 <=> ? [Y0] : ra_Px42(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC118xcomp % 58.78/58.86 fof(axiom_19,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC118xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px42(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC12 % 58.78/58.86 fof(axiom_20,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC12(X) % 58.78/58.86 <=> ? [Y0] : ra_Px18(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC12xcomp % 58.78/58.86 fof(axiom_21,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC12xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px18(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC120 % 58.78/58.86 fof(axiom_22,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC120(X) % 58.78/58.86 <=> ( cC116(X) % 58.78/58.86 & cC118xcomp(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC120 % 58.78/58.86 fof(axiom_23,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC120(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px43(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC120xcomp % 58.78/58.86 fof(axiom_24,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC120xcomp(X) % 58.78/58.86 <=> ? [Y0] : ra_Px43(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC122 % 58.78/58.86 fof(axiom_25,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC122(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC120xcomp(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC124 % 58.78/58.86 fof(axiom_26,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC124(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC122(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC126 % 58.78/58.86 fof(axiom_27,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC126(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC124(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC128 % 58.78/58.86 fof(axiom_28,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC128(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC126(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC130 % 58.78/58.86 fof(axiom_29,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC130(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC128(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC14 % 58.78/58.86 fof(axiom_30,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC14(X) % 58.78/58.86 <=> ? [Y0] : ra_Px74(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC14 % 58.78/58.86 fof(axiom_31,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC14(X) % 58.78/58.86 <=> ( cC10(X) % 58.78/58.86 & cC12(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC14xcomp % 58.78/58.86 fof(axiom_32,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC14xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px74(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC16 % 58.78/58.86 fof(axiom_33,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC16(X) % 58.78/58.86 <=> ? [Y0] : ra_Px27(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC16xcomp % 58.78/58.86 fof(axiom_34,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC16xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px27(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC18 % 58.78/58.86 fof(axiom_35,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC18(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC18 % 58.78/58.86 fof(axiom_36,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC18(X) % 58.78/58.86 <=> ( cC14(X) % 58.78/58.86 & cC16(X) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC18xcomp % 58.78/58.86 fof(axiom_37,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC18xcomp(X) % 58.78/58.86 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC2 % 58.78/58.86 fof(axiom_38,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC2(X) % 58.78/58.86 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC2xcomp % 58.78/58.86 fof(axiom_39,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC2xcomp(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC20 % 58.78/58.86 fof(axiom_40,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC20(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC18xcomp(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC22 % 58.78/58.86 fof(axiom_41,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC22(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC20(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC24 % 58.78/58.86 fof(axiom_42,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC24(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC22(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC26 % 58.78/58.86 fof(axiom_43,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC26(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC24(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC28 % 58.78/58.86 fof(axiom_44,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC28(X) % 58.78/58.86 <=> ? [Y] : % 58.78/58.86 ( rR1(X,Y) % 58.78/58.86 & cC26(Y) ) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC30 % 58.78/58.86 fof(axiom_45,axiom, % 58.78/58.86 ! [X] : % 58.78/58.86 ( cC30(X) % 58.78/58.86 <=> ~ ? [Y] : ra_Px4(X,Y) ) ). % 58.78/58.86 % 58.78/58.86 %----Equality cC30 % 58.78/58.87 fof(axiom_46,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC30(X) % 58.78/58.87 <=> ( cC2(X) % 58.78/58.87 & cC4(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC30xcomp % 58.78/58.87 fof(axiom_47,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC30xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px4(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC32 % 58.78/58.87 fof(axiom_48,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC32(X) % 58.78/58.87 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC32 % 58.78/58.87 fof(axiom_49,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC32(X) % 58.78/58.87 <=> ( cC4xcomp(X) % 58.78/58.87 & cC2xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC32xcomp % 58.78/58.87 fof(axiom_50,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC32xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC34 % 58.78/58.87 fof(axiom_51,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC34(X) % 58.78/58.87 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC34 % 58.78/58.87 fof(axiom_52,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC34(X) % 58.78/58.87 <=> ( cC30xcomp(X) % 58.78/58.87 & cC32xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC34xcomp % 58.78/58.87 fof(axiom_53,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC34xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC36 % 58.78/58.87 fof(axiom_54,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC36(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC36 % 58.78/58.87 fof(axiom_55,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC36(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC34xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC36xcomp % 58.78/58.87 fof(axiom_56,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC36xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC38 % 58.78/58.87 fof(axiom_57,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC38(X) % 58.78/58.87 <=> ( cTOP(X) % 58.78/58.87 & cC36xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC38 % 58.78/58.87 fof(axiom_58,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC38(X) % 58.78/58.87 <=> ? [Y0] : ra_Px8(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC38xcomp % 58.78/58.87 fof(axiom_59,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC38xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px8(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC4 % 58.78/58.87 fof(axiom_60,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC4(X) % 58.78/58.87 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC4xcomp % 58.78/58.87 fof(axiom_61,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC4xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC40 % 58.78/58.87 fof(axiom_62,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC40(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px10(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC40 % 58.78/58.87 fof(axiom_63,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC40(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC38xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC40xcomp % 58.78/58.87 fof(axiom_64,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC40xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px10(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC42 % 58.78/58.87 fof(axiom_65,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC42(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC8xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC44 % 58.78/58.87 fof(axiom_66,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC44(X) % 58.78/58.87 <=> ( cC40xcomp(X) % 58.78/58.87 & cC42(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC46 % 58.78/58.87 fof(axiom_67,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC46(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px13(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC46 % 58.78/58.87 fof(axiom_68,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC46(X) % 58.78/58.87 <=> ( cC8(X) % 58.78/58.87 & cC4(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC46xcomp % 58.78/58.87 fof(axiom_69,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC46xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px13(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC48 % 58.78/58.87 fof(axiom_70,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC48(X) % 58.78/58.87 <=> ( cC4xcomp(X) % 58.78/58.87 & cC8xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC48 % 58.78/58.87 fof(axiom_71,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC48(X) % 58.78/58.87 <=> ? [Y0] : ra_Px14(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC48xcomp % 58.78/58.87 fof(axiom_72,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC48xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px14(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC50 % 58.78/58.87 fof(axiom_73,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC50(X) % 58.78/58.87 <=> ( cC46xcomp(X) % 58.78/58.87 & cC48xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC50 % 58.78/58.87 fof(axiom_74,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC50(X) % 58.78/58.87 <=> ? [Y0] : ra_Px15(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC50xcomp % 58.78/58.87 fof(axiom_75,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC50xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px15(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC52 % 58.78/58.87 fof(axiom_76,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC52(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px49(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC52 % 58.78/58.87 fof(axiom_77,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC52(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC50xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC52xcomp % 58.78/58.87 fof(axiom_78,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC52xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px49(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC54 % 58.78/58.87 fof(axiom_79,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC54(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px16(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC54 % 58.78/58.87 fof(axiom_80,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC54(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC52(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC54xcomp % 58.78/58.87 fof(axiom_81,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC54xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px16(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC56 % 58.78/58.87 fof(axiom_82,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC56(X) % 58.78/58.87 <=> ( cC54xcomp(X) % 58.78/58.87 & cC44(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC56 % 58.78/58.87 fof(axiom_83,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC56(X) % 58.78/58.87 <=> ? [Y0] : ra_Px17(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC56xcomp % 58.78/58.87 fof(axiom_84,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC56xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px17(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC58 % 58.78/58.87 fof(axiom_85,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC58(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC56xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC58 % 58.78/58.87 fof(axiom_86,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC58(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px19(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC58xcomp % 58.78/58.87 fof(axiom_87,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC58xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px19(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC6 % 58.78/58.87 fof(axiom_88,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC6(X) % 58.78/58.87 <=> ( cC2(X) % 58.78/58.87 & cC4(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC6 % 58.78/58.87 fof(axiom_89,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC6(X) % 58.78/58.87 <=> ? [Y0] : ra_Px72(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC6xcomp % 58.78/58.87 fof(axiom_90,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC6xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px72(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC60 % 58.78/58.87 fof(axiom_91,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC60(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC12xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC62 % 58.78/58.87 fof(axiom_92,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC62(X) % 58.78/58.87 <=> ( cC60(X) % 58.78/58.87 & cC58xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC64 % 58.78/58.87 fof(axiom_93,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC64(X) % 58.78/58.87 <=> ( cC8(X) % 58.78/58.87 & cC12(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC64 % 58.78/58.87 fof(axiom_94,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC64(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px22(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC64xcomp % 58.78/58.87 fof(axiom_95,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC64xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px22(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC66 % 58.78/58.87 fof(axiom_96,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC66(X) % 58.78/58.87 <=> ( cC12xcomp(X) % 58.78/58.87 & cC8xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC66 % 58.78/58.87 fof(axiom_97,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC66(X) % 58.78/58.87 <=> ? [Y0] : ra_Px23(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC66xcomp % 58.78/58.87 fof(axiom_98,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC66xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px23(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC68 % 58.78/58.87 fof(axiom_99,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC68(X) % 58.78/58.87 <=> ? [Y0] : ra_Px24(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC68 % 58.78/58.87 fof(axiom_100,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC68(X) % 58.78/58.87 <=> ( cC64xcomp(X) % 58.78/58.87 & cC66xcomp(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC68xcomp % 58.78/58.87 fof(axiom_101,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC68xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px24(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC70 % 58.78/58.87 fof(axiom_102,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC70(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC68xcomp(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC70 % 58.78/58.87 fof(axiom_103,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC70(X) % 58.78/58.87 <=> ? [Y0] : ra_Px51(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC70xcomp % 58.78/58.87 fof(axiom_104,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC70xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px51(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC72 % 58.78/58.87 fof(axiom_105,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC72(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC70(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC72 % 58.78/58.87 fof(axiom_106,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC72(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px58(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC72xcomp % 58.78/58.87 fof(axiom_107,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC72xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px58(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC74 % 58.78/58.87 fof(axiom_108,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC74(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC72(Y) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC74 % 58.78/58.87 fof(axiom_109,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC74(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px25(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC74xcomp % 58.78/58.87 fof(axiom_110,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC74xcomp(X) % 58.78/58.87 <=> ? [Y0] : ra_Px25(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC76 % 58.78/58.87 fof(axiom_111,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC76(X) % 58.78/58.87 <=> ? [Y0] : ra_Px26(X,Y0) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC76 % 58.78/58.87 fof(axiom_112,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC76(X) % 58.78/58.87 <=> ( cC74xcomp(X) % 58.78/58.87 & cC62(X) ) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC76xcomp % 58.78/58.87 fof(axiom_113,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC76xcomp(X) % 58.78/58.87 <=> ~ ? [Y] : ra_Px26(X,Y) ) ). % 58.78/58.87 % 58.78/58.87 %----Equality cC78 % 58.78/58.87 fof(axiom_114,axiom, % 58.78/58.87 ! [X] : % 58.78/58.87 ( cC78(X) % 58.78/58.87 <=> ? [Y] : % 58.78/58.87 ( rR1(X,Y) % 58.78/58.87 & cC76xcomp(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC78 % 58.78/58.88 fof(axiom_115,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC78(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px28(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC78xcomp % 58.78/58.88 fof(axiom_116,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC78xcomp(X) % 58.78/58.88 <=> ? [Y0] : ra_Px28(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC8 % 58.78/58.88 fof(axiom_117,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC8(X) % 58.78/58.88 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC8xcomp % 58.78/58.88 fof(axiom_118,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC8xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC80 % 58.78/58.88 fof(axiom_119,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC80(X) % 58.78/58.88 <=> ? [Y] : % 58.78/58.88 ( rR1(X,Y) % 58.78/58.88 & cC16xcomp(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC82 % 58.78/58.88 fof(axiom_120,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC82(X) % 58.78/58.88 <=> ( cC80(X) % 58.78/58.88 & cC78xcomp(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC84 % 58.78/58.88 fof(axiom_121,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC84(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px31(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC84 % 58.78/58.88 fof(axiom_122,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC84(X) % 58.78/58.88 <=> ( cC2(X) % 58.78/58.88 & cC12(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC84xcomp % 58.78/58.88 fof(axiom_123,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC84xcomp(X) % 58.78/58.88 <=> ? [Y0] : ra_Px31(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC86 % 58.78/58.88 fof(axiom_124,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC86(X) % 58.78/58.88 <=> ( cC12xcomp(X) % 58.78/58.88 & cC2xcomp(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC86 % 58.78/58.88 fof(axiom_125,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC86(X) % 58.78/58.88 <=> ? [Y0] : ra_Px32(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC86xcomp % 58.78/58.88 fof(axiom_126,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC86xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px32(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC88 % 58.78/58.88 fof(axiom_127,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC88(X) % 58.78/58.88 <=> ? [Y0] : ra_Px33(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC88 % 58.78/58.88 fof(axiom_128,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC88(X) % 58.78/58.88 <=> ( cC84xcomp(X) % 58.78/58.88 & cC86xcomp(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC88xcomp % 58.78/58.88 fof(axiom_129,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC88xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px33(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC90 % 58.78/58.88 fof(axiom_130,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC90(X) % 58.78/58.88 <=> ? [Y0] : ra_Px50(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC90 % 58.78/58.88 fof(axiom_131,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC90(X) % 58.78/58.88 <=> ? [Y] : % 58.78/58.88 ( rR1(X,Y) % 58.78/58.88 & cC88xcomp(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC90xcomp % 58.78/58.88 fof(axiom_132,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC90xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px50(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC92 % 58.78/58.88 fof(axiom_133,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC92(X) % 58.78/58.88 <=> ? [Y0] : ra_Px57(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC92 % 58.78/58.88 fof(axiom_134,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC92(X) % 58.78/58.88 <=> ? [Y] : % 58.78/58.88 ( rR1(X,Y) % 58.78/58.88 & cC90(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC92xcomp % 58.78/58.88 fof(axiom_135,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC92xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px57(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC94 % 58.78/58.88 fof(axiom_136,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC94(X) % 58.78/58.88 <=> ? [Y] : % 58.78/58.88 ( rR1(X,Y) % 58.78/58.88 & cC92(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC94 % 58.78/58.88 fof(axiom_137,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC94(X) % 58.78/58.88 <=> ? [Y0] : ra_Px48(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC94xcomp % 58.78/58.88 fof(axiom_138,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC94xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px48(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC96 % 58.78/58.88 fof(axiom_139,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC96(X) % 58.78/58.88 <=> ? [Y] : % 58.78/58.88 ( rR1(X,Y) % 58.78/58.88 & cC94(Y) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC96 % 58.78/58.88 fof(axiom_140,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC96(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px34(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC96xcomp % 58.78/58.88 fof(axiom_141,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC96xcomp(X) % 58.78/58.88 <=> ? [Y0] : ra_Px34(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC98 % 58.78/58.88 fof(axiom_142,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC98(X) % 58.78/58.88 <=> ? [Y0] : ra_Px35(X,Y0) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC98 % 58.78/58.88 fof(axiom_143,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC98(X) % 58.78/58.88 <=> ( cC96xcomp(X) % 58.78/58.88 & cC82(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cC98xcomp % 58.78/58.88 fof(axiom_144,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cC98xcomp(X) % 58.78/58.88 <=> ~ ? [Y] : ra_Px35(X,Y) ) ). % 58.78/58.88 % 58.78/58.88 %----Equality cTEST % 58.78/58.88 fof(axiom_145,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( cTEST(X) % 58.78/58.88 <=> ( cC108(X) % 58.78/58.88 & cC130(X) ) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16439 % 58.78/58.88 fof(axiom_146,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16439,X) % 58.78/58.88 => cC98(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16439 % 58.78/58.88 fof(axiom_147,axiom, % 58.78/58.88 cowlThing(iV16439) ). % 58.78/58.88 % 58.78/58.88 %----iV16439 % 58.78/58.88 fof(axiom_148,axiom, % 58.78/58.88 cC100xcomp(iV16439) ). % 58.78/58.88 % 58.78/58.88 %----iV16439 % 58.78/58.88 fof(axiom_149,axiom, % 58.78/58.88 cTEST(iV16439) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_150,axiom, % 58.78/58.88 rR1(iV16439,iV16440) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_151,axiom, % 58.78/58.88 rR1(iV16439,iV16442) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_152,axiom, % 58.78/58.88 rR1(iV16439,iV16441) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_153,axiom, % 58.78/58.88 cowlThing(iV16440) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_154,axiom, % 58.78/58.88 cC96xcomp(iV16440) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_155,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16440,X) % 58.78/58.88 => cC94xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_156,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16440,X) % 58.78/58.88 => cC76(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_157,axiom, % 58.78/58.88 cC102xcomp(iV16440) ). % 58.78/58.88 % 58.78/58.88 %----iV16440 % 58.78/58.88 fof(axiom_158,axiom, % 58.78/58.88 cC78xcomp(iV16440) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_159,axiom, % 58.78/58.88 rR1(iV16440,iV16463) ). % 58.78/58.88 % 58.78/58.88 %----iV16441 % 58.78/58.88 fof(axiom_160,axiom, % 58.78/58.88 cowlThing(iV16441) ). % 58.78/58.88 % 58.78/58.88 %----iV16442 % 58.78/58.88 fof(axiom_161,axiom, % 58.78/58.88 cowlThing(iV16442) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_162,axiom, % 58.78/58.88 cowlThing(iV16448) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_163,axiom, % 58.78/58.88 cTOP(iV16448) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_164,axiom, % 58.78/58.88 cC52xcomp(iV16448) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_165,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16448,X) % 58.78/58.88 => cC50(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_166,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16448,X) % 58.78/58.88 => cC68(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_167,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16448,X) % 58.78/58.88 => cC34(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_168,axiom, % 58.78/58.88 cC36xcomp(iV16448) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_169,axiom, % 58.78/58.88 cC90xcomp(iV16448) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_170,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16448,X) % 58.78/58.88 => cC88(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16448 % 58.78/58.88 fof(axiom_171,axiom, % 58.78/58.88 cC70xcomp(iV16448) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_172,axiom, % 58.78/58.88 rR1(iV16448,iV16449) ). % 58.78/58.88 % 58.78/58.88 %----iV16449 % 58.78/58.88 fof(axiom_173,axiom, % 58.78/58.88 cowlThing(iV16449) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_174,axiom, % 58.78/58.88 cC74xcomp(iV16453) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_175,axiom, % 58.78/58.88 cowlThing(iV16453) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_176,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16453,X) % 58.78/58.88 => cC72xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_177,axiom, % 58.78/58.88 cC16xcomp(iV16453) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_178,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16453,X) % 58.78/58.88 => cC56(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_179,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16453,X) % 58.78/58.88 => cC92xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_180,axiom, % 58.78/58.88 cC94xcomp(iV16453) ). % 58.78/58.88 % 58.78/58.88 %----iV16453 % 58.78/58.88 fof(axiom_181,axiom, % 58.78/58.88 cC58xcomp(iV16453) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_182,axiom, % 58.78/58.88 rR1(iV16453,iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_183,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16455,X) % 58.78/58.88 => cC52xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_184,axiom, % 58.78/58.88 cowlThing(iV16455) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_185,axiom, % 58.78/58.88 cC40xcomp(iV16455) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_186,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16455,X) % 58.78/58.88 => cC90xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_187,axiom, % 58.78/58.88 cC12xcomp(iV16455) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_188,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16455,X) % 58.78/58.88 => cC38(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_189,axiom, % 58.78/58.88 cC92xcomp(iV16455) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_190,axiom, % 58.78/58.88 cC54xcomp(iV16455) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_191,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16455,X) % 58.78/58.88 => cC70xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16455 % 58.78/58.88 fof(axiom_192,axiom, % 58.78/58.88 cC72xcomp(iV16455) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_193,axiom, % 58.78/58.88 rR1(iV16455,iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_194,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16457,X) % 58.78/58.88 => cC68(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_195,axiom, % 58.78/58.88 cowlThing(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_196,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16457,X) % 58.78/58.88 => cC34(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_197,axiom, % 58.78/58.88 cTOP(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_198,axiom, % 58.78/58.88 cC52xcomp(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_199,axiom, % 58.78/58.88 cC8xcomp(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_200,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16457,X) % 58.78/58.88 => cC88(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_201,axiom, % 58.78/58.88 cC36xcomp(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_202,axiom, % 58.78/58.88 cC90xcomp(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_203,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16457,X) % 58.78/58.88 => cC50(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16457 % 58.78/58.88 fof(axiom_204,axiom, % 58.78/58.88 cC70xcomp(iV16457) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_205,axiom, % 58.78/58.88 cowlThing(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_206,axiom, % 58.78/58.88 cC14xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_207,axiom, % 58.78/58.88 cC8xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_208,axiom, % 58.78/58.88 cC10xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_209,axiom, % 58.78/58.88 cC30xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_210,axiom, % 58.78/58.88 cC84xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_211,axiom, % 58.78/58.88 cC12(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_212,axiom, % 58.78/58.88 cC46xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_213,axiom, % 58.78/58.88 cC64xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_214,axiom, % 58.78/58.88 cC4(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_215,axiom, % 58.78/58.88 cC86xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_216,axiom, % 58.78/58.88 cC32xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_217,axiom, % 58.78/58.88 cC48xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_218,axiom, % 58.78/58.88 cC18xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_219,axiom, % 58.78/58.88 cC2xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_220,axiom, % 58.78/58.88 cC6xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16459 % 58.78/58.88 fof(axiom_221,axiom, % 58.78/58.88 cC66xcomp(iV16459) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_222,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16460,X) % 58.78/58.88 => cC68(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_223,axiom, % 58.78/58.88 cowlThing(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_224,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16460,X) % 58.78/58.88 => cC34(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_225,axiom, % 58.78/58.88 cTOP(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_226,axiom, % 58.78/58.88 cC52xcomp(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_227,axiom, % 58.78/58.88 cC8xcomp(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_228,axiom, % 58.78/58.88 cC36xcomp(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_229,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16460,X) % 58.78/58.88 => cC50(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_230,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16460,X) % 58.78/58.88 => cC88(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_231,axiom, % 58.78/58.88 cC90xcomp(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16460 % 58.78/58.88 fof(axiom_232,axiom, % 58.78/58.88 cC70xcomp(iV16460) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_233,axiom, % 58.78/58.88 cowlThing(iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_234,axiom, % 58.78/58.88 cC40xcomp(iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_235,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16461,X) % 58.78/58.88 => cC90xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_236,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16461,X) % 58.78/58.88 => cC70xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_237,axiom, % 58.78/58.88 cC12xcomp(iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_238,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16461,X) % 58.78/58.88 => cC52xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_239,axiom, % 58.78/58.88 cC92xcomp(iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_240,axiom, % 58.78/58.88 cC54xcomp(iV16461) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_241,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16461,X) % 58.78/58.88 => cC38(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16461 % 58.78/58.88 fof(axiom_242,axiom, % 58.78/58.88 cC72xcomp(iV16461) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_243,axiom, % 58.78/58.88 rR1(iV16461,iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_244,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16462,X) % 58.78/58.88 => cC50(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_245,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16462,X) % 58.78/58.88 => cC68(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_246,axiom, % 58.78/58.88 cowlThing(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_247,axiom, % 58.78/58.88 cTOP(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_248,axiom, % 58.78/58.88 cC52xcomp(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_249,axiom, % 58.78/58.88 cC8xcomp(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_250,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16462,X) % 58.78/58.88 => cC34(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_251,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16462,X) % 58.78/58.88 => cC88(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_252,axiom, % 58.78/58.88 cC36xcomp(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_253,axiom, % 58.78/58.88 cC90xcomp(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16462 % 58.78/58.88 fof(axiom_254,axiom, % 58.78/58.88 cC70xcomp(iV16462) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_255,axiom, % 58.78/58.88 cC74xcomp(iV16463) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_256,axiom, % 58.78/58.88 cowlThing(iV16463) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_257,axiom, % 58.78/58.88 cC16xcomp(iV16463) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_258,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16463,X) % 58.78/58.88 => cC92xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_259,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16463,X) % 58.78/58.88 => cC72xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_260,axiom, % 58.78/58.88 cC94xcomp(iV16463) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_261,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16463,X) % 58.78/58.88 => cC56(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16463 % 58.78/58.88 fof(axiom_262,axiom, % 58.78/58.88 cC58xcomp(iV16463) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_263,axiom, % 58.78/58.88 rR1(iV16463,iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_264,axiom, % 58.78/58.88 cowlThing(iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_265,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16464,X) % 58.78/58.88 => cC38(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_266,axiom, % 58.78/58.88 cC40xcomp(iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_267,axiom, % 58.78/58.88 cC12xcomp(iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_268,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16464,X) % 58.78/58.88 => cC52xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_269,axiom, % 58.78/58.88 cC92xcomp(iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_270,axiom, % 58.78/58.88 cC54xcomp(iV16464) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_271,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16464,X) % 58.78/58.88 => cC90xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_272,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16464,X) % 58.78/58.88 => cC70xcomp(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16464 % 58.78/58.88 fof(axiom_273,axiom, % 58.78/58.88 cC72xcomp(iV16464) ). % 58.78/58.88 % 58.78/58.88 fof(axiom_274,axiom, % 58.78/58.88 rR1(iV16464,iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_275,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16465,X) % 58.78/58.88 => cC34(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_276,axiom, % 58.78/58.88 cowlThing(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_277,axiom, % 58.78/58.88 cTOP(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_278,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16465,X) % 58.78/58.88 => cC88(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_279,axiom, % 58.78/58.88 cC52xcomp(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_280,axiom, % 58.78/58.88 cC8xcomp(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_281,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16465,X) % 58.78/58.88 => cC68(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_282,axiom, % 58.78/58.88 cC36xcomp(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_283,axiom, % 58.78/58.88 cC90xcomp(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_284,axiom, % 58.78/58.88 ! [X] : % 58.78/58.88 ( rR1(iV16465,X) % 58.78/58.88 => cC50(X) ) ). % 58.78/58.88 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(axiom_285,axiom, % 58.78/58.88 cC70xcomp(iV16465) ). % 58.78/58.88 % 58.78/58.88 %----Thing and Nothing % 58.78/58.88 %----String and Integer disjoint % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16439 % 58.78/58.88 %----iV16440 % 58.78/58.88 %----iV16440 % 58.78/58.88 %----iV16440 % 58.78/58.88 %----iV16440 % 58.78/58.88 %----iV16448 % 58.78/58.88 %----iV16448 % 58.78/58.88 %----iV16453 % 58.78/58.88 %----iV16453 % 58.78/58.88 %----iV16453 % 58.78/58.88 %----iV16453 % 58.78/58.88 %----iV16455 % 58.78/58.88 %----iV16455 % 58.78/58.88 %----iV16455 % 58.78/58.88 %----iV16455 % 58.78/58.88 %----iV16457 % 58.78/58.88 %----iV16457 % 58.78/58.88 %----iV16459 % 58.78/58.88 %----iV16459 % 58.78/58.88 %----iV16459 % 58.78/58.88 %----iV16459 % 58.78/58.88 %----iV16459 % 58.78/58.88 %----iV16460 % 58.78/58.88 %----iV16460 % 58.78/58.88 %----iV16461 % 58.78/58.88 %----iV16461 % 58.78/58.88 %----iV16461 % 58.78/58.88 %----iV16461 % 58.78/58.88 %----iV16462 % 58.78/58.88 %----iV16462 % 58.78/58.88 %----iV16463 % 58.78/58.88 %----iV16463 % 58.78/58.88 %----iV16463 % 58.78/58.88 %----iV16463 % 58.78/58.88 %----iV16464 % 58.78/58.88 %----iV16464 % 58.78/58.88 %----iV16464 % 58.78/58.88 %----iV16464 % 58.78/58.88 %----iV16465 % 58.78/58.88 %----iV16465 % 58.78/58.88 fof(the_axiom,conjecture, % 58.78/58.88 ( ! [X] : % 58.78/58.88 ( cowlThing(X) % 58.78/58.88 & ~ cowlNothing(X) ) % 58.78/58.88 & ! [X] : % 58.78/58.88 ( xsd_string(X) % 58.78/58.88 <=> ~ xsd_integer(X) ) % 58.78/58.88 & cC130(iV16439) % 58.78/58.88 & cC108(iV16439) % 58.78/58.88 & cC104(iV16439) % 58.78/58.88 & cC106(iV16439) % 58.78/58.88 & cC28(iV16439) % 58.78/58.88 & cowlThing(iV16439) % 58.78/58.88 & cC98(iV16440) % 58.78/58.88 & cC80(iV16440) % 58.78/58.88 & cC82(iV16440) % 58.78/58.88 & cowlThing(iV16440) % 58.78/58.88 & cC38(iV16448) % 58.78/58.88 & cowlThing(iV16448) % 58.78/58.88 & cC76(iV16453) % 58.78/58.88 & cC62(iV16453) % 58.78/58.88 & cowlThing(iV16453) % 58.78/58.88 & cC60(iV16453) % 58.78/58.88 & cC56(iV16455) % 58.78/58.88 & cC44(iV16455) % 58.78/58.88 & cC42(iV16455) % 58.78/58.88 & cowlThing(iV16455) % 58.78/58.88 & cC38(iV16457) % 58.78/58.88 & cowlThing(iV16457) % 58.78/58.88 & cC50(iV16459) % 58.78/58.88 & cC88(iV16459) % 58.78/58.88 & cC34(iV16459) % 58.78/58.88 & cC68(iV16459) % 58.78/58.88 & cowlThing(iV16459) % 58.78/58.88 & cC38(iV16460) % 58.78/58.88 & cowlThing(iV16460) % 58.78/58.88 & cC42(iV16461) % 58.78/58.88 & cC56(iV16461) % 58.78/58.88 & cC44(iV16461) % 58.78/58.88 & cowlThing(iV16461) % 58.78/58.88 & cC38(iV16462) % 58.78/58.88 & cowlThing(iV16462) % 58.78/58.88 & cC76(iV16463) % 58.78/58.88 & cC62(iV16463) % 58.78/58.88 & cowlThing(iV16463) % 58.78/58.88 & cC60(iV16463) % 58.78/58.88 & cC56(iV16464) % 58.78/58.88 & cC42(iV16464) % 58.78/58.88 & cC44(iV16464) % 58.78/58.88 & cowlThing(iV16464) % 58.78/58.88 & cC38(iV16465) % 58.78/58.88 & cowlThing(iV16465) ) ). % 58.78/58.88 % 58.78/58.88 %------------------------------------------------------------------------------ % 58.78/58.88 %------------------------------------------- % 58.78/58.88 % Proof found % 58.78/58.88 % SZS status Theorem for theBenchmark % 58.78/58.88 % SZS output start Proof % 58.78/58.88 %ClaNum:475(EqnAxiom:0) % 58.78/58.88 %VarNum:1065(SingletonVarNum:504) % 58.78/58.88 %MaxLitNum:35 % 58.78/58.88 %MaxfuncDepth:1 % 58.78/58.88 %SharedTerms:138 % 58.78/58.88 %goalClause: 474 475 % 58.78/58.88 [1]P1(a1) % 58.78/58.88 [2]P2(a2) % 58.78/58.88 [3]P5(a119) % 58.78/58.88 [4]P10(a127) % 58.78/58.88 [5]P10(a120) % 58.78/58.88 [6]P10(a129) % 58.78/58.88 [7]P11(a1) % 58.78/58.88 [8]P25(a1) % 58.78/58.88 [9]P28(a130) % 58.78/58.88 [10]P28(a121) % 58.78/58.88 [11]P30(a1) % 58.78/58.88 [12]P32(a1) % 58.78/58.88 [13]P39(a1) % 58.78/58.88 [14]P40(a1) % 58.78/58.88 [15]P42(a1) % 58.78/58.88 [16]P44(a122) % 58.78/58.88 [17]P44(a128) % 58.78/58.88 [18]P44(a126) % 58.78/58.88 [19]P44(a131) % 58.78/58.88 [20]P44(a132) % 58.78/58.88 [21]P50(a122) % 58.78/58.88 [22]P50(a128) % 58.78/58.88 [23]P50(a126) % 58.78/58.88 [24]P50(a131) % 58.78/58.88 [25]P50(a132) % 58.78/58.88 [26]P51(a127) % 58.78/58.88 [27]P51(a120) % 58.78/58.88 [28]P51(a129) % 58.78/58.88 [29]P53(a128) % 58.78/58.88 [30]P53(a126) % 58.78/58.88 [31]P53(a1) % 58.78/58.88 [32]P53(a131) % 58.78/58.88 [33]P53(a132) % 58.78/58.88 [34]P54(a1) % 58.78/58.88 [35]P58(a1) % 58.78/58.88 [36]P60(a122) % 58.78/58.88 [37]P60(a128) % 58.78/58.88 [38]P60(a126) % 58.78/58.88 [39]P60(a131) % 58.78/58.88 [40]P60(a132) % 58.78/58.88 [41]P65(a127) % 58.78/58.88 [42]P65(a120) % 58.78/58.88 [43]P65(a129) % 58.78/58.88 [44]P67(a130) % 58.78/58.88 [45]P67(a121) % 58.78/58.88 [46]P71(a1) % 58.78/58.88 [47]P72(a1) % 58.78/58.88 [48]P77(a1) % 58.78/58.88 [49]P81(a122) % 58.78/58.88 [50]P81(a128) % 58.78/58.88 [51]P81(a126) % 58.78/58.88 [52]P81(a131) % 58.78/58.88 [53]P81(a132) % 58.78/58.88 [54]P83(a127) % 58.78/58.88 [55]P83(a120) % 58.78/58.88 [56]P83(a129) % 58.78/58.88 [57]P85(a130) % 58.78/58.88 [58]P85(a121) % 58.78/58.88 [59]P87(a119) % 58.78/58.88 [60]P91(a1) % 58.78/58.88 [61]P96(a1) % 58.78/58.88 [62]P100(a122) % 58.78/58.88 [63]P100(a128) % 58.78/58.88 [64]P100(a126) % 58.78/58.88 [65]P100(a131) % 58.78/58.88 [66]P100(a132) % 58.78/58.88 [67]P102(a127) % 58.78/58.88 [68]P102(a120) % 58.78/58.88 [69]P102(a129) % 58.78/58.88 [70]P104(a130) % 58.78/58.88 [71]P104(a121) % 58.78/58.88 [72]P106(a119) % 58.78/58.88 [73]P108(a2) % 58.78/58.88 [74]P111(a2,a119) % 58.78/58.88 [75]P111(a2,a123) % 58.78/58.88 [76]P111(a2,a124) % 58.78/58.88 [77]P111(a119,a130) % 58.78/58.88 [78]P111(a130,a129) % 58.78/58.88 [79]P111(a122,a125) % 58.78/58.88 [80]P111(a121,a127) % 58.78/58.88 [81]P111(a127,a131) % 58.78/58.88 [82]P111(a120,a128) % 58.78/58.88 [83]P111(a129,a132) % 58.78/58.88 [84]~P112(x841) % 58.78/58.88 [85]P114(x851)+P113(x851) % 58.78/58.88 [86]~P26(x861)+P3(x861) % 58.78/58.88 [87]~P3(x871)+P92(x871) % 58.78/58.88 [88]~P55(x881)+P92(x881) % 58.78/58.88 [89]~P73(x891)+P92(x891) % 58.78/58.88 [90]~P3(x901)+P74(x901) % 58.78/58.88 [91]~P7(x911)+P2(x911) % 58.78/58.88 [92]~P12(x921)+P5(x921) % 58.78/58.88 [93]~P7(x931)+P8(x931) % 58.78/58.88 [94]~P9(x941)+P7(x941) % 58.78/58.88 [95]~P108(x951)+P9(x951) % 58.78/58.88 [96]~P9(x961)+P33(x961) % 58.78/58.88 [97]~P12(x971)+P13(x971) % 58.78/58.88 [98]~P13(x981)+P61(x981) % 58.78/58.88 [99]~P43(x991)+P61(x991) % 58.78/58.88 [100]~P59(x1001)+P61(x1001) % 58.78/58.88 [101]~P13(x1011)+P10(x1011) % 58.78/58.88 [102]~P78(x1021)+P10(x1021) % 58.78/58.88 [103]~P97(x1031)+P10(x1031) % 58.78/58.88 [104]~P14(x1041)+P12(x1041) % 58.78/58.88 [105]~P14(x1051)+P15(x1051) % 58.78/58.88 [106]~P19(x1061)+P14(x1061) % 58.78/58.88 [107]~P19(x1071)+P17(x1071) % 58.78/58.88 [108]~P26(x1081)+P11(x1081) % 58.78/58.88 [109]~P73(x1091)+P11(x1091) % 58.78/58.88 [110]~P93(x1101)+P11(x1101) % 58.78/58.88 [111]~P108(x1111)+P27(x1111) % 58.78/58.88 [112]~P31(x1121)+P26(x1121) % 58.78/58.88 [113]~P31(x1131)+P29(x1131) % 58.78/58.88 [114]~P74(x1141)+P34(x1141) % 58.78/58.88 [115]~P41(x1151)+P34(x1151) % 58.78/58.88 [116]~P93(x1161)+P34(x1161) % 58.78/58.88 [117]~P43(x1171)+P32(x1171) % 58.78/58.88 [118]~P97(x1181)+P32(x1181) % 58.78/58.88 [119]~P74(x1191)+P39(x1191) % 58.78/58.88 [120]~P41(x1201)+P39(x1201) % 58.78/58.88 [121]~P55(x1211)+P39(x1211) % 58.78/58.88 [122]~P45(x1221)+P40(x1221) % 58.78/58.88 [123]~P45(x1231)+P42(x1231) % 58.78/58.88 [124]~P48(x1241)+P44(x1241) % 58.78/58.88 [125]~P48(x1251)+P50(x1251) % 58.78/58.89 [126]~P56(x1261)+P51(x1261) % 58.78/58.89 [127]~P56(x1271)+P57(x1271) % 58.78/58.89 [128]~P59(x1281)+P53(x1281) % 58.78/58.89 [129]~P78(x1291)+P53(x1291) % 58.78/58.89 [130]~P68(x1301)+P56(x1301) % 58.78/58.89 [131]~P62(x1311)+P54(x1311) % 58.78/58.89 [132]~P62(x1321)+P58(x1321) % 58.78/58.89 [133]~P68(x1331)+P65(x1331) % 58.78/58.89 [134]~P75(x1341)+P67(x1341) % 58.78/58.89 [135]~P75(x1351)+P76(x1351) % 58.78/58.89 [136]~P88(x1361)+P75(x1361) % 58.78/58.89 [137]~P79(x1371)+P72(x1371) % 58.78/58.89 [138]~P79(x1381)+P77(x1381) % 58.78/58.89 [139]~P88(x1391)+P85(x1391) % 58.78/58.89 [140]~P94(x1401)+P87(x1401) % 58.78/58.89 [141]~P94(x1411)+P95(x1411) % 58.78/58.89 [142]~P109(x1421)+P94(x1421) % 58.78/58.89 [143]~P98(x1431)+P91(x1431) % 58.78/58.89 [144]~P98(x1441)+P96(x1441) % 58.78/58.89 [145]~P109(x1451)+P106(x1451) % 58.78/58.89 [146]~P114(x1461)+~P113(x1461) % 58.78/58.89 [205]P45(x2051)+~P111(a122,x2051) % 58.78/58.89 [206]P45(x2061)+~P111(a128,x2061) % 58.78/58.89 [207]P45(x2071)+~P111(a126,x2071) % 58.78/58.89 [208]P45(x2081)+~P111(a131,x2081) % 58.78/58.89 [209]P45(x2091)+~P111(a132,x2091) % 58.78/58.89 [210]P48(x2101)+~P111(a127,x2101) % 58.78/58.89 [211]P48(x2111)+~P111(a120,x2111) % 58.78/58.89 [212]P48(x2121)+~P111(a129,x2121) % 58.78/58.89 [213]P62(x2131)+~P111(a122,x2131) % 58.78/58.89 [214]P62(x2141)+~P111(a128,x2141) % 58.78/58.89 [215]P62(x2151)+~P111(a126,x2151) % 58.78/58.89 [216]P62(x2161)+~P111(a131,x2161) % 58.78/58.89 [217]P62(x2171)+~P111(a132,x2171) % 58.78/58.89 [218]P60(x2181)+~P111(a127,x2181) % 58.78/58.89 [219]P60(x2191)+~P111(a120,x2191) % 58.78/58.89 [220]P60(x2201)+~P111(a129,x2201) % 58.78/58.89 [221]P68(x2211)+~P111(a130,x2211) % 58.78/58.89 [222]P68(x2221)+~P111(a121,x2221) % 58.78/58.89 [223]P79(x2231)+~P111(a122,x2231) % 58.78/58.89 [224]P79(x2241)+~P111(a128,x2241) % 58.78/58.89 [225]P79(x2251)+~P111(a126,x2251) % 58.78/58.89 [226]P79(x2261)+~P111(a131,x2261) % 58.78/58.89 [227]P79(x2271)+~P111(a132,x2271) % 58.78/58.89 [228]P81(x2281)+~P111(a127,x2281) % 58.78/58.89 [229]P81(x2291)+~P111(a120,x2291) % 58.78/58.89 [230]P81(x2301)+~P111(a129,x2301) % 58.78/58.89 [231]P83(x2311)+~P111(a130,x2311) % 58.78/58.89 [232]P83(x2321)+~P111(a121,x2321) % 58.78/58.89 [233]P88(x2331)+~P111(a119,x2331) % 58.78/58.89 [234]P98(x2341)+~P111(a122,x2341) % 58.78/58.89 [235]P98(x2351)+~P111(a128,x2351) % 58.78/58.89 [236]P98(x2361)+~P111(a126,x2361) % 58.78/58.89 [237]P98(x2371)+~P111(a131,x2371) % 58.78/58.89 [238]P98(x2381)+~P111(a132,x2381) % 58.78/58.89 [239]P100(x2391)+~P111(a127,x2391) % 58.78/58.89 [240]P100(x2401)+~P111(a120,x2401) % 58.78/58.89 [241]P100(x2411)+~P111(a129,x2411) % 58.78/58.89 [242]P102(x2421)+~P111(a130,x2421) % 58.78/58.89 [243]P102(x2431)+~P111(a121,x2431) % 58.78/58.89 [244]P104(x2441)+~P111(a119,x2441) % 58.78/58.89 [245]P109(x2451)+~P111(a2,x2451) % 58.78/58.89 [147]~P4(x1471)+P110(f3(x1471)) % 58.78/58.89 [148]~P8(x1481)+P5(f53(x1481)) % 58.78/58.89 [149]~P76(x1491)+P10(f54(x1491)) % 58.78/58.89 [150]~P21(x1501)+P20(f4(x1501)) % 58.78/58.89 [151]~P22(x1511)+P21(f29(x1511)) % 58.78/58.89 [152]~P23(x1521)+P22(f30(x1521)) % 58.78/58.89 [153]~P24(x1531)+P23(f31(x1531)) % 58.78/58.89 [154]~P27(x1541)+P24(f33(x1541)) % 58.78/58.89 [155]~P95(x1551)+P28(f108(x1551)) % 58.78/58.89 [156]~P35(x1561)+P30(f34(x1561)) % 58.78/58.89 [157]~P36(x1571)+P35(f44(x1571)) % 58.78/58.89 [158]~P37(x1581)+P36(f45(x1581)) % 58.78/58.89 [159]~P38(x1591)+P37(f46(x1591)) % 58.78/58.89 [160]~P33(x1601)+P38(f47(x1601)) % 58.78/58.89 [161]~P47(x1611)+P46(f55(x1611)) % 58.78/58.89 [162]~P52(x1621)+P49(f58(x1621)) % 58.78/58.89 [163]~P57(x1631)+P53(f65(x1631)) % 58.78/58.89 [164]~P64(x1641)+P63(f68(x1641)) % 58.78/58.89 [165]~P66(x1651)+P64(f76(x1651)) % 58.78/58.89 [166]~P70(x1661)+P69(f80(x1661)) % 58.78/58.89 [167]~P82(x1671)+P80(f89(x1671)) % 58.78/58.89 [168]~P84(x1681)+P82(f96(x1681)) % 58.78/58.89 [169]~P86(x1691)+P84(f100(x1691)) % 58.78/58.89 [170]~P90(x1701)+P89(f103(x1701)) % 58.78/58.89 [171]~P101(x1711)+P99(f5(x1711)) % 58.78/58.89 [172]~P103(x1721)+P101(f8(x1721)) % 58.78/58.89 [173]~P105(x1731)+P103(f11(x1731)) % 58.78/58.89 [174]~P107(x1741)+P105(f13(x1741)) % 58.78/58.89 [246]P3(x2461)+P115(x2461,f32(x2461)) % 58.78/58.89 [247]P4(x2471)+P116(x2471,f66(x2471)) % 58.78/58.89 [248]P110(x2481)+P117(x2481,f17(x2481)) % 58.78/58.89 [249]P5(x2491)+P140(x2491,f97(x2491)) % 58.78/58.89 [250]P61(x2501)+P118(x2501,f59(x2501)) % 58.78/58.89 [251]P10(x2511)+P119(x2511,f21(x2511)) % 58.78/58.89 [252]P15(x2521)+P141(x2521,f14(x2521)) % 58.78/58.89 [253]P17(x2531)+P143(x2531,f22(x2531)) % 58.78/58.89 [254]P19(x2541)+P144(x2541,f27(x2541)) % 58.78/58.89 [255]P25(x2551)+P155(x2551,f35(x2551)) % 58.78/58.89 [256]P28(x2561)+P127(x2561,f37(x2561)) % 58.78/58.89 [257]P31(x2571)+P120(x2571,f39(x2571)) % 58.78/58.89 [258]P32(x2581)+P128(x2581,f40(x2581)) % 58.78/58.89 [259]P41(x2591)+P142(x2591,f48(x2591)) % 58.78/58.89 [260]P42(x2601)+P145(x2601,f49(x2601)) % 58.78/58.89 [261]P46(x2611)+P148(x2611,f56(x2611)) % 58.78/58.89 [262]P47(x2621)+P153(x2621,f57(x2621)) % 58.78/58.89 [263]P49(x2631)+P156(x2631,f60(x2631)) % 58.78/58.89 [264]P52(x2641)+P121(x2641,f64(x2641)) % 58.78/58.89 [265]P53(x2651)+P157(x2651,f109(x2651)) % 58.78/58.89 [266]P55(x2661)+P122(x2661,f69(x2661)) % 58.78/58.89 [267]P58(x2671)+P123(x2671,f70(x2671)) % 58.78/58.89 [268]P63(x2681)+P124(x2681,f73(x2681)) % 58.78/58.89 [269]P64(x2691)+P146(x2691,f75(x2691)) % 58.78/58.89 [270]P66(x2701)+P125(x2701,f77(x2701)) % 58.78/58.89 [271]P69(x2711)+P126(x2711,f81(x2711)) % 58.78/58.89 [272]P70(x2721)+P129(x2721,f84(x2721)) % 58.78/58.89 [273]P71(x2731)+P154(x2731,f85(x2731)) % 58.78/58.89 [274]P73(x2741)+P130(x2741,f90(x2741)) % 58.78/58.89 [275]P77(x2751)+P131(x2751,f91(x2751)) % 58.78/58.89 [276]P80(x2761)+P132(x2761,f94(x2761)) % 58.78/58.89 [277]P81(x2771)+P149(x2771,f99(x2771)) % 58.78/58.89 [278]P84(x2781)+P151(x2781,f101(x2781)) % 58.78/58.89 [279]P86(x2791)+P133(x2791,f104(x2791)) % 58.78/58.89 [280]P89(x2801)+P134(x2801,f105(x2801)) % 58.78/58.89 [281]P90(x2811)+P135(x2811,f110(x2811)) % 58.78/58.89 [282]P93(x2821)+P136(x2821,f113(x2821)) % 58.78/58.89 [283]P96(x2831)+P137(x2831,f114(x2831)) % 58.78/58.89 [284]P99(x2841)+P138(x2841,f6(x2841)) % 58.78/58.89 [285]P100(x2851)+P150(x2851,f9(x2851)) % 58.78/58.89 [286]P102(x2861)+P152(x2861,f12(x2861)) % 58.78/58.89 [287]P104(x2871)+P147(x2871,f15(x2871)) % 58.78/58.89 [288]P107(x2881)+P139(x2881,f18(x2881)) % 58.78/58.89 [332]~P1(x3321)+P115(x3321,f43(x3321)) % 58.78/58.89 [333]~P4(x3331)+P111(x3331,f3(x3331)) % 58.78/58.89 [334]~P8(x3341)+P111(x3341,f53(x3341)) % 58.78/58.89 [335]~P21(x3351)+P111(x3351,f4(x3351)) % 58.78/58.89 [336]~P22(x3361)+P111(x3361,f29(x3361)) % 58.78/58.89 [337]~P23(x3371)+P111(x3371,f30(x3371)) % 58.78/58.89 [338]~P24(x3381)+P111(x3381,f31(x3381)) % 58.78/58.89 [339]~P27(x3391)+P111(x3391,f33(x3391)) % 58.78/58.89 [340]~P35(x3401)+P111(x3401,f34(x3401)) % 58.78/58.89 [341]~P36(x3411)+P111(x3411,f44(x3411)) % 58.78/58.89 [342]~P37(x3421)+P111(x3421,f45(x3421)) % 58.78/58.89 [343]~P38(x3431)+P111(x3431,f46(x3431)) % 58.78/58.89 [344]~P33(x3441)+P111(x3441,f47(x3441)) % 58.78/58.89 [345]~P47(x3451)+P111(x3451,f55(x3451)) % 58.78/58.89 [346]~P52(x3461)+P111(x3461,f58(x3461)) % 58.78/58.89 [347]~P57(x3471)+P111(x3471,f65(x3471)) % 58.78/58.89 [348]~P64(x3481)+P111(x3481,f68(x3481)) % 58.78/58.89 [349]~P66(x3491)+P111(x3491,f76(x3491)) % 58.78/58.89 [350]~P70(x3501)+P111(x3501,f80(x3501)) % 58.78/58.89 [351]~P76(x3511)+P111(x3511,f54(x3511)) % 58.78/58.89 [352]~P82(x3521)+P111(x3521,f89(x3521)) % 58.78/58.89 [353]~P84(x3531)+P111(x3531,f96(x3531)) % 58.78/58.89 [354]~P86(x3541)+P111(x3541,f100(x3541)) % 58.78/58.89 [355]~P90(x3551)+P111(x3551,f103(x3551)) % 58.78/58.89 [356]~P95(x3561)+P111(x3561,f108(x3561)) % 58.78/58.89 [357]~P101(x3571)+P111(x3571,f5(x3571)) % 58.78/58.89 [358]~P103(x3581)+P111(x3581,f8(x3581)) % 58.78/58.89 [359]~P105(x3591)+P111(x3591,f11(x3591)) % 58.78/58.89 [360]~P107(x3601)+P111(x3601,f13(x3601)) % 58.78/58.89 [361]~P2(x3611)+P116(x3611,f78(x3611)) % 58.78/58.89 [362]~P6(x3621)+P140(x3621,f86(x3621)) % 58.78/58.89 [363]~P16(x3631)+P141(x3631,f117(x3631)) % 58.78/58.89 [364]~P18(x3641)+P143(x3641,f23(x3641)) % 58.78/58.89 [365]~P11(x3651)+P119(x3651,f26(x3651)) % 58.78/58.89 [366]~P20(x3661)+P144(x3661,f28(x3661)) % 58.78/58.89 [367]~P26(x3671)+P155(x3671,f36(x3671)) % 58.78/58.89 [368]~P29(x3681)+P127(x3681,f38(x3681)) % 58.78/58.89 [369]~P30(x3691)+P120(x3691,f41(x3691)) % 58.78/58.89 [370]~P34(x3701)+P128(x3701,f42(x3701)) % 58.78/58.89 [371]~P40(x3711)+P142(x3711,f50(x3711)) % 58.78/58.89 [372]~P43(x3721)+P145(x3721,f51(x3721)) % 58.78/58.89 [373]~P45(x3731)+P148(x3731,f52(x3731)) % 58.78/58.89 [374]~P44(x3741)+P153(x3741,f61(x3741)) % 58.78/58.89 [375]~P48(x3751)+P156(x3751,f62(x3751)) % 58.78/58.89 [376]~P39(x3761)+P118(x3761,f63(x3761)) % 58.78/58.89 [377]~P51(x3771)+P121(x3771,f67(x3771)) % 58.78/58.89 [378]~P54(x3781)+P122(x3781,f71(x3781)) % 58.78/58.89 [379]~P59(x3791)+P123(x3791,f72(x3791)) % 58.78/58.89 [380]~P62(x3801)+P124(x3801,f74(x3801)) % 58.78/58.89 [381]~P60(x3811)+P146(x3811,f79(x3811)) % 58.78/58.89 [382]~P65(x3821)+P125(x3821,f82(x3821)) % 58.78/58.89 [383]~P68(x3831)+P126(x3831,f83(x3831)) % 58.78/58.89 [384]~P67(x3841)+P129(x3841,f87(x3841)) % 58.78/58.89 [385]~P74(x3851)+P154(x3851,f88(x3851)) % 58.78/58.89 [386]~P72(x3861)+P130(x3861,f92(x3861)) % 58.78/58.89 [387]~P78(x3871)+P131(x3871,f93(x3871)) % 58.78/58.89 [388]~P79(x3881)+P132(x3881,f95(x3881)) % 58.78/58.89 [389]~P82(x3891)+P149(x3891,f98(x3891)) % 58.78/58.89 [390]~P83(x3901)+P151(x3901,f102(x3901)) % 58.78/58.89 [391]~P85(x3911)+P133(x3911,f106(x3911)) % 58.78/58.89 [392]~P88(x3921)+P134(x3921,f107(x3921)) % 58.78/58.89 [393]~P87(x3931)+P135(x3931,f111(x3931)) % 58.78/58.89 [394]~P92(x3941)+P157(x3941,f112(x3941)) % 58.78/58.89 [395]~P91(x3951)+P136(x3951,f115(x3951)) % 58.78/58.89 [396]~P97(x3961)+P137(x3961,f116(x3961)) % 58.78/58.89 [397]~P98(x3971)+P138(x3971,f118(x3971)) % 58.78/58.89 [398]~P101(x3981)+P150(x3981,f7(x3981)) % 58.78/58.89 [399]~P103(x3991)+P152(x3991,f10(x3991)) % 58.78/58.89 [400]~P105(x4001)+P147(x4001,f16(x4001)) % 58.78/58.89 [401]~P106(x4011)+P139(x4011,f19(x4011)) % 58.78/58.89 [402]~P109(x4021)+P117(x4021,f20(x4021)) % 58.78/58.89 [289]P92(x2891)+~P157(x2891,x2892) % 58.78/58.89 [290]P74(x2901)+~P154(x2901,x2902) % 58.78/58.89 [291]P1(x2911)+~P115(x2911,x2912) % 58.78/58.89 [292]P2(x2921)+~P116(x2921,x2922) % 58.78/58.89 [293]P6(x2931)+~P140(x2931,x2932) % 58.78/58.89 [294]P16(x2941)+~P141(x2941,x2942) % 58.78/58.89 [295]P18(x2951)+~P143(x2951,x2952) % 58.78/58.89 [296]P11(x2961)+~P119(x2961,x2962) % 58.78/58.89 [297]P20(x2971)+~P144(x2971,x2972) % 58.78/58.89 [298]P26(x2981)+~P155(x2981,x2982) % 58.78/58.89 [299]P29(x2991)+~P127(x2991,x2992) % 58.78/58.89 [300]P30(x3001)+~P120(x3001,x3002) % 58.78/58.89 [301]P34(x3011)+~P128(x3011,x3012) % 58.78/58.89 [302]P39(x3021)+~P118(x3021,x3022) % 58.78/58.89 [303]P40(x3031)+~P142(x3031,x3032) % 58.78/58.89 [304]P43(x3041)+~P145(x3041,x3042) % 58.78/58.89 [305]P45(x3051)+~P148(x3051,x3052) % 58.78/58.89 [306]P44(x3061)+~P153(x3061,x3062) % 58.78/58.89 [307]P48(x3071)+~P156(x3071,x3072) % 58.78/58.89 [308]P51(x3081)+~P121(x3081,x3082) % 58.78/58.89 [309]P54(x3091)+~P122(x3091,x3092) % 58.78/58.89 [310]P59(x3101)+~P123(x3101,x3102) % 58.78/58.89 [311]P62(x3111)+~P124(x3111,x3112) % 58.78/58.89 [312]P60(x3121)+~P146(x3121,x3122) % 58.78/58.89 [313]P65(x3131)+~P125(x3131,x3132) % 58.78/58.89 [314]P68(x3141)+~P126(x3141,x3142) % 58.78/58.89 [315]P67(x3151)+~P129(x3151,x3152) % 58.78/58.89 [316]P72(x3161)+~P130(x3161,x3162) % 58.78/58.89 [317]P78(x3171)+~P131(x3171,x3172) % 58.78/58.89 [318]P79(x3181)+~P132(x3181,x3182) % 58.78/58.89 [319]P82(x3191)+~P149(x3191,x3192) % 58.78/58.89 [320]P83(x3201)+~P151(x3201,x3202) % 58.78/58.89 [321]P85(x3211)+~P133(x3211,x3212) % 58.78/58.89 [322]P88(x3221)+~P134(x3221,x3222) % 58.78/58.89 [323]P87(x3231)+~P135(x3231,x3232) % 58.78/58.89 [324]P91(x3241)+~P136(x3241,x3242) % 58.78/58.89 [325]P97(x3251)+~P137(x3251,x3252) % 58.78/58.89 [326]P98(x3261)+~P138(x3261,x3262) % 58.78/58.89 [327]P101(x3271)+~P150(x3271,x3272) % 58.78/58.89 [328]P103(x3281)+~P152(x3281,x3282) % 58.78/58.89 [329]P105(x3291)+~P147(x3291,x3292) % 58.78/58.89 [330]P106(x3301)+~P139(x3301,x3302) % 58.78/58.89 [331]P109(x3311)+~P117(x3311,x3312) % 58.78/58.89 [403]~P3(x4031)+~P115(x4031,x4032) % 58.78/58.89 [404]~P4(x4041)+~P116(x4041,x4042) % 58.78/58.89 [405]~P110(x4051)+~P117(x4051,x4052) % 58.78/58.89 [406]~P5(x4061)+~P140(x4061,x4062) % 58.78/58.89 [407]~P61(x4071)+~P118(x4071,x4072) % 58.78/58.89 [408]~P10(x4081)+~P119(x4081,x4082) % 58.78/58.89 [409]~P15(x4091)+~P141(x4091,x4092) % 58.78/58.89 [410]~P17(x4101)+~P143(x4101,x4102) % 58.78/58.89 [411]~P19(x4111)+~P144(x4111,x4112) % 58.78/58.89 [412]~P25(x4121)+~P155(x4121,x4122) % 58.78/58.89 [413]~P28(x4131)+~P127(x4131,x4132) % 58.78/58.89 [414]~P31(x4141)+~P120(x4141,x4142) % 58.78/58.89 [415]~P32(x4151)+~P128(x4151,x4152) % 58.78/58.89 [416]~P41(x4161)+~P142(x4161,x4162) % 58.78/58.89 [417]~P42(x4171)+~P145(x4171,x4172) % 58.78/58.89 [418]~P46(x4181)+~P148(x4181,x4182) % 58.78/58.89 [419]~P47(x4191)+~P153(x4191,x4192) % 58.78/58.89 [420]~P49(x4201)+~P156(x4201,x4202) % 58.78/58.89 [421]~P52(x4211)+~P121(x4211,x4212) % 58.78/58.89 [422]~P53(x4221)+~P157(x4221,x4222) % 58.78/58.89 [423]~P55(x4231)+~P122(x4231,x4232) % 58.78/58.89 [424]~P58(x4241)+~P123(x4241,x4242) % 58.78/58.89 [425]~P63(x4251)+~P124(x4251,x4252) % 58.78/58.89 [426]~P64(x4261)+~P146(x4261,x4262) % 58.78/58.89 [427]~P66(x4271)+~P125(x4271,x4272) % 58.78/58.89 [428]~P69(x4281)+~P126(x4281,x4282) % 58.78/58.89 [429]~P70(x4291)+~P129(x4291,x4292) % 58.78/58.89 [430]~P71(x4301)+~P154(x4301,x4302) % 58.78/58.89 [431]~P73(x4311)+~P130(x4311,x4312) % 58.78/58.89 [432]~P77(x4321)+~P131(x4321,x4322) % 58.78/58.89 [433]~P80(x4331)+~P132(x4331,x4332) % 58.78/58.89 [434]~P81(x4341)+~P149(x4341,x4342) % 58.78/58.89 [435]~P84(x4351)+~P151(x4351,x4352) % 58.78/58.89 [436]~P86(x4361)+~P133(x4361,x4362) % 58.78/58.89 [437]~P89(x4371)+~P134(x4371,x4372) % 58.78/58.89 [438]~P90(x4381)+~P135(x4381,x4382) % 58.78/58.89 [439]~P93(x4391)+~P136(x4391,x4392) % 58.78/58.89 [440]~P96(x4401)+~P137(x4401,x4402) % 58.78/58.89 [441]~P99(x4411)+~P138(x4411,x4412) % 58.78/58.89 [442]~P100(x4421)+~P150(x4421,x4422) % 58.78/58.89 [443]~P102(x4431)+~P152(x4431,x4432) % 58.78/58.89 [444]~P104(x4441)+~P147(x4441,x4442) % 58.78/58.89 [445]~P107(x4451)+~P139(x4451,x4452) % 58.78/58.89 [175]~P92(x1751)+~P74(x1751)+P3(x1751) % 58.78/58.89 [176]~P34(x1761)+~P39(x1761)+P74(x1761) % 58.78/58.89 [177]~P2(x1771)+~P8(x1771)+P7(x1771) % 58.78/58.89 [178]~P7(x1781)+~P33(x1781)+P9(x1781) % 58.78/58.89 [179]~P61(x1791)+~P10(x1791)+P13(x1791) % 58.78/58.89 [180]~P5(x1801)+~P13(x1801)+P12(x1801) % 58.78/58.89 [181]~P12(x1811)+~P15(x1811)+P14(x1811) % 58.78/58.89 [182]~P14(x1821)+~P17(x1821)+P19(x1821) % 58.78/58.89 [183]~P3(x1831)+~P11(x1831)+P26(x1831) % 58.78/58.89 [184]~P26(x1841)+~P29(x1841)+P31(x1841) % 58.78/58.89 [185]~P34(x1851)+~P39(x1851)+P41(x1851) % 58.78/58.89 [186]~P61(x1861)+~P32(x1861)+P43(x1861) % 58.78/58.89 [187]~P40(x1871)+~P42(x1871)+P45(x1871) % 58.78/58.89 [188]~P44(x1881)+~P50(x1881)+P48(x1881) % 58.78/58.89 [189]~P51(x1891)+~P57(x1891)+P56(x1891) % 58.78/58.89 [190]~P92(x1901)+~P39(x1901)+P55(x1901) % 58.78/58.89 [191]~P61(x1911)+~P53(x1911)+P59(x1911) % 58.78/58.89 [192]~P54(x1921)+~P58(x1921)+P62(x1921) % 58.78/58.89 [193]~P56(x1931)+~P65(x1931)+P68(x1931) % 58.78/58.89 [194]~P67(x1941)+~P76(x1941)+P75(x1941) % 58.78/58.89 [195]~P92(x1951)+~P11(x1951)+P73(x1951) % 58.78/58.89 [196]~P10(x1961)+~P53(x1961)+P78(x1961) % 58.78/58.89 [197]~P72(x1971)+~P77(x1971)+P79(x1971) % 58.78/58.89 [198]~P75(x1981)+~P85(x1981)+P88(x1981) % 58.78/58.89 [199]~P87(x1991)+~P95(x1991)+P94(x1991) % 58.78/58.89 [200]~P11(x2001)+~P34(x2001)+P93(x2001) % 58.78/58.89 [201]~P10(x2011)+~P32(x2011)+P97(x2011) % 58.78/58.89 [202]~P91(x2021)+~P96(x2021)+P98(x2021) % 58.78/58.89 [203]~P94(x2031)+~P106(x2031)+P109(x2031) % 58.78/58.89 [204]~P9(x2041)+~P27(x2041)+P108(x2041) % 58.78/58.89 [446]~P111(x4461,x4462)+P4(x4461)+~P110(x4462) % 58.78/58.89 [447]~P111(x4471,x4472)+P8(x4471)+~P5(x4472) % 58.78/58.89 [448]~P111(x4481,x4482)+P33(x4481)+~P38(x4482) % 58.78/58.89 [449]~P111(x4491,x4492)+P21(x4491)+~P20(x4492) % 58.78/58.89 [450]~P111(x4501,x4502)+P22(x4501)+~P21(x4502) % 58.78/58.89 [451]~P111(x4511,x4512)+P23(x4511)+~P22(x4512) % 58.78/58.89 [452]~P111(x4521,x4522)+P24(x4521)+~P23(x4522) % 58.78/58.89 [453]~P111(x4531,x4532)+P27(x4531)+~P24(x4532) % 58.78/58.89 [454]~P111(x4541,x4542)+P35(x4541)+~P30(x4542) % 58.78/58.89 [455]~P111(x4551,x4552)+P36(x4551)+~P35(x4552) % 58.78/58.89 [456]~P111(x4561,x4562)+P37(x4561)+~P36(x4562) % 58.78/58.89 [457]~P111(x4571,x4572)+P38(x4571)+~P37(x4572) % 58.78/58.89 [458]~P111(x4581,x4582)+P47(x4581)+~P46(x4582) % 58.78/58.89 [459]~P111(x4591,x4592)+P52(x4591)+~P49(x4592) % 58.78/58.89 [460]~P111(x4601,x4602)+P57(x4601)+~P53(x4602) % 58.78/58.89 [461]~P111(x4611,x4612)+P64(x4611)+~P63(x4612) % 58.78/58.89 [462]~P111(x4621,x4622)+P66(x4621)+~P64(x4622) % 58.78/58.89 [463]~P111(x4631,x4632)+P70(x4631)+~P69(x4632) % 58.78/58.89 [464]~P111(x4641,x4642)+P76(x4641)+~P10(x4642) % 58.78/58.89 [465]~P111(x4651,x4652)+P82(x4651)+~P80(x4652) % 58.78/58.89 [466]~P111(x4661,x4662)+P84(x4661)+~P82(x4662) % 58.78/58.89 [467]~P111(x4671,x4672)+P86(x4671)+~P84(x4672) % 58.78/58.89 [468]~P111(x4681,x4682)+P90(x4681)+~P89(x4682) % 58.78/58.89 [469]~P111(x4691,x4692)+P95(x4691)+~P28(x4692) % 58.78/58.89 [470]~P111(x4701,x4702)+P101(x4701)+~P99(x4702) % 58.78/58.89 [471]~P111(x4711,x4712)+P103(x4711)+~P101(x4712) % 58.78/58.89 [472]~P111(x4721,x4722)+P105(x4721)+~P103(x4722) % 58.78/58.89 [473]~P111(x4731,x4732)+P107(x4731)+~P105(x4732) % 58.78/58.89 [474]~P75(a130)+~P56(a120)+~P56(a129)+~P62(a1)+~P68(a127)+~P68(a120)+~P68(a129)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P79(a1)+~P88(a130)+~P88(a121)+~P95(a119)+~P94(a119)+~P98(a1)+~P109(a119)+~P48(a122)+P113(a25)+~P114(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P45(a1)+P112(a24)+~P48(a128)+~P48(a126)+~P48(a131)+~P48(a132)+~P57(a127)+~P57(a120)+~P57(a129) % 58.78/58.89 [475]~P75(a130)+~P56(a120)+~P56(a129)+~P62(a1)+~P68(a127)+~P68(a120)+~P68(a129)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P79(a1)+~P88(a130)+~P88(a121)+~P95(a119)+~P94(a119)+~P98(a1)+~P109(a119)+~P48(a122)+P114(a25)+~P113(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P45(a1)+P112(a24)+~P48(a128)+~P48(a126)+~P48(a131)+~P48(a132)+~P57(a127)+~P57(a120)+~P57(a129) % 58.78/58.89 %EqnAxiom % 58.78/58.89 % 58.78/58.89 %------------------------------------------- % 58.78/58.89 cnf(476,plain, % 58.78/58.89 (P45(a125)), % 58.78/58.89 inference(scs_inference,[],[79,205])). % 58.78/58.89 cnf(478,plain, % 58.78/58.89 (P48(a131)), % 58.78/58.89 inference(scs_inference,[],[79,81,205,210])). % 58.78/58.89 cnf(480,plain, % 58.78/58.89 (P48(a128)), % 58.78/58.89 inference(scs_inference,[],[79,81,82,205,210,211])). % 58.78/58.89 cnf(482,plain, % 58.78/58.89 (P48(a132)), % 58.78/58.89 inference(scs_inference,[],[79,81,82,83,205,210,211,212])). % 58.78/58.89 cnf(484,plain, % 58.78/58.89 (P62(a125)), % 58.78/58.89 inference(scs_inference,[],[79,81,82,83,205,210,211,212,213])). % 58.78/58.89 cnf(486,plain, % 58.78/58.89 (P68(a129)), % 58.78/58.89 inference(scs_inference,[],[78,79,81,82,83,205,210,211,212,213,221])). % 58.78/58.89 cnf(488,plain, % 58.78/58.89 (P68(a127)), % 58.78/58.89 inference(scs_inference,[],[78,79,80,81,82,83,205,210,211,212,213,221,222])). % 58.78/58.89 cnf(490,plain, % 58.78/58.89 (P79(a125)), % 58.78/58.89 inference(scs_inference,[],[78,79,80,81,82,83,205,210,211,212,213,221,222,223])). % 58.78/58.89 cnf(492,plain, % 58.78/58.89 (P88(a130)), % 58.78/58.89 inference(scs_inference,[],[77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233])). % 58.78/58.89 cnf(494,plain, % 58.78/58.89 (P98(a125)), % 58.78/58.89 inference(scs_inference,[],[77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234])). % 58.78/58.89 cnf(496,plain, % 58.78/58.89 (P109(a119)), % 58.78/58.89 inference(scs_inference,[],[74,77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234,245])). % 58.78/58.89 cnf(498,plain, % 58.78/58.89 (~P140(a119,x4981)), % 58.78/58.89 inference(scs_inference,[],[3,74,77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234,245,406])). % 58.78/58.89 cnf(500,plain, % 58.78/58.89 (~P119(a127,x5001)), % 58.78/58.89 inference(scs_inference,[],[3,4,74,77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234,245,406,408])). % 58.78/58.89 cnf(506,plain, % 58.78/58.89 (~P157(a128,x5061)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,15,29,74,77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422])). % 58.78/58.89 cnf(526,plain, % 58.78/58.89 (~P92(a128)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,15,29,35,48,61,74,77,78,79,80,81,82,83,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394])). % 58.78/58.89 cnf(542,plain, % 58.78/58.89 (~P31(a127)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,15,29,35,48,61,74,77,78,79,80,81,82,83,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112])). % 58.78/58.89 cnf(550,plain, % 58.78/58.89 (P45(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,29,35,48,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187])). % 58.78/58.89 cnf(552,plain, % 58.78/58.89 (P48(a122)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,35,48,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188])). % 58.78/58.89 cnf(554,plain, % 58.78/58.89 (P62(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,34,35,48,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192])). % 58.78/58.89 cnf(556,plain, % 58.78/58.89 (P79(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,34,35,47,48,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197])). % 58.78/58.89 cnf(558,plain, % 58.78/58.89 (P98(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,34,35,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202])). % 58.78/58.89 cnf(562,plain, % 58.78/58.89 (~P10(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196])). % 58.78/58.89 cnf(570,plain, % 58.78/58.89 (~P55(a128)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88])). % 58.78/58.89 cnf(576,plain, % 58.78/58.89 (~P73(a127)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109])). % 58.78/58.89 cnf(588,plain, % 58.78/58.89 (~P26(a128)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86])). % 58.78/58.89 cnf(594,plain, % 58.78/58.89 (P68(a120)+~P56(a120)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193])). % 58.78/58.89 cnf(596,plain, % 58.78/58.89 (~P80(a125)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465])). % 58.78/58.89 cnf(598,plain, % 58.78/58.89 (~P99(a125)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465,470])). % 58.78/58.89 cnf(602,plain, % 58.78/58.89 (~P103(a129)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465,470,471,472])). % 58.78/58.89 cnf(610,plain, % 58.78/58.89 (~P93(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465,470,471,472,327,328,115,116])). % 58.78/58.89 cnf(612,plain, % 58.78/58.89 (~P74(a1)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465,470,471,472,327,328,115,116,114])). % 58.78/58.89 cnf(616,plain, % 58.78/58.89 (P88(a121)+~P75(a121)), % 58.78/58.89 inference(scs_inference,[],[3,4,9,14,15,16,21,29,31,34,35,42,47,48,58,60,61,74,77,78,79,80,81,82,83,12,49,62,67,70,205,210,211,212,213,221,222,223,233,234,245,406,408,413,417,422,424,432,440,362,365,368,372,379,387,394,396,434,442,443,444,87,108,112,113,298,415,187,188,192,197,202,191,196,101,97,104,88,89,106,109,110,389,398,399,400,86,255,370,193,465,470,471,472,327,328,115,116,114,290,198])). % 58.78/58.89 cnf(621,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P113(a25)+~P114(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P48(a126)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[554,488,486,556,492,558,496,552,550,84,480,478,482,474])). % 58.78/58.89 cnf(622,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P114(a25)+~P113(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P48(a126)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[554,488,486,556,492,558,496,552,550,84,480,478,482,475])). % 58.78/58.89 cnf(635,plain, % 58.78/58.89 (~P26(a1)), % 58.78/58.89 inference(scs_inference,[],[50,63,68,71,588,612,90,434,444,442,298,443,86])). % 58.78/58.89 cnf(649,plain, % 58.78/58.89 (P109(a123)), % 58.78/58.89 inference(scs_inference,[],[30,75,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245])). % 58.78/58.89 cnf(657,plain, % 58.78/58.89 (P48(a126)), % 58.78/58.89 inference(scs_inference,[],[5,10,18,23,30,75,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245,394,413,408,188])). % 58.78/58.89 cnf(661,plain, % 58.78/58.89 (~P3(a126)), % 58.78/58.89 inference(scs_inference,[],[83,5,10,18,23,30,75,602,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245,394,413,408,188,471,87])). % 58.78/58.89 cnf(667,plain, % 58.78/58.89 (~P11(a120)), % 58.78/58.89 inference(scs_inference,[],[83,5,10,18,23,30,75,602,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245,394,413,408,188,471,87,255,327,365])). % 58.78/58.89 cnf(669,plain, % 58.78/58.89 (~P55(a126)), % 58.78/58.89 inference(scs_inference,[],[83,5,10,18,23,30,75,602,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245,394,413,408,188,471,87,255,327,365,88])). % 58.78/58.89 cnf(673,plain, % 58.78/58.89 (~P29(a121)), % 58.78/58.89 inference(scs_inference,[],[83,5,10,18,23,30,75,602,50,63,68,71,588,612,90,434,444,442,298,443,86,398,422,400,389,399,112,245,394,413,408,188,471,87,255,327,365,88,89,368])). % 58.78/58.89 cnf(696,plain, % 58.78/58.89 (~P26(a120)), % 58.78/58.89 inference(scs_inference,[],[667,51,635,434,298,110,108])). % 58.78/58.89 cnf(712,plain, % 58.78/58.89 (P109(a124)), % 58.78/58.89 inference(scs_inference,[],[31,76,667,673,51,64,635,661,434,298,110,108,113,255,442,86,398,389,422,245])). % 58.78/58.89 cnf(722,plain, % 58.78/58.89 (~P11(a129)), % 58.78/58.89 inference(scs_inference,[],[31,6,76,667,673,51,64,635,661,434,298,110,108,113,255,442,86,398,389,422,245,112,394,408,89,365])). % 58.78/58.89 cnf(734,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P113(a25)+~P114(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[657,621])). % 58.78/58.89 cnf(735,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P114(a25)+~P113(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P33(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[657,622])). % 58.78/58.89 cnf(754,plain, % 58.78/58.89 (~P3(a132)), % 58.78/58.89 inference(scs_inference,[],[33,722,52,696,298,108,434,110,389,255,422,394,112,87])). % 58.78/58.89 cnf(841,plain, % 58.78/58.89 (~P7(x8411)+P116(x8411,f78(x8411))), % 58.78/58.89 inference(scs_inference,[],[91,361])). % 58.78/58.89 cnf(844,plain, % 58.78/58.89 (P116(x8441,f78(x8441))+~P9(x8441)), % 58.78/58.89 inference(scs_inference,[],[94,841])). % 58.78/58.89 cnf(845,plain, % 58.78/58.89 (P33(a2)), % 58.78/58.89 inference(scs_inference,[],[73,95,96])). % 58.78/58.89 cnf(846,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P113(a25)+~P114(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[845,734])). % 58.78/58.89 cnf(847,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+~P94(a119)+P114(a25)+~P113(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[845,735])). % 58.78/58.89 cnf(863,plain, % 58.78/58.89 (P142(a125,f50(a125))), % 58.78/58.89 inference(scs_inference,[],[476,122,371])). % 58.78/58.89 cnf(870,plain, % 58.78/58.89 (~P56(x8701)+P121(x8701,f67(x8701))), % 58.78/58.89 inference(scs_inference,[],[126,377])). % 58.78/58.89 cnf(871,plain, % 58.78/58.89 (~P56(x8711)+P53(f65(x8711))), % 58.78/58.89 inference(scs_inference,[],[127,163])). % 58.78/58.89 cnf(874,plain, % 58.78/58.89 (P121(a129,f67(a129))), % 58.78/58.89 inference(scs_inference,[],[486,130,870])). % 58.78/58.89 cnf(875,plain, % 58.78/58.89 (P122(a125,f71(a125))), % 58.78/58.89 inference(scs_inference,[],[484,131,378])). % 58.78/58.89 cnf(881,plain, % 58.78/58.89 (P125(a127,f82(a127))), % 58.78/58.89 inference(scs_inference,[],[488,133,382])). % 58.78/58.89 cnf(882,plain, % 58.78/58.89 (~P75(x8821)+P129(x8821,f87(x8821))), % 58.78/58.89 inference(scs_inference,[],[134,384])). % 58.78/58.89 cnf(884,plain, % 58.78/58.89 (P129(a130,f87(a130))), % 58.78/58.89 inference(scs_inference,[],[492,136,882])). % 58.78/58.89 cnf(885,plain, % 58.78/58.89 (P130(a125,f92(a125))), % 58.78/58.89 inference(scs_inference,[],[490,137,386])). % 58.78/58.89 cnf(891,plain, % 58.78/58.89 (P133(a130,f106(a130))), % 58.78/58.89 inference(scs_inference,[],[492,139,391])). % 58.78/58.89 cnf(892,plain, % 58.78/58.89 (~P94(x8921)+P135(x8921,f111(x8921))), % 58.78/58.89 inference(scs_inference,[],[140,393])). % 58.78/58.89 cnf(893,plain, % 58.78/58.89 (~P94(x8931)+P28(f108(x8931))), % 58.78/58.89 inference(scs_inference,[],[141,155])). % 58.78/58.89 cnf(894,plain, % 58.78/58.89 (P135(a119,f111(a119))), % 58.78/58.89 inference(scs_inference,[],[496,142,892])). % 58.78/58.89 cnf(895,plain, % 58.78/58.89 (P136(a125,f115(a125))), % 58.78/58.89 inference(scs_inference,[],[494,143,395])). % 58.78/58.89 cnf(901,plain, % 58.78/58.89 (P139(a123,f19(a123))), % 58.78/58.89 inference(scs_inference,[],[649,145,401])). % 58.78/58.89 cnf(902,plain, % 58.78/58.89 (P126(a120,f83(a120))+~P56(a120)), % 58.78/58.89 inference(scs_inference,[],[594,383])). % 58.78/58.89 cnf(903,plain, % 58.78/58.89 (P134(a121,f107(a121))+~P75(a121)), % 58.78/58.89 inference(scs_inference,[],[616,392])). % 58.78/58.89 cnf(943,plain, % 58.78/58.89 (P146(a128,f79(a128))), % 58.78/58.89 inference(scs_inference,[],[82,219,381])). % 58.78/58.89 cnf(953,plain, % 58.78/58.89 (P151(a127,f102(a127))), % 58.78/58.89 inference(scs_inference,[],[80,232,390])). % 58.78/58.89 cnf(964,plain, % 58.78/58.89 (~P115(x9641,x9642)+P115(x9641,f43(x9641))), % 58.78/58.89 inference(scs_inference,[],[291,332])). % 58.78/58.89 cnf(965,plain, % 58.78/58.89 (~P116(x9651,x9652)+P116(x9651,f78(x9651))), % 58.78/58.89 inference(scs_inference,[],[292,361])). % 58.78/58.89 cnf(967,plain, % 58.78/58.89 (~P120(x9671,x9672)+P120(x9671,f41(x9671))), % 58.78/58.89 inference(scs_inference,[],[300,369])). % 58.78/58.89 cnf(975,plain, % 58.78/58.89 (P54(a128)), % 58.78/58.89 inference(scs_inference,[],[570,309,266])). % 58.78/58.89 cnf(977,plain, % 58.78/58.89 (P54(x9771)+~P124(x9771,x9772)), % 58.78/58.89 inference(scs_inference,[],[311,131])). % 58.78/58.89 cnf(978,plain, % 58.78/58.89 (P56(x9781)+~P126(x9781,x9782)), % 58.78/58.89 inference(scs_inference,[],[314,130])). % 58.78/58.89 cnf(984,plain, % 58.78/58.89 (P75(x9841)+~P134(x9841,x9842)), % 58.78/58.89 inference(scs_inference,[],[322,136])). % 58.78/58.89 cnf(985,plain, % 58.78/58.89 (~P95(a119)+P94(a119)), % 58.78/58.89 inference(scs_inference,[],[894,323,199])). % 58.78/58.89 cnf(986,plain, % 58.78/58.89 (P94(a119)), % 58.78/58.89 inference(scs_inference,[],[9,77,985,469])). % 58.78/58.89 cnf(987,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P113(a25)+~P114(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[986,846])). % 58.78/58.89 cnf(988,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P114(a25)+~P113(a25)+~P8(a2)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[986,847])). % 58.78/58.89 cnf(994,plain, % 58.78/58.89 (P94(x9941)+~P117(x9941,x9942)), % 58.78/58.89 inference(scs_inference,[],[331,142])). % 58.78/58.89 cnf(995,plain, % 58.78/58.89 (~P115(x9951,x9952)+~P26(x9951)), % 58.78/58.89 inference(scs_inference,[],[403,86])). % 58.78/58.89 cnf(1000,plain, % 58.78/58.89 (~P120(x10001,x10002)+P120(x10001,f39(x10001))), % 58.78/58.89 inference(scs_inference,[],[414,257])). % 58.78/58.89 cnf(1001,plain, % 58.78/58.89 (P142(a125,f48(a125))), % 58.78/58.89 inference(scs_inference,[],[863,416,259])). % 58.78/58.89 cnf(1002,plain, % 58.78/58.89 (~P148(f55(x10021),x10022)+~P47(x10021)), % 58.78/58.89 inference(scs_inference,[],[418,161])). % 58.78/58.89 cnf(1005,plain, % 58.78/58.89 (P121(a129,f64(a129))), % 58.78/58.89 inference(scs_inference,[],[874,421,264])). % 58.78/58.89 cnf(1006,plain, % 58.78/58.89 (P122(a125,f69(a125))), % 58.78/58.89 inference(scs_inference,[],[875,423,266])). % 58.78/58.89 cnf(1011,plain, % 58.78/58.89 (P129(a130,f84(a130))), % 58.78/58.89 inference(scs_inference,[],[884,429,272])). % 58.78/58.89 cnf(1014,plain, % 58.78/58.89 (P133(a130,f104(a130))), % 58.78/58.89 inference(scs_inference,[],[891,436,279])). % 58.78/58.89 cnf(1016,plain, % 58.78/58.89 (P135(a119,f110(a119))), % 58.78/58.89 inference(scs_inference,[],[894,438,281])). % 58.78/58.89 cnf(1017,plain, % 58.78/58.89 (P136(a125,f113(a125))), % 58.78/58.89 inference(scs_inference,[],[895,439,282])). % 58.78/58.89 cnf(1019,plain, % 58.78/58.89 (P139(a123,f18(a123))), % 58.78/58.89 inference(scs_inference,[],[901,445,288])). % 58.78/58.89 cnf(1036,plain, % 58.78/58.89 (~P127(f108(a119),x10361)), % 58.78/58.89 inference(scs_inference,[],[986,893,413])). % 58.78/58.89 cnf(1037,plain, % 58.78/58.89 (P28(f108(a119))), % 58.78/58.89 inference(scs_inference,[],[1036,256])). % 58.78/58.89 cnf(1073,plain, % 58.78/58.89 (~P124(x10731,x10732)+P122(x10731,f71(x10731))), % 58.78/58.89 inference(scs_inference,[],[977,378])). % 58.78/58.89 cnf(1074,plain, % 58.78/58.89 (P51(x10741)+~P126(x10741,x10742)), % 58.78/58.89 inference(scs_inference,[],[978,126])). % 58.78/58.89 cnf(1079,plain, % 58.78/58.89 (P67(x10791)+~P134(x10791,x10792)), % 58.78/58.89 inference(scs_inference,[],[984,134])). % 58.78/58.89 cnf(1084,plain, % 58.78/58.89 (P87(x10841)+~P117(x10841,x10842)), % 58.78/58.89 inference(scs_inference,[],[994,140])). % 58.78/58.89 cnf(1085,plain, % 58.78/58.89 (~P115(x10851,x10852)+~P31(x10851)), % 58.78/58.89 inference(scs_inference,[],[995,112])). % 58.78/58.89 cnf(1089,plain, % 58.78/58.89 (~P126(x10891,x10892)+P121(x10891,f67(x10891))), % 58.78/58.89 inference(scs_inference,[],[1074,377])). % 58.78/58.89 cnf(1090,plain, % 58.78/58.89 (~P134(x10901,x10902)+P129(x10901,f87(x10901))), % 58.78/58.89 inference(scs_inference,[],[1079,384])). % 58.78/58.89 cnf(1091,plain, % 58.78/58.89 (~P117(x10911,x10912)+P135(x10911,f111(x10911))), % 58.78/58.89 inference(scs_inference,[],[1084,393])). % 58.78/58.89 cnf(1092,plain, % 58.78/58.89 (~P115(x10921,x10922)+P120(x10921,f39(x10921))), % 58.78/58.89 inference(scs_inference,[],[1085,257])). % 58.78/58.89 cnf(1097,plain, % 58.78/58.89 (P115(a128,f32(a128))), % 58.78/58.89 inference(scs_inference,[],[526,246,87])). % 58.78/58.89 cnf(1098,plain, % 58.78/58.89 (~P117(x10981,x10982)+P117(x10981,f17(x10981))), % 58.78/58.89 inference(scs_inference,[],[248,405])). % 58.78/58.89 cnf(1099,plain, % 58.78/58.89 (P8(a2)), % 58.78/58.89 inference(scs_inference,[],[498,74,249,447])). % 58.78/58.89 cnf(1100,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P113(a25)+~P114(a25)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1099,987])). % 58.78/58.89 cnf(1101,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P114(a25)+~P113(a25)+~P7(a2)+~P9(a2)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1099,988])). % 58.78/58.89 cnf(1102,plain, % 58.78/58.89 (P7(a2)), % 58.78/58.89 inference(scs_inference,[],[1099,2,177])). % 58.78/58.89 cnf(1104,plain, % 58.78/58.89 (P9(a2)), % 58.78/58.89 inference(scs_inference,[],[845,1099,2,177,178])). % 58.78/58.89 cnf(1106,plain, % 58.78/58.89 (P116(a2,f78(a2))), % 58.78/58.89 inference(scs_inference,[],[845,1099,2,177,178,844])). % 58.78/58.89 cnf(1113,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P113(a25)+~P114(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1102,1104,1100])). % 58.78/58.89 cnf(1114,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P76(a121)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P114(a25)+~P113(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1102,1104,1101])). % 58.78/58.89 cnf(1118,plain, % 58.78/58.89 (P76(a121)), % 58.78/58.89 inference(scs_inference,[],[500,80,251,464])). % 58.78/58.89 cnf(1119,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P113(a25)+~P114(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1118,1113])). % 58.78/58.89 cnf(1120,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P75(a121)+~P88(a121)+~P95(a119)+P114(a25)+~P113(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1118,1114])). % 58.78/58.89 cnf(1121,plain, % 58.78/58.89 (P75(a121)), % 58.78/58.89 inference(scs_inference,[],[1118,45,194])). % 58.78/58.89 cnf(1123,plain, % 58.78/58.89 (P88(a121)), % 58.78/58.89 inference(scs_inference,[],[1118,58,45,194,198])). % 58.78/58.89 cnf(1125,plain, % 58.78/58.89 (P134(a121,f107(a121))), % 58.78/58.89 inference(scs_inference,[],[1118,58,45,194,198,903])). % 58.78/58.89 cnf(1134,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P95(a119)+P113(a25)+~P114(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1121,1123,1119])). % 58.78/58.89 cnf(1135,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P95(a119)+P114(a25)+~P113(a25)+~P27(a2)+~P57(a127)+~P57(a120)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1121,1123,1120])). % 58.78/58.89 cnf(1160,plain, % 58.78/58.89 (~P148(x11601,x11602)+P148(x11601,f56(x11601))), % 58.78/58.89 inference(scs_inference,[],[261,418])). % 58.78/58.89 cnf(1161,plain, % 58.78/58.89 (~P156(x11611,x11612)+P156(x11611,f60(x11611))), % 58.78/58.89 inference(scs_inference,[],[263,420])). % 58.78/58.89 cnf(1162,plain, % 58.78/58.89 (P57(a120)), % 58.78/58.89 inference(scs_inference,[],[506,82,265,460])). % 58.78/58.89 cnf(1163,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P95(a119)+P113(a25)+~P114(a25)+~P27(a2)+~P57(a127)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1162,1134])). % 58.78/58.89 cnf(1164,plain, % 58.78/58.89 (~P75(a130)+~P56(a120)+~P56(a129)+~P68(a120)+~P76(a130)+~P56(a127)+~P95(a119)+P114(a25)+~P113(a25)+~P27(a2)+~P57(a127)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1162,1135])). % 58.78/58.89 cnf(1165,plain, % 58.78/58.89 (P56(a120)), % 58.78/58.89 inference(scs_inference,[],[1162,27,189])). % 58.78/58.89 cnf(1167,plain, % 58.78/58.89 (P68(a120)), % 58.78/58.89 inference(scs_inference,[],[1162,42,27,189,193])). % 58.78/58.89 cnf(1169,plain, % 58.78/58.89 (P126(a120,f83(a120))), % 58.78/58.89 inference(scs_inference,[],[1162,42,27,189,193,902])). % 58.78/58.89 cnf(1178,plain, % 58.78/58.89 (~P75(a130)+~P56(a129)+~P76(a130)+~P56(a127)+~P95(a119)+P113(a25)+~P114(a25)+~P27(a2)+~P57(a127)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1165,1167,1163])). % 58.78/58.89 cnf(1179,plain, % 58.78/58.89 (~P75(a130)+~P56(a129)+~P76(a130)+~P56(a127)+~P95(a119)+P114(a25)+~P113(a25)+~P27(a2)+~P57(a127)+~P57(a129)), % 58.78/58.89 inference(scs_inference,[],[1165,1167,1164])). % 58.78/58.89 cnf(1197,plain, % 58.78/58.89 (~P124(x11971,x11972)+P124(x11971,f73(x11971))), % 58.78/58.89 inference(scs_inference,[],[268,425])). % 58.78/58.89 cnf(1198,plain, % 58.78/58.89 (P126(a120,f81(a120))), % 58.78/58.89 inference(scs_inference,[],[1169,271,428])). % 58.78/58.89 cnf(1200,plain, % 58.78/58.89 (P134(a121,f105(a121))), % 58.78/58.89 inference(scs_inference,[],[1125,280,437])). % 58.78/58.89 cnf(1210,plain, % 58.78/58.89 (P111(a120,f65(a120))), % 58.78/58.89 inference(scs_inference,[],[1165,347,127])). % 58.78/58.89 cnf(1217,plain, % 58.78/58.89 (P48(f65(a120))), % 58.78/58.89 inference(scs_inference,[],[1210,219,229,240,211])). % 58.78/58.89 cnf(1245,plain, % 58.78/58.89 (P111(a119,f108(a119))), % 58.78/58.89 inference(scs_inference,[],[986,356,141])). % 58.78/58.89 cnf(1250,plain, % 58.78/58.89 (P88(f108(a119))), % 58.78/58.89 inference(scs_inference,[],[1245,244,444,233])). % 58.78/58.89 cnf(1276,plain, % 58.78/58.89 (P156(a131,f62(a131))), % 58.78/58.89 inference(scs_inference,[],[81,375,210])). % 58.78/58.89 cnf(1277,plain, % 58.78/58.89 (P117(a123,f20(a123))), % 58.78/58.89 inference(scs_inference,[],[75,402,245])). % 58.78/58.89 cnf(1317,plain, % 58.78/58.89 (~P148(f55(x13171),x13172)+P153(x13171,f57(x13171))), % 58.78/58.89 inference(scs_inference,[],[1002,262])). % 58.78/58.89 cnf(1421,plain, % 58.78/58.89 (P1(a128)), % 58.78/58.89 inference(scs_inference,[],[1097,964,291])). % 58.78/58.89 cnf(1422,plain, % 58.78/58.89 (~P4(a2)), % 58.78/58.89 inference(scs_inference,[],[1106,965,404])). % 58.78/58.89 cnf(1423,plain, % 58.78/58.89 (~P110(a124)), % 58.78/58.89 inference(scs_inference,[],[76,1422,446])). % 58.78/58.89 cnf(1428,plain, % 58.78/58.89 (P120(a128,f41(a128))), % 58.78/58.89 inference(scs_inference,[],[1097,967,1092])). % 58.78/58.89 cnf(1434,plain, % 58.78/58.89 (P30(a128)), % 58.78/58.89 inference(scs_inference,[],[1428,1000,300])). % 58.78/58.89 cnf(1466,plain, % 58.78/58.89 (~P52(a120)), % 58.78/58.89 inference(scs_inference,[],[1198,1089,421])). % 58.78/58.89 cnf(1467,plain, % 58.78/58.89 (~P49(a128)), % 58.78/58.89 inference(scs_inference,[],[82,1466,459])). % 58.78/58.89 cnf(1469,plain, % 58.78/58.89 (~P70(a121)), % 58.78/58.89 inference(scs_inference,[],[1200,1090,429])). % 58.78/58.89 cnf(1470,plain, % 58.78/58.89 (~P69(a127)), % 58.78/58.89 inference(scs_inference,[],[80,1469,463])). % 58.78/58.89 cnf(1472,plain, % 58.78/58.89 (P87(a123)), % 58.78/58.89 inference(scs_inference,[],[1277,1091,323])). % 58.78/58.89 cnf(1474,plain, % 58.78/58.89 (P94(a123)), % 58.78/58.89 inference(scs_inference,[],[1277,1098,994])). % 58.78/58.89 cnf(1475,plain, % 58.78/58.89 (P148(a1,f56(a1))), % 58.78/58.89 inference(scs_inference,[],[550,1160,373])). % 58.78/58.89 cnf(1477,plain, % 58.78/58.89 (P124(a1,f73(a1))), % 58.78/58.89 inference(scs_inference,[],[554,1197,380])). % 58.78/58.89 cnf(1577,plain, % 58.78/58.89 (~P148(f55(x15771),x15772)+P44(x15771)), % 58.78/58.89 inference(scs_inference,[],[1317,306])). % 58.78/58.89 cnf(1578,plain, % 58.78/58.89 (P44(x15781)+~P45(f55(x15781))), % 58.78/58.89 inference(scs_inference,[],[1577,373])). % 58.78/58.89 cnf(1579,plain, % 58.78/58.89 (P44(x15791)+~P111(a122,f55(x15791))), % 58.78/58.89 inference(scs_inference,[],[1578,205])). % 58.78/58.89 cnf(1580,plain, % 58.78/58.89 (~P111(a122,f55(x15801))+P153(x15801,f61(x15801))), % 58.78/58.89 inference(scs_inference,[],[1579,374])). % 58.78/58.89 cnf(1670,plain, % 58.78/58.89 (~P47(x16701)+~P111(a122,f55(x16701))), % 58.78/58.89 inference(scs_inference,[],[1580,419])). % 58.78/58.89 cnf(1671,plain, % 58.78/58.89 (~P111(a122,f55(x16711))+P153(x16711,f57(x16711))), % 58.78/58.89 inference(scs_inference,[],[1670,262])). % 58.78/58.89 cnf(1716,plain, % 58.78/58.89 (P153(a122,f57(a122))+~P47(a122)), % 58.78/58.89 inference(scs_inference,[],[1671,345])). % 58.78/58.89 cnf(1717,plain, % 58.78/58.89 (~P47(a122)), % 58.78/58.89 inference(scs_inference,[],[1716,419])). % 58.78/58.89 cnf(1718,plain, % 58.78/58.89 (~P46(a125)), % 58.78/58.89 inference(scs_inference,[],[79,1717,458])). % 58.78/58.89 cnf(1814,plain, % 58.78/58.89 (P115(a1,f32(a1))), % 58.78/58.89 inference(scs_inference,[],[7,635,183,246])). % 58.78/58.89 cnf(2860,plain, % 58.78/58.89 (P27(a2)), % 58.78/58.89 inference(scs_inference,[],[73,111])). % 58.78/58.89 cnf(2868,plain, % 58.78/58.89 (P56(a129)), % 58.78/58.89 inference(scs_inference,[],[1217,476,486,73,111,122,124,125,130])). % 58.78/58.89 cnf(3036,plain, % 58.78/58.89 (P57(a127)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1276,1277,13,58,7,72,73,82,32,81,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460])). % 58.78/58.89 cnf(3038,plain, % 58.78/58.89 (P76(a130)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1276,1277,13,58,7,78,72,6,73,82,32,81,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460,464])). % 58.78/58.89 cnf(3042,plain, % 58.78/58.89 (P95(a119)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,1037,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1245,1276,1277,13,58,7,78,72,6,73,82,32,81,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460,464,468,469])). % 58.78/58.89 cnf(3048,plain, % 58.78/58.89 (P57(a129)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,1037,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1245,1276,1277,13,58,7,78,72,6,73,82,32,81,83,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460,464,468,469,463,459,127])). % 58.78/58.89 cnf(3068,plain, % 58.78/58.89 (P56(a127)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,1037,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1245,1276,1277,13,58,7,78,72,6,73,82,32,81,83,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460,464,468,469,463,459,127,134,135,140,300,309,316,419,433,441,978])). % 58.78/58.89 cnf(3070,plain, % 58.78/58.89 (P75(a130)), % 58.78/58.89 inference(scs_inference,[],[17,26,36,55,480,542,556,558,576,596,598,610,669,712,975,1421,1423,1434,1467,1470,1472,1474,1718,1814,885,1001,1006,1217,1250,943,953,1005,1011,1014,1017,1019,1037,754,562,43,11,14,45,47,60,476,484,486,490,494,1717,881,1016,1125,1169,1428,1475,1477,1165,1118,492,1245,1276,1277,13,58,7,78,72,6,73,82,32,81,83,111,122,124,125,130,131,136,137,139,141,142,143,145,291,330,416,418,421,423,425,426,427,428,429,435,436,437,438,439,445,155,871,893,246,248,257,261,262,263,266,269,271,274,276,278,282,284,332,339,351,356,369,371,373,374,375,376,377,378,380,381,382,383,384,386,388,390,391,392,393,395,397,401,402,870,892,964,967,1000,1073,1092,1098,1161,1197,251,431,365,454,460,464,468,469,463,459,127,134,135,140,300,309,316,419,433,441,978,984])). % 58.78/58.89 cnf(3103,plain, % 58.78/58.89 (P113(a25)+~P114(a25)), % 58.78/58.89 inference(scs_inference,[],[3038,3068,3042,2860,3036,3048,2868,3070,1178])). % 58.78/58.89 cnf(3104,plain, % 58.78/58.89 (P114(a25)+~P113(a25)), % 58.78/58.89 inference(scs_inference,[],[3038,3068,3042,2860,3036,3048,2868,3070,1179])). % 58.78/58.89 cnf(3105,plain, % 58.78/58.89 (~P114(a25)), % 58.78/58.89 inference(scs_inference,[],[3103,146])). % 58.78/58.89 cnf(3108,plain, % 58.78/58.89 ($false), % 58.78/58.89 inference(scs_inference,[],[3105,85,3104]), % 58.78/58.89 ['proof']). % 58.78/58.89 % SZS output end Proof % 58.78/58.89 % Total time :58.150000s %------------------------------------------------------------------------------